|
|
|---|
|
|
|
|---|
Parallel execution in the ACL2 top-level loop
This documentation topic relates to the experimental extension of ACL2 supporting parallel execution and proof; see parallelism.
Calls of parallelism primitives made explicitly in the ACL2 top-level loop, as opposed to inside function bodies, will never cause parallel execution. Such calls will either execute with serial execution or will cause an error; see set-parallel-execution. For a way around this restriction, see top-level.
Consider for example the following call of pargs in the ACL2
top-level loop. Instead of executing
(pargs (cons (expensive-fn-1 4) (expensive-fn-2 5)))
expands into:
(cons (expensive-fn-1 4) (expensive-fn-2 5))
One trivial way to enable parallel execution of a form is to surround it with a call to macro top-level. Consider the following example.
(top-level (pargs (cons (expensive-fn-1 4) (expensive-fn-2 5))))
Then in an executable image that supports parallel execution — see
compiling-ACL2p for instructions on how to build such an executable
—
A second way to enable parallel execution of a form is to place it inside a function body. For example, consider the following definition.
(defun foo (x y) (pargs (cons (expensive-fn-1 x) (expensive-fn-2 y))))
Then in an executable image that supports parallel execution, submission of
the form
Note that guards need not be verified in order to obtain parallel execution. The only restrictions on parallel execution are to use an ACL2 executable supporting it, to avoid calling parallelism primitives directly in the top-level loop, to have sufficient resources (especially, threads) available, and to avoid explicitly disabling parallel execution (see set-parallel-execution).