[Gcl-devel] Re: xg rebuilt

[Camm Maguire]

Greetings!

Matt Kaufmann <address@hidden> writes:

> Howdy --
> 
> >> Somewhere I think
> >> you guys have some old timings using both regular and Schelter mv --
> >> are these comparable to gcl today with autoproclamations off (or also
> >> hopefully on?)
> 
> If I have such timings for a given GCL, I don't know where they are.  But for
> any given GCL, it's easy enough to come up with such timings.  What's harder
> for me is to compare two different GCLs.  I don't build GCL very often; I tend
> to use what's available.  If you care to build two CLtL1 GCLs that you'd like
> compared (2.6.7 vs. 2.7.0) with the same (or appropriately corresponding
> parameters), then I could build and run stock ACL2 3.0 (with Schelter mv) on
> top of each and also ordinary mv on top of each.
> 
> Now I'll turn to today's results, which compare what I used to call #2 and #3
> on the HONS version of ACL2 3.0.  It looks like ACL2-generated declaiming is
> more efficient than what GCL generates, at least for these runs.
> 
> With the usual ACL2-generated declaiming, from
> /projects/hvg/ACL2/v3-0-hons-jun25/acl2-proclaims.lisp, and with:
> (setq compiler::*compiler-auto-proclaim* nil si::*disable-recompile* t):
> /projects/hvg/ACL2/v3-0-hons-jun25/make-regression.log:
> 16925.205u 434.179s 4:55:01.49 98.0%  0+0k 0+0io 13pf+0w
> 
> Turning off ACL2-generated declaiming, but with default values of
> compiler::*compiler-auto-proclaim* (t) and
> si::*disable-recompile* (nil):
> /projects/hvg/ACL2/v3-0-hons-gcl-proclaim/make-regression.log:
> 17808.712u 560.627s 5:09:51.50 98.8%  0+0k 0+0io 0pf+0w

Thank you so much for this!  This confirms my basic suspicions -- that
we might be off 5 to 10% or so on the proclamations, but that the bulk
of the issue lies elsewhere.  I don't suppose you have gc time broken
out. 

Next step for me is to compile a gprof image at some point and run
under that.

> Perhaps the difference is due to image sizes (about a factor of 4):
> 
> sundance:~> ls -l /projects/hvg/ACL2/v3-0-hons-jun25/saved_acl2.gcl
> -rwxrwxr-x  1 kaufmann hvg 204745243 Jun 25 09:23 
> /projects/hvg/ACL2/v3-0-hons-jun25/saved_acl2.gcl
> sundance:~> ls -l /projects/hvg/ACL2/v3-0-hons-gcl-proclaim/saved_acl2.gcl
> -rwxrwxr-x  1 kaufmann hvg 208157211 Jun 25 15:03 
> /projects/hvg/ACL2/v3-0-hons-gcl-proclaim/saved_acl2.gcl
> sundance:~> ls -l /projects/acl2/v3-0-linux/gcl-saved_acl2.gcl
> -r-xr-xr-x  1 kaufmann acl2 50606495 May 29 01:41 
> /projects/acl2/v3-0-linux/gcl-saved_acl2.gcl
> sundance:~> 
> 

I thought the image size was down to about 80Mb or so?  This is also
illustative in that keeping the function source around is on the order
of 2% in size.

I take it swap is not an issue (as indicated in your 0+0io above)  I
can't see why size per se would slow things down -- in general more
space speeds things up.

Take care,

