[Gcl-devel] Re: address@hidden: address@hidden: Re: benchmarking]]

[Camm Maguire]

Greetings, and thanks!



Matt Kaufmann <address@hidden> writes:

> Howdy --
> 
> When using ACL2's proclaiming we get the following, for example (just start up
> /projects/hvg/ACL2/v3-0-hons-jun25/saved_acl2 and then :q):
> 
>   ACL2>(get 'rewrite 'SYSTEM:PROCLAIMED-ARG-TYPES)
> 
>   (T T T (UNSIGNED-BYTE 28) T T T T T T T T T T T T)
> 
>   ACL2>(get 'rewrite 'SYSTEM:PROCLAIMED-RETURN-TYPE)
> 
>   (VALUES T T)
> 
>   ACL2>
> 
> Using GCL's proclaiming instead (using
> /projects/hvg/ACL2/v3-0-hons-gcl-proclaim/saved_acl2) we get:
> 
>   ACL2>(get 'rewrite 'SYSTEM:PROCLAIMED-ARG-TYPES)
> 
>   (T T T (INTEGER 0 268435455) T T T T T T T T T T T T)
> 
>   ACL2>(get 'rewrite 'SYSTEM:PROCLAIMED-RETURN-TYPE)
> 
>   *
> 
>   ACL2>
> 
> So the arg types came out the same.  I think you said that any VALUES type is
> treated the same as *, so perhaps we can treat the result types as being "the
> same".

I'm working on a better mv call, so I am interested in cases where I
show * and you show something else.  Right now they are equivalent
performance-wise. 

I know the reason for most of my '* returns -- there are several
hundred legacy C functions without signature in GCL, and when these
appear in a return position of any function, '* propagates upward.

What might be kind of cool about the current implementation, is that
say one has found such a function, redefines it in lisp and compiles
it, all recursive callers are updated at once!

What also might be of use is that GCL keeps a complete call graph/tree
hierarchy which makes for useful flow analysis.  Functions which are
called most frequently (in terms of source lines of code) are easily
determined, as are the most important '*s to fix.

Here for example is how to print out gcl's proclaims list:

