for ACL2(p): set thread limit for parallelism primitives

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.