gcl-devel
[Top][All Lists]
Advanced

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [Gcl-devel] -mcmodel=large (was Re: Version_2_6_10pre)


From: Matt Kaufmann
Subject: Re: [Gcl-devel] -mcmodel=large (was Re: Version_2_6_10pre)
Date: Thu, 19 Sep 2013 17:06:44 -0500

Hi, Camm --

My first reaction is to go for #2.  My concern with #1 is that ACL2
users might well have versions of gcc older than 4.7 -- indeed, the
machine I typically use (which I think is less than two years old) has
gcc 4.6 on it.  My concern with #3 is the guesswork required.  Of
course, there is also guesswork with #2, but at least I'm used to it!
I see that (si::set-log-maxpage-bound 31) gives me 1048573 maximum
pages according to (room), and my sense was that this has always been
sufficient, perhaps even for ACL2(h), whose regressions can require
more memory than ACL2.

Sadly, using (si::set-log-maxpage-bound 31) didn't eliminate all the
regression failures that I reported, though it did reduce the number
from 9 to 2.  By increasing from 31 to 32 I was able to certify those
two remaining problem books:

books/rtl/rel9/support/lib3.delta1/division.lisp
books/centaur/regression/common.lisp

Specifically, I updated my local copy of ACL2 for #2 by setting the
maxpages as follows.

#+gcl
(when (fboundp 'si::set-log-maxpage-bound)

; In a preliminary version of GCL 2.6.10pre, we encountered nine regression
; failures.  Camm Maguire took and look and told us that we "exceeded the 2Gb
; relative address limit for the default gcc small memory model."  The setting
; below gives us 2097149 maximum pages according to (room), which we think may
; be sufficient, even for ACL2(h).

  (si::set-log-maxpage-bound 32))

BUT.... Then I tried the full regression from scratch, and got
similar failures for the following (and the regression is still
running):

books/workshops/2004/legato/support/generic-theory-tail-recursion-mult.lisp
books/workshops/2011/cowles-gamboa-sierpinski/support/verifying-macros.lisp
books/workshops/2004/schmaltz-borrione/support/getting_rid_of_mod.lisp
books/workshops/2007/schmaltz/genoc-v1.0/instantiations/routing/octagon-routing/routing_local_lemmas.lisp
books/tau/bounders/elementary-bounders.lisp

So now I'm stumped.

One thing I should mention, though, is that I also had to avoid errors
like the following, which I did by commenting out long-standing code
that messes with the hole size.

  Error: Illegal value for the hole size.
  Fast links are on: do (si::use-fast-links nil) for debugging
  Error signalled by SYSTEM:SET-HOLE-SIZE.

Perhaps I should have continued to set the hole size (but changed the
exiting code for that, to avoid the error).  I don't understand GCL at
that level, though -- I'm basically a vanilla Lisp user -- so I don't
know what to do here.  And by the way, the hole size isn't the only
thing messed with when initializing and saving ACL2.  If you search
for "hole-size" in the sources you'll find it in function
save-acl2-in-akcl (file acl2-init.lisp), in particular here:

  (si::set-hole-size 500) ; wfs suggestion

That suggestion from Bill Schelter was many years ago, so I'm willing
to believe that it's out of date.  Perhaps a lot of the other code in
that function that messes with allocations is also out of date.  It
would be nice to avoid messing with any of that -- I don't recall
doing anything like that for the other six Common Lisps on which we
can build and run ACL2.

Probably the next step would be for you to try to complete a
regression at UT.  I've put the two changed ACL2 source files in a new
subdirectory, from-matt-09-19/, of the directory camm-09-19/ that
you've been using today at UT CS.  You could follow the instructions
from my email this morning (also in file camm-09-19/README-camm) after
replacing the two files with those in from-matt-09-19/.  And of
course, feel free to ask me for help.

Thanks --
-- Matt
   From: Camm Maguire <address@hidden>
   Date: Thu, 19 Sep 2013 11:16:45 -0400

   Greetings!  And thank you again so much for your report!

   We've exceeded the 2Gb relative address limit for the default gcc small
   memory model.  Pointer offsets are stored in 32bits in this model, and
   in the examples you cite below we just go over this.

   There are three possible solutions:

   1) append " -mcmodel=large" to compiler::*cc*.  I'm testing this now on
   seafoam.  The disadvantage here is that this appears to be
   amd64/itanium/ppc64 only at gcc 4.7.  Nonetheless, this is the way of
   the future -- on seafoam, the new dynamic maxpage algorithm has claimed
   68G of heap!

   2) use (si::set-log-maxpage-bound 29) for a 1Gb limit, (or 30 for 2Gb,
   etc.)  As acl2 6.2 will certify in 1Gb, your development version is
   likely to as well.  With a apparently large available heap, gcl will be
   generous with its allocations and will be likely to spread code further
   apart than really necessary.  Disadvantage here is that you look to be
   on the path to outgrow this soon, if not already.

   3) make a large contiguous block allocation (enough for all possible
   code to be loaded) at the beginning with #'si::allocate, placing it low
   in memory.  This is somewhat adhoc as you will never know how to set
   this size precisely.  Yet the code might run faster without huge jumps
   (not sure about this these days.)

   2) and 3) are somewhat obviously available at the lisp level.  1) can
   also be performed by the user either in lisp, or when compiling gcl as
   follows:

   CFLAGS="-mcmodel=large " ./configure && make

   Depending on what we decide to do, I might make this the default on
   amd64 inside configure.

   Take care,


   Matt Kaufmann <address@hidden> writes:

   > Hi, Camm --
   >
   > Thanks for the git instructions.  I followed them and then did this:
   >
   > dunnottar:/projects/acl2/lisps/gcl/2.6.10pre/gcl/gcl% ./configure && make
   >
   > Then I built ACL2 using this script:
   >
   > dunnottar:/projects/acl2/devel% cat ~/bin/my-fast-gcl
   > #!/bin/sh
   >
   > /projects/acl2/lisps/gcl/2.6.10pre/gcl/gcl/bin/gcl -eval '(defparameter 
