		Search-engine friendly clone of the ACL2 documentation.

Pargs

Parallel evaluation of arguments in a function call

This documentation topic relates to the experimental extension of ACL2 supporting parallel execution and proof; see parallelism, and see parallel-programming, which has a disclaimer.

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.