Automated Verification of Parallel Nested DFS
261
1 void dfsblue(s, tid )
2
s.color [tid ] := cyan;
3
for t ∈ succ(s) do
4
if t.color [tid ] = cyan then
5
if s.acc ∨ t.acc then
6
report cycle; exit all;
7
( )
if t.color [tid ] = cyan then
if s.acc ∨ t.acc then
report cycle; exit all;
if t.color [tid ] = white then
8
if ¬t.red then
9
dfsblue(t, tid );
10
if s.acc ∧ ¬s.red then
11
s.count := s.count + 1;
12
dfsred(s, tid );
13
s.color [tid ] := blue;
(a) The “early cycle detection” extension
1 void dfsblue(s, tid )
2
allred := true;
3
,
allred := true;
s.color [tid ] := cyan;
4
for t ∈ succ(s) do
5
if t.color [tid ] = white then
6
if ¬t.red then
dfsblue(t, tid );
7
if ¬t.red then allred := false;
if ¬t.red then allred := false;
8
if allred then
9
await s.count = 0;
10
s.red := true;
11
if allred then
await s.count = 0;
s.red := true;
else if s.acc ∧ ¬s.red then
12
s.count := s.count + 1;
13
dfsred(s, tid );
14
s.color [tid ] := blue;
(b) The “all-red” extension
Fig. 7: Two extensions (highlighted grey) to dfsblue that improve work sharing.
search from s I . Combining this information with the information in the resource
invariant allows one to prove all the premises of Theorem 1. Therefore its ghost
method encoding can be applied on line 22, from which completeness is derived.
The encoding of parallel NDFS in VerCors [35] comprises roughly 2500 lines
of code (of which ∼85% is proof overhead), which includes the mechanisation of
all proof steps described in §3.1. The verification time is about 140s, measured
on a Macbook with an Intel Core i5 CPU with 2,9 GHz, and 8Gb memory.
4 Optimisations
One major benefit of mechanically verified code is that optimisations can be
applied with full confidence. Without verification, changes to critical code are
often avoided, to ensure that no errors are introduced. A verified algorithm allows
to apply optimisations easily, as these often do not change the outer contract, at
most requiring only minor adaptions to the invariants. We illustrate this with two
optimisations, for which [25] experimentally demonstrated improved speedup.
“Early cycle detection” checks already in the blue search if an accepting cycle
is closed, cf. lines 4–6 in Figure 7a. It is known that for weak LTL properties,
all accepting cycles will be found in the blue search when applying early cycle
detection. To show that this optimisation indeed preserves all invariants, we
simply inserted these 3 lines in the VerCors specification. The proof introduces
a case distinction on whether s or t is accepting and constructs a witness path.
This adds another 10 lines: two for the case distinction and four in each branch
to show that a witness accepting cycle exists. Collectively, these extra 13 lines
constitute indeed very little effort to prove this particular optimisation correct.
The second optimisation, called “all-red”, checks if all successors of s became
red during the blue search (lines 2 and 7 in Figure 7b). If so, we can mark s.red
261
1 void dfsblue(s, tid )
2
s.color [tid ] := cyan;
3
for t ∈ succ(s) do
4
if t.color [tid ] = cyan then
5
if s.acc ∨ t.acc then
6
report cycle; exit all;
7
( )
if t.color [tid ] = cyan then
if s.acc ∨ t.acc then
report cycle; exit all;
if t.color [tid ] = white then
8
if ¬t.red then
9
dfsblue(t, tid );
10
if s.acc ∧ ¬s.red then
11
s.count := s.count + 1;
12
dfsred(s, tid );
13
s.color [tid ] := blue;
(a) The “early cycle detection” extension
1 void dfsblue(s, tid )
2
allred := true;
3
,
allred := true;
s.color [tid ] := cyan;
4
for t ∈ succ(s) do
5
if t.color [tid ] = white then
6
if ¬t.red then
dfsblue(t, tid );
7
if ¬t.red then allred := false;
if ¬t.red then allred := false;
8
if allred then
9
await s.count = 0;
10
s.red := true;
11
if allred then
await s.count = 0;
s.red := true;
else if s.acc ∧ ¬s.red then
12
s.count := s.count + 1;
13
dfsred(s, tid );
14
s.color [tid ] := blue;
(b) The “all-red” extension
Fig. 7: Two extensions (highlighted grey) to dfsblue that improve work sharing.
search from s I . Combining this information with the information in the resource
invariant allows one to prove all the premises of Theorem 1. Therefore its ghost
method encoding can be applied on line 22, from which completeness is derived.
The encoding of parallel NDFS in VerCors [35] comprises roughly 2500 lines
of code (of which ∼85% is proof overhead), which includes the mechanisation of
all proof steps described in §3.1. The verification time is about 140s, measured
on a Macbook with an Intel Core i5 CPU with 2,9 GHz, and 8Gb memory.
4 Optimisations
One major benefit of mechanically verified code is that optimisations can be
applied with full confidence. Without verification, changes to critical code are
often avoided, to ensure that no errors are introduced. A verified algorithm allows
to apply optimisations easily, as these often do not change the outer contract, at
most requiring only minor adaptions to the invariants. We illustrate this with two
optimisations, for which [25] experimentally demonstrated improved speedup.
“Early cycle detection” checks already in the blue search if an accepting cycle
is closed, cf. lines 4–6 in Figure 7a. It is known that for weak LTL properties,
all accepting cycles will be found in the blue search when applying early cycle
detection. To show that this optimisation indeed preserves all invariants, we
simply inserted these 3 lines in the VerCors specification. The proof introduces
a case distinction on whether s or t is accepting and constructs a witness path.
This adds another 10 lines: two for the case distinction and four in each branch
to show that a witness accepting cycle exists. Collectively, these extra 13 lines
constitute indeed very little effort to prove this particular optimisation correct.
The second optimisation, called “all-red”, checks if all successors of s became
red during the blue search (lines 2 and 7 in Figure 7b). If so, we can mark s.red