Major Section: SWITCHES-PARAMETERS-AND-MODES
This documentation topic relates to the experimental extension of ACL2 supporting parallel execution and proof; see parallelism. See parallel and 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
pargs (but not
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
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.
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.
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.