Major Section: PARALLELISM
This documentation topic relates to the experimental extension of ACL2 supporting parallel evaluation and proof; see parallelism.
Example Forms: (plet ((a (fibonacci (- x 1))) (b (fibonacci (- x 2)))) (+ a b)) (plet (declare (granularity (> x 35))) ((a (fibonacci (- x 1))) (b (fibonacci (- x 2)))) (+ a b)) General Form: (plet (declare (granularity expr)) ; optional granularity declaration ((var1 val1) ... (varN valN)) (declare ...) ... (declare ...) ; optional declarations body)The syntax of
pletis identical to the syntax of
let, except that
pletpermits an optional granularity declaration in the first argument position; see granularity. In the logic a call of
pletmacroexpands to the corresponding call of
let, where the granularity declaration (if any) is dropped.
Plet cause the evaluation of each
vali above to be done in parallel
before processing the body. If the above
granularity declaration is
present, then its expression (
expr above) is first evaluated, and if the
nil, then such parallelism is avoided. Even if parallelism is
not thus avoided, parallelism may be limited by available resources.
See parallelism-at-the-top-level for restrictions on evaluating parallelism primitives from within the ACL2 top-level loop.