user::*fast-acl2-gcl-build* t)' "$@"
   > dunnottar:/projects/acl2/devel% 
   >
   > Here's the build command:
   >
   > dunnottar:/projects/acl2/devel% alias fast-make-linux-gcl-acl2
   > rm -f TAGS ; mv make-fast-gcl.log make-fast-gcl.old.log ; (time nice make 
PREFIX=fast-linux-gcl- LISP=my-fast-gcl) >& make-fast-gcl.log&
   > dunnottar:/projects/acl2/devel% fast-make-linux-gcl-acl2
   >
   > Then I ran the regression:
   >
   > dunnottar:/projects/acl2/devel% (time nice make -j 8 regression-fresh 
ACL2=acl2l-gcl-fast) >& logs/make-regression-gcl-j-8-sept18.log&
   >
   > Sadly, there were 9 failures (18 matches below, 2 matches per
   > failure):
   >
   > dunnottar:/projects/acl2/devel% fgrep FAILED 
logs/make-regression-gcl-j-8-sept18.log
   > **CERTIFICATION FAILED** for 
/v/filer4b/v11q002/acl2space/acl2/devel/books/workshops/2004/legato/support/generic-theory-tail-recursion-mult.lisp
   > **CERTIFICATION FAILED** for 
/v/filer4b/v11q002/acl2space/acl2/devel/books/workshops/2004/legato/support/generic-theory-tail-recursion-mult.lisp
   > **CERTIFICATION FAILED** for 
/v/filer4b/v11q002/acl2space/acl2/devel/books/workshops/2011/cowles-gamboa-sierpinski/support/verifying-macros.lisp
   > **CERTIFICATION FAILED** for 
/v/filer4b/v11q002/acl2space/acl2/devel/books/workshops/2011/cowles-gamboa-sierpinski/support/verifying-macros.lisp
   > **CERTIFICATION FAILED** for 
/v/filer4b/v11q002/acl2space/acl2/devel/books/workshops/2004/schmaltz-borrione/support/getting_rid_of_mod.lisp
   > **CERTIFICATION FAILED** for 
/v/filer4b/v11q002/acl2space/acl2/devel/books/workshops/2004/schmaltz-borrione/support/getting_rid_of_mod.lisp
   > **CERTIFICATION FAILED** for 
/v/filer4b/v11q002/acl2space/acl2/devel/books/workshops/2007/schmaltz/genoc-v1.0/instantiations/routing/octagon-routing/routing_local_lemmas.lisp
   > **CERTIFICATION FAILED** for 
/v/filer4b/v11q002/acl2space/acl2/devel/books/workshops/2007/schmaltz/genoc-v1.0/instantiations/routing/octagon-routing/routing_local_lemmas.lisp
   > **CERTIFICATION FAILED** for 
/v/filer4b/v11q002/acl2space/acl2/devel/books/models/jvm/guard-verified-m1/find-k!.lisp
   > **CERTIFICATION FAILED** for 
/v/filer4b/v11q002/acl2space/acl2/devel/books/models/jvm/guard-verified-m1/find-k!.lisp
   > **CERTIFICATION FAILED** for 
/v/filer4b/v11q002/acl2space/acl2/devel/books/models/jvm/m1/find-k!.lisp
   > **CERTIFICATION FAILED** for 
/v/filer4b/v11q002/acl2space/acl2/devel/books/models/jvm/m1/find-k!.lisp
   > **CERTIFICATION FAILED** for 
