ACL2 Version 8.3 Performance Comparisons

ACL2 Version 8.3 Performance Comparisons

The information below is based on runs of make -j 8 regression using the community books, skipping directory books/clause-processors/SULFA/, with Glucose installed. Each regression was run on Ubuntu Linux, on a 3.5 GHz 4-core Intel(R) Xeon(R) with Hyper-Threading. (Not shown are results of successful testing with CCL on Mac OS 10.13.6.)

NOTE. Although these comparisons are intended to give some sense of how these Lisps perform, they are far from definitive, mostly because they don't certify exactly the same books. For example certification has been skipped in SBCL for demos/meta-wf-guarantee-example.lisp: some time ago (admittedly, using what is now an old version of SBCL), we aborted certification after 75 minutes, while in CCL for example, certification took about 3 minutes; other than that, however, the same books were certified with CCL and SBCL. Note also for example that while the time posted for CCL is more than the time posted for GCL, the file for CCL, certs-ccl.txt, has 6646 lines, but the file for GCL, certs-gcl.txt, has only 6298 lines. Another reason to be cautious in using these statistics is that compilation in some Lisps could slow down the regression but produce better code (e.g., for running proofs or user applications). Finally, note that although SBCL is quite clearly the "winner" (even with the caveat above), it has been reported that CCL performs better on applications that make heavy use of hons, fast alists, and memoization.

Here are links to files that each contain a list of all books certified using the host Lisp indicated in its filename.

number of books    filename

   6408            certs-allegro.txt
   6646            certs-ccl.txt
   6298            certs-gcl.txt
   6462            certs-lispworks.txt
   6645            certs-sbcl.txt

Please bear in mind the discrepancy in sets of books certified, as noted above, when comparing the times listed below. This listing is alphabetized by host Common Lisp.