[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Gcl-devel] Boyer benchmark results
|
From: |
Camm Maguire |
|
Subject: |
Re: [Gcl-devel] Boyer benchmark results |
|
Date: |
21 Jun 2004 12:54:17 -0400 |
|
User-agent: |
Gnus/5.09 (Gnus v5.9.0) Emacs/21.2 |
Greetings, and thanks very much for your reply! Please let me first
reiterate that I am not out to skew results in gcl's favor or mislead
in any way. This having been said, I cannot reproduce your results
below.
There are a number of relevant issues here which I will try to
summarize to the best of my understanding:
1) It is essential in gcl's case at least that one makes use of the
automatic function proclamation facility to get optimal
performance. Even without this, however, I still cannot reproduce
your results.
One can make use of the proclamation feature in this setting in at
least two ways. The test suite that I ran evaluated function
proclamations for each file before compiling via the
'make-declare.lsp' file in the suite. One can also achieve the
same result without any files outside of gcl by first compiling
with '(compiler::emit-fn t)(compile-file "...")', and then making
the 'sys-proclaim.lisp' file via '(compiler::emit-fn t)
(compiler::make-all-proclaims "*.fn")', and then recompiling a
second time with '(load "sys-proclaim.lisp")(compile-file "...")'.
I've included a sys-proclaim.lisp file for the gabriel benchmarks
below.
2) My initial results on the web page did not turn off *gc-verbose*
for cmucl. I've rerun the results with this in, but the effect
appears quite minor, even undetectable.
3) My initial results on the web page, like yours, looped over the
original gabriel tests many times as each test is quite fast on
modern hardware. Unlike yours, each iteration in my case had a
(print (time (test...))) as opposed to simply (test). This does
appear to penalize cmucl more than gcl, so I am removing it -- it
is irrelevant to the purpose of the test in any case. This
improves the cmucl/gcl situation slightly, but I still cannot
reproduce your findings.
4) I've downloaded the file you mention and retraced your steps with
this version of 'boyer', but again get different numbers: (gcl with
proclamations: 1.87 sec, gcl without proclamations: 2.59 sec, cmucl
in either case: 3.55 sec, clisp in either case: 15.00 sec).
This file seems to have a slight disadvantage compared to the one
that I've been using at ftp://ftp.ma.utexas.edu/gcl/gabriel.tgz, in
that it apparently includes the (setup-boyer) in the timing
results, and perhaps even more annoyingly, appears to increase the
theorem size on each load of the file. I haven't looked into this
very carefully, but I think the issue is that your file uses the
more modern
(eval-when (:load-toplevel :execute)
(setup-boyer))
whereas my file uses the ancient
(defvar setup-performed-p (prog1 t (boyer-setup)))
With my version, the timings are (gcl with proclamations: 1.40 sec,
gcl without proclamations: 2.32 sec, cmucl in either case: 3.13
sec, clisp in either case: 13.3 sec).
5) Paul, I was also a bit concerned with the posted results when you
indicated that the clisp/cmucl ration should be 10x. I just
thought it worth noting that Peter gets 6.2x below, and with my
rerun results without the printing I get 4.2x. My machine is a
dual 2.4Ghz Intel Xeon, and I'm wondering if we are seeing effects
of differing memory bandwidths.
6) I think to get to the bottom of this, we need to use the same
binary images, and I would propose that we use those currently in
Debian sid. I suggest proceeding on three fronts if there is time
and interest:
a) I will be looking into running cl-bench. This will take a
bit of work, as the default setup for gcl in this package does
not appear to make use of the function proclamation feature.
b) Shortly after writing this, I will put up at
http://people.debian.org/~camm/gabriel.tgz
the benchmark suite I used with the slight modifications as
mentioned on the web page. I'd be most appreciative if
those in the know could run this suite as well, as well as
look it over for mistakes/oversights.
This is the same file as at
ftp://ftp.ma.utexas.edu/gcl/gabriel.tgz with the following
modifications:
a) .cl2 files were made from the .cl files by removing
the (print (time ....)) around the test
b) .cl1 files are made from .cl2 files by adding the
(declaim (optimize)) at the top for cmucl (gcl
defaults to this mode)
c) The number of iterations in test-help.lsp has been
increased by a factor of 400
d) *gc-verbose* has been turned off for cmucl in
test-help.lsp.
e) the old init.lsp preallocation of memory for gcl
has been moved to initori.lsp as it is now mostly
obsolete.
f) the makefile has been changed to use the
sys-proclaim.lisp file as opposed to the
make-declare.lsp for function proclamations. The
alternative method is left in as a comment. The
makefile can obviously be improved.
c) I suggest we try to run the boyer comparison with the same
images and with the same files. To this end I've put together
a little script we might all be able to use, with
modifications of course possible should any see the need.
Ideally, one could run this on an up to date Debian sid
system with at least gcl, cmucl, and clisp installed. There
is no significant difference between gcl and gclcvs here, nor
between the traditional and ansi images. As we are trying to
release 2.6.2, however, can we please confine our discussions
to this branch, as I'd like to get some numbers we can all
agree on for the release notes.
=============================================================================
my results: ('result' image (t indicates ansi image) file load-proclamations?
time)
=============================================================================
Desired=Unknown/Install/Remove/Purge/Hold
| Status=Not/Installed/Config-files/Unpacked/Failed-config/Half-installed
|/ Err?=(none)/Hold/Reinst-required/X=both-problems (Status,Err: uppercase=bad)
||/ Name Version Description
+++-========================-========================-================================================================
ii gcl 2.6.1-40 GNU Common Lisp compiler
ii gclcvs 2.7.0-24 GNU Common Lisp compiler,
CVS snapshot
ii cmucl 18e-9 The CMUCL lisp compiler
and development system
ii clisp 2.33-2 GNU CLISP, a Common Lisp
implementation
result gcl "boyer.lisp" T 1.8700000000000001
result gcl "boyer.lisp" NIL 2.5899999999999999
result gcl "boyer1.cl2" T 1.3999999999999999
result gcl "boyer1.cl2" NIL 2.3199999999999998
result gcl t "boyer.lisp" T 1.8999999999999999
result gcl t "boyer.lisp" NIL 2.6200000000000001
result gcl t "boyer1.cl2" T 1.45
result gcl t "boyer1.cl2" NIL 2.3599999999999999
result gclcvs "boyer.lisp" T 1.8500000000000001
result gclcvs "boyer.lisp" NIL 2.5499999999999998
result gclcvs "boyer1.cl2" T 1.45
result gclcvs "boyer1.cl2" NIL 2.2999999999999998
result gclcvs t "boyer.lisp" T 1.8700000000000001
result gclcvs t "boyer.lisp" NIL 2.5899999999999999
result gclcvs t "boyer1.cl2" T 1.6299999999999999
result gclcvs t "boyer1.cl2" NIL 2.3599999999999999
result lisp "boyer.lisp" T 3.57
result lisp "boyer.lisp" NIL 3.55
result lisp "boyer1.cl2" T 3.14
result lisp "boyer1.cl2" NIL 3.12
result clisp "boyer.lisp" T 15.01
result clisp "boyer.lisp" NIL 14.99
result clisp "boyer1.cl2" T 13.3
result clisp "boyer1.cl2" NIL 13.31
=============================================================================
do_results
=============================================================================
#!/bin/bash
dpkg -l gcl gclcvs cmucl clisp
for l in gcl gclcvs lisp clisp; do
for a in "" t ; do
if [ "$a" = "" ] || [ "$l" = "gcl" ] || [ "$l" = "gclcvs" ] ;
then
for fn in boyer.lisp boyer1.cl2 ; do
for sys in t nil ; do
echo "(let ((fn \"$fn\")(sys $sys))(when sys
(load \"sys-proclaim.lisp\"))(compile-file fn))(quit)" | GCL_ANSI=$a $l -
>/dev/null 2>&1
echo "(let ((fn \"$fn\")(sys $sys))(load
(pathname-name fn))(format t \"result $l $a ~S ~S ~S~%\" fn sys (min (test 100)
(test 100) (test 100))))(quit)" | GCL_ANSI=$a $l - 2>&1 | grep result
done
done
fi
done
done
=============================================================================
sys-proclaim.lisp
=============================================================================
(IN-PACKAGE "USER")
(PROCLAIM
'(FTYPE (FUNCTION (FIXNUM FIXNUM FIXNUM) T) TAK53 TAK54 TAK18 TAK94
TAK98 TAK99 TAK0 TAK9 TAK10 TAK70 TAK36 TAK37 TAK29 TAK7
TAK69 TAK88 TAK89 TAK13 TAK79 TAK93 TAK96 TAK97 TAK49 TAK67
TAK8 TAK33 TAK19 TAK20 TAK40 TAK77 TAK78 TAK26 TAK58 TAK86
TAK59 TAK60 TAK66 TAK39 TAK6 TAK55 TAK56 TAK52 TAK16 TAK72
TAK85 TAK62 TAK46 TAK82 TAK5 TAK2 TAK22 TAK68 TAK73 TAK44
TAK45 TAK95 TAK65 TAK48 TAK4 TAK51 TAK84 TAK24 TAK34 TAK74
TAK3 TAK35 TAK23 TAK91 TAK75 TAK25 TAK11 TAK17 TAK12 TAK32
TAK38 TAK1 TAK90 TAK47 TAK80 TAK71 TAK92 TAK64 TAK61 TAK57
TAK27 TAK15 TAK83 TAK28 TAK50 TAK87 TAK81 TAK43 TAK63 TAK41
TAK42 TAK14 TAK76 STAK TAK30 TAK31 TAK21 CTAK-AUX))
(PROCLAIM
'(FTYPE (FUNCTION (FIXNUM FIXNUM T) T) INIT-AUX TPRINT-INIT-AUX))
(PROCLAIM '(FTYPE (FUNCTION (FIXNUM FIXNUM FIXNUM T) T) BROWSE-INIT))
(PROCLAIM
'(FTYPE (FUNCTION (FIXNUM) T) CREATE-N TRIAL
TRAVERSE-CREATE-STRUCTURE LISTN))
(PROCLAIM '(FTYPE (FUNCTION (T) FIXNUM) TRAVERSE))
(PROCLAIM
'(FTYPE (FUNCTION ((VECTOR LONG-FLOAT) (VECTOR LONG-FLOAT)) T) FFT))
(PROCLAIM
'(FTYPE (FUNCTION (FIXNUM T) T) TRAVERSE-SELECT TRAVERSE-REMOVE))
(PROCLAIM '(FTYPE (FUNCTION (T FIXNUM) T) FIND-ROOT))
(PROCLAIM '(FTYPE (FUNCTION (FIXNUM FIXNUM FIXNUM) FIXNUM) TAK))
(PROCLAIM
'(FTYPE (FUNCTION (FIXNUM FIXNUM) T) TRY DESTRUCTIVE PUZZLE-REMOVE
FIT))
(PROCLAIM '(FTYPE (FUNCTION (T T T) *) CTAK))
(PROCLAIM
'(FTYPE (FUNCTION (T T T) T) FPRINT-INIT PCOEFADD TAUTOLOGYP MATCH
TPRINT-INIT MAS))
(PROCLAIM '(FTYPE (FUNCTION (FIXNUM FIXNUM) FIXNUM) PLACE))
(PROCLAIM
'(FTYPE (FUNCTION NIL *) SHOW-FFT PRINT-FFT CLEAR-FFT TESTPUZZLE
TESTCTAK))
(PROCLAIM
'(FTYPE (FUNCTION NIL T) TESTTRIANG TESTDERIV TRIANG-SETUP
DERIV-RUN TESTDESTRU TESTDIV2-RECUR TESTDIV2-ITER TESTDIV2
TESTFFT FFT-BENCH TESTFPRINT FPRINT TESTFREAD FREAD
TESTTRAVERSE-RUN TESTFRPOLY-4 STANDARD-FRPOLY-TEST4
TESTFRPOLY-3 STANDARD-FRPOLY-TEST3 TESTFRPOLY-2
STANDARD-FRPOLY-TEST2 TESTFRPOLY-1 STANDARD-FRPOLY-TEST1
TESTFRPOLY BOYER-SETUP TESTTAKR RUN-TRAVERSE TESTBOYER
BOYER-TEST PUZZLE-START TESTTRAVERSE-INIT INIT-TRAVERSE
TESTBROWSE TESTSTAK BROWSE STAK-AUX TESTTRAVERSE TESTTAK
TESTTPRINT STANDARD-TPRINT-TEST TESTTAKL TESTDDERIV
DDERIV-RUN))
(PROCLAIM '(FTYPE (FUNCTION (T) T) DDERIV))
(PROCLAIM '(FTYPE (FUNCTION (*) T) MAKE-NODE))
(PROCLAIM '(FTYPE (FUNCTION (T FIXNUM FIXNUM FIXNUM) T) DEFINEPIECE))
(PROCLAIM
'(FTYPE (FUNCTION (T) T) -DDERIV +DDERIV NODE-ENTRY2 GOGOGO DERIV
SIMPLE-VECTOR-TO-LIST DERIV-AUX NODE-ENTRY1 NODE-SN
NODE-SONS TEST-2 TEST-1 RECURSIVE-DIV2 ITERATIVE-DIV2
NODE-PARENTS NODE-MARK NODE-P NODE-ENTRY6 PTIMES3 PTIMES2
ADD-LEMMA-LST REWRITE-ARGS REWRITE ADD-LEMMA TAUTP
NODE-ENTRY5 BROWSE-RANDOMIZE NODE-ENTRY4 NODE-ENTRY3
//DDERIV *DDERIV DDERIV-AUX))
(PROCLAIM '(FTYPE (FUNCTION (T *) *) SETUP-FFT-COMPONENT))
(PROCLAIM
'(FTYPE (FUNCTION (T T) T) PEXPTSQ PTIMES PPLUS PPLUS1 PTIMES1
PSIMP PCTIMES PCTIMES1 PCPLUS REWRITE-WITH-LEMMAS PCPLUS1
APPLY-SUBST ONE-WAY-UNIFY ONE-WAY-UNIFY1-&LST
ONE-WAY-UNIFY1 FALSEP APPLY-SUBST-LST TRUEP INVESTIGATE
TRAVERS SHORTERP TRAVERSE-ADD))
(PROCLAIM
'(FTYPE (FUNCTION NIL FIXNUM) TRAVERSE-SEED LAST-POSITION SNB JIL
BROWSE-RANDOM TRAVERSE-RANDOM))
=============================================================================
boyer.lisp (identical to the one at armedbear, or should be)
=============================================================================
;;; BOYER -- Logic programming benchmark, originally written by Bob Boyer.
;;; Fairly CONS intensive.
(declaim (optimize speed))
#+cmu
(setf *gc-verbose* nil)
(defvar unify-subst)
(defvar temp-temp)
(defun add-lemma (term)
(cond ((and (not (atom term))
(eq (car term)
(quote equal))
(not (atom (cadr term))))
(setf (get (car (cadr term)) (quote lemmas))
(cons term (get (car (cadr term)) (quote lemmas)))))
(t (error "ADD-LEMMA did not like term: ~a" term))))
(defun add-lemma-lst (lst)
(cond ((null lst)
t)
(t (add-lemma (car lst))
(add-lemma-lst (cdr lst)))))
(defun apply-subst (alist term)
(cond ((atom term)
(cond ((setq temp-temp (assoc term alist :test #'eq))
(cdr temp-temp))
(t term)))
(t (cons (car term)
(apply-subst-lst alist (cdr term))))))
(defun apply-subst-lst (alist lst)
(cond ((null lst)
nil)
(t (cons (apply-subst alist (car lst))
(apply-subst-lst alist (cdr lst))))))
(defun falsep (x lst)
(or (equal x (quote (f)))
(member x lst :test #'eq)))
(defun one-way-unify (term1 term2)
(progn (setq unify-subst nil)
(one-way-unify1 term1 term2)))
;; this function is buggy -- see "The Boyer Benchmark Meets Linear
;; Logic" by Henry Baker. Corrected version below.
;; (defun one-way-unify1 (term1 term2)
;; (cond ((atom term2)
;; (cond ((setq temp-temp (assoc term2 unify-subst :test #'eq))
;; (equal term1 (cdr temp-temp)))
;; (t (setq unify-subst (cons (cons term2 term1)
;; unify-subst))
;; t)))
;; ((atom term1)
;; nil)
;; ((eq (car term1)
;; (car term2))
;; (one-way-unify1-lst (cdr term1)
;; (cdr term2)))
;; (t nil)))
(defun one-way-unify1 (term1 term2) ;
With bug fixed.
(cond ((atom term2)
(cond ((setq temp-temp (assoc term2 unify-subst :test #'eq))
(equal term1 (cdr temp-temp)))
;; this clause added
((numberp term2) (equal term1 term2))
(t (setq unify-subst (cons (cons term2 term1) unify-subst)) t)))
((atom term1) nil)
((eq (car term1) (car term2)) (one-way-unify1-lst (cdr term1) (cdr
term2)))
(t nil)))
(defun one-way-unify1-lst (lst1 lst2)
(cond ((null lst1)
t)
((one-way-unify1 (car lst1)
(car lst2))
(one-way-unify1-lst (cdr lst1)
(cdr lst2)))
(t nil)))
(defun rewrite (term)
(cond ((atom term)
term)
(t (rewrite-with-lemmas (cons (car term)
(rewrite-args (cdr term)))
(get (car term)
(quote lemmas))))))
(defun rewrite-args (lst)
(cond ((null lst)
nil)
(t (cons (rewrite (car lst))
(rewrite-args (cdr lst))))))
(defun rewrite-with-lemmas (term lst)
(cond ((null lst)
term)
((one-way-unify term (cadr (car lst)))
(rewrite (apply-subst unify-subst (caddr (car lst)))))
(t (rewrite-with-lemmas term (cdr lst)))))
(defun setup-boyer ()
(add-lemma-lst
(quote ((equal (compile form)
(reverse (codegen (optimize form)
(nil))))
(equal (eqp x y)
(equal (fix x)
(fix y)))
(equal (greaterp x y)
(lessp y x))
(equal (lesseqp x y)
(not (lessp y x)))
(equal (greatereqp x y)
(not (lessp x y)))
(equal (boolean x)
(or (equal x (t))
(equal x (f))))
(equal (iff x y)
(and (implies x y)
(implies y x)))
(equal (even1 x)
(if (zerop x)
(t)
(odd (1- x))))
(equal (countps- l pred)
(countps-loop l pred (zero)))
(equal (fact- i)
(fact-loop i 1))
(equal (reverse- x)
(reverse-loop x (nil)))
(equal (divides x y)
(zerop (remainder y x)))
(equal (assume-true var alist)
(cons (cons var (t))
alist))
(equal (assume-false var alist)
(cons (cons var (f))
alist))
(equal (tautology-checker x)
(tautologyp (normalize x)
(nil)))
(equal (falsify x)
(falsify1 (normalize x)
(nil)))
(equal (prime x)
(and (not (zerop x))
(not (equal x (add1 (zero))))
(prime1 x (1- x))))
(equal (and p q)
(if p (if q (t)
(f))
(f)))
(equal (or p q)
(if p (t)
(if q (t)
(f))
(f)))
(equal (not p)
(if p (f)
(t)))
(equal (implies p q)
(if p (if q (t)
(f))
(t)))
(equal (fix x)
(if (numberp x)
x
(zero)))
(equal (if (if a b c)
d e)
(if a (if b d e)
(if c d e)))
(equal (zerop x)
(or (equal x (zero))
(not (numberp x))))
(equal (plus (plus x y)
z)
(plus x (plus y z)))
(equal (equal (plus a b)
(zero))
(and (zerop a)
(zerop b)))
(equal (difference x x)
(zero))
(equal (equal (plus a b)
(plus a c))
(equal (fix b)
(fix c)))
(equal (equal (zero)
(difference x y))
(not (lessp y x)))
(equal (equal x (difference x y))
(and (numberp x)
(or (equal x (zero))
(zerop y))))
(equal (meaning (plus-tree (append x y))
a)
(plus (meaning (plus-tree x)
a)
(meaning (plus-tree y)
a)))
(equal (meaning (plus-tree (plus-fringe x))
a)
(fix (meaning x a)))
(equal (append (append x y)
z)
(append x (append y z)))
(equal (reverse (append a b))
(append (reverse b)
(reverse a)))
(equal (times x (plus y z))
(plus (times x y)
(times x z)))
(equal (times (times x y)
z)
(times x (times y z)))
(equal (equal (times x y)
(zero))
(or (zerop x)
(zerop y)))
(equal (exec (append x y)
pds envrn)
(exec y (exec x pds envrn)
envrn))
(equal (mc-flatten x y)
(append (flatten x)
y))
(equal (member x (append a b))
(or (member x a)
(member x b)))
(equal (member x (reverse y))
(member x y))
(equal (length (reverse x))
(length x))
(equal (member a (intersect b c))
(and (member a b)
(member a c)))
(equal (nth (zero)
i)
(zero))
(equal (exp i (plus j k))
(times (exp i j)
(exp i k)))
(equal (exp i (times j k))
(exp (exp i j)
k))
(equal (reverse-loop x y)
(append (reverse x)
y))
(equal (reverse-loop x (nil))
(reverse x))
(equal (count-list z (sort-lp x y))
(plus (count-list z x)
(count-list z y)))
(equal (equal (append a b)
(append a c))
(equal b c))
(equal (plus (remainder x y)
(times y (quotient x y)))
(fix x))
(equal (power-eval (big-plus1 l i base)
base)
(plus (power-eval l base)
i))
(equal (power-eval (big-plus x y i base)
base)
(plus i (plus (power-eval x base)
(power-eval y base))))
(equal (remainder y 1)
(zero))
(equal (lessp (remainder x y)
y)
(not (zerop y)))
(equal (remainder x x)
(zero))
(equal (lessp (quotient i j)
i)
(and (not (zerop i))
(or (zerop j)
(not (equal j 1)))))
(equal (lessp (remainder x y)
x)
(and (not (zerop y))
(not (zerop x))
(not (lessp x y))))
(equal (power-eval (power-rep i base)
base)
(fix i))
(equal (power-eval (big-plus (power-rep i base)
(power-rep j base)
(zero)
base)
base)
(plus i j))
(equal (gcd x y)
(gcd y x))
(equal (nth (append a b)
i)
(append (nth a i)
(nth b (difference i (length a)))))
(equal (difference (plus x y)
x)
(fix y))
(equal (difference (plus y x)
x)
(fix y))
(equal (difference (plus x y)
(plus x z))
(difference y z))
(equal (times x (difference c w))
(difference (times c x)
(times w x)))
(equal (remainder (times x z)
z)
(zero))
(equal (difference (plus b (plus a c))
a)
(plus b c))
(equal (difference (add1 (plus y z))
z)
(add1 y))
(equal (lessp (plus x y)
(plus x z))
(lessp y z))
(equal (lessp (times x z)
(times y z))
(and (not (zerop z))
(lessp x y)))
(equal (lessp y (plus x y))
(not (zerop x)))
(equal (gcd (times x z)
(times y z))
(times z (gcd x y)))
(equal (value (normalize x)
a)
(value x a))
(equal (equal (flatten x)
(cons y (nil)))
(and (nlistp x)
(equal x y)))
(equal (listp (gopher x))
(listp x))
(equal (samefringe x y)
(equal (flatten x)
(flatten y)))
(equal (equal (greatest-factor x y)
(zero))
(and (or (zerop y)
(equal y 1))
(equal x (zero))))
(equal (equal (greatest-factor x y)
1)
(equal x 1))
(equal (numberp (greatest-factor x y))
(not (and (or (zerop y)
(equal y 1))
(not (numberp x)))))
(equal (times-list (append x y))
(times (times-list x)
(times-list y)))
(equal (prime-list (append x y))
(and (prime-list x)
(prime-list y)))
(equal (equal z (times w z))
(and (numberp z)
(or (equal z (zero))
(equal w 1))))
(equal (greatereqpr x y)
(not (lessp x y)))
(equal (equal x (times x y))
(or (equal x (zero))
(and (numberp x)
(equal y 1))))
(equal (remainder (times y x)
y)
(zero))
(equal (equal (times a b)
1)
(and (not (equal a (zero)))
(not (equal b (zero)))
(numberp a)
(numberp b)
(equal (1- a)
(zero))
(equal (1- b)
(zero))))
(equal (lessp (length (delete x l))
(length l))
(member x l))
(equal (sort2 (delete x l))
(delete x (sort2 l)))
(equal (dsort x)
(sort2 x))
(equal (length (cons x1
(cons x2
(cons x3 (cons x4
(cons x5
(cons x6 x7)))))))
(plus 6 (length x7)))
(equal (difference (add1 (add1 x))
2)
(fix x))
(equal (quotient (plus x (plus x y))
2)
(plus x (quotient y 2)))
(equal (sigma (zero)
i)
(quotient (times i (add1 i))
2))
(equal (plus x (add1 y))
(if (numberp y)
(add1 (plus x y))
(add1 x)))
(equal (equal (difference x y)
(difference z y))
(if (lessp x y)
(not (lessp y z))
(if (lessp z y)
(not (lessp y x))
(equal (fix x)
(fix z)))))
(equal (meaning (plus-tree (delete x y))
a)
(if (member x y)
(difference (meaning (plus-tree y)
a)
(meaning x a))
(meaning (plus-tree y)
a)))
(equal (times x (add1 y))
(if (numberp y)
(plus x (times x y))
(fix x)))
(equal (nth (nil)
i)
(if (zerop i)
(nil)
(zero)))
(equal (last (append a b))
(if (listp b)
(last b)
(if (listp a)
(cons (car (last a))
b)
b)))
(equal (equal (lessp x y)
z)
(if (lessp x y)
(equal t z)
(equal f z)))
(equal (assignment x (append a b))
(if (assignedp x a)
(assignment x a)
(assignment x b)))
(equal (car (gopher x))
(if (listp x)
(car (flatten x))
(zero)))
(equal (flatten (cdr (gopher x)))
(if (listp x)
(cdr (flatten x))
(cons (zero)
(nil))))
(equal (quotient (times y x)
y)
(if (zerop y)
(zero)
(fix x)))
(equal (get j (set i val mem))
(if (eqp j i)
val
(get j mem)))))))
(defun tautologyp (x true-lst false-lst)
(cond ((truep x true-lst)
t)
((falsep x false-lst)
nil)
((atom x)
nil)
((eq (car x)
(quote if))
(cond ((truep (cadr x)
true-lst)
(tautologyp (caddr x)
true-lst false-lst))
((falsep (cadr x)
false-lst)
(tautologyp (cadddr x)
true-lst false-lst))
(t (and (tautologyp (caddr x)
(cons (cadr x)
true-lst)
false-lst)
(tautologyp (cadddr x)
true-lst
(cons (cadr x)
false-lst))))))
(t nil)))
(defun tautp (x)
(tautologyp (rewrite x)
nil nil))
(defun boyer ()
(let (term)
(setq term
(apply-subst
(quote ((x f (plus (plus a b)
(plus c (zero))))
(y f (times (times a b)
(plus c d)))
(z f (reverse (append (append a b)
(nil))))
(u equal (plus a b)
(difference x y))
(w lessp (remainder a b)
(member a (length b)))))
(quote (implies (and (implies x y)
(and (implies y z)
(and (implies z u)
(implies u w))))
(implies x w)))))
(tautp term)))
(defun trans-of-implies (n)
(list (quote implies)
(trans-of-implies1 n)
(list (quote implies)
0 n)))
(defun trans-of-implies1 (n)
(declare (fixnum n))
(cond ((eql n 1)
(list (quote implies)
0 1))
(t (list (quote and)
(list (quote implies)
(1- n)
n)
(trans-of-implies1 (1- n))))))
(defun truep (x lst)
(or (equal x (quote (t)))
(member x lst :test #'eq)))
(defun test (count)
(let (before after)
(setf before (get-internal-run-time))
(dotimes (i count) (boyer))
(setf after (get-internal-run-time))
(float (/ (- after before) internal-time-units-per-second))))
(eval-when (:load-toplevel :execute)
(setup-boyer))
=============================================================================
boyer1.cl2 (slightly modified from the version at
ftp://ftp.ma.utexas.edu)
=============================================================================
;; $Header: boyer.cl,v 1.2 88/01/03 19:28:19 layer Exp $
;; $Locker: $
;;; BOYER -- Logic programming benchmark, originally written by Bob Boyer.
;;; Fairly CONS intensive.
(declaim (optimize speed))
#+cmu
(setf *gc-verbose* nil)
(defvar **unify-subst**)
(defvar **temp-temp**)
(defun add-lemma (term)
(cond ((and (not (atom term))
(eq (car term)
(quote equal))
(not (atom (cadr term))))
(setf (get (car (cadr term)) (quote lemmas))
(cons term (get (car (cadr term)) (quote lemmas)))))
(t (error "~%ADD-LEMMA did not like term: ~a" term))))
(defun add-lemma-lst (lst)
(cond ((null lst)
t)
(t (add-lemma (car lst))
(add-lemma-lst (cdr lst)))))
(defun apply-subst (alist term)
(cond ((atom term)
(cond ((setq **temp-temp** (assoc term alist :test #'eq))
(cdr **temp-temp**))
(t term)))
(t (cons (car term)
(apply-subst-lst alist (cdr term))))))
(defun apply-subst-lst (alist lst)
(cond ((null lst)
nil)
(t (cons (apply-subst alist (car lst))
(apply-subst-lst alist (cdr lst))))))
(defun falsep (x lst)
(or (equal x (quote (f)))
(member x lst)))
(defun one-way-unify (term1 term2)
(progn (setq **unify-subst** nil)
(one-way-unify1 term1 term2)))
(defun one-way-unify1 (term1 term2)
(cond ((atom term2)
(cond ((setq **temp-temp** (assoc term2 **unify-subst** :test #'eq))
(equal term1 (cdr **temp-temp**)))
(t (setq **unify-subst** (cons (cons term2 term1)
**unify-subst**))
t)))
((atom term1)
nil)
((eq (car term1)
(car term2))
(one-way-unify1-&lst (cdr term1)
(cdr term2)))
(t nil)))
(defun one-way-unify1-&lst (lst1 lst2)
(cond ((null lst1)
t)
((one-way-unify1 (car lst1)
(car lst2))
(one-way-unify1-&lst (cdr lst1)
(cdr lst2)))
(t nil)))
(defun rewrite (term)
(cond ((atom term)
term)
(t (rewrite-with-lemmas (cons (car term)
(rewrite-args (cdr term)))
(get (car term)
(quote lemmas))))))
(defun rewrite-args (lst)
(cond ((null lst)
nil)
(t (cons (rewrite (car lst))
(rewrite-args (cdr lst))))))
(defun rewrite-with-lemmas (term lst)
(cond ((null lst)
term)
((one-way-unify term (cadr (car lst)))
(rewrite (apply-subst **unify-subst** (caddr (car lst)))))
(t (rewrite-with-lemmas term (cdr lst)))))
(defun boyer-setup ()
(add-lemma-lst
(quote ((equal (compile form)
(reverse (codegen (optimize form)
(nil))))
(equal (eqp x y)
(equal (fix x)
(fix y)))
(equal (greaterp x y)
(lessp y x))
(equal (lesseqp x y)
(not (lessp y x)))
(equal (greatereqp x y)
(not (lessp x y)))
(equal (boolean x)
(or (equal x (t))
(equal x (f))))
(equal (iff x y)
(and (implies x y)
(implies y x)))
(equal (even1 x)
(if (zerop x)
(t)
(odd (1- x))))
(equal (countps- l pred)
(countps-loop l pred (zero)))
(equal (fact- i)
(fact-loop i 1))
(equal (reverse- x)
(reverse-loop x (nil)))
(equal (divides x y)
(zerop (remainder y x)))
(equal (assume-true var alist)
(cons (cons var (t))
alist))
(equal (assume-false var alist)
(cons (cons var (f))
alist))
(equal (tautology-checker x)
(tautologyp (normalize x)
(nil)))
(equal (falsify x)
(falsify1 (normalize x)
(nil)))
(equal (prime x)
(and (not (zerop x))
(not (equal x (add1 (zero))))
(prime1 x (1- x))))
(equal (and p q)
(if p (if q (t)
(f))
(f)))
(equal (or p q)
(if p (t)
(if q (t)
(f))
(f)))
(equal (not p)
(if p (f)
(t)))
(equal (implies p q)
(if p (if q (t)
(f))
(t)))
(equal (fix x)
(if (numberp x)
x
(zero)))
(equal (if (if a b c)
d e)
(if a (if b d e)
(if c d e)))
(equal (zerop x)
(or (equal x (zero))
(not (numberp x))))
(equal (plus (plus x y)
z)
(plus x (plus y z)))
(equal (equal (plus a b)
(zero))
(and (zerop a)
(zerop b)))
(equal (difference x x)
(zero))
(equal (equal (plus a b)
(plus a c))
(equal (fix b)
(fix c)))
(equal (equal (zero)
(difference x y))
(not (lessp y x)))
(equal (equal x (difference x y))
(and (numberp x)
(or (equal x (zero))
(zerop y))))
(equal (meaning (plus-tree (append x y))
a)
(plus (meaning (plus-tree x)
a)
(meaning (plus-tree y)
a)))
(equal (meaning (plus-tree (plus-fringe x))
a)
(fix (meaning x a)))
(equal (append (append x y)
z)
(append x (append y z)))
(equal (reverse (append a b))
(append (reverse b)
(reverse a)))
(equal (times x (plus y z))
(plus (times x y)
(times x z)))
(equal (times (times x y)
z)
(times x (times y z)))
(equal (equal (times x y)
(zero))
(or (zerop x)
(zerop y)))
(equal (exec (append x y)
pds envrn)
(exec y (exec x pds envrn)
envrn))
(equal (mc-flatten x y)
(append (flatten x)
y))
(equal (member x (append a b))
(or (member x a)
(member x b)))
(equal (member x (reverse y))
(member x y))
(equal (length (reverse x))
(length x))
(equal (member a (intersect b c))
(and (member a b)
(member a c)))
(equal (nth (zero)
i)
(zero))
(equal (exp i (plus j k))
(times (exp i j)
(exp i k)))
(equal (exp i (times j k))
(exp (exp i j)
k))
(equal (reverse-loop x y)
(append (reverse x)
y))
(equal (reverse-loop x (nil))
(reverse x))
(equal (count-list z (sort-lp x y))
(plus (count-list z x)
(count-list z y)))
(equal (equal (append a b)
(append a c))
(equal b c))
(equal (plus (remainder x y)
(times y (quotient x y)))
(fix x))
(equal (power-eval (big-plus1 l i base)
base)
(plus (power-eval l base)
i))
(equal (power-eval (big-plus x y i base)
base)
(plus i (plus (power-eval x base)
(power-eval y base))))
(equal (remainder y 1)
(zero))
(equal (lessp (remainder x y)
y)
(not (zerop y)))
(equal (remainder x x)
(zero))
(equal (lessp (quotient i j)
i)
(and (not (zerop i))
(or (zerop j)
(not (equal j 1)))))
(equal (lessp (remainder x y)
x)
(and (not (zerop y))
(not (zerop x))
(not (lessp x y))))
(equal (power-eval (power-rep i base)
base)
(fix i))
(equal (power-eval (big-plus (power-rep i base)
(power-rep j base)
(zero)
base)
base)
(plus i j))
(equal (gcd x y)
(gcd y x))
(equal (nth (append a b)
i)
(append (nth a i)
(nth b (difference i (length a)))))
(equal (difference (plus x y)
x)
(fix y))
(equal (difference (plus y x)
x)
(fix y))
(equal (difference (plus x y)
(plus x z))
(difference y z))
(equal (times x (difference c w))
(difference (times c x)
(times w x)))
(equal (remainder (times x z)
z)
(zero))
(equal (difference (plus b (plus a c))
a)
(plus b c))
(equal (difference (add1 (plus y z))
z)
(add1 y))
(equal (lessp (plus x y)
(plus x z))
(lessp y z))
(equal (lessp (times x z)
(times y z))
(and (not (zerop z))
(lessp x y)))
(equal (lessp y (plus x y))
(not (zerop x)))
(equal (gcd (times x z)
(times y z))
(times z (gcd x y)))
(equal (value (normalize x)
a)
(value x a))
(equal (equal (flatten x)
(cons y (nil)))
(and (nlistp x)
(equal x y)))
(equal (listp (gopher x))
(listp x))
(equal (samefringe x y)
(equal (flatten x)
(flatten y)))
(equal (equal (greatest-factor x y)
(zero))
(and (or (zerop y)
(equal y 1))
(equal x (zero))))
(equal (equal (greatest-factor x y)
1)
(equal x 1))
(equal (numberp (greatest-factor x y))
(not (and (or (zerop y)
(equal y 1))
(not (numberp x)))))
(equal (times-list (append x y))
(times (times-list x)
(times-list y)))
(equal (prime-list (append x y))
(and (prime-list x)
(prime-list y)))
(equal (equal z (times w z))
(and (numberp z)
(or (equal z (zero))
(equal w 1))))
(equal (greatereqpr x y)
(not (lessp x y)))
(equal (equal x (times x y))
(or (equal x (zero))
(and (numberp x)
(equal y 1))))
(equal (remainder (times y x)
y)
(zero))
(equal (equal (times a b)
1)
(and (not (equal a (zero)))
(not (equal b (zero)))
(numberp a)
(numberp b)
(equal (1- a)
(zero))
(equal (1- b)
(zero))))
(equal (lessp (length (delete x l))
(length l))
(member x l))
(equal (sort2 (delete x l))
(delete x (sort2 l)))
(equal (dsort x)
(sort2 x))
(equal (length (cons x1
(cons x2
(cons x3 (cons x4
(cons x5
(cons x6 x7)))))))
(plus 6 (length x7)))
(equal (difference (add1 (add1 x))
2)
(fix x))
(equal (quotient (plus x (plus x y))
2)
(plus x (quotient y 2)))
(equal (sigma (zero)
i)
(quotient (times i (add1 i))
2))
(equal (plus x (add1 y))
(if (numberp y)
(add1 (plus x y))
(add1 x)))
(equal (equal (difference x y)
(difference z y))
(if (lessp x y)
(not (lessp y z))
(if (lessp z y)
(not (lessp y x))
(equal (fix x)
(fix z)))))
(equal (meaning (plus-tree (delete x y))
a)
(if (member x y)
(difference (meaning (plus-tree y)
a)
(meaning x a))
(meaning (plus-tree y)
a)))
(equal (times x (add1 y))
(if (numberp y)
(plus x (times x y))
(fix x)))
(equal (nth (nil)
i)
(if (zerop i)
(nil)
(zero)))
(equal (last (append a b))
(if (listp b)
(last b)
(if (listp a)
(cons (car (last a))
b)
b)))
(equal (equal (lessp x y)
z)
(if (lessp x y)
(equal t z)
(equal f z)))
(equal (assignment x (append a b))
(if (assignedp x a)
(assignment x a)
(assignment x b)))
(equal (car (gopher x))
(if (listp x)
(car (flatten x))
(zero)))
(equal (flatten (cdr (gopher x)))
(if (listp x)
(cdr (flatten x))
(cons (zero)
(nil))))
(equal (quotient (times y x)
y)
(if (zerop y)
(zero)
(fix x)))
(equal (get j (set i val mem))
(if (eqp j i)
val
(get j mem)))))))
(defun tautologyp (x true-lst false-lst)
(cond ((truep x true-lst)
t)
((falsep x false-lst)
nil)
((atom x)
nil)
((eq (car x)
(quote if))
(cond ((truep (cadr x)
true-lst)
(tautologyp (caddr x)
true-lst false-lst))
((falsep (cadr x)
false-lst)
(tautologyp (cadddr x)
true-lst false-lst))
(t (and (tautologyp (caddr x)
(cons (cadr x)
true-lst)
false-lst)
(tautologyp (cadddr x)
true-lst
(cons (cadr x)
false-lst))))))
(t nil)))
(defun tautp (x)
(tautologyp (rewrite x)
nil nil))
(defun boyer-test ()
(prog (ans term)
(setq term
(apply-subst
(quote ((x f (plus (plus a b)
(plus c (zero))))
(y f (times (times a b)
(plus c d)))
(z f (reverse (append (append a b)
(nil))))
(u equal (plus a b)
(difference x y))
(w lessp (remainder a b)
(member a (length b)))))
(quote (implies (and (implies x y)
(and (implies y z)
(and (implies z u)
(implies u w))))
(implies x w)))))
(setq ans (tautp term))))
#|
(defun trans-of-implies (n)
(list (quote implies)
(trans-of-implies1 n)
(list (quote implies)
0 n)))
(defun trans-of-implies1 (n)
(cond ((eql n 1)
(list (quote implies)
0 1))
(t (list (quote and)
(list (quote implies)
(1- n)
n)
(trans-of-implies1 (1- n))))))
|#
(defun truep (x lst)
(or (equal x (quote (t)))
(member x lst)))
(defvar setup-performed-p (prog1 t (boyer-setup)))
(defun testboyer ()
(boyer-test))
(defun test (count)
(declare (fixnum count))
(let (before after)
(setf before (get-internal-run-time))
(dotimes (i count) (declare (fixnum i))(boyer-test))
(setf after (get-internal-run-time))
(float (/ (- after before) internal-time-units-per-second))))
=============================================================================
Take care,
Peter Graves <address@hidden> writes:
> Hi,
>
> There was a little discussion on #lisp yesterday about the benchmark
> results on this page:
>
> http://people.debian.org/~camm/GCL_2_6_2_tests.html
>
> To add another data point, I ran the Boyer benchmark on GCL CVS head
> (built with --enable-ansi) and several other implementations, using an
> Athlon XP 2100+ machine running Linux 2.6.0, with the results below.
>
> The benchmark I used was extracted from Eric Marsden's cl-bench suite
> and is available here:
>
> http://armedbear.org/boyer.lisp
>
> I added (declaim (optimize speed)) at the top of the file (and turned
> off *gc-verbose* for CMUCL).
>
> For each system, I simply did (compile-file "boyer.lisp"), (load *),
> and then (test 100) 3 times.
>
> GET-INTERNAL-RUN-TIME was used for timing.
>
> The results (best of 3 runs for each system):
>
> GCL (GNU Common Lisp) 2.7.0 ANSI Jun 17 2004 17:50:11
>
> 3.22 seconds
>
> CMU Common Lisp CVS release-18e-branch + minimal debian patches
>
> 2.87 seconds
>
> SBCL 0.8.11
>
> 2.592 seconds
>
> Allegro CL 6.2 Trial Edition
>
> 3.79 seconds
>
> CLISP 2.33.1 (2004-05-22)
>
> 18.059256 seconds
>
> ABCL 0.0.3.15+ (Jun 17 2004 12:21:53) (Java 1.5.0-beta2)
>
> 16.786 seconds
>
> -Peter
>
>
> _______________________________________________
> Gcl-devel mailing list
> address@hidden
> http://lists.gnu.org/mailman/listinfo/gcl-devel
>
>
>
--
Camm Maguire address@hidden
==========================================================================
"The earth is but one country, and mankind its citizens." -- Baha'u'llah
- [Gcl-devel] Boyer benchmark results, Peter Graves, 2004/06/18
- Re: [Gcl-devel] Boyer benchmark results,
Camm Maguire <=
- Re: [Gcl-devel] Boyer benchmark results, Vadim V. Zhytnikov, 2004/06/21
- Re: [Gcl-devel] Boyer benchmark results, Camm Maguire, 2004/06/21
- Re: [Gcl-devel] Boyer benchmark results, Peter Graves, 2004/06/22
- Re: [Gcl-devel] Boyer benchmark results, Christophe Rhodes, 2004/06/22
- Re: [Gcl-devel] Boyer benchmark results, Camm Maguire, 2004/06/22
- Re: [Gcl-devel] Boyer benchmark results, Christophe Rhodes, 2004/06/22
- Re: [Gcl-devel] Boyer benchmark results, Camm Maguire, 2004/06/22
- Re: [Gcl-devel] Boyer benchmark results, Raymond Toy, 2004/06/28
- Re: [Gcl-devel] Boyer benchmark results, Camm Maguire, 2004/06/29
- Re: [Gcl-devel] Boyer benchmark results, Vadim V. Zhytnikov, 2004/06/23