Major Section: SWITCHES-PARAMETERS-AND-MODES
This documentation topic relates to the experimental extension of ACL2
supporting parallel execution and proof; see parallelism. While the most
common use of the limit described below is in parallel proof
(see parallel-proof), it also applies to all parallelism primitives
(see parallel-programming) except spec-mv-let -- though we expect
that rather few programming applications will encouter this limit.
General Forms: (set-total-parallelism-work-limit :none) ; disable the limit (set-total-parallelism-work-limit <integer>) ; set limit to <integer>
See parallelism-tutorial, Section ``Another Granularity Issue Related to Thread Limitations'', for an explanation of how the host Lisp can run out of threads. Also see set-total-parallelism-work-limit-error.
If the underlying runtime system (the Operating System, the host Lisp, etc.) is unable to provide enough threads to finish executing the parallelism work given to it, the runtime system can crash in a very unpleasant manner (ranging from a Lisp error to completely freezing the machine). To avoid this unpleasantness, ACL2(p) will attempt to avoid creating so much parallelism that the runtime system crashes.
ACL2 initially uses a conservative estimate to limit the number of threads.
To tell ACL2(p) to use a different limit, call
set-total-parallelism-work-limit with the new limit. For example, if the
current default limit is 10,000, then to allow 13,000 threads to exist, issue
the following form at the top level.
(set-total-parallelism-work-limit 13000)
To disable this limit altogether, evaluate the following form:
(set-total-parallelism-work-limit :none)
The default value of total-parallelism-work-limit can be found by calling
function default-total-parallelism-work-limit. If the default value is
too high for your system please notify the ACL2 maintainers with a limit that
does work for your system, as they might then lower the default limit.
