Proving Concurrent Data Structures Linearizable

Vineet Singh, Iulian Neamtiu, Rajiv Gupta

Research output: Chapter in Book/Report/Conference proceedingConference contribution

4 Scopus citations

Abstract

Linearizability of concurrent data structure implementationsis notoriously hard to prove. Consequently, currentverification techniques can only prove linearizability for certainclasses of data structures. We introduce a generic, sound, andpractical technique to statically check the linearizability of concurrentdata structure implementations. Our technique involvesspecifying the concurrent operations as a list of sub-operationsand passing this specification on to an automated checker thatverifies linearizability using relationships between individual sub-operations. We have proven the soundness of our technique. Ourapproach is expressive: we have successfully verified the linearizabilityof 12 popular concurrent data structure implementationsincluding algorithms that are considered to be challenging toprove linearizable such as elimination back-off stack, lazy linkedlist, and time-stamped stack. Our checker is effective, as it canverify the specifications in less than a second.

Original languageEnglish (US)
Title of host publicationProceedings - 2016 IEEE 27th International Symposium on Software Reliability Engineering, ISSRE 2016
PublisherIEEE Computer Society
Pages230-240
Number of pages11
ISBN (Electronic)9781467390019
DOIs
StatePublished - Dec 5 2016
Event27th IEEE International Symposium on Software Reliability Engineering, ISSRE 2016 - Ottawa, United States
Duration: Oct 23 2016Oct 27 2016

Publication series

NameProceedings - International Symposium on Software Reliability Engineering, ISSRE
ISSN (Print)1071-9458

Other

Other27th IEEE International Symposium on Software Reliability Engineering, ISSRE 2016
Country/TerritoryUnited States
CityOttawa
Period10/23/1610/27/16

All Science Journal Classification (ASJC) codes

  • Software
  • Safety, Risk, Reliability and Quality

Keywords

  • Linearizability
  • concurrent data structures
  • verification

Fingerprint

Dive into the research topics of 'Proving Concurrent Data Structures Linearizable'. Together they form a unique fingerprint.

Cite this