ACL2 Version 3.0 News

Performance Comparisons

The following times were for the full ACL2 regression suite (distributed and workshop books).

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