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 threads are allowed to spawn. 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,
pcall, 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
Integration of our library into ACL2 is still in progress, and a link to download ACL2 will be posted once the integration is complete.
A side-effect of our ACL2 efforts is that our four parallelism primitives
also function in raw LISP, namely OpenMCL 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 in the tarball 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.