performance issues for parallel execution

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

See granularity for an important construct that limits the spawning of parallel computations, which can be important when a computation is too short-lived to warrant a separate thread.

There are times in which parallelism provides no speedup because of garbage collection in the underlying Lisp implementation. The following example illustrates this phenomenon. If you change the granularity declaration so that the depth bound is 3, 4, or larger instead of 2, you may still find no speedup. In all cases you may find that parallelism results in a significantly greater time spent in garbage collection.

(include-book "finite-set-theory/osets/sets" :dir :system)
(defun sets::pmergesort-exec (x depth)
    (declare (xargs :mode :program))
    (cond ((endp x) nil)
          ((endp (cdr x)) (sets::insert (car x) nil))
          (t (mv-let (part1 part2)
                     (sets::split-list x nil nil)
                      (declare (granularity (< depth 2)))
                      (sets::union (sets::pmergesort-exec part1
                                                          (1+ depth))
                                   (sets::pmergesort-exec part2
                                                          (1+ depth))))))))
(defconst *x* (reverse (fromto 1 400000)))
(time$ (length (sets::pmergesort-exec *x* 0)))
(set-parallel-execution nil)
(time$ (length (sets::pmergesort-exec *x* 0)))