Major Section: PARALLEL-PROGRAMMING
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)
(pargs
(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)))
