Major Section: SWITCHES-PARAMETERS-AND-MODES
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)
To enable waterfall parallelism for book certification using ACL2(p), see waterfall-parallelism-for-book-certification.
