Advertisement
Published in:
2013 | OriginalPaper | Chapter
SPIN as a Linearizability Checker under Weak Memory Models
Authors : Oleg Travkin, Annika Mütze, Heike Wehrheim
Published in: Hardware and Software: Verification and Testing
Publisher: Springer International Publishing
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. 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.