For ACL2(p): enabling parallel execution for four parallelism primitives
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)
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
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.