Section 3.2 discusses how parallel NDFS is specified in VerCors. In particular,
this requires the specification of permissions, to verify data race-free access to
shared data structures. Moreover, we encode the colour maps and the transition
relation of the input automaton as matrices, which greatly contribute to the feasibility of proof checking. We also explain how atomic updates are specified, which
was left implicit in the high-level pseudo code. Similarly, we implement asymmetric termination detection: if one worker finds a counterexample, all workers
can terminate immediately; if, on the other hand, all workers have completely
finished their exploration, only then may one conclude that the model is correct.
Section 3.3 explains the techniques to formalise the full functional correctness
proof in VerCors. In particular, this requires the distribution of permissions and
invariants over threads and locks, and the introduction of auxiliary ghost state
to track the precise progress of the various nested search phases of all workers.
Section 4 demonstrates how our verification is reused to verify optimisations
to the algorithm. In particular, we check the optimisation “early cycle detection”
that, for weak LTL properties, detects all cycles in the outer search instead of
the nested inner search. We also propose and verify a repair to the “all-red”
extension, by inserting an extra check that was missing in [25]. This extension
improves the speedup of parallel NDFS by sharing more global information.
Finally, Section 5 concludes with a perspective on reusing our techniques for
verifying other parallel graph algorithms.
2 Preliminaries
Section 2.1 recalls the standard sequential NDFS algorithm for finding reachable
accepting cycles in automata. We verified a parallel version of NDFS, which is
introduced in Section 2.2. The verification has been performed with VerCors;
Section 2.3 gives prerequisites on concurrency verification and separation logic.
Before discussing the NDFS algorithms, let us first recall the basic definitions
of automata and accepting cycles. An automaton G is a quadruple (S, s I , succ, A)
consisting of a finite set S of states, an initial state s I ∈ S, a next-state relation
succ : S → 2
S and a set A ⊆ S of accepting states. A path in G is a sequence
P = s 0 , . . . , s n+1 of S-states so that s i+1 ∈ succ(s i ) for every 0 ≤ i ≤ n. The
notation |P | n + 2 denotes the length of P , P [i] s i the ith state on P , and
P [i..] the subpath s i , . . . , s n+1 . Any state s is defined to be reachable (in G) if
there exists an (s I , s)-path. Any path P is a cycle whenever P [0] = P [|P | − 1]
and 1 < |P |. Finally, any cycle P is accepting if P [i] ∈ A for some 0 ≤ i < |P |.
2.1 Nested Depth-First Search
Figure 1 presents a standard, sequential implementation of NDFS, consisting
of two nested DFS searches: dfsblue and dfsred. The blue search processes
successors recursively in DFS order, marking them blue when done on line 8. The
colour cyan indicates a partially explored state, i.e., not all of its successors have
been visited yet by the blue search. Just before backtracking from an accepting
250
W. Oortwijn et al.
this requires the specification of permissions, to verify data race-free access to
shared data structures. Moreover, we encode the colour maps and the transition
relation of the input automaton as matrices, which greatly contribute to the feasibility of proof checking. We also explain how atomic updates are specified, which
was left implicit in the high-level pseudo code. Similarly, we implement asymmetric termination detection: if one worker finds a counterexample, all workers
can terminate immediately; if, on the other hand, all workers have completely
finished their exploration, only then may one conclude that the model is correct.
Section 3.3 explains the techniques to formalise the full functional correctness
proof in VerCors. In particular, this requires the distribution of permissions and
invariants over threads and locks, and the introduction of auxiliary ghost state
to track the precise progress of the various nested search phases of all workers.
Section 4 demonstrates how our verification is reused to verify optimisations
to the algorithm. In particular, we check the optimisation “early cycle detection”
that, for weak LTL properties, detects all cycles in the outer search instead of
the nested inner search. We also propose and verify a repair to the “all-red”
extension, by inserting an extra check that was missing in [25]. This extension
improves the speedup of parallel NDFS by sharing more global information.
Finally, Section 5 concludes with a perspective on reusing our techniques for
verifying other parallel graph algorithms.
2 Preliminaries
Section 2.1 recalls the standard sequential NDFS algorithm for finding reachable
accepting cycles in automata. We verified a parallel version of NDFS, which is
introduced in Section 2.2. The verification has been performed with VerCors;
Section 2.3 gives prerequisites on concurrency verification and separation logic.
Before discussing the NDFS algorithms, let us first recall the basic definitions
of automata and accepting cycles. An automaton G is a quadruple (S, s I , succ, A)
consisting of a finite set S of states, an initial state s I ∈ S, a next-state relation
succ : S → 2
S and a set A ⊆ S of accepting states. A path in G is a sequence
P = s 0 , . . . , s n+1 of S-states so that s i+1 ∈ succ(s i ) for every 0 ≤ i ≤ n. The
notation |P | n + 2 denotes the length of P , P [i] s i the ith state on P , and
P [i..] the subpath s i , . . . , s n+1 . Any state s is defined to be reachable (in G) if
there exists an (s I , s)-path. Any path P is a cycle whenever P [0] = P [|P | − 1]
and 1 < |P |. Finally, any cycle P is accepting if P [i] ∈ A for some 0 ≤ i < |P |.
2.1 Nested Depth-First Search
Figure 1 presents a standard, sequential implementation of NDFS, consisting
of two nested DFS searches: dfsblue and dfsred. The blue search processes
successors recursively in DFS order, marking them blue when done on line 8. The
colour cyan indicates a partially explored state, i.e., not all of its successors have
been visited yet by the blue search. Just before backtracking from an accepting
250
W. Oortwijn et al.