ACL2 Version 3.4 News

Table of Contents

• ACL2 Books Repository
• Patch files
• Performance Comparisons
• ACL2 Course Materials

This site is for community-driven development for the basic ACL2 libraries, which deal with topics like arithmetic, data structures, and hardware modelling. We're working with the authors of ACL2 and our changes are eventually incorporated into official ACL2 releases.

Patch files

We have fixed bugs in the handling of flet expressions, one of which had the capability of rendering ACL2 unsound. Thanks to Sol Swords for his help in identifying these problems. To read more and download the patch file, which includes installation instructions, visit:

http://www.cs.utexas.edu/users/moore/acl2/v3-4/new/flet-patch/index.html

Performance Comparisons

The various cases below correspond to runs of the ACL2 regression suite (distributed and workshop books) for ACL2 executables built on different platforms, as indicated. In each case below, the first number, User time in seconds, is by far the best one to use for comparisons (as opposed to System time or Elapsed time). Not shown here are successful runs on several other platforms: Lispworks 4.4.6 on 32-bit Ubuntu Linux; CMU Common Lisp 18d on Sun/Solaris (SunOS 5.9); CCL 1.2 (1.2-r9918M-trunk DarwinPPC32) and SBCL 1.0.2 on a PowerPC Mac; and GCL 2.6.7 and SBCL 1.0.13 on Windows/MinGW.

All statistics shown below are for running make regression on 8-core machines. The option -j 8 was used (i.e., up to 8 parallel jobs), so again, the first number in each case (marked with "u"), User seconds, is more relevant than the rest. Each regression run was on a 2.2 GHz AMD Opteron (tm) Processor 850 running Ubuntu Linux. One such machine was used for the 32-bit OS runs; another for 64-bit OS runs. NOTE: The 64-bit runs skipped the directory books/clause-processors/SULFA/, which accounts for about 4 or 5 minutes of User time; so the GCL penalty for 64-bit linux may be greater than appears below.

32-bit OS runs

• Gnu Common Lisp (GCL), Version 2.6.7:
  

  10775.357u 538.793s   34:29.15 546.8%  0+0k 0+0io 868pf+0w

• Allegro Common Lisp, Version 8.0:
  

  11820.018u 258.680s   38:01.23 529.4%  0+0k 0+0io 671pf+0w

• CMU Common Lisp (CMUCL), Version 19e:
  

  15751.688u 495.538s   50:45.49 533.4%  0+0k 0+0io 1723pf+0w

• CLISP, Version 2.41:
  

  67041.405u 776.160s 3:48:57.35 493.6%  0+0k 0+0io 0pf+0w

64-bit OS runs

• Gnu Common Lisp (GCL), Version 2.6.7:
  

  11314.551u 716.868s   34:58.16 573.4%  0+0k 0+0io 1795pf+0w

• CCL (OpenMCL) Version 1.2-r10372M-trunk:
  

  12628.561u 175.486s   41:02.47 519.9%  0+0k 0+0io 1158pf+0w

• SBCL Version 1.0.19:
  

  14076.155u 408.825s   45:15.77 533.3%  0+0k 0+0io 2597pf+0w

ACL2 Course Materials

• The following two interfaces to ACL2 support the teaching of ACL2 to undergraduates:
  • The ACL2 Sedan (ACL2s)
  • DrACuLa
• Here is a link to the web page for Yishai Feldman's Computer-Aided Reasoning course at The Interdisciplinary Center, Herzliya.
• John Cowles, COSC5010: Formalizing the JVM in ACL2, Univ. of Wyoming.
• Links to some of Warren Hunt's courses, many of which use ACL2, may be found here.
• Logic and Computation, a freshman class taught by Pete Manolios and Riccardo Pucella at Northeastern.
• Here is are links to web pages for two courses taught by Pete Manolios at Georgia Tech
  • CS 8803 Computational Logic (Spring 2005)
  • CS 8001 Hardware Verification Fall 2004
• Links to some of J Moore's courses, many of which use ACL2, may be found here.
• A course taught by Rex Page at the Univ. of Oklahoma, and related links.
• Eric Smith's web page for a class at Stanford