1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
|
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
|
