ACL2 Version 4.1 News

Table of Contents

• ACL2 Books Repository
• 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.

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. Not shown are results of testing on Windows and Mac OS X or of running with safety 3 using CCL.

Statistics shown below are for running make regression. Each 32-bit Linux regression reported below was run with make option -j 8 on an 8-core 2.2 GHz AMD Opteron (tm) Processor 850 running Ubuntu Linux. Each 64-bit Linux regression reported below was run with make option -j 24 on a 2.6GHz machine with four processors, each a Six-Core AMD Opteron(tm) Processor 8435. Also, the 64-bit runs skipped directory books/clause-processors/SULFA/. So comparisons between a 32-bit run and 64-bit run are ill-advised.

32-bit Linux runs using make -j 8

• Allegro Common Lisp (Allegro CL), Version 8.0:
  

  21507.912u 391.984s 1:18:32.06 464.7%	0+0k 0+968536io 0pf+0w

• CCL Version 1.6-dev-r13902M-trunk:
  

  26377.076u 409.081s 1:39:44.37 447.6%	0+0k 169240+915072io 216pf+0w

• Gnu Common Lisp (GCL), Version 2.6.7:
  

  22751.109u 1088.488s 1:12:12.10 550.3%	0+0k 114952+2174256io 0pf+0w

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

  25421.292u 1571.322s 1:36:34.76 465.8%	0+0k 182680+1074336io 243pf+0w

64-bit Linux runs using make -j 24

• CCL Version 1.6-dev-r13902M-trunk:
  

  17874.477u 310.343s 1:08:15.93 443.9%	0+0k 253168+656968io 1197pf+0w

• Gnu Common Lisp (GCL), Version 2.6.7:
  

  45138.004u 2625.456s 1:20:57.38 983.3%	0+0k 335608+1997728io 0pf+0w

• SBCL Version 1.0.37:
  

  22349.060u 1172.229s 1:01:30.15 637.4%	0+0k 56936+837904io 0pf+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 are links to web pages for courses taught by Pete Manolios at Georgia Tech:
  • CS 8803 Computational Logic (Spring 2005)
  • CS 8001 Hardware Verification Fall 2004
  • CS 3220 Processor Design.
• 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