Major Section: 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. However, 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
set-parallel-evaluation, as follows.
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.