[Gcl-devel] Re: contiguous blocks exhausted

[Matt Kaufmann]

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