TY - GEN
T1 - Proving Concurrent Data Structures Linearizable
AU - Singh, Vineet
AU - Neamtiu, Iulian
AU - Gupta, Rajiv
N1 - Funding Information:
This work was supported in part by National Science Foundation grants CCF-1149632 and CCF-1318103.
Publisher Copyright:
© 2016 IEEE.
PY - 2016/12/5
Y1 - 2016/12/5
N2 - 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.
AB - 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.
KW - Linearizability
KW - concurrent data structures
KW - verification
UR - http://www.scopus.com/inward/record.url?scp=85013288101&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85013288101&partnerID=8YFLogxK
U2 - 10.1109/ISSRE.2016.31
DO - 10.1109/ISSRE.2016.31
M3 - Conference contribution
AN - SCOPUS:85013288101
T3 - Proceedings - International Symposium on Software Reliability Engineering, ISSRE
SP - 230
EP - 240
BT - Proceedings - 2016 IEEE 27th International Symposium on Software Reliability Engineering, ISSRE 2016
PB - IEEE Computer Society
T2 - 27th IEEE International Symposium on Software Reliability Engineering, ISSRE 2016
Y2 - 23 October 2016 through 27 October 2016
ER -