Portal de Periódicos da CAPES

Formal Verification of a Lazy Concurrent List-Based Set Algorithm

2006; Springer Science+Business Media; Linguagem: Inglês

10.1007/11817963_44

1611-3349

Robert J. Colvin, Lindsay Groves, Victor Luchangco, Mark Moir,

Logic, programming, and type systems

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 of an abstract set and the implementation. The automata and simulation proof obligations are specified and verified using PVS.