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 <[email protected]> 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 <[email protected]> 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 <[email protected]> > Date: Wed, 18 Sep 2013 20:57:28 -0400 > > Greetings! > > Matt Kaufmann <[email protected]> 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 [email protected] > ========================================================================== > "The earth is but one country, and mankind its citizens." -- Baha'u'llah > > > > > -- Camm Maguire [email protected] ========================================================================== "The earth is but one country, and mankind its citizens." -- Baha'u'llah _______________________________________________ Gcl-devel mailing list [email protected] https://lists.gnu.org/mailman/listinfo/gcl-devel
