[Gcl-devel] Re: contiguous blocks exhausted

[Camm Maguire]

Greetings!  Just to report, compiled a gcl with debugging turned on
just in case, and with maxpages = 1024*1024.  This command completes
both with and without the (si::set-gmp-allocate-relocatable t)
command, with the following timings out of the box:

(si::set-gmp-allocate-relocatable nil) real     0m18.685s
(si::set-gmp-allocate-relocatable t)   real     0m14.810s

It appears as if this can be further improved via some memory
preallocation along Vadim's suggestions.

Please let me know if you need instructions as to building an acl2
image on top of such an expanded gcl.

Take care,


Matt Kaufmann <address@hidden> writes:

> Hi, Camm --
> 
> Below is a file foo.lisp (Cynthia's file, with stuff added that was missing).
> Then just start ACL2 and do the following.
> 
> (certify-book "foo")
> (lastclause 10 487 349)
> 
> In subsequent ACL2 sessions you can instead do:
> 
> (include-book "foo")
> (lastclause 10 487 349)
> 
> ============================== file foo.lisp ==============================
> 
> (in-package "ACL2")
> 
> (program)
> 
> (defun nat-p (n)
>   (if (and (integerp n)
>            (> n 0))
>       t
>     nil))
> 
> (defun fact1 (n acc)
>   (declare (type (signed-byte 29) n))
>   (if (zp n)
>       acc
>     (fact1 (1-f n) (* n acc))))
> 
> (defun fact (n)
>   (declare (type (signed-byte 29) n))
>   (fact1 n 1))
> 
> (defun choose (k n)
>   (floor (fact n)
>          (* (fact k) (fact (- n k)))))
> 
> (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)))
> 
> ======================================================================
> 
> -- Matt
>    Cc: address@hidden, address@hidden
>    From: Camm Maguire <address@hidden>
>    Date: 12 Dec 2003 15:00:35 -0500
>    User-Agent: Gnus/5.09 (Gnus v5.9.0) Emacs/21.2
>    Content-Type: text/plain; charset=us-ascii
> 
>    Greetings!  BTW, I just built an ACL2 with 4G maxpages for testing.  I
>    entered the original code, but get:
> 
>    ACL2 Error in ( DEFUN BIN-EXPANSION ...):  The symbol CHOOSE (in package
>    "ACL2") has neither a function nor macro definition in ACL2.  Please
>    define it.
> 
>    How does one actually run this test, step by step?
> 
>    Take care,
> 
>    Matt Kaufmann <address@hidden> writes:
> 
>    > Hi --
>    > 
>    > In a nutshell, I believe that what is happening is that the underlying 
> Lisp,
>    > which appears to be GCL, is running out of (a certain kind of) space 
> because of
>    > the way it handles numbers.  I was able to execute (lastclause 10 487 
> 349)
>    > successfully in ACL2 2.7 built on Allegro Common Lisp, which handles 
> numbers
>    > differently.  Now for details.
>    > 
>    > First, I should mention that in order to try your example I had to fill 
> in the
>    > definition of choose (I didn't see it in your email, but it is used in 
> your
>    > definition of bin-expansion).  I decided to turn your script into a 
> certifiable
>    > book, by prepending the following events.  The reason I start with 
> (program) is
>    > a bit subtle, pertaining to guards and evaluation; I'll discuss that 
> later
>    > below.
>    > 
>    >   (in-package "ACL2")
>    > 
>    >   (program)
>    > 
>    >   (defun nat-p (n)
>    >     (if (and (integerp n)
>    >       (> n 0))
>    >  t
>    >       nil))
>    > 
>    >   (defun fact1 (n acc)
>    >     (if (zp n)
>    >  acc
>    >       (fact1 (1- n) (* n acc))))
>    > 
>    >   (defun fact (n)
>    >     (fact1 n 1))
>    > 
>    >   (defun choose (k n)
>    >     (floor (fact n)
>    >     (* (fact k) (fact (- n k)))))
>    > 
>    > Then I executed the following in an Allegro Common Lisp build of ACL2 
> Version
>    > 2.7:
>    > 
>    >   (certify-book "foo")
>    >   :q
>    >   (time (lastclause 10 487 349))
>    > 
>    > The result of the last of these was as follows:
>    > 
>    >   ACL2(2): (time (lastclause 10 487 349))
>    >   ; cpu time (non-gc) 31,440 msec user, 10 msec system
>    >   ; cpu time (gc)     2,480 msec user, 0 msec system
>    >   ; cpu time (total)  33,920 msec user, 10 msec system
>    >   ; real time  33,925 msec
>    >   ; space allocation:
>    >   ;  1,462,993 cons cells, 1,061,547,136 other bytes, 0 static bytes
>    >   899
>    >   ACL2(3): 
>    > 
>    > The reason I used (program) is that otherwise, ACL2 will execute in the 
> logic.
>    > Since you didn't provide any guards, that execution will not take place 
> using
>    > raw Common Lisp and could therefore be slow (though :comp t would help; 
> but I
>    > don't want to over-complicate things here).  See the documentation topic 
> GUARD
>    > for more on this.
>    > 
>    > So, back to GCL.  Sometimes you can speed up GCL (to be even faster than
>    > Allegro, I think) by adding appropriate declarations.  I tried the 
> following.
>    > 
>    >   (defun fact1 (n acc)
>    >     (declare (type (signed-byte 29) n))
>    >     (if (zp n)
>    >  acc
>    >       (fact1 (1-f n) (* n acc))))
>    > 
>    >   (defun fact (n)
>    >     (declare (type (signed-byte 29) n))
>    >     (fact1 n 1))
>    > 
>    > But that wasn't sufficient.  What I really wanted to do was to declare 
> acc to
>    > be a fixnum as well, but the problem is:  it's not, in general.  Some of 
> the
>    > calls of factorial return really huge numbers.
>    > 
>    > Perhaps I should have defined (choose k n) recursively, just to multiply 
> the
>    > integers from n down to k+1.  But I'm guessing that wouldn't have helped.
>    > 
>    > 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.
>    > 
>    > Let me know if you have any questions.
>    > 
>    > -- 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
> 
> 
> 

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