for ACL2(p): configuring the parallel execution of the waterfall

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

General Forms:
(set-waterfall-parallelism nil)        ; never parallelize (serial execution)
(set-waterfall-parallelism :full)      ; always parallelize
(set-waterfall-parallelism :top-level) ; parallelize top-level subgoals
(set-waterfall-parallelism             ; parallelize if sufficient resources
  :resource-based)                     ;   (recommended setting)
(set-waterfall-parallelism             ; parallelize if sufficient resources
  :resource-and-timing-based           ;   and suggested by prior attempts
(set-waterfall-parallelism             ; never parallelize but use parallel
  :pseudo-parallel)                    ;   code base (a debug mode)

Set-waterfall-parallelism takes an argument that specifies the enabling or disabling of the parallel execution of ACL2's main proof process, the waterfall.

It also sets state global waterfall-printing to an appropriate value. See set-waterfall-printing.

Note that not all ACL2 features are supported when waterfall-parallelism is set to non-nil (see unsupported-waterfall-parallelism-features).

A value of nil indicates that ACL2(p) should never prove subgoals in parallel.

A value of :full indicates that ACL2(p) should always prove independent subgoals in parallel.

A value of :top-level indicates that ACL2(p) should prove each of the top-level subgoals in parallel but otherwise prove subgoals in a serial manner. This mode is useful when the user knows that there are enough top-level subgoals, many of which take a non-trivial amount of time to be proved, such that proving them in parallel will result in a useful reduction in overall proof time.

A value of :resource-based indicates that ACL2(p) should use its built-in heuristics to determine whether CPU core resources are available for parallel execution. Note that ACL2(p) does not hook into the operating system to determine the workload on the machine. ACL2(p) works off the assumption that it is the only process using significant CPU resources, and it optimizes the amount of parallelism based on the number of CPU cores in the system. (Note that ACL2(p) knows how to obtain the number of CPU cores from the operating system in CCL, but that, in SBCL and in Lispworks, a constant is used instead). :Resource-based is the recommended setting for ACL2(p).

During the first proof attempt of a given conjecture, a value of :resource-and-timing-based results in the same behavior as with :resource-based. However, on subsequent proof attempts, the time it took to prove each subgoal will be considered when deciding whether to parallelize execution. If a particular theorem's proof is already achieving satisfactory speedup via :resource-based parallelism, there is no reason to try this setting. However, if the user wishes to experiment, the :resource-and-timing-based setting may improve performance. Note that since the initial run does not have the subgoal proof times available, this mode will never be better than the :resource-based setting for non-interactive theorem proving.

A value of :pseudo-parallel results in using the parallel waterfall code, but with serial execution. This setting is useful for debugging the code base that supports parallel execution of the waterfall. For example, you may wish to use this mode if you are an ``ACL2 Hacker'' who would like to see comprehensible output from tracing (see trace$) the @par versions of the waterfall functions.

Note: This is an event! It does not print the usual event summary but nevertheless changes the ACL2 logical world and is so recorded. Moreover, set-waterfall-parallelism events are never redundant (see redundant-events).