		Search-engine friendly clone of the ACL2 documentation.

Parallelism

Set-total-parallelism-work-limit-error

For ACL2(p): control the action taken when the thread limit is exceeded

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)