Sciweavers

Share
CAV
2006
Springer

Formal Verification of a Lazy Concurrent List-Based Set Algorithm

9 years 11 months ago
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.
Robert Colvin, Lindsay Groves, Victor Luchangco, M
Added 20 Aug 2010
Updated 20 Aug 2010
Type Conference
Year 2006
Where CAV
Authors Robert Colvin, Lindsay Groves, Victor Luchangco, Mark Moir
Comments (0)
books