Limit the amount of parallelism

This documentation topic relates to the experimental extension of ACL2 supporting parallel execution and proof; see parallelism.

Some function calls are on arguments whose evaluation time is long enough to warrant parallel execution, while others are not. A granularity form can be used to make appropriate restrictions on the use of parallelism.

For example, consider the Fibonacci function. Experiments have suggested that execution time can be reduced if whenever the argument is less than 27, a serial version of the Fibonacci function is called. One way to utilize this information is to write two definitions of the Fibonacci function, one serial and one parallel.

(defun fib (x) (declare (xargs :guard (natp x))) (cond ((or (zp x) (<= x 0)) 0) ((= x 1) 1) (t (binary-+ (fib (- x 1)) (fib (- x 2)))))) (defun pfib (x) (declare (xargs :guard (natp x))) (cond ((or (zp x) (<= x 0)) 0) ((= x 1) 1) ((< x 27) (binary-+ (fib (- x 1)) (fib (- x 2)))) (t (pargs (binary-+ (pfib (- x 1)) (pfib (- x 2)))))))

We realize quickly that writing both of these function definitions is
cumbersome and redundant. This problem can be avoided by using a

(defun pfib (x) (declare (xargs :guard (natp x))) (cond ((or (zp x) (<= x 0)) 0) ((= x 1) 1) (t (pargs (declare (granularity (>= x 27))) (binary-+ (pfib (- x 1)) (pfib (- x 2)))))))

A granularity form can reference an extra formal parameter that describes
the call depth of the function the user is parallelizing. Consider for
example the following parallel

(include-book "finite-set-theory/osets/sets" :dir :system) (defun set::pmergesort-exec (x depth) (declare (xargs :mode :program)) (cond ((endp x) nil) ((endp (cdr x)) (set::insert (car x) nil)) (t (mv-let (part1 part2) (set::split-list x nil nil) (pargs (declare (granularity (< depth 2))) (set::union (set::pmergesort-exec part1 (1+ depth)) (set::pmergesort-exec part2 (1+ depth))))))))

A less intrusive method (i.e., not requiring an extra formal parameter like
the

(defun some-depth-exceeds (x n) (declare (xargs :guard (natp n))) (if (atom x) nil (if (zp n) t (or (some-depth-exceeds (car x) (1- n)) (some-depth-exceeds (cdr x) (1- n)))))) (defun valid-tip (x) (declare (xargs :guard t)) (or (eq x 'A) (eq x 'T) (eq x 'C) (eq x 'G))) (defun pvalid-tree (x) (declare (xargs :guard t)) (if (atom x) (valid-tip x) (pand (declare (granularity (some-depth-exceeds x 3))) (pvalid-tree (car x)) (pvalid-tree (cdr x)))))

If you experiment with calls of