EARLY-TERMINATION

Major Section:  PARALLEL-PROGRAMMING

This documentation topic relates to the experimental extension of ACL2 supporting parallel execution and proof; see parallelism.

The evaluation of (and expr1 expr2) returns nil if expr1 evaluates to nil, avoiding the evaluation of expr2. More generally, the evaluation of (and expr1 expr2 ... exprk) terminates with a return value of nil as soon as any expri evaluates to nil -- no exprj is evaluated in this case for j > i. This so-called ``lazy evaluation'' of and terms can thus save some computation; roughly speaking, the smaller the i, the more computation is saved.

If the above call of and is replaced by its parallel version, pand, then there can be even more opportunity for skipping work. The arguments to pand can be evaluated in parallel, in which case the first such evaluation that returns with a value of nil, if any, causes the remaining such evaluations to abort.

Consider the following functions that compute whether a tree is valid (see granularity for a discussion of the granularity form).

(defun valid-tip (x)
  (declare (xargs :guard t))
  (or (eq x 'A)
      (eq x 'T)
      (eq x 'C)
      (eq x 'G)))

(defun pvalid-tree (x depth)
  (declare (xargs :guard (natp depth)))
  (if (atom x)
      (valid-tip x)
    (pand (declare (granularity (< depth 10)))
          (pvalid-tree (car x) (1+ depth))
          (pvalid-tree (cdr x) (1+ depth)))))

We would like to stop execution as soon as any tip is found to be invalid. So, when computing the conjunction of terms by using pand, once one of those terms evaluates to nil, the computations for the other terms are aborted and the pand call returns nil. By using pand, we can in principle attain a speedup factor greater than the number of available cores.

The concept of early termination also applies to por, except that early termination occurs when an argument evaluates to non-nil.