> -- Matt
>    Cc: address@hidden
>    From: Camm Maguire <address@hidden>
>    Date: 25 Jun 2006 20:35:14 -0400
>    X-SpamAssassin-Status: No, hits=-2.5 required=5.0
>    X-UTCS-Spam-Status: No, hits=-240 required=200
> 
>    Greetings!
> 
>    Matt Kaufmann <address@hidden> writes:
> 
>    > Bob, Camm --
>    > 
>    > I can re-run any regressions you like.  And, I'd like to build one 
> version that
>    > has as little new stuff as possible, and that we can leave in place for 
> awhile,
>    > so that UT students Sol, David, and Serita can comfortably use it (and 
> Warren
>    > and Bob too).
>    > 
> 
>    Great!  All I was after is some idea of whether the gcl
>    autoproclamations have slowed things down, and if so by how much.  So
>    your #2 and #3 last time around are of most interest.
> 
>    I also know that there is some slowdown associated with regular mv.
>    What I'd like to know is whether there is any other slowdown that
>    cannot be accounted for either in mv or autoproclamation -- i.e. have
>    I done anything else recently to kill performance.  Somewhere I think
>    you guys have some old timings using both regular and Schelter mv --
>    are these comparable to gcl today with autoproclamations off (or also
>    hopefully on?)
> 
>    I get the rough idea that we're 50% slower than the fastest 2.7 we've
>    tested.  I think its great to leave an xg around for a while in a semi
>    stable state.  If you'd like, we can tag in cvs any state you find
>    particularly useful.  It is just that at present we're in the middle
>    of this autoproclamation stuff, and things always get a little worse
>    right after something this new is introduced.  As long as people
>    understand that I'm ok.
> 
>    So many little things to worry about -- e.g. currently we store
>    function comments in the function source, which is not compressed in
>    the fasd format -- I imagine this is quite big in acl2's case, and can
>    easily be ommitted.
> 
>    Finally, I think I have a plan now re: mv fast-linking and mutual
>    recursion.  I won't commit for some considerable time, and will let
>    you know when its ready.  If anyone is interested I can describe, but
>    I don't expect any takers!
> 
>    Take care,
> 
>    > So here's what I propose:
>    > 
>    > A. (Like #3 in my email 23 Jun 2006 10:46:17) build in
>    > /projects/hvg/ACL2/v3-0-hons/, making full use of ACL2 proclaiming, but 
> with
>    > GCL auto-proclaim turned off.  The only modification I'll make to the 
> ACL2
>    > sources is this:
>    > 
>    >     (setq compiler::*compiler-auto-proclaim* nil si::*disable-recompile* 
> t)
>    > 
>    > B. (Like #2 in my email 23 Jun 2006 10:46:17) I'll build in
>    > /projects/hvg/ACL2/v3-0-hons-gcl-proclaim/, relying on GCL to do its
>    > auto-proclaims (with no ACL2 proclaiming).
>    > 
>    > C. Bob, it would be great if you'd keep /p/bin/xg unchanged till that's
>    > completed (at which time I'll send email).
>    > 
>    > D. I'll delete or smash these at any time:
>    > 
>    > /projects/hvg/ACL2/v3-0-hons-no-acl2-proclaim/
>    > /projects/hvg/ACL2/v3-0-hons-no-gcl-proclaim/
>    > /projects/hvg/ACL2/v3-0-hons-matt-backup/
>    > 
>    > (Camm, are you done with /v/filer3/v0q048/acl2/v3-0-debian/?)
>    > 
>    > OK with you both?  Should I do any of this with 
> si::*optimize-maximum-pages*
>    > on and avoid all explicit allocation??  If so, should I do so instead or 
> in
>    > addition to the existing approach of si::*optimize-maximum-pages* nil 
> with
>    > explicit allocation?
>    > 
>    > Thanks --
>    > --- Matt
>    >    Date: Sat, 24 Jun 2006 19:25:07 -0500
>    >    From: Robert Boyer <address@hidden>
>    >    Cc: address@hidden
>    > 
>    >    I have rebuilt /p/bin/xg and I have some evidence that you
>    >    will be able to get further with the regression that you
>    >    were last having trouble with, viz., I executed the text
>    >    below with this new /p/bin/xg, and it no longer caused that
>    >    weird error message in the compilation of axioms.lisp.
>    >    However, I'm not sure I understood the bug or the fix.
>    > 
>    >    We now face some questions.  1.  Should you now re-run all
>    >    three of those regressions on your machine with the new
>    >    /p/bin/xg to get more reliable data?  2.  Should I leave the
>    >    new xg as is until you are done with this?  Please advise.
>    >    No hurry.  If there are further problems, please cc me and
>    >    I'll try to work on them.
>    > 
>    >    Bob
>    > 
>    >    cd /u/boyer/acl2/acl2-sources
>    >    xg
>    >    (setq compiler::*default-c-file* t)
>    >    (setq compiler::*compiler-auto-proclaim* nil)
>    >    (setq si::*disable-recompile* t)
>    >    (load "init.lisp")
>    >    (in-package "ACL2")
>    >    (load "axioms.lisp")
>    >    (proclaim-file "axioms.lisp")
>    >    (compile-file "axioms.lisp")
>    > 
>    > 
>    > 
>    > 
> 
>    -- 
>    Camm Maguire                                               address@hidden
>    ==========================================================================
>    "The earth is but one country, and mankind its citizens."  --  Baha'u'llah
> 
> 
> 

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