Major Section: PARALLEL-PROGRAMMING
This documentation topic relates to the experimental extension of ACL2 supporting parallel execution and proof; see parallelism.
Example Forms:
(pargs (binary-+ (fibonacci (- x 1)) (fibonacci (- x 2))))
(pargs (declare (granularity (> x 35)))
(binary-+ (fibonacci (- x 1)) (fibonacci (- x 2))))
General Form:
(pargs (declare (granularity expr)) ; optional granularity declaration
(f arg1 ... argN))
where N >= 0 and each argi and expr are arbitrary terms.
Logically, pargs is just the identity macro, in the sense that the above
forms can logically be replaced by (f arg1 ... argN). However, this
pargs form may parallelize the evaluation of arguments arg1 through
argN before applying function f to those results. If the above
granularity declaration is present, then its expression (expr
above) is first evaluated, and if the result is nil, then such
parallelism is avoided. Even if parallelism is not thus avoided, parallelism
may be limited by available resources.Since macros can change expressions in unexpected ways, it is illegal to call
pargs on a form that is a macro call. To parallelize computation of
arguments to a macro, see plet.
See parallelism-at-the-top-level for restrictions on evaluating parallelism primitives from within the ACL2 top-level loop.
