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, avoiding the evaluation of
expr2. More generally,
the evaluation of
(and expr1 expr2 ... exprk) terminates with a return
nil as soon as any
expri evaluates to
nil -- no
exprj is evaluated in this case for
j > i. This so-called ``lazy
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
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
The concept of early termination also applies to
por, except that early
termination occurs when an argument evaluates to non-