Major Section: PARALLELISM
This documentation topic relates to the experimental extension of ACL2
supporting parallel evaluation and proof; see parallelism. See parallel and
see parallelism-tutorial for an introduction to parallel evaluation in ACL2
using parallelism primitives
General Forms: (set-parallel-evaluation nil) ; default for images not built for parallelism (set-parallel-evaluation t) ; default for images built for parallelism (set-parallel-evaluation :bogus-parallelism-ok)
Set-parallel-evaluation takes an argument that specifies the enabling or
disabling of parallel evaluation for the primitives
pargs (but not
parallel evaluation 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 evaluation; see parallelism-at-the-top-level. Parallel evaluation
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 evaluation 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 evaluation for these primitives.
All parallelism primitives will degrade to their serial equivalents, include their calls made directly in the ACL2 top-level loop, which does not cause an error.