Major Section: SWITCHES-PARAMETERS-AND-MODES
This documentation topic relates to the experimental extension of ACL2 supporting parallel execution and proof; see parallelism. See parallelism-tutorial for an introduction to parallel execution in ACL2.
General Forms: (set-parallel-execution nil) ; default for images not built for parallelism (set-parallel-execution t) ; default for images built for parallelism (set-parallel-execution :bogus-parallelism-ok)
Set-parallel-execution takes an argument that specifies the enabling or
disabling of parallel execution for the primitives pand,
por, plet, and pargs (but not spec-mv-let, whose
parallel execution remains enabled). However, without using
top-level, calls of parallelism primitives made explicitly in the ACL2
top-level loop, as opposed to inside function bodies, will never cause
parallel execution; see parallelism-at-the-top-level. Parallel execution
is determined by the value of the argument to set-parallel-execution, as
follows.
Value t:
All parallelism primitives used in bodies of function definitions are given
the opportunity to execute in parallel. However, the use of parallelism
primitives directly in the ACL2 top-level loop causes an error.
Value :bogus-parallelism-ok:
Parallel execution is enabled, as for value t. However, the use of
parallelism primitives directly in the ACL2 top-level loop does not cause an
error, but rather, simply results in serial execution for these primitives.
Value nil:
All parallelism primitives degrade to their serial equivalents, including
their calls made directly in the ACL2 top-level loop. Thus, uses of
parallelism primitives do not in themselves cause errors.
