Proof features not supported with waterfall-parallelism enabled
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 set-waterfall-parallelism.
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.
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
The accumulated-persistence utility is not supported.
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-
Use wormholes at your own risk. Although they use locks, there has been some concern that they may cause race conditions. They are used in ACL2(p) source code (macro observation-cw), however, thus we have hope that they perform acceptably.
Output specific to
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
Also with regards to interrupting a proof attempt, sometimes the user may
need to issue a
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
Proof output for splitter rules (see splitter) is currently unsupported when waterfall-parallelism is enabled.
Profiling may cause proofs to hang when waterfall-parallelism is enabled (GitHub Issue #638).
During proofs with waterfall-parallelism enabled, you may see