Sciweavers

Share
CAV
2010
Springer

Model Checking of Linearizability of Concurrent List Implementations

9 years 2 months ago
Model Checking of Linearizability of Concurrent List Implementations
Abstract. Concurrent data structures with fine-grained synchronization are notoriously difficult to implement correctly. The difficulty of reasoning about these implementations does not stem from the number of variables or the program size, but rather from the large number of possible interleavings. These implementations are therefore prime candidates for model checking. We introduce an algorithm for verifying linearizability of singly-linked heap-based concurrent data structures. We consider a model consisting of an unbounded heap where each vertex stores an element from an unbounded data domain, with a restricted set of operations for testing and updating pointers and data elements. Our main result is that linearizability is decidable for programs that invoke a fixed number of methods, possibly in parallel. This decidable fragment covers many of the common implementation techniques — fine-grained locking, lazy synchronization, and lock-free synchronization. We also show how the ...
Pavol Cerný, Arjun Radhakrishna, Damien Zuf
Added 15 Aug 2010
Updated 15 Aug 2010
Type Conference
Year 2010
Where CAV
Authors Pavol Cerný, Arjun Radhakrishna, Damien Zufferey, Swarat Chaudhuri, Rajeev Alur
Comments (0)
books