[Top][All Lists]
[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
- [Gcl-devel] Re: running out of space,
Camm Maguire <=