Re: [Gcl-devel] Omnibus gcl/acl2 performance post

[Camm Maguire]

Matt Kaufmann <address@hidden> writes:

> Hi, Camm --

> That looks promising!

>> I'm considering merging this into 2.6.10pre.

> I didn't notice any mention of a downside, in which case I imagine
> you'll do this.  If you do, and you want me to test the result with
> the development copy of ACL2 (and latest books), let me know.  (Or you
> can obtain all that here: http://acl2-devel.googlecode.com/)

OK, this is pushed, so you can test if you'd like, but please don't go
to unnecessary trouble unless interested.

Separately, regarding our discussion on runtime vs realtime, your
suspicion proved correct -- the gap between the two is larger for gcl.
This may be due to calling the external gcc compiler, though I don't
really know if your certifications compile stuff.

My seafoam results, now showing both real and runtime, are at

http://people.debian.org/~camm/acl2/r2.6.10prefi 
http://people.debian.org/~camm/acl2/rccl1

The fields for the gcl file are:
run real #gc gc_time #sgc_off name

and for the ccl file are:
run real name

Comparing runtimes with:

join <(awk '{print $6,$1,$2,$3,$4,$5}' r10fi1|sort) \
     <(awk '{print $3,$1,$2}' rccl1|sort) | \
     awk '{print $2-$7,$0}' | sort -n 

we get

-99.79 books/rtl/rel9/support/lib3.delta1/seed.cert.out 360.85 362.44 83 2083 2 
460.64 461.73
-88.82 books/workshops/2013/greve-slind/defung/defung-stress.cert.out 469.07 
471.89 48 1375 2 557.89 559.65
-82.63 books/tau/bounders/elementary-bounders.cert.out 863.85 873.20 94 6080 2 
946.48 955.64
...
21.84 books/models/jvm/guard-verified-m1/find-k!.cert.out 54.40 61.09 29 558 2 
32.56 32.70
22.26 books/models/jvm/m1/find-k!.cert.out 54.38 60.86 29 557 2 32.12 32.54
32.05 books/centaur/vl/top.cert.out 136.66 162.17 162 4393 2 104.61 111.28

totaling -1603.11 seconds.

Comparing realtimes with:

join <(awk '{print $6,$1,$2,$3,$4,$5}' r10fi1|sort) \
     <(awk '{print $3,$1,$2}' rccl1|sort) | \
     awk '{print $3-$8,$0}' | sort -n 

we get

-99.29 books/rtl/rel9/support/lib3.delta1/seed.cert.out 360.85 362.44 83 2083 2 
460.64 461.73
-87.76 books/workshops/2013/greve-slind/defung/defung-stress.cert.out 469.07 
471.89 48 1375 2 557.89 559.65
-82.44 books/tau/bounders/elementary-bounders.cert.out 863.85 873.20 94 6080 2 
946.48 955.64
...
28.39 books/models/jvm/guard-verified-m1/find-k!.cert.out 54.40 61.09 29 558 2 
32.56 32.70
50.89 books/centaur/vl/top.cert.out 136.66 162.17 162 4393 2 104.61 111.28
123.41 books/workshops/2009/sumners/support/kas.cert.out 22.63 164.11 29 374 2 
40.33 40.70

totaling 1460.11 seconds.

The 'time' output for the whole regression was

real    73m16.371s
user    450m42.042s
sys     16m21.313s

for gcl and 

real    73m10.402s
user    433m15.205s
sys     9m8.050s

for ccl.  At least now 1460 ~ (450-433+16-9)*60.  (But -1603.11 is not
approximately (450-433)*60, as we earlier discussed.)

gcl's runtime is via the 'times' system call, and returns the number of
'user' seconds in the calculation.  My guess the rest is in 'system'
seconds, but there are also times for children reported, though gcl does
little forking.  Perhaps
books/workshops/2009/sumners/support/kas.cert.out might stand out in
terms of compiling or other such computation?

This is really nothing to fret about, but if I can believe -1603.11, I
know I can confine my search to gcc integration and the like, but if
(450-433)*60 is more accurate, further work can be done in gcl proper.

Take care,
-- 
Camm Maguire                                        address@hidden
==========================================================================
"The earth is but one country, and mankind its citizens."  --  Baha'u'llah