[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Gcl-devel] Re: contiguous blocks exhausted
From: |
Matt Kaufmann |
Subject: |
[Gcl-devel] Re: contiguous blocks exhausted |
Date: |
Fri, 12 Dec 2003 09:33:44 -0600 |
Thanks! (For members of the acl2-help list who may not know: Camm Maguire is
the principal maintainer of GCL, which has probably been the underlying Lisp
chosen by most ACL2 users, perhaps by far. Thanks, Camm!)
I just tried (si::set-gmp-allocate-relocatable t) after including the book,
with ACL2 2.7 on GCL 2.5.0, Debian Gnu Linux 2.4.23. Apparently GCL needs a
larger number of maximum pages in order for this to help (probably that's what
you were saying, but at first I thought you meant that
si::set-gmp-allocate-relocatable was an alternative to increasing the max
pages).
ACL2 !>(lastclause 2 487 349)
[SGC for 0 RELOCATABLE-BLOCKS pages..(3100 writable)..(T=5).GC finished]
[SGC for 0 RELOCATABLE-BLOCKS pages..(3600 writable)..(T=6).GC finished]
[SGC for 0 RELOCATABLE-BLOCKS pages..(4100 writable)..(T=9).GC finished]
[SGC for 0 RELOCATABLE-BLOCKS pages..(4850 writable)..(T=11).GC finished]
[SGC for 0 RELOCATABLE-BLOCKS pages..(5974 writable)..(T=16).GC finished]
[SGC for 0 RELOCATABLE-BLOCKS pages..(7660 writable)..(T=21).GC finished]
[SGC for 0 RELOCATABLE-BLOCKS pages..(9660 writable)..(T=24).GC finished]
[SGC for 0 CFUN pages..(11664 writable)..[SGC off] (doing full gc)[SGC
on](T=25).GC finished]
[SGC for 0 RELOCATABLE-BLOCKS pages..(2221 writable)..(T=2).GC finished]
[SGC for 0 RELOCATABLE-BLOCKS pages..(5302 writable)..(T=7).GC finished]
[SGC for 0 RELOCATABLE-BLOCKS pages..(8448 writable)..(T=11).GC finished]
[SGC for 0 RELOCATABLE-BLOCKS pages..(12001 writable)..(T=18).GC finished]
[SGC for 0 RELOCATABLE-BLOCKS pages..(14088 writable)..(T=23).GC finished]
[SGC for 0 CFUN pages..(16140 writable)..[SGC off] (doing full gc)[SGC
on](T=24).GC finished]
[SGC for 0 RELOCATABLE-BLOCKS pages..(2606 writable)..(T=5).GC finished]
[SGC for 0 RELOCATABLE-BLOCKS pages..(5695 writable)..(T=10).GC finished]
[SGC for 0 RELOCATABLE-BLOCKS pages..(9202 writable)..(T=11).GC finished]
Error: Relocatable blocks exhausted.
Currently, 12375 pages are allocated.
Use ALLOCATE-RELOCATABLE-PAGES to expand the space.
Fast links are on: do (si::use-fast-links nil) for debugging
Error signalled by RETURN-FROM.
Broken at COND. Type :H for Help.
ACL2>>:q
ACL2 !>:q
Exiting the ACL2 read-eval-print loop. To re-enter, execute (LP).
ACL2>(si::allocate-relocatable-pages 13000)
Error: Can't set the limit for relocatable blocks to 13000.
Fast links are on: do (si::use-fast-links nil) for debugging
Error signalled by SYSTEM:ALLOCATE-RELOCATABLE-PAGES.
Broken at COND. Type :H for Help.
ACL2>>
-- Matt
Cc: address@hidden, address@hidden, address@hidden
From: Camm Maguire <address@hidden>
Date: 12 Dec 2003 10:20:42 -0500
User-Agent: Gnus/5.09 (Gnus v5.9.0) Emacs/21.2
Content-Type: text/plain; charset=us-ascii
Reply-To: address@hidden
Sender: address@hidden
X-Listprocessor-Version: 8.2.10/020311/17:52 -- ListProc(tm) by CREN
Greetings!
Matt Kaufmann <address@hidden> writes:
> ; 1,462,993 cons cells, 1,061,547,136 other bytes, 0 static bytes
^^^^^^^^^^^^^
If this means what I think it means, then GCL will have to be compiled
with a larger number of maximum pages. Right now that is set at 128M
by default. This is easy to do.
It might not be a bad idea to hardcode the default maxpages to 4G on
32bit systems, the maximum amount addressable. For 64bit systems, I
don't know what a sane default would be. This would no affect the
default image size much.
> To be fair to GCL, I don't think things would go any better in C without
some
> work. The numbers involved far exceed 2^64.
>
> So, unfortunately, my suggestion is either to switch to Allegro Common
Lisp if
> you can, or else to think about an algorithm that keeps the numbers in the
GCL
> fixnum range.
>
Fixnum's are of course much faster, but there is something else you
can do for a dramatic speedup on computations like this:
(si::set-gmp-allocate-relocatable t)
I'm considering making this the default. It depends on a local patch
to the gmp library which ideally I'd like to be supported upstream,
but what we have now does appear to work.
> Let me know if you have any questions.
>
If anyone would like me to try these options and report back, I can do
that.
Take care,
> -- Matt
> Date: Thu, 11 Dec 2003 20:45:51 -0700 (MST)
> From: Cynthia Campos <address@hidden>
> X-Sender: <address@hidden>
> Content-Type: TEXT/PLAIN; charset=US-ASCII
> Reply-To: address@hidden
> Sender: address@hidden
> X-Listprocessor-Version: 8.2.10/020311/17:52 -- ListProc(tm) by CREN
>
> Hi all,
>
> this is the first time I've written to the helplist. I'm trying to
> implement the AKS primality testing algorithm and to do so, I need to
> implement a function computes the remainder of the binary expansion of a
> polynomial of the form (x + a)^n divided by another polynomial of the
form
> (x^r -1). I also have to compute the remainder of (x^n + a) divided by
> (x^r - 1). When this is done, I need to check that the mod of each
> element by n is equal.
>
> After many different implementations, I keep getting the following
error:
>
> Error: Contiguous blocks exhausted.
> Currently, 26670 pages are allocated.
> Use ALLOCATE-CONTIGUOUS-PAGES to expand the space.
> Fast links are on: do (si::use-fast-links nil) for debugging
> [SGC for 0 CONTIGUOUS-BLOCKS pages..(2498 writable)..(T=10).GC finished]
>
> For example, I got this error when i ran the following:
>
> (lastclause 2 487 349)
>
> However, when I restarted acl2 and loaded everything, I tried this same
> function and it was successful.
>
> I'm including the code that I've written. The majority of the functions
> are written for the specific case of dividing by a polynomial of the
form
> (X^r -1). I'm sure I'll have to prove theorems about some of the
> assumptions I've made, but I'm barely in the beginning stages.
>
> In order to reproduce the error, you can just run
> (lastclause 10 487 349)
>
> The factorial, binomial and mod-gcd books also need to be included.
>
> Any ideas would sure be of help because I'm unsure if this is a
> programming error.
>
> Thanks,
> Cynthia
>
> (defun nat-p (n)
> (if (and (integerp n)
> (> n 0))
> t
> nil))
>
> (defun bin-expansion (x y k n acc)
> (declare (xargs :measure (nfix (1+ (- n k)))))
> (if (and (integerp k) (integerp n) (<= 0 k) (<= k n))
> (bin-expansion x y (1+ k) n (cons (* (choose k n)
> (expt x k)
> (expt y (- n k)))
> acc))
> acc))
>
> (defun be (a n)
> (bin-expansion 1 a 0 n nil))
>
> (defun changelist (key new left right)
> (cond ((zp key) (cons left (cons (- (car right) new) (cdr right))))
> ((and (>= key 0)
> (listp left)
> (listp right))
> (changelist (1- key)
> new
> (cons (car right) left)
> (cdr right)))))
>
> (defun nl (pair)
> (if (consp pair)
> (append (reverse (car pair)) (cdr pair))
> nil))
>
> (defun polymod (pr cfl r)
> (cond ((and (zp pr)
> (consp cfl))
> (cdr (nl (changelist r (* (car cfl) -1) nil cfl))))
> ((and (consp cfl)
> (nat-p pr)
> (> pr 0))
> (polymod (- pr 1)
> (cdr (nl (changelist r (* (car cfl) -1) nil cfl)))
> r))
> (:else -900)))
> (defun comparelistswithmod (lh index rhi ra n length)
> (cond ((null lh) 199)
> ((and (int= length 1)
> (consp lh)
> (int= (mod (car lh) n) ra))
> (comparelistswithmod (cdr lh) (1+ index) rhi ra n (1- length)))
> ((and (consp lh)
> (not (int= index rhi))
> (zp (mod (car lh) n)))
> (comparelistswithmod (cdr lh) (1+ index) rhi ra n (1- length)))
> ((and (consp lh)
> (int= index rhi)
> (int= (mod (car lh) n) 1))
> (comparelistswithmod (cdr lh) (1+ index) rhi ra n (1- length)))
> (t -10)))
>
> (defun lastclause (a n r)
> (cond ((zp a) 899)
> ((or (not (nat-p a))
> (not (nat-p n))
> (not (nat-p r))) -3)
> ((> (comparelistswithmod
> (polymod (- n r) (be a n) r)
> 1 (- r (- n r)) a n r)
> 0)
> (lastclause (- a 1) n r))
> (:else -899)))
>
>
>
>
--
Camm Maguire address@hidden
==========================================================================
"The earth is but one country, and mankind its citizens." -- Baha'u'llah