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 >= 0and each
exprare arbitrary terms. Logically,
pargsis just the identity macro, in the sense that the above forms can logically be replaced by
(f arg1 ... argN). However, this
pargsform may parallelize the evaluation of arguments
argNbefore applying function
fto those results. If the above
granularitydeclaration is present, then its expression (
exprabove) 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.