Major Section: SWITCHES-PARAMETERS-AND-MODES
This documentation topic relates to the experimental extension of ACL2 supporting parallel execution and proof; see parallelism.
General Forms:
(set-total-parallelism-work-limit-error t) ; cause error (default)
(set-total-parallelism-work-limit-error nil) ; disable error and
; continue serially
See parallelism-tutorial, Section ``Another Granularity Issue Related to Thread Limitations'', for an explanation of how the host Lisp can run out of threads. See set-total-parallelism-work-limit for further details, including an explanation of how to manage the limit that triggers this error.
The value of state global total-parallelism-work-limit-error dictates
what occurs when the underlying runtime system runs reaches a limit on the
number of threads for parallel computation. By default, when this limit is
reached, the ACL2(p) user will receive an error and computation will halt.
At this point, the ACL2(p) user has the following options.
(1) Remove the limit by evaluating the following form.
(set-total-parallelism-work-limit :none)
(2) Disable the error so that execution continues serially once the available thread resources have been exhausted.
(set-total-parallelism-work-limit-error nil)
(3) Increase the limit on number of threads that ACL2(p) is willing to create, in spite of potential risk (see set-total-parallelism-work-limit). In this case, the following query returns the current limit.
(f-get-global 'total-parallelism-work-limit)Then to increase that limit, evaluate the following form:
(set-total-parallelism-work-limit <new-integer-value>)
For example, suppose that the value of total-parallelism-work-limit was
originally 10,000. Then evaluation of the following form increases that
limit to 13,000.
(set-total-parallelism-work-limit 13000)
