[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Gcl-devel] Re: xg rebuilt
From: |
Camm Maguire |
Subject: |
[Gcl-devel] Re: xg rebuilt |
Date: |
26 Jun 2006 15:45:30 -0400 |
User-agent: |
Gnus/5.09 (Gnus v5.9.0) Emacs/21.2 |
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
[Prev in Thread] |
Current Thread |
[Next in Thread] |
- [Gcl-devel] Re: xg rebuilt,
Camm Maguire <=