mv-letsupporting speculative and parallel execution
Major Section: PARALLEL-PROGRAMMING
This documentation topic relates to the experimental extension of ACL2 supporting parallel execution and proof; see parallelism.
Example Form: (defun pfib-with-step-count (x) (declare (xargs :mode :program)) (if (or (zp x) (< x 33)) (fib-with-step-count x) (spec-mv-let (a cnt1) (pfib-with-step-count (- x 1)) (mv-let (b cnt2) (pfib-with-step-count (- x 2)) (if t (mv (+ a b) (+ 1 cnt1 cnt2)) (mv "speculative result is always needed" -1)))))) General Form: (spec-mv-let (v1 ... vn) ; bind distinct variables <spec> ; evaluate speculatively; return n values (mv-let ; or, use mv?-let if k=1 below (w1 ... wk) ; bind distinct variables <eager> ; evaluate eagerly (if <test> ; use results from <spec> if true <typical-case> ; may mention v1 ... vn <abort-case>))) ; does not mention v1 ... vn
Our design of
spec-mv-let is guided by its use in ACL2 source code to
parallelize part of ACL2's proof process, in the experimental parallel
extension of ACL2. The user can think of
spec-mv-let as a speculative
mv-let. (In ordinary ACL2, the semantics agree with this
description but without speculative or parallel execution.)
Evaluation of the above general form proceeds as suggested by the comments.
<spec> is executed speculatively. Control then passes immediately
mv-let call, without waiting for the result of evaluating
<spec>. The variables
(w1 ... wk) are bound to the result of
<eager>, and then
<test> is evaluated. If the value of
<test> is true, then the values of
(v1 ... vn) are needed, and
<typical-case> blocks until they are available. If the value of
<test> is false, then the values of
(v1 ... vn) are not needed, and
the evaluation of
<spec> may be aborted.
The calls to
mv-let and to
if displayed above in the General Form are
an essential part of the design of
spec-mv-let, and are thus required.
The following definition of
fib-with-step-count completes the example
(defun fib-with-step-count (x) (declare (xargs :mode :program)) (cond ((<= x 0) (mv 0 1)) ((= x 1) (mv 1 1)) (t (mv-let (a cnt1) (fib-with-step-count (- x 1)) (mv-let (b cnt2) (fib-with-step-count (- x 2)) (mv (+ a b) (+ 1 cnt1 cnt2)))))))