(in-package 'si)
(let ((h (make-hash-table :test 'equal))) 
        (maphash (lambda (x y) 
                    (let ((z (or (gethash (call-sig y) h) 
                             (setf (gethash (call-sig y) h) (list (call-sig y) 
nil))))) 
                         (pushnew x (cadr z)))) *call-hash-table*) 
        (maphash (lambda (x y) (princ `(proclaim (ftype (function 
,@y))))(terpri)) h))

Other useful functions here:

(function-src 'foo)
(recompile 'foo)
(call-callees (gethash 'foo *call-hash-table*))
(call-callers (gethash 'foo *call-hash-table*))
(all-callees 'foo nil)
(all-callers 'foo nil)

and, while you might have missed the email, for mutually recursive
functions 'foo and 'bar

(compile (convert-to-state 'foo))

makes them mutually tail-recursive where possible, like in scheme.

Take care,

> 
> I could run a test that every type declaration in acl2-proclaims.lisp (used by
> for the first version above) is the same as the type declaration from GCL (the
> second version above), where "same as" means that VALUES results are treated 
> as
> * and UNSIGNED-BYTE (etc.) is expanded to INTEGER range types.  Is that the
> right test, and if so, does it seem of interest?
> 

Any light you can shed on this, especially of a general nature, is
most useful.  Soon I'm going to commit an enlargement of
compiler::+useful-c-types+ which should give you identical integer
ranges as opposed to expanded ones at present.  As you know, limiting
the expansion limits the expansion of propagated types too.

Take care,

> -- Matt
>    Cc: address@hidden, address@hidden, address@hidden
>    From: Camm Maguire <address@hidden>
>    Date: 24 Jun 2006 14:26:47 -0400
>    X-SpamAssassin-Status: No, hits=-1.9 required=5.0
>    X-UTCS-Spam-Status: No, hits=-215 required=200
> 
>    P.S. just a note in passing as before stated, it certainly appears
>    that gcl and acl2 are both implementing very similar type inferencing
>    logic.  It would be great some day to consolidate.
> 
>    Take care,
> 
>    Matt Kaufmann <address@hidden> writes:
> 
>    > Good morning --
>    > 
>    > Thank you for looking into this.
>    > 
>    > I agree with Bob's answer:
>    > 
>    > >> I think that you should regard any xargs declaration as
>    > >> nothing more than a comment to be ignored.
>    > 
>    > But just in case you're simply looking for some intuition about this 
> (and since
>    > I've written most of this reply already!), I'll send this along in case 
> you
>    > find it useful.  (Feel free to ignore it!)
>    > 
>    > Roughly speaking, the (declare (xargs :guard form)) syntax asserts that 
> ACL2
>    > expects form to be true whenever the function is called.  More 
> precisely, ACL2
>    > is set up so that only when the above assertion is suitably proved, will 
> ACL2
>    > invoke Common Lisp to evaluate calls of the function whose arguments 
> satisfy
>    > the guard.
>    > 
>    > However, Common Lisp itself will ignore such declare forms (that's Bob's 
> point,
>    > I think).
>    > 
>    > In the case of aset1, the guard does imply that we have an 
> (unsigned-byte 31).
>    > Maybe that's what you were asking.  The rest of this email justifies that
>    > claim, but please don't feel obligated to read it, of course!
>    > 
>    > In the definition of aset1 we find:
>    > 
>    >   #+acl2-loop-only
>    >   (declare (xargs :guard (and (array1p name l)
>    >                               (integerp n)
>    >                               (>= n 0)
>    >                               (< n (car (dimensions name l))))))
>    > 
>    > But the definition of array1p implies that (car (dimensions name l)) is 
> less
>    > than 2^31; hence from the above, so is n.  Here are the relevant 
> snippets of
>    > code.
>    > 
>    > (defun array1p (name l)
>    > ....
>    >        (let ((header-keyword-list (cdr (assoc-eq :header l))))
>    > .....
>    >               (let ((dimensions (cadr (assoc-keyword :dimensions 
> header-keyword-list)))
>    > .....
>    >                 (and
>    > .....
>    >                      (integerp (car dimensions))
>    >                      (integerp maximum-length)
>    >                      (< 0 (car dimensions))
>    >                      (< (car dimensions) maximum-length)
>    >                      (<= maximum-length 
> *maximum-positive-32-bit-integer*)
>    > ....
>    > 
>    > where:
>    > 
>    > (defconst *maximum-positive-32-bit-integer*
>    >   (1- (expt 2 31)))
>    > 
>    > (defun dimensions (name l)
>    > .....
>    >   (cadr (assoc-keyword :dimensions
>    >                        (cdr (header name l)))))
>    > 
>    > (defun header (name l)
>    > .....
>    >           (assoc-eq :header l))
>    > .....
>    > 
>    > -- Matt
>    >    Cc: address@hidden, address@hidden
>    >    From: Camm Maguire <address@hidden>
>    >    Date: 24 Jun 2006 10:45:50 -0400
>    >    X-SpamAssassin-Status: No, hits=-1.9 required=5.0
>    >    X-UTCS-Spam-Status: No, hits=-225 required=200
>    > 
>    >    Greetings, and thanks!  Am looking nto this but had one question.  I
>    >    don't understand the (declare (xargs :guard ...)) syntax.  Though
>    >    aset1 in axioms.lisp is declaimed with an (unsigned-byte 31) arg, this
>    >    declaration appears to be asserting an integer type.  If you had any
>    >    illumination to spare, it would be most appreciated.
>    > 
>    >    Take care,
>    > 
>    >    Matt Kaufmann <address@hidden> writes:
>    > 
>    >    > P.S. I forgot to mention that in
>    >    > 
>    >    > /projects/hvg/ACL2/v3-0-hons-no-gcl-proclaim/
>    >    > 
>    >    > I did the build with:
>    >    > 
>    >    > ../build-acl2.jun23
>    >    > 
>    >    > -- Matt
>    >    > From: Matt Kaufmann <address@hidden>
>    >    > Subject: address@hidden: Re: benchmarking]
>    >    > To: address@hidden
>    >    > CC: boyer, hunt
>    >    > Date: 23 Jun 2006 23:59:28 -0500
>    >    > 
>    >    > Hi, Camm --
>    >    > 
>    >    > I think that you asked for a comparison of runs using different 
> proclaim
>    >    > approaches.  The results are below.  The third one didn't work, but 
> I'll leave
>    >    > that directory around for now:
>    >    > 
>    >    > /projects/hvg/ACL2/v3-0-hons-no-gcl-proclaim/
>    >    > 
>    >    > You're welcome to do what you will with it.  Please let me know 
> when I can
>    >    > delete it.
>    >    > 
>    >    > ============================================================
>    >    > 
>    >    > Using some sort of hybrid of ACL2 and GCL proclaims:
>    >    > /projects/hvg/ACL2/v3-0-hons/make-regression.log,
>    >    > 17438.565u 493.162s 5:02:49.31 98.6%        0+0k 0+0io 3pf+0w
>    >    > [Minor point: I think about 30 seconds of the above was from 
> cleaning books,
>    >    > not necessary and hence skipped below.]
>    >    > 
>    >    > ============================================================
>    >    > 
>    >    > Using GCL proclaims only:
>    >    > /projects/hvg/ACL2/v3-0-hons-no-acl2-proclaim/make-regression.log,
>    >    > 17939.093u 560.419s 5:16:23.49 97.4%        0+0k 0+0io 0pf+0w
>    >    > 
>    >    > ============================================================
>    >    > 
>    >    > Using ACL2 proclaims only, with
>    >    > (setq compiler::*compiler-auto-proclaim* nil 
> si::*disable-recompile* t):
>    >    > Build failed.
>    >    > 
>    >    > Here's the first error I noticed in the log file,
>    >    > /projects/hvg/ACL2/v3-0-hons-no-gcl-proclaim/compile-acl2.log:
>    >    > 
>    >    > .....
>    >    > 
>    >    > Finished loading axioms.lisp
>    >    > ;; Compiling axioms.lisp.
>    >    > ;; End of Pass 1.  
>    >    > ;; End of Pass 2.  
>    >    > axioms.c: In function `LI268':
>    >    > axioms.c:19663: warning: initialization from incompatible pointer 
> type
>    >    > axioms.c:19720: warning: assignment from incompatible pointer type
>    >    > axioms.c:19720: warning: passing arg 1 of `make_cons1' from 
> incompatible pointer type
>    >    > axioms.c:19723: warning: initialization from incompatible pointer 
> type
>    >    > axioms.c:19734: warning: assignment from incompatible pointer type
>    >    > axioms.c:19734: warning: passing arg 1 of `make_cons1' from 
> incompatible pointer type
>    >    > axioms.c: In function `LI428':
>    >    > axioms.c:28102: warning: initialization from incompatible pointer 
> type
>    >    > axioms.c: In function `L459':
>    >    > axioms.c:30000: warning: comparison is always true due to limited 
> range of data type
>    >    > ;; OPTIMIZE levels: Safety=0 (No runtime error checking), Space=0, 
> Speed=3, (Debug quality ignored)
>    >    > ;; Finished compiling axioms.o.
>    >    > Loading axioms.o
>    >    > 
>    >    > .....
>    >    > 
>    >    > Then later (as mentioned in earlier email):
>    >    > 
>    >    > .....
>    >    > 
>    >    > Loading type-set-b.lisp
>    >    > 
>    >    > Raw Lisp Break.
>    >    > Error in LET [or a callee]: Arg or result mismatch in call to  
> TYPE-SET-BINARY-+-ALIST-ENTRY
>    >    > 
>    >    > .....
>    >    > 
>    >    > I don't really know how to investigate this further, so I don't 
> plan to do
>    >    > anything further here.
>    >    > 
>    >    > - -- Matt
>    >    > - ------- Start of forwarded message -------
>    >    > Date: 23 Jun 2006 22:48:13 -0500
>    >    > From: Matt Kaufmann <address@hidden>
>    >    > To: address@hidden
>    >    > CC: address@hidden, address@hidden
>    >    > In-reply-to: <address@hidden> (message from
>    >    >     Robert Boyer on Fri, 23 Jun 2006 12:59:55 -0500)
>    >    > Subject: Re: benchmarking
>    >    > 
>    >    > [Sorry if you all get this twice; I can't tell if it was sent.]
>    >    > 
>    >    > Hi, Bob --
>    >    > 
>    >    > I completed the run shown here
>    >    > /projects/hvg/ACL2/v3-0-hons-no-acl2-proclaim/make-regression.log
>    >    > but I failed in the build as shown here
>    >    > /projects/hvg/ACL2/v3-0-hons-no-gcl-proclaim/compile-acl2.log
>    >    > where you'll see:
>    >    > 
>    >    > Raw Lisp Break.
>    >    > Error in LET [or a callee]: Arg or result mismatch in call to  
> TYPE-SET-BINARY-+-ALIST-ENTRY
>    >    > 
>    >    > The latter was a run where I started with this change to the 
> sources copied
>    >    > from /projects/hvg/ACL2/v3-0-hons/:
>    >    > 
>    >    > ;;; #+GCL (setq si::*disable-recompile* t)
>    >    > ;;; Even more than the above:
>    >    > (setq compiler::*compiler-auto-proclaim* nil 
> si::*disable-recompile* t)
>    >    > 
>    >    > I have no idea what's wrong; maybe I'll take a look tomorrow.
>    >    > 
>    >    > - - -- Matt
>    >    >    Date: Fri, 23 Jun 2006 12:59:55 -0500
>    >    >    From: Robert Boyer <address@hidden>
>    >    >    CC: address@hidden, address@hidden
>    >    > 
>    >    >    > I will leave /p/bin/xg untouched until I hear you are done
>    >    >    > with it.
>    >    > 
>    >    >    Bob
>    >    > - ------- End of forwarded message -------
>    >    > ----------
>    >    > 
>    >    > 
>    >    > 
>    >    > 
>    > 
>    >    -- 
>    >    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
> 
> 
> 

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