Major Section: PARALLEL-PROOF
For a general introduction to ACL2(p), an experimental extension of ACL2 that supports parallel execution and proof, see parallelism. Please note that although this extension is usable and, we hope, robust in its behavior, there are still known issues to address beyond those listed explicitly below. While we expect ACL2(p) to perform correctly, it may never have the same level of attention to correctness as is given to ACL2; see parallelism, specifically the ``IMPORTANT NOTE'' there.
Below we list proof features of ACL2 that are not yet supported when parallel
execution is enabled for the primary ACL2 proof process, generally known as
``the waterfall'', typically by calling
Please note that this topic is limited to the case that such waterfall parallelism is enabled. We believe that all ACL2 proof procedures are supported when waterfall parallelism is disabled, even in executables that support parallelism (see compiling-acl2p).
Without a trust tag (see defttag): We support clause-processors, computed-hints, and custom-keyword-hints that do not modify state, but we do not permit override-hints, regardless of whether they modify state. With a trust tag, the user can use clause-processors that modify state and can also use override-hints (see set-waterfall-parallelism-hacks-enabled for a convenient mechanism for adding a trust tag). See error-triples-and-parallelism for a discussion of how to avoid modifying state in such situations. Regardless of whether a trust tag is active: We do not support checkers of custom-keyword-hints to be anything but the default checker.
GNU Make versions 3.81 and 3.82 formerly caused a lot of problems (version 3.80 somewhat less so), at least on Linux, when certifying books with ACL2 built on a host Lisp of CCL using `make'. CCL was updated around March 23, 2011 to fix this problem, so if you get segfaults (for example) with CCL, try updating your CCL installation.
Book certification should generally work but may present some issues, including the following.
o The standard `make'-based process for book certification will not use waterfall-parallelism, which is disabled by default (even when compiling-acl2p by using the
ACL2_PARflag). See books-certification and see books-certification-classic, which explain that acl2-customization files are ignored during that process unless specified explicitly on the command line or in the environment.
o A book certified with ACL2(p) might subsequently cause an error when included with ACL2. As of this writing, however, we have only seen this for a book in which
o In general, ACL2(p) is primarily intended to support more rapid interactive development. While we are unaware of an unsoundness likely to affect an ACL2(p) user, we suggest using ACL2 for final book certification, rather than ACL2(p), to lower the risk of unsound book certification.
Proof output can contain repeated printing of the same subgoal name.
Gag-mode isn't officially supported, although it has proved helpful to
use ACL2(p) in conjunction with
(set-gag-mode t) (because this setting
suppresses the output that occurs outside the waterfall). This being said,
ACL2(p) also prints key checkpoints (for example
see introduction-to-key-checkpoints), but with a notion of ``key
checkpoint'' that does not take into account whether the goal is later proved
by induction. See acl2p-key-checkpoints for further explanation of these
key checkpoints. Note that
pso is also not supported.
brr utility is not supported.
accumulated-persistence utility is not supported.
Tracking for forward-chaining-reports is not supported (see set-fc-criteria).
Time limits (see with-prover-time-limit) aren't supported.
The timing information printed at the end of a proof attempt, which is
intended to represent cpu time (not wall-clock time), may be somewhat
inaccurate when waterfall-parallelism is non-
nil. Consider using
time$ to obtain timing information.
The use of
wormholes is not recommended, as there may be race
Output specific to
:OR hints is disabled.
Proof trees are likely not to work as originally designed.
The use of
set-inhibit-output-lst may not fully inhibit proof output.
Reporting of splitter rules is currently unsupported when waterfall-parallelism is on.
Interrupting a proof attempt is not yet properly supported. At a minimum,
interrupts are trickier with waterfall parallelism enabled. For one, the
user typically needs to issue the interrupt twice before the proof attempt is
actually interrupted. Additionally, on rare occasions the theorem is
registered as proved, even though the prover did not finish the proof. If
this occurs, issue a
:u (see ubt) and you will likely be at a stable
Also with regards to interrupting a proof attempt, sometimes the user may
need to issue a
lp to reset properly the parallelism
implementation to a stable state. The primary symptom that the user is
experiencing this issue is that threads will continue to compute in the
background, even though there should be no proof attempt in progress. The
user can observe this symptom by examining the CPU utilization of their ACL2
process, for example on Linux/Unix with the shell process
usage greater than a few percent is indicative of this problem.
Because of how ACL2 arrays are designed, the user may find that, in practice, ACL2 arrays work (but perhaps with some slow-array-warning messages). However, we are aware of race conditions that can cause problems.
Instead of dynamically monitoring rewrites, dmr instead dynamically outputs information helpful for debugging the performance of proof parallelism. The instructions concerning how to see this debugging information are the same as the instructions for enabling dmr mode.
If you are working with LispWorks 6.0 or 6.0.1, then you may see messages about misaligned conses. The state of the system may be corrupted after such a message has been printed. This LispWorks bug is fixed in LispWorks 6.1.
The waterfall parallelism mode
:resource-and-timing-based is not fully
supported when the host Lisp is other than CCL. It may work, but we have not
attempted to address a potential race condition.
Proof output for splitter rules (see splitter) is currently unsupported when waterfall-parallelism is enabled.
(Comment for ACL2(h) users; see hons-and-memoization.) Memoization may not
work as intended when executing in parallel (including the waterfall). In an
effort to be helpful to the user, the functions automatically memoized by
ACL2(h) are unmemoized when setting waterfall parallelism to anything but
nil. Those exact functions are again memoized once waterfall parallelism
is disabled. Additionally, any functions memoized within the ACL2 loop (by a
memoize) are also unmemoized when enabling waterfall
parallelism and once again memoized when disabling waterfall parallelism.
This is implemented by returning the memoization state to what it was before
enabling waterfall parallelism. As such, the user should be aware that any
changes made to the memoization state while waterfall parallelism is enabled
will be lost once waterfall parallelism is disabled.