Proof Methodologies for Concurrent Algorithms

This is a joint project between Victoria University of Wellington and Sun Microsystems.

The chief protagonists are Lindsay Groves (VUW) and Mark Moir (Sun).

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)

Publications

• We recently verified the lazy list 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)