[Gcl-devel] Re: CONS Problem

[Camm Maguire]

Greetings, and thanks for the feedback!  I'm assuming you are
referring to GCL's three word cons below.  If so, which would you feel
has higher priority, a two word cons, or unlimited heap?

Take care,

"Warren A. Hunt Jr." <address@hidden> writes:

> Hi Camm,
> 
> I consider this very important.  I sometimes use OpenMCL, even though
> it is slower, because it is more frugal in its memory usage and it
> doesn't seem to suffer from having to identify types of space that
> require specific allocation.
> 
> Warren
> ++++++
> 
>   To: address@hidden
>   Cc: address@hidden, address@hidden,
>         address@hidden, address@hidden
>   Subject: Re: CONS Problem
>   From: Camm Maguire <address@hidden>
>   Date: 04 Jan 2005 10:15:15 -0500
> 
>   Greetings!  How would you all rate the importance of removing fixed
>   heap size bounds in GCL, allowing the image to expand until physical
>   memory is exhausted?  This would have to be done in a way which does
>   not trigger any performance penalties as observed by Matt, which I
>   believe are caused by the larger hole and relocatable block sizes that
>   come perforce at present with any image configured with extended
>   maxpages.  (e.g. right now the hole is 1/10 maxpages).  Rather these
>   areas should grow dynamically with the heap as well.
> 
>   I think this could be done rather straightforwardly on Linux.  I would
>   have to ask our Windows and MacOSX people about it, as they emulate
>   Unix's sbrk().
> 
>   BTW, to the fellow from rockwell -- we are working on unsigned long,
>   long long, and unsigned long long support in the compiler right now in
>   2.7 (cvs head).
> 
>   Take care,
> 
>   Matt Kaufmann <address@hidden> writes:
> 
>   > Hi --
>   > 
>   > I believe that the memory limit we're discussing is completely determined 
> by
>   > the underlying Lisp (GCL, Allegro CL, etc.).  When you build ACL2 
> (typically
>   > with "make"), the available memory is determined by how the underlying 
> Lisp
>   > executable was built.
>   > 
>   > Perhaps ACL2's installation instructions should clarify this point as 
> follows:
>   > 
>   >   PLEASE NOTE: The available memory for ACL2 is determined by the 
> underlying
>   >   Common Lisp executable.  If you need more memory, refer to your Common 
> Lisp's
>   >   instructions for building an executable.
>   > 
>   > I've added the above words for future releases to our development copy of 
> file
>   > installation.html, section "Creating An Executable Image".  Please let me 
> know
>   > if it seems that I'm missing something here.
>   > 
>   > -- Matt
>   >    X-IronPort-MID: 429621954
>   >    X-SBRS: 3.5
>   >    X-BrightmailFiltered: true
>   >    X-Ironport-AV: i="3.88,96,1102312800"; 
>   >       d="scan'208"; a="429621954:sNHT21577160"
>   >    From: <address@hidden>
>   >    Date: Mon, 3 Jan 2005 10:19:05 -0600
>   >    X-MIMETrack: Serialize by Router on 
> CollinsCRSMTP02/CedarRapids/RockwellCollins(Release
>   >     6.5.3|September 14, 2004) at 01/03/2005 10:26:40 AM,
>   >      Serialize complete at 01/03/2005 10:26:40 AM
>   >    Content-Type: multipart/alternative; boundary="=_alternative 
> 0059A39786256F7E_="
>   >    Reply-To: address@hidden
>   >    Sender: address@hidden
>   >    X-Listprocessor-Version: 8.2.10/020311/17:52 -- ListProc(tm) by CREN
>   >    X-SpamAssassin-Status: No, hits=-2.5 required=5.0
>   >    X-UTCS-Spam-Status: No, hits=-290 required=180
>   > 
>   >    This is a multipart message in MIME format.
>   >    --=_alternative 0059A39786256F7E_=
>   >    Content-Type: text/plain; charset="US-ASCII"
>   > 
>   >    Matt, Bill, Warren:
>   > 
>   >    Is there some way of making the memory space limit a compile-time 
> option 
>   >    for some future ACL2 release?  (A lot of other open source packages 
> ask 
>   >    the user to answer configuration questions before a compilation 
> begins, 
>   >    using a configure script and then autoconf and automake.) 
>   > 
>   >    FYI, we have been routinely running out of CONS space here at Rockwell 
>   >    since last summer.  We have survived using a special 
> extra-memory-enabled 
>   >    binary that Eric Smith built us.  So the out-of-memory issue is a 
> little 
>   >    more prevalent than one might think, and I suspect that more of us 
> will 
>   >    run into this limit as the size of our projects (and the proof 
>   >    capabilities of ACL2) slowly grow.
>   > 
>   >    The text for the user query might read:
>   > 
>   >      Do you want to allow ACL2 to use as much memory as possible [y/N]
>   >              By default, ACL2's maximum memory limit is set to a level 
>   >    intended
>   >              to optimize overall performance.  This limit is large 
>   >    enough for almost 
>   >              all applications.  However, a very large proof set may 
>   >    occasionally
>   >              need more memory.  Say "n" here to use the default limit, 
>   >    or "y" to use 
>   >              as much memory as possible.  If you aren't sure, answer 
>   >    "n".
>   > 
>   > 
>   >    Hope this helps.
>   > 
>   > 
>   >    May the Force be with you,
>   > 
>   >      -- Christian
>   > 
>   > 
>   > 
>   > 
>   > 
>   >    Matt Kaufmann <address@hidden> 
>   >    Sent by: address@hidden
>   >    01/02/2005 12:01 PM
>   >    Please respond to
>   >    address@hidden
>   > 
>   > 
>   >    To
>   >    address@hidden, address@hidden
>   >    cc
>   >    address@hidden
>   >    Subject
>   >    Re: CONS Problem
>   > 
>   > 
>   > 
>   > 
>   > 
>   > 
>   >    Bill --
>   > 
>   >    Are you using Linux or Solaris?  If you are using Linux then I might 
> be 
>   >    able to
>   >    build a larger image at UT (but let me know if you are using ACL2 2.9 
> or 
>   >    ACL2
>   >    2.9.1).  It would be interesting to compare performance.  Read on....
>   > 
>   >    Warren --
>   > 
>   >    I believe that in the past I've seen some performance degradation when 
> the
>   >    underlying GCL has enlarged memory.  I suspect that only very few users
>   >    (specifically, you and Bill!) have run out of memory using ACL2 built 
> on 
>   >    GCL
>   >    2.6.5.  Of course, users are welcome to build their own images, since 
> we
>   >    distribute the sources; the distributed image is only for convenience.
>   > 
>   >    -- Matt
>   >       Date: Tue, 28 Dec 2004 10:51:48 -0600
>   >       From: "Warren A. Hunt Jr." <address@hidden>
>   >       CC: address@hidden, address@hidden
>   > 
>   >       Hi Bill,
>   > 
>   >       I don't use the default ACL2 binary because of the GCL on which the
>   >       default ACL2 is built.  The storage limitations can be observed with
>   >       the (ROOM T) command (see below).
>   > 
>   >       I always first build a GCL with the maximum pages set to 262,144,
>   >       which is about as large as can be built on a 32-bit system.  This
>   >       provides a great deal more space.
>   > 
>   >       Matt,
>   > 
>   >       May I suggest that GCL-ACL2 systems be built with as large a memory 
> as
>   >       possible?  The 1/2 GByte configurations are of lessening value.
>   > 
>   >       Cheers,
>   > 
>   >       Warren
>   >       ++++++
>   > 
>   >   [hunt:~/] > acl2
>   >   GCL (GNU Common Lisp)  2.6.5 CLtL1    Aug 18 2004 10:07:03
>   >   Source License: LGPL(gcl,gmp), GPL(unexec,bfd)
>   >   Binary License:  GPL due to GPL'ed components: (BFD UNEXEC)
>   >   Modifications of this banner must retain notice of a compatible 
>   >    license
>   >   Dedicated to the memory of W. Schelter
>   > 
>   >   Use (help) to get some basic information on how to use GCL.
>   > 
>   >    ACL2 Version 2.9 built November 11, 2004  18:07:01.
>   >    Copyright (C) 2004  University of Texas at Austin
>   >    ACL2 comes with ABSOLUTELY NO WARRANTY.  This is free software and 
>   >    you
>   >    are welcome to redistribute it under certain conditions.  For 
>   >    details,
>   >    see the GNU General Public License.
>   > 
>   >    Initialized with (INITIALIZE-ACL2 'INCLUDE-BOOK *ACL2-PASS-2-FILES*
>   >                                                  NIL).
>   >    See the documentation topic note-2-9 for recent changes.
>   > 
>   >    NOTE!!  Proof trees are disabled in ACL2.  To enable them in emacs,
>   >    look under the ACL2 source directory in interface/emacs/README.doc; 
>   >    and, to turn on proof trees, execute :START-PROOF-TREE in the ACL2 
>   >    command loop.   Look in the ACL2 documentation under PROOF-TREE.
>   > 
>   >   ACL2 Version 2.9.  Level 1.  Cbd "/v/filer2/hunt/s/intel-data/".
>   >   Type :help for help.
>   >   Type (good-bye) to quit completely out of ACL2.
>   > 
>   >   ACL2 !>:q
>   > 
>   >   Exiting the ACL2 read-eval-print loop.  To re-enter, execute (LP).
>   >   ACL2>(room t)
>   > 
>   >     5141/5141   93.1%         CONS RATIO LONG-FLOAT COMPLEX STRUCTURE
>   >                43/28     45.8%         FIXNUM SHORT-FLOAT CHARACTER 
>   >    RANDOM-STATE READTABLE NIL
>   >               207/209    99.1%         SYMBOL STREAM
>   >                 1/2      37.2%         PACKAGE
>   >               227/228     0.3%         ARRAY HASH-TABLE VECTOR 
>   >    BIT-VECTOR PATHNAME CCLOSURE FAT-STRING
>   >               167/172    91.0%         STRING
>   >                21/27     31.2%         CFUN BIGNUM
>   >                62/115    91.8%         SFUN GFUN CFDATA SPICE NIL
>   > 
>   >     2599/2602                 contiguous (2705 blocks)
>   >                   13036                hole
>   >                   5242    0.0%         relocatable
>   > 
>   >                  5869 pages for cells
>   >                 26746 total pages
>   >                 92978 pages available
>   >                 11348 pages in heap but not gc'd + pages needed for gc 
>   >    marking
>   >                131072 maximum pages
>   > 
>   >   ACL2>
> 
> 
> 
> 

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