Automated Verification of Parallel Nested DFS
249
be checked independently, also in case the property holds. Recently, an IC3style symbolic LTL model checker has been extended with deductive proofs as
well [16]. However, these approaches do not prove correctness of the model checking algorithm, but only validate its outcome for each specific use.
Alternatively, one can formalise the model checking algorithm and its correctness proof in an interactive theorem prover. An early example of this approach
was the verification of a model checker for the modal μ-calculus in Coq [43]. A
framework for verifying sequential depth-first search algorithms was developed
in Isabelle [27,28], and applied to the verification of NDFS with partial order
reduction [9] as well as a model checker for timed automata [47]. The recent
formalisations of Tarjan’s SCC algorithm [10] fit in the same line of research.
These approaches require to model and verify the algorithm in an interactive
theorem prover, allowing one to use the full power of the theorem prover.
If one wishes to verify the code of the algorithm directly, yet another approach is to model the algorithm and its specification in a (semi-)automated
program verifier, where the code is enriched with sufficient annotations to prove
its correctness. This approach was followed for several standard sequential graph
algorithms in Why3 [46] and for sequential NDFS in Dafny [37]. However, there
is hardly any work on automated verification of parallel graph algorithms. Raad
et al. [38] verified four concurrent graph algorithms in the context of CoLoSL,
but the proofs have not been automated. Sergey et al. [42] verified a concurrent
spanning tree algorithm, but interactively, through an embedding in Coq.
To support the verification of shared-memory parallel software, program verifiers typically use concurrent separation logic. VeriFast [20] aims at sequential
and multi-threaded C and Java programs. VerCors [6] verifies concurrent programs in Java and OpenCL, by applying a correctness-preserving translation into
a sequential imperative language, delegating the generation of the verification
conditions to Viper [32] and their verification ultimately to Z3 [31].
1.3 Contributions and Outline
This paper discusses the mechanical verification of the parallel NDFS algorithm
of Laarman et al. [25] using VerCors. To the best of our knowledge, this is the
first mechanical verification of a parallel graph (and model checking) algorithm.
Section 2 recalls both sequential and parallel NDFS (§2.1–2.2), and gives preliminaries on concurrency verification with VerCors (§2.3). It also explains that
parallel NDFS uses various colour markings on the input graph to administer
the status of the nested searches of workers. Some of these colours are local to a
single worker, while other colours are globally shared among all workers.
Section 3.1 presents our new (informal) correctness proof of parallel NDFS,
that is based on a number of global invariants on the possible colour configurations. The main challenge lies in proving completeness, which is particularly
difficult since workers can delegate the detection of accepting cycles to other
workers. To be able to mechanise our completeness proof, we contribute a new
invariant (Lemma 4) that guarantees the preservation of so-called special paths.
This allows to circumvent using the complicated inductive argument used by [25].
249
be checked independently, also in case the property holds. Recently, an IC3style symbolic LTL model checker has been extended with deductive proofs as
well [16]. However, these approaches do not prove correctness of the model checking algorithm, but only validate its outcome for each specific use.
Alternatively, one can formalise the model checking algorithm and its correctness proof in an interactive theorem prover. An early example of this approach
was the verification of a model checker for the modal μ-calculus in Coq [43]. A
framework for verifying sequential depth-first search algorithms was developed
in Isabelle [27,28], and applied to the verification of NDFS with partial order
reduction [9] as well as a model checker for timed automata [47]. The recent
formalisations of Tarjan’s SCC algorithm [10] fit in the same line of research.
These approaches require to model and verify the algorithm in an interactive
theorem prover, allowing one to use the full power of the theorem prover.
If one wishes to verify the code of the algorithm directly, yet another approach is to model the algorithm and its specification in a (semi-)automated
program verifier, where the code is enriched with sufficient annotations to prove
its correctness. This approach was followed for several standard sequential graph
algorithms in Why3 [46] and for sequential NDFS in Dafny [37]. However, there
is hardly any work on automated verification of parallel graph algorithms. Raad
et al. [38] verified four concurrent graph algorithms in the context of CoLoSL,
but the proofs have not been automated. Sergey et al. [42] verified a concurrent
spanning tree algorithm, but interactively, through an embedding in Coq.
To support the verification of shared-memory parallel software, program verifiers typically use concurrent separation logic. VeriFast [20] aims at sequential
and multi-threaded C and Java programs. VerCors [6] verifies concurrent programs in Java and OpenCL, by applying a correctness-preserving translation into
a sequential imperative language, delegating the generation of the verification
conditions to Viper [32] and their verification ultimately to Z3 [31].
1.3 Contributions and Outline
This paper discusses the mechanical verification of the parallel NDFS algorithm
of Laarman et al. [25] using VerCors. To the best of our knowledge, this is the
first mechanical verification of a parallel graph (and model checking) algorithm.
Section 2 recalls both sequential and parallel NDFS (§2.1–2.2), and gives preliminaries on concurrency verification with VerCors (§2.3). It also explains that
parallel NDFS uses various colour markings on the input graph to administer
the status of the nested searches of workers. Some of these colours are local to a
single worker, while other colours are globally shared among all workers.
Section 3.1 presents our new (informal) correctness proof of parallel NDFS,
that is based on a number of global invariants on the possible colour configurations. The main challenge lies in proving completeness, which is particularly
difficult since workers can delegate the detection of accepting cycles to other
workers. To be able to mechanise our completeness proof, we contribute a new
invariant (Lemma 4) that guarantees the preservation of so-called special paths.
This allows to circumvent using the complicated inductive argument used by [25].