[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Gcl-devel] Re: address@hidden: address@hidden: Re: benchmarking]]
|
From: |
Camm Maguire |
|
Subject: |
[Gcl-devel] Re: address@hidden: address@hidden: Re: benchmarking]] |
|
Date: |
29 Jun 2006 11:15:49 -0400 |
|
User-agent: |
Gnus/5.09 (Gnus v5.9.0) Emacs/21.2 |
Greetings, and thanks so much for this very helpful and infomative
comparison!
I'm still going through this list, but regarding mutual recursion, I'd
like to point out this session:
=============================================================================
cd v3-0-hons-gcl-proclaim
./saved_acl2
GCL (GNU Common Lisp) 2.7.0 ANSI Jun 24 2006 18:43:43
Source License: LGPL(gcl,gmp,pargcl), GPL(unexec,bfd)
Binary License: GPL due to GPL'ed components: (BFD UNEXEC)
Modifications of this banner must retain notice of a compatible license
Dedicated to the memory of W. Schelter
Use (help) to get some basic information on how to use GCL.
Temporary directory for compiler files set to /tmp/
ACL2 Version 3.0 built June 25, 2006 14:59:57.
Copyright (C) 2006 University of Texas at Austin
ACL2 comes with ABSOLUTELY NO WARRANTY. This is free software and you
are welcome to redistribute it under certain conditions. For details,
see the GNU General Public License.
Initialized with (INITIALIZE-ACL2 'INCLUDE-BOOK *ACL2-PASS-2-FILES*).
MODIFIED for hons and such.
See the documentation topic note-3-0 for recent changes.
Note: We have modified the prompt in some underlying Lisps to further
distinguish it from the ACL2 prompt.
NOTE!! Proof trees are disabled in ACL2. To enable them in emacs,
look under the ACL2 source directory in interface/emacs/README.doc;
and, to turn on proof trees, execute :START-PROOF-TREE in the ACL2
command loop. Look in the ACL2 documentation under PROOF-TREE.
ACL2 Version 3.0. Level 1. Cbd
"/v/filer3/projects-hunt/hvg/ACL2/v3-0-hons-gcl-proclaim/".
Type :help for help.
Type (good-bye) to quit completely out of ACL2.
ACL2 !>:q
Exiting the ACL2 read-eval-print loop. To re-enter, execute (LP).
ACL2>(in-package 'si)
#<"SYSTEM" package>
SYSTEM>(maphash (lambda (x y)
(when (eq '* (cadr (call-sig y)))
(let* ((e (all-callees x nil))
(r (all-callers x nil))
(i (intersection e r)))
(when (and (remove x i)
(every (lambda (z) (equal (call-sig
(gethash z
*call-hash-table*)) (call-sig y))) i))
(print (list x i)))))) *call-hash-table*)
(ACL2::BACKQUOTE-LST (ACL2::BACKQUOTE-LST ACL2::BACKQUOTE))
(ACL2::BACKQUOTE (ACL2::BACKQUOTE-LST ACL2::BACKQUOTE))
(ACL2::GET-INDUCTION-CANDS (ACL2::GET-INDUCTION-CANDS-LST))
(ACL2::GET-INDUCTION-CANDS-LST
(ACL2::GET-INDUCTION-CANDS ACL2::GET-INDUCTION-CANDS-LST))
(ACL2::DEREF-VAR (ACL2::DEREF-VAR ACL2::DEREF))
(ACL2::DEREF (ACL2::DEREF-VAR ACL2::DEREF))
(ACL2::OCCUR-CNT-REC (ACL2::OCCUR-CNT-LST ACL2::OCCUR-CNT-REC))
(ACL2::OCCUR-CNT-LST (ACL2::OCCUR-CNT-REC ACL2::OCCUR-CNT-LST))
(ACL2::MEMBER-TERM (ACL2::MEMBER-COMPLEMENT-TERM ACL2::MEMBER-TERM))
(ACL2::MEMBER-COMPLEMENT-TERM
(ACL2::MEMBER-TERM ACL2::MEMBER-COMPLEMENT-TERM))
NIL
SYSTEM>(call-sig (gethash 'acl2::member-term *call-hash-table*))
((T T) *)
SYSTEM>(convert-to-state 'acl2::member-term)
ACL2::MEMBER-TERM4313
SYSTEM>(function-src 'ACL2::MEMBER-TERM4313)
(LAMBDA (ACL2::LIT ACL2::CL STATE)
(DECLARE (FIXNUM STATE))
(DECLARE (OPTIMIZE (SAFETY 0)))
(BLOCK ACL2::MEMBER-TERM4313
(MACROLET
((ACL2::MEMBER-COMPLEMENT-TERM (ACL2::LIT ACL2::CL)
(LIST 'ACL2::MEMBER-TERM4313 ACL2::LIT ACL2::CL 0))
(ACL2::MEMBER-TERM (ACL2::LIT ACL2::CL)
(LIST 'ACL2::MEMBER-TERM4313 ACL2::LIT ACL2::CL 1)))
(CASE STATE
(0
(FUNCALL (LAMBDA (ACL2::LIT ACL2::CL)
(DECLARE (OPTIMIZE (SAFETY 0)))
(BLOCK ACL2::MEMBER-COMPLEMENT-TERM
(LET* ()
(IF (ATOM ACL2::LIT)
(ACL2::MEMBER-COMPLEMENT-TERM1 ACL2::LIT
ACL2::CL)
(IF (EQ 'QUOTE (CAR ACL2::LIT))
(ACL2::MEMBER-COMPLEMENT-TERM1
ACL2::LIT ACL2::CL)
(IF (LET
((#:G15388
(EQ (CAR ACL2::LIT) 'EQUAL)))
(IF #:G15388 #:G15388
(EQ (CAR ACL2::LIT) 'ACL2::IFF)))
(ACL2::MEMBER-COMPLEMENT-TERM2
(CAR ACL2::LIT)
(CAR (CDR ACL2::LIT))
(CAR (CDR (CDR ACL2::LIT)))
ACL2::CL)
(IF (EQ (CAR ACL2::LIT) 'NOT)
(ACL2::MEMBER-TERM
(CAR (CDR ACL2::LIT)) ACL2::CL)
(ACL2::MEMBER-COMPLEMENT-TERM1
ACL2::LIT ACL2::CL))))))))
ACL2::LIT ACL2::CL))
(OTHERWISE
(FUNCALL (LAMBDA (ACL2::LIT ACL2::CL)
(DECLARE (OPTIMIZE (SAFETY 0)))
(DECLARE (OPTIMIZE (SAFETY 0)))
(BLOCK ACL2::MEMBER-TERM
(LET* ()
(BLOCK ACL2::MEMBER-TERM
(LET* ()
(IF (ATOM ACL2::LIT)
(ACL2::MEMBER-EQ ACL2::LIT ACL2::CL)
(IF (EQ 'QUOTE (CAR ACL2::LIT))
(ACL2::MEMBER-EQUAL ACL2::LIT
ACL2::CL)
(IF
(LET
((#:G15387
(EQ (CAR ACL2::LIT) 'EQUAL)))
(IF #:G15387 #:G15387
(EQ (CAR ACL2::LIT) 'ACL2::IFF)))
(ACL2::MEMBER-TERM2
(CAR ACL2::LIT)
(CAR (CDR ACL2::LIT))
(CAR (CDR (CDR ACL2::LIT)))
ACL2::CL)
(IF (EQ (CAR ACL2::LIT) 'NOT)
(ACL2::MEMBER-COMPLEMENT-TERM
(CAR (CDR ACL2::LIT)) ACL2::CL)
(ACL2::MEMBER-EQUAL ACL2::LIT
ACL2::CL))))))))))
ACL2::LIT ACL2::CL))))))
NIL
ACL2::MEMBER-TERM4313
SYSTEM>(compile 'ACL2::MEMBER-TERM4313)
;; Compiling /tmp/gazonk_7059_0.lsp.
;; End of Pass 1.
;; End of Pass 2.
;; OPTIMIZE levels: Safety=0 (No runtime error checking), Space=0, Speed=3,
(Debug quality ignored)
;; Finished compiling /tmp/gazonk_7059_0.o.
Loading /tmp/gazonk_7059_0.o
Callee ACL2::MEMBER-TERM4313 sigchange NIL to ((T T
(INTEGER -2147483648
2147483647))
T), recompiling
ACL2::MEMBER-COMPLEMENT-TERM
Callee ACL2::MEMBER-TERM4313 sigchange NIL to ((T T
(INTEGER -2147483648
2147483647))
T), recompiling ACL2::MEMBER-TERM
;; Compiling /tmp/gazonk_7059_ymjCh7.lsp.
;; End of Pass 1.
;; End of Pass 2.
;; OPTIMIZE levels: Safety=0 (No runtime error checking), Space=0, Speed=3,
(Debug quality ignored)
;; Finished compiling /tmp/gazonk_7059_ymjCh7.o.
Loading /tmp/gazonk_7059_ymjCh7.o
start address -T 0xadd8f58 Finished loading /tmp/gazonk_7059_ymjCh7.o
Callee ACL2::MEMBER-COMPLEMENT-TERM sigchange ((T T) *) to ((T T) T),
recompiling ACL2::SOME-ELEMENT-MEMBER-COMPLEMENT-TERM
Callee ACL2::MEMBER-COMPLEMENT-TERM sigchange ((T T) *) to ((T T) T),
recompiling ACL2::ADD-LITERAL
Callee ACL2::MEMBER-COMPLEMENT-TERM sigchange ((T T) *) to ((T T) T),
recompiling ACL2::ADD-LITERAL-AND-PT
;; Compiling /tmp/gazonk_7059_sxyINA.lsp.
;; End of Pass 1.
;; End of Pass 2.
;; OPTIMIZE levels: Safety=0 (No runtime error checking), Space=0, Speed=3,
(Debug quality ignored)
;; Finished compiling /tmp/gazonk_7059_sxyINA.o.
Loading /tmp/gazonk_7059_sxyINA.o
start address -T 0xadda7a0 Finished loading /tmp/gazonk_7059_sxyINA.o
start address -T 0xadc24e0 Finished loading /tmp/gazonk_7059_0.o
#<compiled-function ACL2::MEMBER-TERM4313>
NIL
NIL
SYSTEM>
=============================================================================
The questions are:
1) what is the proper mutual recursion detection mechanism --
i.e. if we only require that the arg types of the mutual recursion
members match, then we get the following list:
(ACL2::NORMALIZE-OR-DISTRIBUTE-FIRST-IF
(ACL2::DISTRIBUTE-FIRST-IF ACL2::NORMALIZE ACL2::NORMALIZE-LST
ACL2::NORMALIZE-OR-DISTRIBUTE-FIRST-IF))
(ACL2::DISTRIBUTE-FIRST-IF
(ACL2::NORMALIZE-OR-DISTRIBUTE-FIRST-IF ACL2::NORMALIZE
ACL2::NORMALIZE-LST))
(ACL2::NORMALIZE
(ACL2::DISTRIBUTE-FIRST-IF ACL2::NORMALIZE ACL2::NORMALIZE-LST
ACL2::NORMALIZE-OR-DISTRIBUTE-FIRST-IF))
(ACL2::BACKQUOTE-LST (ACL2::BACKQUOTE-LST ACL2::BACKQUOTE))
(ACL2::BACKQUOTE (ACL2::BACKQUOTE-LST ACL2::BACKQUOTE))
(ACL2::OUTPUT-TYPE-FOR-DECLARE-FORM-REC
(ACL2::OUTPUT-TYPE-FOR-DECLARE-FORM-REC-LIST
ACL2::OUTPUT-TYPE-FOR-DECLARE-FORM-REC))
(ACL2::TS-INTERSECTION-FN
(ACL2::EVAL-TYPE-SET-LST ACL2::EVAL-TYPE-SET ACL2::TS-UNION-FN
ACL2::TS-INTERSECTION-FN ACL2::TS-COMPLEMENT-FN))
(ACL2::TS-UNION-FN
(ACL2::EVAL-TYPE-SET-LST ACL2::EVAL-TYPE-SET ACL2::TS-UNION-FN
ACL2::TS-INTERSECTION-FN ACL2::TS-COMPLEMENT-FN))
(ACL2::EVAL-TYPE-SET
(ACL2::TS-UNION-FN ACL2::TS-INTERSECTION-FN ACL2::TS-COMPLEMENT-FN
ACL2::EVAL-TYPE-SET-LST))
(ACL2::CONTAINS-CONSTRAINED-CONSTANTP
(ACL2::CONTAINS-CONSTRAINED-CONSTANTP
ACL2::CONTAINS-CONSTRAINED-CONSTANTP-LST))
(ACL2::FREE-OR-BOUND-VARS
(ACL2::FREE-OR-BOUND-VARS-LST ACL2::FREE-OR-BOUND-VARS))
(COMPILER::T1EXPR (COMPILER::T1ORDINARY COMPILER::T1EXPR))
(ACL2::FFNNAMES-SUBSETP
(ACL2::FFNNAMES-SUBSETP ACL2::FFNNAMES-SUBSETP-LISTP))
(ACL2::GET-INDUCTION-CANDS (ACL2::GET-INDUCTION-CANDS-LST))
(ACL2::GET-INDUCTION-CANDS-LST
(ACL2::GET-INDUCTION-CANDS ACL2::GET-INDUCTION-CANDS-LST))
(ACL2::ALMOST-QUOTEP1
(ACL2::ALMOST-QUOTEP1-LISTP ACL2::ALMOST-QUOTEP1))
(ACL2::MULT-RELIEVE-FC-HYPS
(ACL2::MULT-RELIEVE-FC-HYPS ACL2::MULT-RELIEVE-ALL-FC-HYPS))
(ACL2::FIND-FIRST-NON-LOCAL-NAME
(ACL2::FIND-FIRST-NON-LOCAL-NAME-LST
ACL2::FIND-FIRST-NON-LOCAL-NAME))
(ACL2::ALL-CALLS (ACL2::ALL-CALLS-LST ACL2::ALL-CALLS))
(ACL2::FFNNAMEP-MOD-MBE
(ACL2::FFNNAMEP-MOD-MBE-LST ACL2::FFNNAMEP-MOD-MBE))
(ACL2::EV-REC
(ACL2::EV-REC-ACL2-UNWIND-PROTECT ACL2::EV-REC ACL2::EV-REC-LST
ACL2::EV-FNCALL-REC ACL2::EV-FNCALL-REC-LOGICAL))
(ACL2::DEREF-VAR (ACL2::DEREF-VAR ACL2::DEREF))
(ACL2::DEREF (ACL2::DEREF-VAR ACL2::DEREF))
(ACL2::OCCUR-CNT-REC (ACL2::OCCUR-CNT-LST ACL2::OCCUR-CNT-REC))
(ACL2::OCCUR-CNT-LST (ACL2::OCCUR-CNT-REC ACL2::OCCUR-CNT-LST))
(ACL2::COLLECT-FFNNAMES
(ACL2::COLLECT-FFNNAMES-LST ACL2::COLLECT-FFNNAMES))
=============================================================================
SYSTEM>(mapcar (lambda (x) (call-sig (gethash x *call-hash-table*)))
'(ACL2::NOTE-CERTIFICATION-WORLD ACL2::NOTE-CERTIFICATION-WORLD-LST))
(((T T T T T T) *) ((T T T T T T) (VALUES T T T)))
SYSTEM>(compile (convert-to-state 'ACL2::NOTE-CERTIFICATION-WORLD))
;; Compiling /tmp/gazonk_7059_0.lsp.
;; End of Pass 1.
;; End of Pass 2.
;; OPTIMIZE levels: Safety=0 (No runtime error checking), Space=0, Speed=3,
(Debug quality ignored)
;; Finished compiling /tmp/gazonk_7059_0.o.
Loading /tmp/gazonk_7059_0.o
Callee ACL2::NOTE-CERTIFICATION-WORLD4331 sigchange NIL to ((T T T T T
T
(INTEGER
-2147483648
2147483647))
(VALUES T T
T)), recompiling
ACL2::NOTE-CERTIFICATION-WORLD
Callee ACL2::NOTE-CERTIFICATION-WORLD4331 sigchange NIL to ((T T T T T
T
(INTEGER
-2147483648
2147483647))
(VALUES T T
T)), recompiling
ACL2::NOTE-CERTIFICATION-WORLD-LST
;; Compiling /tmp/gazonk_7059_8mFHt7.lsp.
;; End of Pass 1.
;; End of Pass 2.
;; OPTIMIZE levels: Safety=0 (No runtime error checking), Space=0, Speed=3,
(Debug quality ignored)
;; Finished compiling /tmp/gazonk_7059_8mFHt7.o.
Loading /tmp/gazonk_7059_8mFHt7.o
start address -T 0xadc2710 Finished loading /tmp/gazonk_7059_8mFHt7.o
start address -T 0xadbd000 Finished loading /tmp/gazonk_7059_0.o
#<compiled-function ACL2::NOTE-CERTIFICATION-WORLD4331>
NIL
NIL
=============================================================================
2) How does one unwind the state function when any of its elements are
redefined? At one point I was thinking of passing the state
integer straight from the caller and relying on the existing
fast-link redirect mechanism to redeirect the call to the newly
redefined function from the compiled code of the caller -- this
however misses all the implicit calls from the other members of the
mutual recursion group, as they are now just wrappers to a
self-recursive state function. Now I'm thinking the cleanest
solution is to simply redefine all the group members when any one
of them are redefined.
More explicitly:
(defun foo (x) (unless (< x 0) (not (bar (1- x)))))
(defun bar (x) (unless (< x 0) (not (foo (1- x)))))
convert-to-state ->
(defun foo4351 (X STATE)
(DECLARE (FIXNUM STATE))
(DECLARE (OPTIMIZE (SAFETY 0)))
(BLOCK FOO4351
(MACROLET
((BAR (X) (LIST 'FOO4351 X 0)) (FOO (X) (LIST 'FOO4351 X 1)))
(CASE STATE
(0
(FUNCALL (LAMBDA (X)
(DECLARE (OPTIMIZE (SAFETY 0)))
(BLOCK BAR
(LET* ()
(IF (NOT (< X 0)) (PROGN (NOT (FOO (- X 1))))))))
X))
(OTHERWISE
(FUNCALL (LAMBDA (X)
(DECLARE (OPTIMIZE (SAFETY 0)))
(DECLARE (OPTIMIZE (SAFETY 0)))
(BLOCK FOO
(LET* ()
(BLOCK FOO
(LET* ()
(IF (NOT (< X 0))
(PROGN (NOT (BAR (- X 1))))))))))
X))))))
(defun foo (X) (BLOCK FOO (FOO4351 X 1)))
(defun bar (X) (BLOCK BAR (FOO4351 X 0)))
If then any of foo or bar are redefined, the other one needs to be
redefined to its origianl source.
Eventually this should be an automatic part of do-recompile.
I don't know if any performance sensitive code of yours is in this
form, but if so this should definitely be an improvement. Tha takr
benchmark is dramatically accelerated.
Take care,
Matt Kaufmann <address@hidden> writes:
> Howdy --
>
> Attached is a file that I used to explore discrepancies between ACL2 and GCL
> in
> auto-generation of function type declarations. You probably don't need to
> look
> at it unless you want to tweak it to get a more refined comparison (I don't
> think I'll have time to do more of this for awhile but I can add comments to
> the code and/or answer questions if you want to play with the code) or see
> detailed results -- I'll summarize key things of interest to you just below.
>
> First, here's the most interesting thing I found: a compiler bug that appears
> to be due to a mistaken automatic proclaim involving multiple-value-prog1.
>
> sundance:~> /p/bin/xg
> GCL (GNU Common Lisp) 2.7.0 ANSI Jun 24 2006 18:43:43
> Source License: LGPL(gcl,gmp,pargcl), GPL(unexec,bfd)
> Binary License: GPL due to GPL'ed components: (BFD UNEXEC)
> Modifications of this banner must retain notice of a compatible license
> Dedicated to the memory of W. Schelter
>
> Use (help) to get some basic information on how to use GCL.
>
> Temporary directory for compiler files set to /tmp/
>
> >(defun buggy ()
> (multiple-value-prog1
> (values 3 4)
> 5))
>
> BUGGY
>
> >(buggy)
>
> 3
> 4
>
> >(compile 'buggy)
>
> ;; Compiling /tmp/gazonk_25691_0.lsp.
> ;; End of Pass 1.
> ;; End of Pass 2.
> ;; OPTIMIZE levels: Safety=0 (No runtime error checking), Space=0, Speed=3,
> (Debug quality ignored)
> ;; Finished compiling /tmp/gazonk_25691_0.o.
> Loading /tmp/gazonk_25691_0.o
> start address -T 0xac70fe0 Finished loading /tmp/gazonk_25691_0.o
> #<compiled-function BUGGY>
> NIL
> NIL
>
> >(buggy)
>
> 3
>
> >(get 'buggy 'si:proclaimed-return-type)
>
> T
>
> >
>
> The only other thing you are likely to find interesting is the following,
> where
> I suspect that the return type could also correctly be deduced as T rather
> than
> as the weaker *.
>
> (compile (defun weak (name) (setf (get name 'abc) nil)))
>
> ;; Compiling /tmp/gazonk_25691_0.lsp.
> ;; End of Pass 1.
> ;; End of Pass 2.
> ;; OPTIMIZE levels: Safety=0 (No runtime error checking), Space=0, Speed=3,
> (Debug quality ignored)
> ;; Finished compiling /tmp/gazonk_25691_0.o.
> Loading /tmp/gazonk_25691_0.o
> start address -T 0xac795d8 Finished loading /tmp/gazonk_25691_0.o
> #<compiled-function WEAK>
> NIL
> NIL
>
> >(get 'weak 'si:proclaimed-return-type)
>
> *
>
> >
>
> Note that I deliberately coerced every declaration that implies fixnum into
> simply 'fixnum for purposes of limiting discrepancies to interesting cases.
> So
> for example, if ACL2 deduced an type of (integer 0 1000) for some function
> argument and GCL had (signed-byte 28) for thta same argument, then this would
> not be considered a discrepancy (both would be treated as fixnum).
>
> Most of the file is the analysis of input type discrepancies (see "Resulting
> value of *args-mismatches*:") and output type discrepancies (see "Resulting
> value of *output-mismatches*:"). Here are the parts of that that I think you
> might find a little interesting, but there's nothing else major.
>
> + Many are marked with "; Mutual recursion", meaning that GCL made a weaker
> inference than ACL2, but the function is mutually recursive with others
> (specifically, defined using (mutual-recursion (defun ...) (defun ...) ...)
> in the ACL2 sources), so maybe this isn't news to you.
>
> + Many are marked with "GCL is missing STRING declaration (maybe not
> important?)", or substitute other types for STRING. My guess on an
> explanation is that you simply don't bother inferring types that don't do
> the
> compiler any good.
>
> + There is a bug in the ACL2 3.0 sources, since fixed (thanks to Bob Boyer),
> such that functions calling intern (or functions calling THOSE functions,
> etc.) are returning two values instead of the intended single value.
> Mismatches due to this bug are marked with "[Intern]" and are probably of no
> interest to you.
>
> + In a few cases GCL gets a type where ACL2 does not (marked with "GCL nicely
> propagates where ACL2 does not:" or "Nice job by GCL").
>
> + One GCL type inference was wrong due to the compiler bug mentioned early in
> this email (search for "problem with multiple-value-prog1").
>
> + One GCL type inference was weak due to the weak handling of setf shown
> earlier in this email.
>
--
Camm Maguire address@hidden
==========================================================================
"The earth is but one country, and mankind its citizens." -- Baha'u'llah