Timings

[Bill Schelter <wfs@CLI.COM>]

Notes on the tests in letter from Bob Boyer.

We were using a version of the gabriel benchmarks provided me by
Blewett at ATT.   As Bob mentioned the directory, complete with
the makefile I constructed for running the tests, is available on
rascal for anonymous ftp, so there is no need to speculate about
what proclamations or declarations were included.   On looking
at the code, it did seem to be be fairly well declared for common
lisp (eg all the declarations you mention for tak were there.)
In fact WHENEVER I changed a declaration either by addition or deletion
it slowed lucid down.  So I think it was declared well for lucid.
In fact with triang, when I tried making the declarations more
suitable for AKCL, the time for AKCL decreased to 65.3 seconds
and LUCID increased to 255.4 seconds.  (see file triang-mod.cl)

We compared to LUCID since it is (in my opinion) an excellent lisp,
and also the only other lisp we have on our machine.  I currently use
3 different Sun 280's, and the timings on rascal(the machine used) are
in between the other two.  There certainly do seem to be cpu
differences.  Naturally we wanted to run on exactly the same machine,
in the same circumstances.  The tests were run using the same make and
the same output conditions.  I too have sometimes seen faster times on
other 280's.  I have also seen slower.


Each test time is a sum of the subtests.   In the version we were
given, there is a (testfrpoly) or (testtak) ..It is the total run
time that is given.

It is hard to single out a small group of changes which have improved
performance.  I think there were many good design decisions made by
the original authors (Hagiya & Yuasa) of KCL.  The speed-up in the
heavy consing routines is in part due to, getting locals, args, etc
into the c stack and into registers,  speeding up comparison, and many
other factors.  Actually, what I feel is one of the substantial
changes I have made in AKCL, is the elimination of block compiling
within a single file, and the speedup of calling across files.  Thus
in AKCL it is possible to trace or redefine a single function in the
file.  This of course only slows us down (albeit very slightly) in
these simple unrealistic one file tests, but helps in large multiple
file systems like the boyer moore theorem prover.


As for realistic situations: we certainly have found in heavy day to
day use on automatic theorem proving, and program verification, that
KCL and AKCL provide good fast service.  The number of cpu hours
devoted to heavy lisp computation at Computational Logic, for example,
is very substantial.

Bill Schelter