UNSUPPORTED-WATERFALL-PARALLELISM-FEATURES

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

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

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

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.

The :brr utility is 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.

The use of wormholes is not recommended, as there may be race conditions.

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.

(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 call of 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.