SET-PARALLEL-EVALUATION

Major Section:  PARALLELISM

See parallel and see parallelism-tutorial for an introduction to parallel evaluation in ACL2 using parallelism primitives pand, por, plet, and pargs.

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.

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 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.

Value nil:
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.