Automated Verification of Parallel Nested DFS
253
predicates can be split into disjoint parts and be combined as follows:
Perm(s, π 1 + π 2 ) ⇐⇒ Perm(s, π 1 ) ∗∗ Perm(s, π 2 )
A standard pattern in concurrency verification is to split and distribute the
ownership of all shared memory over threads and locks. Clarifying the latter; in
case multiple threads need to write to a common footprint of shared memory,
the ownerships to this footprint are typically protected by a resource invariant.
Threads can then only use the resources protected by this invariant when they
execute atomic instructions (i.e., when no other threads can interfere). For more
details we refer to the standard papers on concurrent separation logic [34,8,44].
3 Automated Verification of Parallel NDFS
This section elaborates on the verification of pndfs with VerCors [35]. Section 3.1
presents and discusses our new correctness argument for pndfs, which includes
the new invariant on the red colours and a proof of its correctness. Sections 3.2
and 3.3 discuss the mechanisation of this proof in VerCors.
3.1 Correctness of pndfs
The soundness proof of pndfs is not very different from the soundness argument
of sequential NDFS: every time report cycle is executed, a witness cycle can be
found. The main challenge lies in proving completeness, i.e., proving that if there
exists any accepting cycle, pndfs will report it. This is difficult since workers can
obstruct each other’s red searches and thereby prevent the detection of accepting
cycles. This section proposes a new key invariant and completeness proof that
is suitable for deductive verification.
We start by introducing a number of low-level invariants on the local configurations of colours that can arise during a run of pndfs. Let Cyan tid be the set of
cyan-coloured states {s ∈ S | s.color [tid ] = cyan} private to worker tid , and likewise for White tid , Blue tid and Pink tid . Moreover, let Red be the set of globally
red states, and succ(X) ∪ s∈X succ(s) the successor set of a given set X ⊆ S.
Lemma 1. pndfs maintains the following global invariants during execution:
1.1. ∀tid : succ(Blue tid ∪ Pink tid ) ⊆ Blue tid ∪ Cyan tid ∪ Red
1.2. succ(Red ) ⊆ Red ∪ ∪ tid (Pink tid \ Cyan tid )
1.3. ∀tid : A ∩ Blue tid ⊆ Red
1.4. ∀tid : A ∩ Pink tid ⊆ Cyan tid
1.5. ∀tid : Pink tid ⊆ Blue tid ∪ Cyan tid
1.6. ∀tid : |A ∩ Pink tid | ≤ 1
Proof. The proof basically checks their preservation by each line of the program.
Invariants 1.1 –1.5 are reused from [25], whereas 1.6 is new and needed for
the new completeness proof. Proving completeness amounts to proving that not
all reachable accepting cycles can be missed due to search space pruning. To help
proving this, we identify a new class of paths, which we call tid-special paths.
253
predicates can be split into disjoint parts and be combined as follows:
Perm(s, π 1 + π 2 ) ⇐⇒ Perm(s, π 1 ) ∗∗ Perm(s, π 2 )
A standard pattern in concurrency verification is to split and distribute the
ownership of all shared memory over threads and locks. Clarifying the latter; in
case multiple threads need to write to a common footprint of shared memory,
the ownerships to this footprint are typically protected by a resource invariant.
Threads can then only use the resources protected by this invariant when they
execute atomic instructions (i.e., when no other threads can interfere). For more
details we refer to the standard papers on concurrent separation logic [34,8,44].
3 Automated Verification of Parallel NDFS
This section elaborates on the verification of pndfs with VerCors [35]. Section 3.1
presents and discusses our new correctness argument for pndfs, which includes
the new invariant on the red colours and a proof of its correctness. Sections 3.2
and 3.3 discuss the mechanisation of this proof in VerCors.
3.1 Correctness of pndfs
The soundness proof of pndfs is not very different from the soundness argument
of sequential NDFS: every time report cycle is executed, a witness cycle can be
found. The main challenge lies in proving completeness, i.e., proving that if there
exists any accepting cycle, pndfs will report it. This is difficult since workers can
obstruct each other’s red searches and thereby prevent the detection of accepting
cycles. This section proposes a new key invariant and completeness proof that
is suitable for deductive verification.
We start by introducing a number of low-level invariants on the local configurations of colours that can arise during a run of pndfs. Let Cyan tid be the set of
cyan-coloured states {s ∈ S | s.color [tid ] = cyan} private to worker tid , and likewise for White tid , Blue tid and Pink tid . Moreover, let Red be the set of globally
red states, and succ(X) ∪ s∈X succ(s) the successor set of a given set X ⊆ S.
Lemma 1. pndfs maintains the following global invariants during execution:
1.1. ∀tid : succ(Blue tid ∪ Pink tid ) ⊆ Blue tid ∪ Cyan tid ∪ Red
1.2. succ(Red ) ⊆ Red ∪ ∪ tid (Pink tid \ Cyan tid )
1.3. ∀tid : A ∩ Blue tid ⊆ Red
1.4. ∀tid : A ∩ Pink tid ⊆ Cyan tid
1.5. ∀tid : Pink tid ⊆ Blue tid ∪ Cyan tid
1.6. ∀tid : |A ∩ Pink tid | ≤ 1
Proof. The proof basically checks their preservation by each line of the program.
Invariants 1.1 –1.5 are reused from [25], whereas 1.6 is new and needed for
the new completeness proof. Proving completeness amounts to proving that not
all reachable accepting cycles can be missed due to search space pruning. To help
proving this, we identify a new class of paths, which we call tid-special paths.