/v/filer4b/v11q002/acl2space/acl2/devel/books/tau/bounders/elementary-bounders.lisp
   > **CERTIFICATION FAILED** for 
/v/filer4b/v11q002/acl2space/acl2/devel/books/tau/bounders/elementary-bounders.lisp
   > **CERTIFICATION FAILED** for 
/v/filer4b/v11q002/acl2space/acl2/devel/books/workshops/2013/greve-slind/defung/defung-stress.lisp
   > **CERTIFICATION FAILED** for 
/v/filer4b/v11q002/acl2space/acl2/devel/books/workshops/2013/greve-slind/defung/defung-stress.lisp
   > **CERTIFICATION FAILED** for 
/v/filer4b/v11q002/acl2space/acl2/devel/books/rtl/rel9/support/lib3.delta1/sqrt.lisp
   > **CERTIFICATION FAILED** for 
/v/filer4b/v11q002/acl2space/acl2/devel/books/rtl/rel9/support/lib3.delta1/sqrt.lisp
   > dunnottar:/projects/acl2/devel% 
   >
   > I have no idea how to debug these.  All of the backtraces suggest that
   > the break was during load of a compiled file near the end of
   > certification.  I tried certifying one of the books manually after the
   > failure,
   > 
books/workshops/2011/cowles-gamboa-sierpinski/support/verifying-macros.lisp,
   > by using this sequence of input in order to get a more complete
   > backtrace by avoiding fast links.
   >
   > (defpkg "U" (union-eq *acl2-exports*
   >                  *common-lisp-symbols-from-main-lisp-package*))
   > :q
   > (si::use-fast-links nil)
   > (LP)
   > (certify-book "verifying-macros" ? t)
   >
   > Here's the error:
   >
   > * Step 3:  That completes the admissibility check.  Each form read
   > was an embedded event form and was admissible. We now retract back
   > to the initial world and try to include the book.  This may expose
   > local incompatibilities.
   > [SGC off][GC for 12672 CONTIGUOUS-BLOCKS pages..(T=35).GC finished]
   > [SGC on]Loading 
/v/filer4b/v11q002/acl2space/acl2/devel/books/data-structures/utilities.o
   > [SGC off]
   > Error: Caught fatal error [memory may be damaged]
   > Error signalled by LOAD-COMPILED.
   > Backtrace: eval > lp > ld-fn > ld-fn0 > ld-fn-body > ld-loop > 
ld-read-eval-print > trans-eval > ev-for-trans-eval > ev > ev-rec > 
ev-fncall-rec > raw-ev-fncall > acl2_*1*_acl2::certify-book-fn > 
certify-book-fn > include-book-fn > include-book-fn1 > process-embedded-events 
> eval-event-lst > trans-eval > ev-for-trans-eval > ev > ev-rec > ev-fncall-rec 
> raw-ev-fncall > acl2_*1*_acl2::include-book-fn > include-book-fn > 
include-book-raw-top > include-book-raw > load-compiled-book > load-compiled > 
load > system:universal-error-handler > system::break-level-for-acl2 > let* > 
UNLESS
   > ACL2 !>
   >
   > I still don't know what to do with it.  Load-compiled is really just
   > load, and somehow loading utilities.o caused a break.  I checked the
   > other 8 failures and none seemed to involve utilities.o, so I don't
   > think it was just that isolated file that's involved.
   >
   > If you like, I'll make you a directory on a CS machine so that you can
   > play with this.  Speaking of that, may I delete these old directories?
   >
   > /projects/acl2/camm/
   > /projects/acl2/camm-2013-09-04/
   >
   > Thanks --
   > -- Matt
   >    From: Camm Maguire <address@hidden>
   >    Date: Wed, 18 Sep 2013 20:57:28 -0400
   >
   >    Greetings!
   >
   >    Matt Kaufmann <address@hidden> writes:
   >
   >    > Hi, Camm --
   >    >
   >    > Great!  Would you be willing to send instructions for fetching GCL
   >    > 2.6.10pre, either by git or as a tarball (but probably git, I guess,
   >    > since my read is that you haven't yet made a final tarball)?  I might
   >    > put that on the ACL2 website soon, but for now I'd simply like to try
   >    > 2.6.10pre on Linux and Mac (OS 10.6.8).
   >    >
   >
   >    git clone git://git.sv.gnu.org/gcl.git
   >    cd gcl
   >    git checkout Version_2_6_10pre
   >    cd gcl
   >    ./configure && make 
   >
   >    or 
   >
   >    ./configure --enable-ansi && make 
   >
   >    Tarball in a few days, but like to make sure we're not slower than 2.6.8
   >    first. 
   >
   >    Take care,
   >    -- 
   >    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




reply via email to

[Prev in Thread] Current Thread [Next in Thread]