Definition 1 (Special path). Any path P = s 0 , . . . , s n+1 is defined to be tid -
special if s 0 ∈ Pink tid , s n+1 ∈ Cyan tid , and none of the states on P are red, i.e.,
s k ∈ Red for every k such that 0 ≤ k ≤ n + 1.
Any path P is special if P is tid -special for some worker tid . Intuitively, the
existence of a tid -special path during execution of pndfs means that (i ) worker
tid is doing a red search, since it has pink states, and (ii ) this worker will eventually find an accepting cycle, unless other workers obstruct this path. Thus the
above definition allows to formally define obstruction: a worker tid is obstructed
(will miss an accepting cycle) if any state on a tid -special path is coloured red.
Our main strategy for proving completeness involves showing that every time
a worker gets obstructed, a new special path can be found. A direct consequence
of this is that not all accepting cycles can be missed: upon termination of pndfs,
there are no more cyan or pink states. To help prove this, we use the following
property (taken from [25], but rephrased to handle our special paths), that allows
to find special paths by using the colouring invariants.
Lemma 2. If invariants 1.1–1.6 are satisfied, then every path P = s 0 , . . . , s n+1
with s 0 ∈ Red and s n+1 ∈ A \ Red contains a special subpath.
Proof. The original handwritten proof from [25] shows that this lemma follows
from invariants 1.1 –1.6 , by induction on P .
The original completeness proof of [25] performs induction on the number of
obstructed accepting cycles, to show the absence of such cycles upon termination
as a result of Lemma 2. However, such an argument is out of reach for Hoare-style
reasoning, since it is not an inductive invariant. We propose a new invariant that
is inductive, which builds on the insight that, under certain colouring conditions,
new special paths can always be found when workers get obstructed, as is shown
by Lemma 3. In particular, pndfs guarantees that if there exists a special path
before executing line 24, then there also exists a special path after its execution.
Lemma 3. For any non-red state r ∈ S \ Red that is on a tid -special path, if:
i. r ∈ A =⇒ succ(r) ⊆ Red , and
ii. r ∈ A ∩ Pink tid =⇒ Pink tid = {r},
then there still exists a special path after adding r to Red .
Proof. Let P = s 0 . . . s n+1 be a tid-special path and assume that r is on P , so
that r = s for some such that 0 ≤ ≤ n + 1. Since Pink tid = ∅, worker tid is
performing dfsred that was started from some accepting state a ∈ A ∩ Pink tid .
Then a = r, as otherwise s 0 = a due to ii., which by i. would contradict that P
is special. Moreover, since s n+1 ∈ Cyan tid there exists a (s n+1 , a)-path Q (this
is a standard property of dfsblue; the path Q must be on the recursive call
stack). Then Lemma 2 applies on the path s , . . . , s n+1 , Q[1..] and gives a new
special path when considering Red ∪ {r} as the new set of red states.
Lemma 3 implies that every time an accepting cycle is missed due to pruning,
there is always another accepting cycle that will eventually be reported. This is
enough to establish completeness of pndfs, via the following key invariant.
254
W. Oortwijn et al.
special if s 0 ∈ Pink tid , s n+1 ∈ Cyan tid , and none of the states on P are red, i.e.,
s k ∈ Red for every k such that 0 ≤ k ≤ n + 1.
Any path P is special if P is tid -special for some worker tid . Intuitively, the
existence of a tid -special path during execution of pndfs means that (i ) worker
tid is doing a red search, since it has pink states, and (ii ) this worker will eventually find an accepting cycle, unless other workers obstruct this path. Thus the
above definition allows to formally define obstruction: a worker tid is obstructed
(will miss an accepting cycle) if any state on a tid -special path is coloured red.
Our main strategy for proving completeness involves showing that every time
a worker gets obstructed, a new special path can be found. A direct consequence
of this is that not all accepting cycles can be missed: upon termination of pndfs,
there are no more cyan or pink states. To help prove this, we use the following
property (taken from [25], but rephrased to handle our special paths), that allows
to find special paths by using the colouring invariants.
Lemma 2. If invariants 1.1–1.6 are satisfied, then every path P = s 0 , . . . , s n+1
with s 0 ∈ Red and s n+1 ∈ A \ Red contains a special subpath.
Proof. The original handwritten proof from [25] shows that this lemma follows
from invariants 1.1 –1.6 , by induction on P .
The original completeness proof of [25] performs induction on the number of
obstructed accepting cycles, to show the absence of such cycles upon termination
as a result of Lemma 2. However, such an argument is out of reach for Hoare-style
reasoning, since it is not an inductive invariant. We propose a new invariant that
is inductive, which builds on the insight that, under certain colouring conditions,
new special paths can always be found when workers get obstructed, as is shown
by Lemma 3. In particular, pndfs guarantees that if there exists a special path
before executing line 24, then there also exists a special path after its execution.
Lemma 3. For any non-red state r ∈ S \ Red that is on a tid -special path, if:
i. r ∈ A =⇒ succ(r) ⊆ Red , and
ii. r ∈ A ∩ Pink tid =⇒ Pink tid = {r},
then there still exists a special path after adding r to Red .
Proof. Let P = s 0 . . . s n+1 be a tid-special path and assume that r is on P , so
that r = s for some such that 0 ≤ ≤ n + 1. Since Pink tid = ∅, worker tid is
performing dfsred that was started from some accepting state a ∈ A ∩ Pink tid .
Then a = r, as otherwise s 0 = a due to ii., which by i. would contradict that P
is special. Moreover, since s n+1 ∈ Cyan tid there exists a (s n+1 , a)-path Q (this
is a standard property of dfsblue; the path Q must be on the recursive call
stack). Then Lemma 2 applies on the path s , . . . , s n+1 , Q[1..] and gives a new
special path when considering Red ∪ {r} as the new set of red states.
Lemma 3 implies that every time an accepting cycle is missed due to pruning,
there is always another accepting cycle that will eventually be reported. This is
enough to establish completeness of pndfs, via the following key invariant.
254
W. Oortwijn et al.