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