gcl-devel
[Top][All Lists]
Advanced

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Gcl-devel] Re: running out of space


From: Camm Maguire
Subject: [Gcl-devel] Re: running out of space
Date: 19 Jun 2006 17:11:46 -0400
User-agent: Gnus/5.09 (Gnus v5.9.0) Emacs/21.2

Greetings!  OK, will do, but my result will be the same as yours on
this class of machine.

It is conceivable we could get closer to 3 gb by relaxing the power of
2 constraint.  Separately, did we not get a 1 billion cons acl2 image
on some 64bit machine of yours?  Lastly, while I know the Linux kernel
has some recent work in this area, something special needs to be done
at this level to get a 32bit kernel even to be able to address more
than about 2.7 or 3gb, if memory serves.

I'm testing a small patch now to 
1) prevent recompilation in the final link, and 
2) execute it with si::*optimize-maximum-pages* at nil.

Image size is going down from ~15k pages to 4200.

Take care,

Robert Boyer <address@hidden> writes:

> Just out of curiosity, can I ask you to spend a minute or
> two to get into your biggest ACL2 Gnu-Linux GCL environment
> and execute these two commands and send me the output?
> 
>   (room t)
> 
>   (loop for i from 1 collect (progn (print i) (make-list 1000000)))
> 
> Here's what I get here in a big, static, ansi, GCL 2.7.0,
> with some enlarged stacks, 32 bit, x86 Intel,
> elgin.cs.utexas.edu, with an ACL2 saved image alone that is
> now about 220 megabytes.  The total number of conses limit
> seems to be about 230 million conses, which seems
> arithmetically about right at 8 bytes per cons, 1 gb for the
> c control stack (where one might instead secret away another
> 100 million conses), and 1 gb for the Gnu-Linux/os (and
> immediate fixnums).  I'd be most happy to send you my
> cvs/build commands for these.
> 
>    ls -l /p/bin/xa
>    lrwxrwxrwx  1 boyer public 41 May 26 12:27 /p/bin/xa -> 
> /u/boyer/acl2/acl2-sources/saved_acl2.gcl
> 
> 
> Bob
> 
> -------------------------------------------------------------------------------
> 
> % xa
> GCL (GNU Common Lisp)  2.7.0 ANSI    Jun 19 2006 13:26:51
> Source License: LGPL(gcl,gmp,pargcl), 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.
> 
> Temporary directory for compiler files set to /tmp/
> 
>  ACL2 Version 3.0 built June 19, 2006  14:05:21.
>  Copyright (C) 2006  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*).
>  See the documentation topic note-3-0 for recent changes.
>  Note: We have modified the prompt in some underlying Lisps to further
>  distinguish it from the ACL2 prompt.
> 
>  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 3.0.  Level 1.  Cbd "/v/filer2/boyer/acl2/acl2-sources/".
> 
> 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)
> 
> WS      UP/MP     FI%      GC TYPES
> 
>  2   10000/10000  53.8%       CONS FIXNUM SHORT-FLOAT CHARACTER IFUN SPICE
>  8    2448/2448   2.5%        ARRAY PATHNAME BIT-VECTOR VECTOR HASH-TABLE 
> STREAM CCLOSURE CLOSURE
>  4    1196/1196   7.1%        STRUCTURE BIGNUM RATIONAL LONG-FLOAT COMPLEX 
> READTABLE CFUN
> 10     600/600  58.9%         SYMBOL
> 14       1/2    52.1%         PACKAGE
>  6    1000/1000  25.0%        SFUN STRING RANDOM-STATE GFUN VFUN AFUN CFDATA
> 
>      20803/24690              contiguous (233 blocks)
>            10000              hole
>            2610   0.0%        relocatable
> 
>      15245 pages for cells
>      48658 total pages
>     450397 pages available
>      25233 pages in heap but not gc'd + pages needed for gc marking
>     524288 maximum pages
> 
> 
> Key:
> 
> WS: words per struct
> UP: allocated pages
> MP: maximum pages
> FI: fraction of cells in use on allocated pages
> GC: number of gc triggers allocating this type
> 
> word size:            32 bits
> page size:            4096 bytes
> heap start:           0x8000000
> heap max :            0x88000000
> shared library start: 0x0
> cstack start:         0xc0000000
> cstack mark offset:   223 bytes
> cstack direction:     downward
> cstack alignment:     16 bytes
> cstack max:           934215679 bytes
> immfix start:         0xc0000000
> immfix size:          536870912 fixnums
> NIL
> 
> ACL2>(loop for i from 1 collect (progn (print i) (make-list 1000000)))
> 
> 1 [SGC for 465 CONS pages..(9378 writable)..(T=7).GC finished]
> 
> 2 
> 3 [SGC for 5465 CONS pages..(14378 writable)..(T=29).GC finished]
> 
> 4 [SGC for 7167 CONS pages..(16080 writable)..(T=35).GC finished]
> 
> 5 
> 6 [SGC off][GC for 2610 RELOCATABLE-BLOCKS pages..(T=64).GC finished]
> [GC for 2610 RELOCATABLE-BLOCKS pages..(T=64).GC finished]
> [SGC on][SGC for 19970 CONS pages..(26240 writable)..(T=16).GC finished]
> 
> 7 
> 8 
> 9 
> 10 
> 11 
> ... much deleted
> 216 
> 217 
> 218 
> 219 
> 220 
> 221 
> 222 
> 223 [SGC for 66434 CONS pages..(72708 writable)..(T=369).GC finished]
> [SGC for 66434 CONS pages..(72708 writable)..(T=370).GC finished]
> [SGC for 66434 CONS pages..(72709 writable)..(T=371).GC finished]
> [SGC for 66434 CONS pages..(72709 writable)..(T=279).GC finished]
> 
> time to give up
> 
> 
> 

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




reply via email to

[Prev in Thread] Current Thread [Next in Thread]