[Gcl-devel] Re: allocate woes

[Camm Maguire]

Greetings!

Bad news here -- it appears as if the stock Linux kernel won't let you
sbrk past 0x40000000 regardless of whether or not you are using
dynamic linking and regardless of shell ulimit settings:

=============================================================================
[SGC for 89450 CONS pages..(95024 writable)..(T=461).GC finished]
[SGC off][GC for 1848 RELOCATABLE-BLOCKS pages..
Unrecoverable error: Can't allocate.  Good-bye!.

Program received signal SIGABRT, Aborted.
0x0834ce91 in kill ()
(gdb) up
#1  0x0837e2e5 in raise ()
(gdb) up
#2  0x0834d108 in abort ()
(gdb) up
#3  0x08048c48 in error (s=0x83b048f "Can't allocate.  Good-bye!") at main.c:451
(gdb) up
#4  0x080aaa7f in alloc_page (n=135512) at alloc.c:160
(gdb) p core_end
$11 = 0x24efc000 <Address 0x24efc000 out of bounds>
(gdb) p n-m
$12 = 133633
(gdb) p 133633*4096
$13 = 547360768
(gdb) p/x core_end + 547360768
$14 = 0x458fd000
(gdb) p/x 0x458fd000-core_end
Argument to arithmetic operation not a number or boolean.
(gdb) p/x 0x458fd000-0x24efc000
$15 = 0x20a01000
(gdb) p/x 0x40000000-0x24efc000
$16 = 0x1b104000
(gdb) p sbrk(0x1a104000)
$17 = 619692032
(gdb) p/x 619692032
$18 = 0x24efc000
(gdb) p sbrk(0)
$19 = 1056964608
(gdb) p/x 1056964608
$20 = 0x3f000000
(gdb) p sbrk(0x800000)
$21 = 1056964608
(gdb) p sbrk(0x800000)
$22 = 1065353216
(gdb) p sbrk(0)
$23 = 1073741824
(gdb) p/x sbrk(0)
$24 = 0x40000000
(gdb) p sbrk(0x800000)
$25 = -1
(gdb) shell
address@hidden:/fix/t1/camm/debian/acl2/acl2-2.9.3$ ldd saved_acl2
        not a dynamic executable
address@hidden:/fix/t1/camm/debian/acl2/acl2-2.9.3$ ulimit -a
core file size        (blocks, -c) 0
data seg size         (kbytes, -d) unlimited
file size             (blocks, -f) unlimited
max locked memory     (kbytes, -l) unlimited
max memory size       (kbytes, -m) unlimited
open files                    (-n) 1024
pipe size          (512 bytes, -p) 8
stack size            (kbytes, -s) 8192
cpu time             (seconds, -t) unlimited
max user processes            (-u) 7168
virtual memory        (kbytes, -v) unlimited
address@hidden:/fix/t1/camm/debian/acl2/acl2-2.9.3$ uname -a
Linux intech19 2.4.25 #5 SMP Thu Feb 24 18:54:17 EST 2005 i686 GNU/Linux
address@hidden:/fix/t1/camm/debian/acl2/acl2-2.9.3$ 
=============================================================================

Needless to say, this is quite depressing.  It does appear that some
of your ACL2 users are running 2Gb cores on 32bit with some special
kernel, the patches to which must of a necessity be open source.  As
stated earlier, I'd be happy to package same for Debian should someone
kindly isolate them.

Robert Boyer <address@hidden> writes:

> Here is about the dumbest and least helpful bug-report/complaint I can recall
> making.
> 
> Concerning the static, maximally large, 2.7.0 GCL, it builds fine.  Wonderful.
> 
> And I can build ACL2 in it fine.  Even ANSI.  Also wonderful.
> 
> But in such an ACL2 saved image, I cannot allocate nearly as much as I would
> seem to have space for.  Below is a simple transcript.  The only hint of a
> clue/problem I can see is the
> 
>     -55726 pages in heap but not gc'd + pages needed for gc marking
> 

This is a long standing bug in the room report which I must fix.  Now
might not be a bad time :-) -- we'll see.

Also need to install your helpful modifications to same.  Might it not
be a good idea to set you and Warren up with cvs write access?

Take care,


> in the (room t) message.
> 
> Help!
> 
> Bob
> 
> P. S.  It seems one should
> 
>    (install-old-raw-prompt)
> 
> in this version of ACL2 to get decent error breaks and recovery therefrom.
> 
> 
> ACL2>% acl2
> GCL (GNU Common Lisp)  2.7.0 ANSI    Sep 28 2005 09:43:07
> 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.3 built September 28, 2005  10:20:33.
>  Copyright (C) 2005  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-3 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 2.9.3.  Level 1.  Cbd "/v/filer2/boyer/work/bdd-code/".
> 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    5013/4939  91.8%        CONS FIXNUM SHORT-FLOAT CHARACTER PATHNAME CFUN 
> NIL
>  8     328/330  17.5%         VECTOR SYMBOL HASH-TABLE ARRAY STRING 
> RANDOM-STATE SFUN CFDATA
>  4     107/112  27.3%         BIT-VECTOR BIGNUM RATIO LONG-FLOAT COMPLEX 
> CCLOSURE
> 10     319/328  99.3%         STRUCTURE
> 14       1/2    47.9%         STREAM
>  6     195/198  94.5%         GFUN PACKAGE READTABLE VFUN AFUN CLOSURE SPICE
> 
>       1310/1318               contiguous (208 blocks)
>            104857             hole
>            1498   0.0%        relocatable
> 
>       5963 pages for cells
>     113628 total pages
>     466386 pages available
>     -55726 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:           2097152 bytes
> immfix start:         0xc0000000
> immfix size:          536870912 fixnums
> 
> ACL2>(setq foo (make-list 70000000) bar nil)
> [SGC for 73 CONS pages..(3078 writable)..(T=0).GC finished]
> [SGC for 2468 CONS pages..(5473 writable)..(T=6).GC finished]
> [SGC for 6172 CONS pages..(9177 writable)..(T=17).GC finished]
> [SGC for 11728 CONS pages..(14733 writable)..(T=32).GC finished]
> [SGC for 20062 CONS pages..(23067 writable)..(T=55).GC finished]
> [SGC for 32563 CONS pages..(35568 writable)..(T=86).GC finished]
> [SGC for 51314 CONS pages..(54319 writable)..(T=140).GC finished]
> [SGC for 79441 CONS pages..(82446 writable)..(T=204).GC finished]
> [SGC off][GC for 1498 RELOCATABLE-BLOCKS pages..
> Unrecoverable error: Can't allocate.  Good-bye!.
> Abort
> % 
> 
> Final arithmetic note.  (70,000,000 * 8)/4000 = 140,000 pages I should need
> to the make list.  (room t) says I have 466386 pages available.  So what's
> the problem?
> 
> Thanks so much,
> 
> Bob
> 
> 
> 

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