ACL2 Version 3.0 News

Performance Comparisons

The following times were for the full ACL2 regression suite (distributed and workshop books). Not shown is a successful regression run on Windows using GCL.

In each case below, the first number, User time, is probably the most relevant for comparisons. The format is essentially:

         %Uuser %Ssystem %Eelapsed %PCPU (%Xtext+%Ddata %Mmax)k
         %Iinputs+%Ooutputs (%Fmajor+%Rminor)pagefaults %Wswaps

Linux times:

Each of the Linux runs was on the same, almost surely unloaded machine running Debian GNU/Linux 2.6.13.2.

Gnu Common Lisp (GCL), Version 2.6.7:
12712.650u 232.366s 3:38:32.41 98.7% 0+0k 0+0io 1pf+0w
SBCL 0.98:
19496.062u 590.336s 5:37:17.49 99.2% 0+0k 0+0io 0pf+0w
Allegro Common Lisp, Version 7.0:
20236.888u 187.415s 5:43:06.93 99.2% 0+0k 0+0io 0pf+0w
CMUCL 19b:
20530.959u 494.658s 5:53:09.77 99.2% 0+0k 0+0io 0pf+0w
Lispworks:
28889.313u 243.047s 8:08:04.13 99.4% 0+0k 0+0io 0pf+0w
CLISP 2.38:
72702.279u 515.380s 20:32:36.02 99.0% 0+0k 0+0io 2pf+0w

Note: Noah Friedman has observed that the difference in performance for CLISP is due to its bytecode-interpreted runtime vs. [for example] GCL's native object code execution.

Mac OS X times:

Each of the Macintosh runs was on the same unloaded Macintosh 2P G5 running Mac OS 10.4.5.

OpenMCL 1.0 with -j 2:
23021.449u 879.092s 3:28:30.71 191.0% 0+0k 0+6912io 0pf+0w
SBCL 0.9.12 without -j (apparently cannot run successfully with -j 2):
23818.622u 2021.217s 7:25:12.69 96.7% 0+0k 0+9797io 0pf+0w
GCL 2.6.8pre with -j 2:
25229.008u 9517.534s 5:11:23.07 185.9% 0+0k 0+10168io 0pf+0w

Sun/Solaris times:

Each of the Sun/Solaris runs was on the same reasonably unloaded Sun4u sparc machine running Solaris 2.9.

Allegro 6.2:
33600.0u 367.0s 9:56:57 94% 0+0k 0+0io 0pf+0w
CMUCL 18d:
52551.0u 1579.0s 15:47:15 95% 0+0k 0+0io 0pf+0w