Automated Verification of Parallel Nested DFS
259
1 context Perm(N ) ∗∗ Perm(nthreads) ∗∗ Perm(G) ∗∗ Perm(acc);
2 context 0 ≤ s < N;
3 context 0 ≤ tid < nthreads;
4 context ∀t : 0 ≤ t < N ⇒ Perm(color [tid ][t],
1
2
) ∗∗ Perm(pink [tid ][t],
1
2
);
5 requires color [tid ][s] = white;
6 requires ∀t : (0 ≤ t < N ∧ color [tid ][t] = cyan) ⇒ ExPath(t, s, 1);
7 ensures \result ⇒ ∃a : 0 ≤ a < N ∧ acc[a] ∧ ExPath(sI , a, 1) ∧ ExPath(a, a, 2);
8 ensures ¬\result ⇒ ∀t : color [tid ][t] = cyan ⇔ \old(color [tid ][t]) = cyan;
9 ensures ¬\result ⇒ pink [tid ] = \old(pink [tid ]) ∧ color [tid ][s] = blue;
10 bool dfsblue(s, tid )
11
· · ·
Fig. 5: The ownership specification in the contract dfsblue for thread tid . Annotations of the form context P abbreviate requires P ; ensures P .
atomically. This distribution of ownership matches with the encoding of atomic
operations discussed earlier. Line 7 expresses soundness of dfsblue, captured
in the resource invariant (line 8 of Fig. 4) on global termination. This allows to
deduce soundness of pndfs from the resource invariant, after all threads have
terminated as result of the detection of an accepting cycle.
Auxiliary ghost state. As mentioned earlier, to prove that pndfs also preserves the (encodings of) Invariants 1.1 –1.6 and 4.1 –4.2 after every computation step, additional ghost state needs to be maintained. In particular, we need
to make explicit that every worker tid with Pink tid = ∅ is doing a dfsred search
that was started from some root state a ∈ A ∩ Pink tid . In addition, the proof of
Lemma 3 needs that there exists an (s, a)-path for every s ∈ Cyan tid . To prove
the preservation of Lemma 4 we also need that, if worker tid is not yet executing
the await instruction, we have that a ∈ Red , and otherwise that Pink tid = {a}.
This extra information is encoded in the loop invariant on lines 20–27 (Figure 4), via three ghost arrays, named exploringred , redroot and waiting. Firstly,
exploringred administrates which workers are doing a red search. For verification
purposes we added ghost code to the program, to set exploringred [tid ] to true
whenever dfsred(a, tid ) is invoked by worker tid from a blue search, and back
to false whenever dfsred(a, tid ) returns. Secondly, redroot stores the root state
on which dfsred was invoked. Finally, waiting administrates which workers are
executing an await instruction. These three ghost arrays together are closely related to the s.count fields in the program of Figure 2, via the following invariant:
∀s : s.count = |{tid | exploringred [tid ] ∧ redroot [tid ] = s ∧ ¬waiting[tid ]}|.
Establishing that pndfs adheres to the invariants in Lemmas 1 and 4 was
highly non-trivial and required various complex auxiliary lemmas to be encoded
and proven. These are all encoded in VerCors as ghost methods: side-effect-free
helper methods on which the lemma is encoded in the method’s contract [21,22].
Induction proofs, for example, are encoded using either loop invariants or recursion. Application of a lemma then translates to a function call on the specification
level. The proofs in Section 3.1 are all encoded and applied in this way.
259
1 context Perm(N ) ∗∗ Perm(nthreads) ∗∗ Perm(G) ∗∗ Perm(acc);
2 context 0 ≤ s < N;
3 context 0 ≤ tid < nthreads;
4 context ∀t : 0 ≤ t < N ⇒ Perm(color [tid ][t],
1
2
) ∗∗ Perm(pink [tid ][t],
1
2
);
5 requires color [tid ][s] = white;
6 requires ∀t : (0 ≤ t < N ∧ color [tid ][t] = cyan) ⇒ ExPath(t, s, 1);
7 ensures \result ⇒ ∃a : 0 ≤ a < N ∧ acc[a] ∧ ExPath(sI , a, 1) ∧ ExPath(a, a, 2);
8 ensures ¬\result ⇒ ∀t : color [tid ][t] = cyan ⇔ \old(color [tid ][t]) = cyan;
9 ensures ¬\result ⇒ pink [tid ] = \old(pink [tid ]) ∧ color [tid ][s] = blue;
10 bool dfsblue(s, tid )
11
· · ·
Fig. 5: The ownership specification in the contract dfsblue for thread tid . Annotations of the form context P abbreviate requires P ; ensures P .
atomically. This distribution of ownership matches with the encoding of atomic
operations discussed earlier. Line 7 expresses soundness of dfsblue, captured
in the resource invariant (line 8 of Fig. 4) on global termination. This allows to
deduce soundness of pndfs from the resource invariant, after all threads have
terminated as result of the detection of an accepting cycle.
Auxiliary ghost state. As mentioned earlier, to prove that pndfs also preserves the (encodings of) Invariants 1.1 –1.6 and 4.1 –4.2 after every computation step, additional ghost state needs to be maintained. In particular, we need
to make explicit that every worker tid with Pink tid = ∅ is doing a dfsred search
that was started from some root state a ∈ A ∩ Pink tid . In addition, the proof of
Lemma 3 needs that there exists an (s, a)-path for every s ∈ Cyan tid . To prove
the preservation of Lemma 4 we also need that, if worker tid is not yet executing
the await instruction, we have that a ∈ Red , and otherwise that Pink tid = {a}.
This extra information is encoded in the loop invariant on lines 20–27 (Figure 4), via three ghost arrays, named exploringred , redroot and waiting. Firstly,
exploringred administrates which workers are doing a red search. For verification
purposes we added ghost code to the program, to set exploringred [tid ] to true
whenever dfsred(a, tid ) is invoked by worker tid from a blue search, and back
to false whenever dfsred(a, tid ) returns. Secondly, redroot stores the root state
on which dfsred was invoked. Finally, waiting administrates which workers are
executing an await instruction. These three ghost arrays together are closely related to the s.count fields in the program of Figure 2, via the following invariant:
∀s : s.count = |{tid | exploringred [tid ] ∧ redroot [tid ] = s ∧ ¬waiting[tid ]}|.
Establishing that pndfs adheres to the invariants in Lemmas 1 and 4 was
highly non-trivial and required various complex auxiliary lemmas to be encoded
and proven. These are all encoded in VerCors as ghost methods: side-effect-free
helper methods on which the lemma is encoded in the method’s contract [21,22].
Induction proofs, for example, are encoded using either loop invariants or recursion. Application of a lemma then translates to a function call on the specification
level. The proofs in Section 3.1 are all encoded and applied in this way.