Major Section: PARALLELISM
Here we document support for parallel programming in ACL2(p), an experimental extension of ACL2; also see parallelism.
mv-letsupporting speculative and parallel execution
One of ACL2's strengths lies in its ability to execute industrial models efficiently. The ACL2 source code provides an experimental parallel execution 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-
respectively, thus potentially improving on the efficiency of lazy
Spec-mv-let is a modification of
supports speculative and parallel execution.
Of the above five parallelism primitives, all but
spec-mv-let allow for
limiting parallel execution (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. You can use such granularity declarations in
recursively-defined functions to implement data-dependent parallelism in
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.
In addition to providing parallel programming primitives, ACL2(p) also provides the ability to execute the main ACL2 proof process in parallel. See set-waterfall-parallelism for further details.