Automated Verification of Parallel Nested DFS
255
Lemma 4. The pndfs algorithm maintains the global invariant that either:
4.1. All reachable accepting cycles contain an accepting state that is not red; or
4.2. There exists a special path.
Proof. The interesting case is showing that this invariant remains preserved after
making a non-red state s ∈ Pink tid \ Red red (on line 24 of Fig. 2), by some
worker tid that is doing a red search from some accepting state a ∈ A ∩ Pink tid .
– Suppose s ∈ A. If s is on a special path, then Invariant 4.2 is reestablished
due to Lemma 3, and otherwise the key invariant remains preserved.
– Suppose s ∈ A. Then s = a by Invariant 1.6 . Since worker tid is about to
finish its red exploration, we have that (†) Pink tid = {s} (i.e., all other pink
states have been fully explored) and consequently that (‡) succ(s) ⊆ Red .
Furthermore, due to the await s instruction on line 23 we have that (†) and
(‡) hold for all workers that are doing a red exploration that involves s. If s
is on a special path, then Invariant 4.2 is reestablished due to Lemma 3. So
now suppose that s is on an accepting cycle P . Without loss of generality,
assume that P [0] = s. Then (‡) implies that 1 < |P | and that P [1] ∈ Red .
Thus Lemma 3 applies on the path P [1..] to establish Invariant 4.2 .
The next theorem shows how Lemma 4 allows deriving completeness of parallel NDFS. In particular, it shows that no accepting cycles can exist when all
threads have terminated, in which case all the theorem’s premises are fulfilled.
Theorem 1. If for every worker tid it holds that Pink tid = ∅, Cyan tid = ∅ and
s I ∈ Blue tid , then there does not exist a reachable accepting cycle.
Proof. Towards a contradiction, suppose that there exists an accepting cycle P
that is reachable via an (s I , P [0])-path Q. Due to the theorem’s premises no
special paths can exist, and therefore by Lemma 4 there is an accepting state
on P that is not red. Without loss of generality, assume that (†) P [0] ∈ A \ Red .
Since Q[0] ∈ Blue 0 (since there is at least one worker), by induction on Q together with Lemma 1 we have that P [0] ∈ Red , which contradicts (†).
All the above invariants and proof steps have been encoded in VerCors, which
was highly non-trivial. While mechanising the proofs, many implicit proof steps
had to be made explicit. Section 3.3 further details the proof mechanisation.
3.2 Encoding of pndfs in VerCors
Graph structures are notoriously difficult to handle in separation logics, as they
usually rely on pointer aliasing, which complicates ownership handling and prevents easy use of the frame rule [38]. However, since automata have a fixed and
finite set of states, we can overcome this limitation by representing the input
automata as an |S| × |S| adjacency matrix. This does not impose serious restrictions: other automata encodings can be transformed at the specification level
to an adjacency matrix, e.g., via model fields in the style of JML [11,29]. The
suitability of adjacency matrices for deductive verification is confirmed by [24].
255
Lemma 4. The pndfs algorithm maintains the global invariant that either:
4.1. All reachable accepting cycles contain an accepting state that is not red; or
4.2. There exists a special path.
Proof. The interesting case is showing that this invariant remains preserved after
making a non-red state s ∈ Pink tid \ Red red (on line 24 of Fig. 2), by some
worker tid that is doing a red search from some accepting state a ∈ A ∩ Pink tid .
– Suppose s ∈ A. If s is on a special path, then Invariant 4.2 is reestablished
due to Lemma 3, and otherwise the key invariant remains preserved.
– Suppose s ∈ A. Then s = a by Invariant 1.6 . Since worker tid is about to
finish its red exploration, we have that (†) Pink tid = {s} (i.e., all other pink
states have been fully explored) and consequently that (‡) succ(s) ⊆ Red .
Furthermore, due to the await s instruction on line 23 we have that (†) and
(‡) hold for all workers that are doing a red exploration that involves s. If s
is on a special path, then Invariant 4.2 is reestablished due to Lemma 3. So
now suppose that s is on an accepting cycle P . Without loss of generality,
assume that P [0] = s. Then (‡) implies that 1 < |P | and that P [1] ∈ Red .
Thus Lemma 3 applies on the path P [1..] to establish Invariant 4.2 .
The next theorem shows how Lemma 4 allows deriving completeness of parallel NDFS. In particular, it shows that no accepting cycles can exist when all
threads have terminated, in which case all the theorem’s premises are fulfilled.
Theorem 1. If for every worker tid it holds that Pink tid = ∅, Cyan tid = ∅ and
s I ∈ Blue tid , then there does not exist a reachable accepting cycle.
Proof. Towards a contradiction, suppose that there exists an accepting cycle P
that is reachable via an (s I , P [0])-path Q. Due to the theorem’s premises no
special paths can exist, and therefore by Lemma 4 there is an accepting state
on P that is not red. Without loss of generality, assume that (†) P [0] ∈ A \ Red .
Since Q[0] ∈ Blue 0 (since there is at least one worker), by induction on Q together with Lemma 1 we have that P [0] ∈ Red , which contradicts (†).
All the above invariants and proof steps have been encoded in VerCors, which
was highly non-trivial. While mechanising the proofs, many implicit proof steps
had to be made explicit. Section 3.3 further details the proof mechanisation.
3.2 Encoding of pndfs in VerCors
Graph structures are notoriously difficult to handle in separation logics, as they
usually rely on pointer aliasing, which complicates ownership handling and prevents easy use of the frame rule [38]. However, since automata have a fixed and
finite set of states, we can overcome this limitation by representing the input
automata as an |S| × |S| adjacency matrix. This does not impose serious restrictions: other automata encodings can be transformed at the specification level
to an adjacency matrix, e.g., via model fields in the style of JML [11,29]. The
suitability of adjacency matrices for deductive verification is confirmed by [24].