Model Checking of Linearizability of Concurrent List Implementations Conference Paper


Author(s): Cerný, Pavol; Radhakrishna, Arjun; Zufferey, Damien; Chaudhuri, Swarat; Alur, Rajeev
Editor(s): Touili, Tayssir; Cook, Byron; Jackson, Paul
Title: Model Checking of Linearizability of Concurrent List Implementations
Title Series: LNCS
Affiliation IST Austria
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 technique can be used to verify optimistic implementations with the help of programmer annotations. We developed a verification tool CoLT and evaluated it on a representative sample of Java implementations of the concurrent set data structure. The tool verified linearizability of a number of implementations, found a known error in a lock-free implementation and proved that the corrected version is linearizable.
Keywords: model checking; linearizability
Conference Title: CAV: Computer Aided Verification
Volume: 6174
Conference Dates: July 15-19, 2010
Conference Location: Edinburgh, UK
Publisher: Springer  
Date Published: 2010-01-01
Start Page: 465
End Page: 479
Sponsor: This research was partially supported by NSF grants CCF 0905464 and CAREER Award 0953507 and by the Gigascale Systems Research Center.
URL:
DOI: 10.1007/978-3-642-14295-6_41
Open access: yes (repository)
IST Austria Authors
  1. Pavol Černý
    25 Cerný
Related IST Austria Work