Hi --
I'm at a bit of a loss. I tried again, this time with more allocation done at
the start based on the result of (room) at the end of the previous run. But
this time I ran out of cons space:
Error: The storage for CONS is exhausted.
Currently, 52275 pages are allocated.
Use ALLOCATE to expand the space.
Below is the test file that I used, in case this gives you any ideas. (The
main test is the call (certify-book "model-eq" ?), but I can't include input
file model-eq.lisp.) Perhaps we have to build with more than 64K pages.
++++++++++++++++++++++++++++++ test file ++++++++++++++++++++++++++++++
(value :q) ; exit ACL2 loop
(room)
; Allocate extra room.
(sloop::sloop for (type . n) in
'((hole . 500) ; unchanged
(relocatable . 750) ; was 500
(cons . 40000) ; was 2917
(fixnum . 250) ; was 100
(bignum . 400) ; unchanged
(symbol . 900) ; was 400
(array . 40) ; was unassigned
(string . 1000); was 200
(sfun . 60) ; was 40
)
when n
do
(cond
((eq type 'HOLE)
(si::set-hole-size n))
((eq type 'RELOCATABLE)
(si::allocate-relocatable-pages n))
(t (si::allocate type n t))))
(room)
(si::gbc-time 0)
(format t "*** Internal time: ~s~%" (get-internal-run-time))
(format t "*** Internal-time-units-per-second: ~s~%"
internal-time-units-per-second)
(lp) ; enter ACL2 read-eval-print loop
(ld "pkgs.lisp") ; some constant and package definitions
(certify-book "model-eq" ?) ; the main test
(value :q) ; exit ACL2 loop
(format t "*** Internal time: ~s~%" (get-internal-run-time))
(si::gbc-time)
(room)
++++++++++++++++++++++++++++++ end of test file ++++++++++++++++++++++++++++++
-- Matt
Date: Sat, 19 Jul 2003 21:18:45 +0300
From: "Vadim V. Zhytnikov" <address@hidden>
User-Agent: Mozilla/5.0 (Windows; U; Windows NT 5.1; ru-RU; rv:1.4)
Gecko/20030630
X-Accept-Language: ru-ru, ru
cc: address@hidden
X-MIME-Autoconverted: from 8bit to quoted-printable by amdext.amd.com id
h6JHJ1bk029276
X-WSS-ID: 1307A21C5363219-01-01
Content-Type: text/plain;
charset=koi8-r;
format=flowed
X-MIME-Autoconverted: from quoted-printable to 8bit by timon.amd.com id
h6JHMJm22449
Matt Kaufmann пишет:
> Hi --
>
> Sorry I couldn't reply soon (I just returned from vacation).
>
> I'm also really sorry to say that I can't provide the test example, since it's
> derived directly from AMD design data and I think it would take
considerable
> effort to "sanitize" it, if that's even possible. But below are some
details
> from the run, and if someone cares to suggest some allocate settings then
I'd
> be happy to re-run. Anyhow, here's some info that may halp.
>
> Here I'm focusing on one run from a suite of runs. The timing was as follows:
>
> ACL2 built on GCL:
> real 93m14.066s
> user 92m47.830s
> sys 0m16.260s
>
> ACL2 built on Allegro CL dynamic runtime:
> real 32m40.528s
> user 32m21.530s
> sys 0m10.140s
>
> I built ACL2 by starting with modest allocations and causing growth to occur
> slowly (details upon request). Here is the room available when I first
> started up ACL2.
>
> ACL2>(room)
> 2917/2917 82.0%CONS RATIO LONG-FLOAT COMPLEX STRUCTURE
> 100/100 18.4% FIXNUM SHORT-FLOAT CHARACTER RANDOM-STATE READTABLE
NIL
> 400/400 35.2% SYMBOL STREAM
> 1/2 37.2% PACKAGE
> 5/38 13.8% ARRAY HASH-TABLE VECTOR BIT-VECTOR PATHNAME CCLOSURE
FAT-STRING
> 200/200 46.4% STRING
> 400/400 1.8% CFUN BIGNUM
> 40/40 56.7% SFUN GFUN CFDATA SPICE NIL
>
> 1/100 contiguous (1 blocks)
> 1000 hole
> 500 0.1% relocatable
>
> 4063 pages for cells
> 5564 total pages
> 55769 pages available
> 4203 pages in heap but not gc'd + pages needed for gc marking
> 65536 maximum pages
>
> ACL2>
>
> At the end of the run, (room) gave the following.
>
> ACL2>(room)
> 50251/51062 98.9%350CONS RATIO LONG-FLOAT COMPLEX STRUCTURE
> 245/225 62.6% 77 FIXNUM SHORT-FLOAT CHARACTER RANDOM-STATE READTABLE
NIL
> 790/900 99.3% 2 SYMBOL STREAM
> 1/2 64.1% PACKAGE
> 29/38 3.2% ARRAY HASH-TABLE VECTOR BIT-VECTOR PATHNAME CCLOSURE
FAT-STRING
> 450/450 97.4%3916STRING
> 400/400 74.9% 9 CFUN BIGNUM
> 43/60 97.1% 1 SFUN GFUN CFDATA SPICE NIL
>
> 6414/6553 669 contiguous (17 blocks)
> 382 hole
> 750 68.2%669 relocatable
>
> 52209 pages for cells
> 59755 total pages
> 710 pages available
> 5071 pages in heap but not gc'd + pages needed for gc marking
> 65536 maximum pages
>
> ACL2>
>
> I particularly noticed a lot of string GCs, such as:
>
> [SGC for 93 STRING pages..(11793 writable)..(T=14).GC finished]
>
> Here are total counts of gc messages.
>
> [SGC for ... CONS pages]: 350
> [SGC for ... STRING pages]: 3916
> [SGC for ... FIXNUM pages]: 77
> [SGC for ... SYMBOL pages]: 2
> [SGC for ... CFUN pages]: 9
> [SGC for ... SFUN pages]: 1
> [SGC for 0 CONTIGUOUS-BLOCKS pages]: 12
> [SGC for 0 RELOCATABLE-BLOCKS pages]: 553
>
> I can send you all 4920 lines of SGC messages if you like. I also got this count:
>
> [GC for ... RELOCATABLE-BLOCKS pages]: 116
>
Try to call
(si::gbc-time 0)
before starting ACL2 test. This function activates
internal GC timing counter. Finally (si::gbc-time) will
give total time spent by GCL in GC (the sum of T=... in GC messages)
in some internal units (1/100 of second as far as I recall).
I'm perfectly sure that from 60% to 90% of total time
is wasted in the GC. If you increase preallocated space
(especially for storage types which cause more frequent GC)
then total GC time should go down significantly keeping
(net time) = (total time) - (total GC time)
approximately constant.
--
Vadim V. Zhytnikov
<address@hidden>
<address@hidden>