Major Section: PARALLEL-PROOF
This documentation topic relates to the experimental extension of ACL2 supporting parallel execution and proof; see parallelism.
The following discussion, concerning the naming of subgoals pushed for proof by induction and the timeliness of aborting when two or more goals are pushed for proof by induction, only applies when waterfall parallelism is enabled (see set-waterfall-parallelism).
When two sibling subgoals (e.g. 4.5 and 4.6) both push goals to be proved by induction (e.g., 4.6 pushes *1 and 4.5 pushes *2), a name is assigned to the second pushed subgoal (e.g., *2) as if the first push hasn't happened (e.g., *2 is mistakenly called *1). In such a case, we say what the name _could_ be. The following non-theorem illustrates how this works.
(set-waterfall-parallelism :full) (thm (equal (append (car (cons x x)) y z) (append x x y)))
There is another consequence of the way the parallelized waterfall pushes
subgoals for proof by induction. Without waterfall parallelism enabled, ACL2
sometimes decides to abort instead of pushing a goal for later proof by
induction, preferring instead to induct on the original conjecture. But with
waterfall parallelism enabled, the prover no longer necessarily immediately
aborts to prove the original conjecture. Suppose for example that sibling
subgoals, Subgoal 4.6 and Subgoal 4.5, each push a subgoal for induction. If
the waterfall is performing the proof of each of these subgoals in parallel,
the proof will no longer abort immediately after the second push occurs, that
is at Subgoal 4.5. As a result, the prover will continue through Subgoal
4.4, Subgoal 4.3, and beyond. It is not until the results of combining the
proof results of Subgoal 4.6 with the results from the remaining sibling
subgoals (4.5, 4.4, and so on), that the proof attempt will abort and revert
to prove the original conjecture by induction. This example illustrates
behavior that is rather like the case that :otf-flg is t, in
the sense that the abort does not happen immediately, but also rather like
the case that :otf-flg is nil, in the sense that the abort does
occur before getting to Subgoal 3.
