[Gcl-devel] Re: address@hidden: increasing number of CONS pages?]

[Camm Maguire]

Greetings!

One immediate thing you can do is (setq si::*optimize-maximum-pages*
nil).  This will result in quite a bit more gc time, but will keep the
heap size to an absolute minimum.  A less draconian measure is to
preallocate more cons pages before the run to prevent the memory
balancing algorithm from placing the pages elsewhere, but I'd try the
former first.

FYI, we just completed successful tests of a gcl with a 2 word cons,
giving 50% more cons space in the same heap, together with a heap
start lowering algorithm giving 1/8 more heap on Linux, together with
an immediate fixnum table covering 1/4 the range accelerating
undeclared fixnum arithmetic by a factor of 2.8.  It will still be a
while before this reaches a stable release.  One item which will
likely be obsolete is the larger fixnum table you use, which also will
free up some space.

You know about (room), right?

Take care,

"Matt Kaufmann" <address@hidden> writes:

> Hi, Camm --
> 
> I hope you can make a suggestion for John on this, because I have no idea!
> 
> In the longer term, I hope to find ways for ACL2 to reduce memory usage.  And 
> I
> have a particular area in which to look (theory handling) when I have time.
> But in general, are there any simple tools for tracking memory usage in GCL?
> 
> Thanks --
> -- Matt
> From: "John Matthews" <address@hidden>
> Subject: increasing number of CONS pages?
> To: address@hidden
> Date: Tue, 7 Jun 2005 09:08:01 -0700
> Reply-to: address@hidden
> 
> I am running into problems in certifying large ACL2 books on the 
> Macintosh. I am currently running Mac OS version 10.3.9 (7W98), on a 
> 15" powerbook with a 1.5GHz G4 CPU, and 1GB of memory. I am running 
> ACL2 on top of GCL 2.6.6, with configuration option enable-maxpages set 
> to 192*1024.
> 
> One of the books I am trying to certify fails with the following error:
> 
>    Summary
>    Form:  ( INCLUDE-BOOK "aamp_ops-3" ...)
>    Rules: NIL
>    Warnings:  None
>    Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
>    :REDUNDANT
>    [GC for 58999 CONS pages..(T=254).GC finished]
>    [GC for 58999 CONS pages..(T=261).GC finished]
>    [GC for 58999 CONS pages..(T=244).GC finished]
>    [GC for 58999 CONS pages..(T=267).GC finished]
>    [GC for 58999 CONS pages..(T=263).GC finished]
>    [GC for 58999 CONS pages..(T=251).GC finished]
>    [GC for 58999 CONS pages..(T=260).GC finished]
>    [GC for 58999 CONS pages..(T=286).GC finished]
>    [GC for 38066 RELOCATABLE-BLOCKS pages..(T=282).GC finished]
>    [GC for 95211 RELOCATABLE-BLOCKS pages..(T=267).GC finished]
>    [GC for 59470 CONS pages..(T=277).GC finished]
> 
>    Error: The storage for CONS is exhausted.
>        Currently, 59470 pages are allocated.
>        Use ALLOCATE to expand the space.
>    Fast links are on: do (si::use-fast-links nil) for debugging
>    Error signalled by DEFUN-FN.
>    Broken at COND.  Type :H for Help.
>    ACL2>>
> 
> How can I increase the default number of pages allocated for CONS 
> cells, without modifying the books I am trying to certify?
> 
> Thanks!
> - -john
> ----------
> 
> 
> 
> 
> 

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