Re: [Gcl-devel] address@hidden: Re: -mcmodel=large

[Camm Maguire]

Greetings, and thanks so much for your report!

For the record, #1 worked, but -mcmodel=large fails to compile gcl
itself in a few places due to a few remaining gcc bugs.  Apparently this
option suffers from little use.  So solution #1 is for the future.

While both #2 and #3 require some guesswork, #3 leaves the heap
unbounded for general purpose, which seems critical in the 'modern'
era.  

Gcl's philosophy here is that of lisp in general -- code is data.  How
reasonable to design data to hold code at any particular location.  This
2Gb limit is a temporary gcc compiler/computer architecture limitation
and should thus call for a workaround, not a redesign.  

I've added the following to 2.6.10pre:

1) to prefer low memory when loading code, easily reversible when the
time comes.
2) enhancements to make this area available in sgc.  Contiguous memory
had no sgc bit like cells, and thus could not support old data on sgc
pages.  Thus sgc contiguous pages were required to be completely free,
which would make a large preallocated region in low memory unavailable
after the first use followed by sgc-off/sgc-on.  I've added the support
for partially free contiguous sgc pages via a sgc bit table in the page
structure.   Apparently this alone suffices to build the regression
without errors, but in case the low memory again fills up for some
reason, one now has recourse to

(si::allocate 'contiguous 30000 t);allocate 30000 contiguous block pages
and 
(si::allocate-sgc 30000 100000 10) ;require a minimum of 30000 contiguous
                                   ;block pages when setting up sgc, a
                                   ;maximum of 100000, and don't use
                                   ;blocks that are less than 10% free.

I preallocated such a region on an earlier run and regressed without
failure, but this appears unnecessary.

Anyway, please let me know what you think.  I've uploaded 2.6.10pre to
Debian unstable as 2.6.9-2 to see where we stand on the autobuilders.
I'm ready to release 2.6.10 if this looks good.

As for the hole size, I think gcl's automatic behavior should be good
for now, but we can revisit this later if necessary.  I agree its best
for the user not to have to do anything here, and have put some work
into making the default behavior good.  The hole shrinks to a page on
image save, expands to a constant fraction of the maxpages in force on
first relocatable gc, and shrinks as the available heap remaining
shrinks. 

Take care,

Matt Kaufmann <address@hidden> writes:

> P.S. The failures using (si::set-log-maxpage-bound 32) [with no
> manipulation of the hole size] were the same as before I messed with
> maxpages.
>
> From: Matt Kaufmann <address@hidden>
> Subject: Re: -mcmodel=large (was Re: Version_2_6_10pre)
> To: Camm Maguire <address@hidden>
> CC: address@hidden
> Date: 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
> ----------
>

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