Formal Verification of a Lazy Concurrent List-Based Set Algorithm

We describe a formal verification of a recent concurrent list-based set algorithm due to Heller et al. The algorithm is optimistic: the add and remove operations traverse the list without locking, and lock only the nodes affected by the operation; the contains operation uses no locks and is wait-free. These properties make the algorithm challenging to prove correct, much more so than simple coarse-grained locking algorithms. We have proved that the algorithm is linearisable, using simulation between input/output automata modelling the behaviour stract set and the implementation. The automata and simulation proof obligations are specified and verified using PVS.

• Type: Conference
• Year: 2006
• Where: CAV
• Authors: Robert Colvin, Lindsay Groves, Victor Luchangco, Mark Moir
• Keywords: Algorithm, CAV 2006, Hardware, List-based Set Algorithm, Simple Coarse-grained Locking