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

[Matt Kaufmann]

Hi, Camm --

>> This may be due to calling the external gcc compiler, though I don't
>> really know if your certifications compile stuff.

Yes, absolutely!  I can easily imagine that the total time spent in
compilation is significant for GCL.  I suppose you could instrument
ACL2 source function compile-certified-file to find out how much time
that is; let me know if you want assistance with that.  Perhaps such
information would explain everything you discuss, at least if it's
confirmed that GCL's "user" runtime does not include the GCC
compilation time.

For what it's worth, my vague sense from using GCL and CCL over the
years is the GCL compares very well except for compilation time.

By the way, you might get more accurate info avoiding make's -j option
-- I've found kind of implausible results from the "user" times and
perhaps "sys" times reported from multi-threaded runs.

Thanks --
-- Matt
   From: Camm Maguire <address@hidden>
   Cc: address@hidden
   Date: Fri, 11 Oct 2013 12:04:35 -0400

   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