[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Gcl-devel] Omnibus gcl/acl2 performance post
From: |
Matt Kaufmann |
Subject: |
Re: [Gcl-devel] Omnibus gcl/acl2 performance post |
Date: |
Fri, 11 Oct 2013 17:42:02 -0500 |
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