early (lines 8–10). This optimisation is important, since it allows the global red
colour to spread even in portions of the graph that are not under an accepting
state, thereby allowing more pruning. However, this optimisation only preserves
the invariants if we wait until s.count = 0 (on line 9). This test was erroneously
omitted in [25]
7 . Fortunately, the version in Figure 7b is correct, which has now
been checked in VerCors in a straightforward manner.
5 Conclusion
This paper presents the first automated deductive verification of a parallel graph
algorithm: we verified soundness and completeness of parallel nested depth-first
search using VerCors. We also show that this mechanisation is helpful in quickly
discovering whether optimisations of the algorithm preserve its correctness.
Many of the presented verification techniques, e.g., the use of separate contracts for single statements, the way we handle termination, and the construction
of explicit witnesses through ghost variables, will be useful for the verification of
other similar algorithms. Moreover, our encoding of parallel nested DFS closely
resembles the implementation of such an algorithm in mainstream programming
languages like C++ and Java. It would be interesting to investigate how our
VerCors encoding can be automatically deployed on multi-core architectures,
for example to enable comparing its performance and scalability with LTSmin.
There are many possibilities to extend the line of research on the verification of parallel model checking algorithms initiated in this paper. First, one may
consider to extend the scope of this verification closer towards the actual efficient C-implementation in LTSmin. This would involve verifying the underlying
concurrent hash table to store visited states (a simplified version of which has
been verified before with VerCors [1]), the encoding of the colours as “bits” in
the hash table buckets, and the use of CAS to manipulate these bits.
One might consider alternative parallel NDFS versions, notably [15], which
shares the blue colour, invoking a repair procedure when the depth-first order is
violated. Both algorithms have been reconciled in [14], sharing both blue and red.
This work could be extended to a wealth of other optimisations like partial-order
reduction, or other parallel model checking algorithms, for example [26,4,40].
Our work can be considered as a first step towards a library for the verification
of graph-based (multi-core) model checking algorithms. It will be an interesting
line of future work to continue this: developing a full-fledged verification library
for common subtasks, like graph manipulations and termination detection.
Acknowledgments and data availability statement. This work is partially
supported by the NWO VICI 639.023.710 Mercedes project and by the NWO
TOP 612.001.403 VerDi project. The datasets for this case study are available
at: https://doi.org/10.4121/uuid:36c00955-5574-44d9-9b26-340f7a1ea03b.
7 Wan Fokkink and his students Stefan Vijzelaar and Pieter Hijma already found in
2012 that the “all-red” extension required an extra check ’await s.count = 0’ in [25],
and wondered whether ’await s.count ≤ 1’ would be sufficient. Independently, Akos
Hajdu reported this omission in 2015.
262
W. Oortwijn et al.
colour to spread even in portions of the graph that are not under an accepting
state, thereby allowing more pruning. However, this optimisation only preserves
the invariants if we wait until s.count = 0 (on line 9). This test was erroneously
omitted in [25]
7 . Fortunately, the version in Figure 7b is correct, which has now
been checked in VerCors in a straightforward manner.
5 Conclusion
This paper presents the first automated deductive verification of a parallel graph
algorithm: we verified soundness and completeness of parallel nested depth-first
search using VerCors. We also show that this mechanisation is helpful in quickly
discovering whether optimisations of the algorithm preserve its correctness.
Many of the presented verification techniques, e.g., the use of separate contracts for single statements, the way we handle termination, and the construction
of explicit witnesses through ghost variables, will be useful for the verification of
other similar algorithms. Moreover, our encoding of parallel nested DFS closely
resembles the implementation of such an algorithm in mainstream programming
languages like C++ and Java. It would be interesting to investigate how our
VerCors encoding can be automatically deployed on multi-core architectures,
for example to enable comparing its performance and scalability with LTSmin.
There are many possibilities to extend the line of research on the verification of parallel model checking algorithms initiated in this paper. First, one may
consider to extend the scope of this verification closer towards the actual efficient C-implementation in LTSmin. This would involve verifying the underlying
concurrent hash table to store visited states (a simplified version of which has
been verified before with VerCors [1]), the encoding of the colours as “bits” in
the hash table buckets, and the use of CAS to manipulate these bits.
One might consider alternative parallel NDFS versions, notably [15], which
shares the blue colour, invoking a repair procedure when the depth-first order is
violated. Both algorithms have been reconciled in [14], sharing both blue and red.
This work could be extended to a wealth of other optimisations like partial-order
reduction, or other parallel model checking algorithms, for example [26,4,40].
Our work can be considered as a first step towards a library for the verification
of graph-based (multi-core) model checking algorithms. It will be an interesting
line of future work to continue this: developing a full-fledged verification library
for common subtasks, like graph manipulations and termination detection.
Acknowledgments and data availability statement. This work is partially
supported by the NWO VICI 639.023.710 Mercedes project and by the NWO
TOP 612.001.403 VerDi project. The datasets for this case study are available
at: https://doi.org/10.4121/uuid:36c00955-5574-44d9-9b26-340f7a1ea03b.
7 Wan Fokkink and his students Stefan Vijzelaar and Pieter Hijma already found in
2012 that the “all-red” extension required an extra check ’await s.count = 0’ in [25],
and wondered whether ’await s.count ≤ 1’ would be sufficient. Independently, Akos
Hajdu reported this omission in 2015.
262
W. Oortwijn et al.