Major Section: ACL2 Documentation
This documentation topic relates to an experimental extension of ACL2,
created initially by David L. Rager. See parallelism-build for how to build
an executable image that supports parallel evaluation. Also see
books/parallel for examples.
One of ACL2's strengths lies in its ability to execute industrial models efficiently. The ACL2 source code provides an experimental parallel evaluation capability that can increase the speed of explicit evaluation, including simulator runs using such models, and it can also decrease the time required for proofs that make heavy use of the evaluation of ground terms.
The parallelism primitives are
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.
We recommend that in order to learn to use the parallelism primitives, you
begin by reading examples: see parallelism-tutorial. That section will
direct you to further documentation topics.