Modification of mv-let supporting speculative and parallel execution
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 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
Evaluation of the above general form proceeds as suggested by the comments.
The calls to
The following definition of
(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)))))))