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

[Camm Maguire]

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