and parallel programs. The presented verification is inspired by a previous mechanical verification of sequential NDFS [37] that was carried out in Dafny [30].
This paper demonstrates the feasibility of mechanical program verification of
parallel graph algorithms, like multi-core NDFS. To the best of our knowledge
we present the first mechanical verification of a parallel graph algorithm. Our
formalisation provides reusable components that can be used to verify variations
of parallel NDFS, as well as other algorithms for parallel model checking.
Before listing our contributions (§1.3) we first provide more background on
model checking algorithms (§1.1) and related work on their verification (§1.2).
1.1 Background on Model Checking
Pnueli introduced the Linear-time Temporal Logic (LTL) [36] to specify properties of reactive systems. The model checking problem [12] decides whether a transition system satisfies a given LTL property. The automata-based approach [45]
reduces the model checking problem to the graph-theoretic problem of checking
the reachability of accepting cycles. Reachability of accepting cycles in directed
graphs can be checked in linear time, with the nested depth-first search (NDFS)
algorithm [13,19,41], which forms the basis of the Spin model checker [17].
Several distributed and parallel model checking algorithms have been proposed, to allocate more memory and processors to the problem [2]. NDFS is
based on depth-first search, which is considered hard (impossible) to parallelise
efficiently [39]. For distributed approaches, the best strategy is to turn to BFS algorithms [3], which are straightforward to parallelise but at the cost of increasing
the amount of work beyond linear time. For the shared-memory setting, swarm
verification was proposed [18], where each worker runs its own instance of NDFS.
Various DFS-based multi-core algorithms for full LTL model checking have been
devised for this strategy [14,15,25]. This paper considers the version by Laarman
et al. [25], which is a parallel version of improved sequential NDFS [41].
The correctness of parallel NDFS is quite subtle. In particular, parallel DFS
does not fully respect a global depth-first ordering, since each worker maintains
its own search stack, yet the correctness of NDFS depends on the search order.
Also, to realise speedups, the implementation avoids locking shared data structures by using atomics. This raises the question whether the implementation of
a parallel model checker, meant to verify the correctness of safety-critical systems, is itself correct. For this reason the original paper [25] contains a detailed
pen-and-paper correctness proof, which is based on a number of invariants.
1.2 Related Work
To raise the level of confidence in model checkers, one approach is to certify each
of their individual runs. Obviously, the counterexample returned by a model
checker is itself a certificate that can easily be verified independently. However,
double-checking the absence of errors is harder. Namjoshi [33] proposed to instrument a μ-calculus model checker, to generate a deductive proof that can
248
W. Oortwijn et al.
This paper demonstrates the feasibility of mechanical program verification of
parallel graph algorithms, like multi-core NDFS. To the best of our knowledge
we present the first mechanical verification of a parallel graph algorithm. Our
formalisation provides reusable components that can be used to verify variations
of parallel NDFS, as well as other algorithms for parallel model checking.
Before listing our contributions (§1.3) we first provide more background on
model checking algorithms (§1.1) and related work on their verification (§1.2).
1.1 Background on Model Checking
Pnueli introduced the Linear-time Temporal Logic (LTL) [36] to specify properties of reactive systems. The model checking problem [12] decides whether a transition system satisfies a given LTL property. The automata-based approach [45]
reduces the model checking problem to the graph-theoretic problem of checking
the reachability of accepting cycles. Reachability of accepting cycles in directed
graphs can be checked in linear time, with the nested depth-first search (NDFS)
algorithm [13,19,41], which forms the basis of the Spin model checker [17].
Several distributed and parallel model checking algorithms have been proposed, to allocate more memory and processors to the problem [2]. NDFS is
based on depth-first search, which is considered hard (impossible) to parallelise
efficiently [39]. For distributed approaches, the best strategy is to turn to BFS algorithms [3], which are straightforward to parallelise but at the cost of increasing
the amount of work beyond linear time. For the shared-memory setting, swarm
verification was proposed [18], where each worker runs its own instance of NDFS.
Various DFS-based multi-core algorithms for full LTL model checking have been
devised for this strategy [14,15,25]. This paper considers the version by Laarman
et al. [25], which is a parallel version of improved sequential NDFS [41].
The correctness of parallel NDFS is quite subtle. In particular, parallel DFS
does not fully respect a global depth-first ordering, since each worker maintains
its own search stack, yet the correctness of NDFS depends on the search order.
Also, to realise speedups, the implementation avoids locking shared data structures by using atomics. This raises the question whether the implementation of
a parallel model checker, meant to verify the correctness of safety-critical systems, is itself correct. For this reason the original paper [25] contains a detailed
pen-and-paper correctness proof, which is based on a number of invariants.
1.2 Related Work
To raise the level of confidence in model checkers, one approach is to certify each
of their individual runs. Obviously, the counterexample returned by a model
checker is itself a certificate that can easily be verified independently. However,
double-checking the absence of errors is harder. Namjoshi [33] proposed to instrument a μ-calculus model checker, to generate a deductive proof that can
248
W. Oortwijn et al.