Proof Methodologies for Concurrent Algorithms
This is a joint project between
Victoria University of Wellington and
The chief protagonists are
Lindsay Groves (VUW)
Others who are, or have been, involved in the project are:
- Ray Nickson
- Simon Doherty
- Robert Colvin
- David Friggens
- Brijesh Dongol
- Keith Bauer
- Victor Luchangco (Sun)
We recently verified the
concurrent set implementation.
Our paper Formal Verification of a Lazy Concurrent List-Based Set
Algorithm, by Robert Colvin, Lindsay Groves, Victor Luchangco and Mark
Moir, was published in CAV 2006.
The PVS files for out verification can be found
here, or here in zipped form.
Here is Simon's MSc thesis,
"Modelling and Verifying Non-blocking Algoroithms that Use Dynamically
Allocated Memory", 2003.
Simon's attempt at mechnical verification uncovered a subtle bug in the "Snark" algorithm
for concurrent deques, and a proposed correction.
The corrected version has subsequently been fully verified, but the proof has
not as yet been published.
(Others to be added)