Anzeige
Erschienen in:
2006 | OriginalPaper | Buchkapitel
Formal Verification of a Lazy Concurrent List-Based Set Algorithm
verfasst von : Robert Colvin, Lindsay Groves, Victor Luchangco, Mark Moir
Erschienen in: Computer Aided Verification
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.