SPEC-MV-LET

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