2013 | OriginalPaper | Buchkapitel
SPIN as a Linearizability Checker under Weak Memory Models
verfasst von : Oleg Travkin, Annika Mütze, Heike Wehrheim
Erschienen in: Hardware and Software: Verification and Testing
Verlag: Springer International Publishing
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
Linearizability is the key correctness criterion for concurrent data structures like stacks, queues or sets. Consequently, much effort has been spent on developing techniques for showing linearizability. However, most of these approaches assume a sequentially consistent memory model whereas today’s multicore processors provide relaxed out-of-order execution semantics.
In this paper, we present a new approach for checking linearizability of concurrent algorithms under weak memory models, in particular the TSO memory model. Our technique first compiles the algorithm into intermediate low-level code. For achieving the out-of-order execution, we (abstractly) model the processor’s architecture with shared memory and local buffers. Low-level code as well as architecture model are given as input to the model checker SPIN which checks whether the out-of-order execution of the particular algorithm is linearizable. We report on experiments with different algorithms.