Automated Verification of Parallel Nested DFS
257
the assignment, which are otherwise protected by the resource invariant declared
on line 11 (Fig. 3). The exact definition of resource invariant is deferred to
§3.3, and the type resource is the type of separation logic assertions. Moreover,
the await instruction on line 23 (Fig. 2) is implemented as a busy while-loop
that only stops when s.count = 0, which is checked atomically in every iteration.
Termination handling. The pseudocode in Figure 2 uses an “exit all” command to terminate all threads when an accepting cycle has been found. However,
this mechanism was left implicit. Our formalisation in VerCors makes the termination system explicit: it consists primarily of a global abort flag that is declared
on line 9 in Figure 3. All workers regularly poll this flag to determine whether
they continue or not. The abort flag is set to true by the main thread—the thread
that started pndfs and spawned all worker threads on line 11 of Fig. 2—as soon
as one of the workers returns with an accepting cycle.
3.3 Verification of pndfs in VerCors
One major challenge of concurrency verification is finding a proper distribution
of shared-memory ownership, that allows proving memory safety as well as any
functional properties of interest. This section starts by discussing how we distribute the ownership of the input automaton over threads and the resource
invariant, in such a way that Invariants 1.1 –1.6 and 4.1 –4.2 can be encoded.
To prove the preservation of these invariants after every computation step,
auxiliary bookkeeping is needed on the specification level. For example, to mechanise the proof of Lemmas 3 and 4 we need to make explicit that all workers
tid with Pink tid = ∅ are doing a red search that was started from some root
state a ∈ A ∩ Pink tid . This auxiliary bookkeeping is maintained in the resource
invariant, via auxiliary ghost state, which is explained later. Finally, we give the
fully annotated version of pndfs and explain how completeness is proven from
Lemma 4, by applying the VerCors encoding of Theorem 1.
Ownership distribution. We start by explaining how the ownership of the
automaton encoding (lines 2–8 in Fig. 3) is distributed among workers and the
resource invariant. First observe that all colouring invariants express global properties that span over (i ) the shared red colourings, as well as (ii ) the local configurations color [tid ] and pink [tid ] of every worker tid . To define the ownership
distribution for (i ), observe that the only way to distribute the access rights to
red to enable all threads to regain write access, is to let the resource invariant
protect full ownership of red . The resource invariant therefore fully captures the
properties about red states expressed in Lemmas 1 and 4. However, to be able
to specify that, it also requires partial ownership of all thread-local colourings.
Figure 4 presents the full resource invariant, that includes: access rights to
both global and thread-local colourings on lines 2–4; the encoding of Lemma 1 on
lines 10–17 and 22; and the encoding of Lemma 4 on lines 30–32. In addition, the
resource invariant holds partial ownership of the abort flag on line 8, to ensure
that global termination is only announced when an accepting cycle is found.
257
the assignment, which are otherwise protected by the resource invariant declared
on line 11 (Fig. 3). The exact definition of resource invariant is deferred to
§3.3, and the type resource is the type of separation logic assertions. Moreover,
the await instruction on line 23 (Fig. 2) is implemented as a busy while-loop
that only stops when s.count = 0, which is checked atomically in every iteration.
Termination handling. The pseudocode in Figure 2 uses an “exit all” command to terminate all threads when an accepting cycle has been found. However,
this mechanism was left implicit. Our formalisation in VerCors makes the termination system explicit: it consists primarily of a global abort flag that is declared
on line 9 in Figure 3. All workers regularly poll this flag to determine whether
they continue or not. The abort flag is set to true by the main thread—the thread
that started pndfs and spawned all worker threads on line 11 of Fig. 2—as soon
as one of the workers returns with an accepting cycle.
3.3 Verification of pndfs in VerCors
One major challenge of concurrency verification is finding a proper distribution
of shared-memory ownership, that allows proving memory safety as well as any
functional properties of interest. This section starts by discussing how we distribute the ownership of the input automaton over threads and the resource
invariant, in such a way that Invariants 1.1 –1.6 and 4.1 –4.2 can be encoded.
To prove the preservation of these invariants after every computation step,
auxiliary bookkeeping is needed on the specification level. For example, to mechanise the proof of Lemmas 3 and 4 we need to make explicit that all workers
tid with Pink tid = ∅ are doing a red search that was started from some root
state a ∈ A ∩ Pink tid . This auxiliary bookkeeping is maintained in the resource
invariant, via auxiliary ghost state, which is explained later. Finally, we give the
fully annotated version of pndfs and explain how completeness is proven from
Lemma 4, by applying the VerCors encoding of Theorem 1.
Ownership distribution. We start by explaining how the ownership of the
automaton encoding (lines 2–8 in Fig. 3) is distributed among workers and the
resource invariant. First observe that all colouring invariants express global properties that span over (i ) the shared red colourings, as well as (ii ) the local configurations color [tid ] and pink [tid ] of every worker tid . To define the ownership
distribution for (i ), observe that the only way to distribute the access rights to
red to enable all threads to regain write access, is to let the resource invariant
protect full ownership of red . The resource invariant therefore fully captures the
properties about red states expressed in Lemmas 1 and 4. However, to be able
to specify that, it also requires partial ownership of all thread-local colourings.
Figure 4 presents the full resource invariant, that includes: access rights to
both global and thread-local colourings on lines 2–4; the encoding of Lemma 1 on
lines 10–17 and 22; and the encoding of Lemma 4 on lines 30–32. In addition, the
resource invariant holds partial ownership of the abort flag on line 8, to ensure
that global termination is only announced when an accepting cycle is found.