Major Section: PARALLELISM
This documentation topic relates to the experimental extension of ACL2 supporting parallel execution and proof; see parallelism. See parallelism-tutorial for an introduction to parallel programming in ACL2.
For 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'', see unsupported-waterfall-parallelism-features.
Please note that this topic discusses ACL2 features that are disabled when using ACL2(p) (see compiling-acl2p). These features are disabled regardless of whether waterfall parallelism is enabled.
Calls of observation-cw simply convert to calls of cw, so
suppressing observations (see set-inhibit-output-lst) will not
suppress these messages.
Memoization is not supported when executing in parallel. See Unsupported-waterfall-parallelism-features for memoization details related to waterfall parallelism.
Since, as of April 2012, garbage collection is inherently sequential, ACL2(p) minimizes the use of garbage collection by setting a high garbage collection threshold. As a result, ACL2(p) is not expected to perform well on machines with less memory than this threshold (1 gigabyte, as of April 2012).
In CCL, the underlying parallel execution engine is tuned for the number of CPU cores (or hardware threads) actually available in the machine. SBCL and LispWorks are tuned for a machine with 16 CPU cores.
CCL is considered to be the ``flagship Lisp'' for parallel execution in ACL2. The SBCL and LispWorks implementations are thought to be generally stable. However, due to their relatively less common use, the SBCL and LispWorks implementations are likely less robust than the CCL implementation.
The time-tracker utility is a no-op for ACL2(p).
