One of ACL2's strengths lies in its ability to execute industrial models efficiently. ACL2 provides the capability to execute models in parallel. This capability can increase the speed of explicit calls to simulators written in ACL2, and it can also decrease the time required for proofs that make heavy use of the evaluation of ground terms. The parallelism primitives allow for limiting parallel evaluation (spawning of so-called ``threads'') depending on resource availability. Specifically, the primitives allow specification of a size condition to control the granularity under which parallelism is limited. If you use the parallelism primitives in recursive functions, you get data-dependent parallelism of the program's execution.
Our API consists of the ACL2 primitives plet,
pargs, pand, and por, which
all accept an optional granularity condition. Pand
and por terminate early when an argument is found to
evaluate to nil or non-nil, respectively,
thus potentially improving on the efficiency of lazy evaluation.
ACL2 Parallelism Documentation
The most strategic and abstract explanation can be found in a paper published at the 2009 International LISP Conference. There are also slides for the accompanying talk.
More detailed explanations of the library can be found in my master's thesis and the files parallel.lisp and parallel-raw.lisp in the ACL2 source code.
Integration of our library as a build option for ACL2 is done, It's
still considered experimental, but it should work for you (and please let
me know if it doesn't). The following command is an example of how to use
CCL to build ACL2 with the parallelism library enabled:
make PREFIX=ccl- LISP=/your-ccl-directory/ccl-1.3/ccl/scripts/ccl64 ACL2_PAR=p
A side-effect of our ACL2 efforts is that our four parallelism primitives
also function in raw LISP, namely CCL and SBCL. In an effort to gain
user feedback and exposure to more interesting programs, a raw LISP
version of the parallelism library is available below. For simplicity's
sake, the file is intended to be load'ed into the LISP read
eval print loop.
Please see the ACL2 Documentation for an explanation of how to use the parallelism primitives.