Experimental extension for parallel execution and proofs

This documentation topic relates to an experimental extension of
ACL2, ACL2(p), created initially by David L. Rager. See compiling-ACL2p for how to build an executable image that supports parallel
execution. Also see community books directory

IMPORTANT NOTE. We hope and expect that every evaluation result is correctly computed by ACL2(p), and that every formula proved using ACL2(p) is a theorem of the ACL2 logic (and in fact is provable using ACL2). However, we do not guarantee these properties. Since ACL2(p) is intended to be an aid in efficient evaluation and proof development, we focus less on ironclad soundness and more on providing an efficient and working implementation. Nevertheless, if you encounter a case where ACL2(p) computes an incorrect result, or produces a proof where ACL2 fails to do so (and this failure is not discussed in unsupported-waterfall-parallelism-features), please notify the implementors.

The ACL2 source code provides experimental parallel execution and proof capabilities. For example, one of ACL2's strengths lies in its ability to simulate industrial models efficiently, and it can also decrease the time required for proofs about such models both by making use of parallel evaluation and by dispatching proof subgoals in parallel.

While we aim to support Clozure Common Lisp (CCL), Steel Bank Common Lisp (SBCL), and Lispworks, SBCL and Lispworks both currently sometimes experience problems when evaluating the ACL2 proof process (the ``waterfall'') in parallel. Therefore, CCL is the recommend Lisp for anyone that wants to use parallelism and isn't working on fixing those problems.

- Set-waterfall-parallelism
- For ACL2(p): configuring the parallel execution of the waterfall
- Parallel-programming
- Parallel programming in ACL2(p)
- Set-waterfall-printing
- For ACL2(p): configuring the printing that occurs within the parallelized waterfall
- Unsupported-parallelism-features
- ACL2 features not supported in ACL2(p)
- Set-total-parallelism-work-limit
- For ACL2(p): set thread limit for parallelism primitives
- Set-parallel-execution
- For ACL2(p): enabling parallel execution for four parallelism primitives
- Set-total-parallelism-work-limit-error
- For ACL2(p): control the action taken when the thread limit is exceeded
- Compiling-ACL2p
- Compiling ACL2(p)
- Waterfall-parallelism-for-book-certification
- For ACL2(p): using waterfall parallelism during book certification
- Cpu-core-count
- The number of cpu cores
- Set-waterfall-parallelism-hacks-enabled
- For ACL2(p): enable waterfall-parallelism hacks
- Parallel-proof
- Parallel proof in ACL2(p)
- Non-parallel-book
- Mark a book as incompatible with ACL2(p) waterfall parallelism.
- Parallel
- Evaluating forms in parallel
- Without-waterfall-parallelism
- Disable waterfall parallelism for an enclosed event
- Set-waterfall-parallelism-hacks-enabled!
- For ACL2(p): enabling waterfall parallelism hacks
- With-waterfall-parallelism
- Enable waterfall parallelism for an enclosed event
- Parallelism-build
- Building an ACL2 executable with parallel execution enabled