The following five files are useful for running regressions with
ACL2(p):

  parallel-full.lisp
  parallel-resource-based.lisp
  parallel-top-level.lisp
  pseudo-parallel.lisp
  serial.lisp

For example:

(time nice make -j 8 regression-fresh ACL2_CENTAUR=skip ACL2=/projects/acl2/devel/ccl-saved_acl2p ACL2_CUSTOMIZATION=/projects/acl2/devel/acl2-customization-files/parallel-full.lisp) >& logs/make-regression-par-ccl-j-8-feb27.log&

To find all calls of set-waterfall-parallelism, issue the following
command in your books directory.

grep -l "set-waterfall-parallelism" `find . -name "*.acl2" -o -name "*.lisp"`

Note: Sometimes parallelism is defeated or modified for individual
books.  To find some of these occurrences, you can issue the following
command in your books directory.

  grep -l acl2-par `find . -name "*.acl2"`

For example, hints/basic-tests.acl2 has this:

  #+acl2-par
  ; computed hints that modify state
  (set-waterfall-parallelism nil)

And models/jvm/m5/apprentice.acl2 has this:

  #+acl2-par
  (set-waterfall-parallelism t)

A utility, without-waterfall-parallelism, may be useful.  For example,
in defsort/generic.lisp we find:

  (local (include-book "misc/without-waterfall-parallelism" :dir :system))
  ...
  (without-waterfall-parallelism
  (def-saved-obligs fast-comparable-mergesort-fixnums-guards
    :proofs ((fast-comparable-mergesort-fixnums-guards))
    (verify-guards fast-comparable-mergesort-fixnums))
  )

Some books use a stylized make-event inside the actual file to disable
parallelism.  To find these, issue:

  cd books
  grep -l "Disabling waterfall parallelism" `find . -name "*.lisp"`

However, set-waterfall-parallelism is now itself a make-event, so we
often do something simpler than that.  For example,
books/std/util/tests/define.lisp has the following; notice the use of
local to avoid affecting waterfall-parallelism when including the
book.

; Matt K.: Avoid ACL2(p) error in ac-g1 below pertaining to override hints.
(local (set-waterfall-parallelism nil))

Sometimes it makes sense to put such a form, but without local, in a
.acl2 file, such as this form in books/demos/gl-and-std/cert.acl2.

; Matt K.: Avoid ACL2(p) errors.
(set-waterfall-parallelism nil)

Here is a note relevant to ACL2(p) from David Rager.

  Some of the books will perform better under :resource-based waterfall
  parallelism than :full waterfall parallelism.  This is because these
  books have so many subgoals and such a strange dependency tree between
  those subgoals that the waterfall parallelism resources become
  exhausted and the proofs must execute serially at times to maintain a
  stable system.  As such, it may be good to override any :full setting
  that a customization file provides and use :resource-based waterfall
  parallelism instead -- just for these few books.  Note that even
  without overriding the waterfall parallelism setting, the system will
  remain stable.  Changing the waterfall parallelism mode is just a
  performance optimization.  As of April 2012, the books to which this
  statement may apply are the following:

  models/jvm/m5/apprentice.lisp
  coi/termination/assuming/complex.lisp
  concurrent-programs/bakery/stutter2.lisp