`mv-let`

supporting 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
version of `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.
First, `<spec>`

is executed speculatively. Control then passes immediately
to the `mv-let`

call, without waiting for the result of evaluating
`<spec>`

. The variables `(w1 ... wk)`

are bound to the result of
evaluating `<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
above:

(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)))))))