		Search-engine friendly clone of the ACL2 documentation.

Parallel-proof

Unsupported-waterfall-parallelism-features

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.

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_PAR flag). 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.
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 deftheory-static is used.
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.

The :brr and with-brr-data utilities are not supported.

The 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.

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 :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 state.

Also with regards to interrupting a proof attempt, sometimes the user may need to issue a :q and 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 top. Lisp 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.

Profiling may cause proofs to hang when waterfall-parallelism is enabled (GitHub Issue #638).

During proofs with waterfall-parallelism enabled, you may see messages about "Fast alist discipline" violations, even when using hons-get appropriately. This can happen because each thread uses its own underlying hash table for fast access by hons-get, but typical top-level calls of hons-acons and make-fast-alist only affect that main thread's hash table. You can use (set-slow-alist-action nil) to eliminate this warning entirely; see slow-alist-warning.