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

This documentation topic relates to the experimental extension of ACL2 supporting parallel execution 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 t)          ; alias for :resource-based
(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 evaluates its argument, which 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 t is treated the same as a value of :resource-based and is provided for user convenience.

:Resource-based waterfall parallelism typically achieves the best performance in ACL2(p), while maintaining system stability, so :resource-based (or equivalently, t) is the recommended value.

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 (or equivalently, t) 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).

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.

The following remark pertains to those using the `HONS' experimental extension of ACL2 (see hons-and-memoization; in particular, see memoize). Since memoization is not supported when waterfall parallelism is enabled (see unsupported-waterfall-parallelism-features), then when set-waterfall-parallelism is called with a non-nil value, all memoized functions are unmemoized. When set-waterfall-parallelism is again called with a nil value, those memoization settings are restored.

Set-waterfall-parallelism is an embedded event form. However, a call of this macro will not affect waterfall-parallelism when including a certified book that contains that call. For such an effect, you may use the following make-event form.

(make-event (er-progn (set-waterfall-parallelism :full)
                      (value '(value-triple nil)))
            :check-expansion t)