Automated Verification of Parallel Nested DFS
251
1 void dfsblue(s)
2
s.color1 := cyan;
3
for t ∈ succ(s) do
4
if t.color1 = white then
5
dfsblue(t);
6
if s ∈ A then
7
dfsred(s);
8
s.color1 := blue;
9 void dfsred(s)
10
s.color2 := pink;
11
for t ∈ succ(s) do
12
if t.color1 = cyan then
13
report cycle; exit;
14
if t.color2 = white then
15
dfsred(t);
16
s.color2 := red;
Fig. 1: A standard sequential implementation of nested DFS.
state, dfsblue calls the red search on line 7, to report any accepting cycle. This
colours a state red after processing its successors recursively on line 16. The pink
colour denotes states that are only partially explored by dfsred
5 .
It is straightforward to see that NDFS is sound, meaning that it only reports
true accepting cycles. To see that NDFS is also complete, i.e., finds an accepting
cycle if one exists, observe that dfsred will indeed be started from every accepting state. This in itself is not enough: the red search ignores states marked
red in a previous call. It is essential that dfsred explores accepting states in the
right order. The crucial insight is that dfsred only visits cyan and blue states
and that accepting states coloured blue cannot be part of any accepting cycle.
The correctness of NDFS has been verified with Dafny [37]. We ported this
correctness proof to VerCors as the basis for the verification of parallel NDFS.
2.2 Parallel Nested Depth-First Search
A naive strategy for parallelising NDFS is swarming [18]: running several instances of NDFS in parallel, each working on a private set of colours. Swarmed
NDFS tends to find accepting cycles faster, since its workers are expected to explore different parts of the input graph. The correctness of swarmed NDFS with
respect to sequential NDFS is almost immediate, except for termination handling: workers only share information about the exit condition. We also verified
swarmed NDFS in VerCors, as a stepping stone for verifying parallel NDFS.
Laarman et al. improve on the swarming algorithm by sharing information
of the red search in the backtrack phase. Figure 2 presents the improved algorithm. Here every line of code is supposed to be executed atomically. The entry
point is pndfs(s I , n), which spawns n parallel instances of dfsblue(s I , tid ) in
the fashion of swarming. However, the red colourings are shared now, by which
workers can guarantee that certain states are, or will be, sufficiently explored. So
the red states can now be skipped in both the red search (line 19) and the blue
search (line 4). PNDFS thus improves performance, since workers prune each
other’s search space. At the same time this significantly complicates the correctness argument, since workers may now prevent each other from finding accepting
5 In the sequential algorithm, pink and red do not need to be distinguished, but having
the distinction here makes the parallel version easier to explain.
251
1 void dfsblue(s)
2
s.color1 := cyan;
3
for t ∈ succ(s) do
4
if t.color1 = white then
5
dfsblue(t);
6
if s ∈ A then
7
dfsred(s);
8
s.color1 := blue;
9 void dfsred(s)
10
s.color2 := pink;
11
for t ∈ succ(s) do
12
if t.color1 = cyan then
13
report cycle; exit;
14
if t.color2 = white then
15
dfsred(t);
16
s.color2 := red;
Fig. 1: A standard sequential implementation of nested DFS.
state, dfsblue calls the red search on line 7, to report any accepting cycle. This
colours a state red after processing its successors recursively on line 16. The pink
colour denotes states that are only partially explored by dfsred
5 .
It is straightforward to see that NDFS is sound, meaning that it only reports
true accepting cycles. To see that NDFS is also complete, i.e., finds an accepting
cycle if one exists, observe that dfsred will indeed be started from every accepting state. This in itself is not enough: the red search ignores states marked
red in a previous call. It is essential that dfsred explores accepting states in the
right order. The crucial insight is that dfsred only visits cyan and blue states
and that accepting states coloured blue cannot be part of any accepting cycle.
The correctness of NDFS has been verified with Dafny [37]. We ported this
correctness proof to VerCors as the basis for the verification of parallel NDFS.
2.2 Parallel Nested Depth-First Search
A naive strategy for parallelising NDFS is swarming [18]: running several instances of NDFS in parallel, each working on a private set of colours. Swarmed
NDFS tends to find accepting cycles faster, since its workers are expected to explore different parts of the input graph. The correctness of swarmed NDFS with
respect to sequential NDFS is almost immediate, except for termination handling: workers only share information about the exit condition. We also verified
swarmed NDFS in VerCors, as a stepping stone for verifying parallel NDFS.
Laarman et al. improve on the swarming algorithm by sharing information
of the red search in the backtrack phase. Figure 2 presents the improved algorithm. Here every line of code is supposed to be executed atomically. The entry
point is pndfs(s I , n), which spawns n parallel instances of dfsblue(s I , tid ) in
the fashion of swarming. However, the red colourings are shared now, by which
workers can guarantee that certain states are, or will be, sufficiently explored. So
the red states can now be skipped in both the red search (line 19) and the blue
search (line 4). PNDFS thus improves performance, since workers prune each
other’s search space. At the same time this significantly complicates the correctness argument, since workers may now prevent each other from finding accepting
5 In the sequential algorithm, pink and red do not need to be distinguished, but having
the distinction here makes the parallel version easier to explain.