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 encounter 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
To disable this limit altogether, evaluate the following form:
The default value of total-parallelism-work-limit can be found by calling