		Search-engine friendly clone of the ACL2 documentation.

Parallelism

Set-parallel-execution

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)

Set-parallel-execution takes an argument that specifies the enabling or disabling of parallel execution for the primitives pand, por, plet, and pargs (but not spec-mv-let, whose 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 set-parallel-execution, 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 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.

Value nil:

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.