Article

Proving Linearizability Using Partial Orders

Authors:

Alexey Gotsman,

Matthew ParkinsonAuthors Info & Claims

Programming Languages and Systems: 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22–29, 2017, Proceedings

Pages 639 - 667

https://doi.org/10.1007/978-3-662-54434-1_24

Published: 25 April 2017 Publication History

Abstract

Linearizability is the commonly accepted notion of correctness for concurrent data structures. It requires that any execution of the data structure is justified by a linearization—a linear order on operations satisfying the data structure’s sequential specification. Proving linearizability is often challenging because an operation’s position in the linearization order may depend on future operations. This makes it very difficult to incrementally construct the linearization in a proof.

We propose a new proof method that can handle data structures with such future-dependent linearizations. Our key idea is to incrementally construct not a single linear order of operations, but a partial order that describes multiple linearizations satisfying the sequential specification. This allows decisions about the ordering of operations to be delayed, mirroring the behaviour of data structure implementations. We formalise our method as a program logic based on rely-guarantee reasoning, and demonstrate its effectiveness by verifying several challenging data structures: the Herlihy-Wing queue, the TS queue and the Optimistic set.

References

[1]

Dinsdale-Young T, Dodds M, Gardner P, Parkinson MJ, and Vafeiadis V D’Hondt T Concurrent abstract predicates ECOOP 2010 – Object-Oriented Programming 2010 Heidelberg Springer 504-528

[2]

Dodds, M., Haas, A., Kirsch, C.M.: A scalable, correct time-stamped stack. In: POPL (2015)

[3]

Dongol, B., Derrick, J.: Verifying linearizability: a comparative survey. arXiv CoRR, 1410.6268 (2014)

[4]

Filipovic I, O’Hearn PW, Rinetzky N, and Yang H Abstraction for concurrent objects Theor. Comput. Sci. 2010 411 51–52 4379-4398

[5]

Fishburn PC Intransitive indifference with unequal indifference intervals J. Math. Psychol. 1970 7 144-149

[6]

Gotsman A and Yang H Koutny M and Ulidowski I Linearizability with ownership transfer CONCUR 2012 – Concurrency Theory 2012 Heidelberg Springer 256-271

[7]

Haas, A.: Fast concurrent data structures through timestamping. Ph.D. thesis, University of Salzburg (2015)

[8]

Heller S, Herlihy M, Luchangco V, Moir M, Scherer WN, and Shavit N Anderson JH, Prencipe G, and Wattenhofer R A lazy concurrent list-based set algorithm Principles of Distributed Systems 2006 Heidelberg Springer 3-16

[9]

Hemed N, Rinetzky N, and Vafeiadis V Moses Y Modular verification of concurrency-aware linearizability Distributed Computing 2015 Heidelberg Springer 371-387

[10]

Henzinger TA, Sezgin A, and Vafeiadis V D’Argenio PR and Melgratti H Aspect-oriented linearizability proofs CONCUR 2013 – Concurrency Theory 2013 Heidelberg Springer 242-256

[11]

Herlihy, M., Wing, J.M.: Linearizability: a correctness condition for concurrent objects. In: ACM TOPLAS (1990)

[12]

Hoffman M, Shalev O, and Shavit N Tovar E, Tsigas P, and Fouchal H The baskets queue Principles of Distributed Systems 2007 Heidelberg Springer 401-414

[13]

Jones, C.B.: Specification and design of (parallel) programs. In: IFIP Congress (1983)

[14]

Khyzha, A., Dodds, M., Gotsman, A., Parkinson, M.: Proving linearizability using partial orders (extended version). arXiv CoRR, 1701.05463 (2017)

[15]

Liang, H., Feng, X.: Modular verification of linearizability with non-fixed linearization points. In: PLDI (2013)

[16]

Morrison, A., Afek, Y.: Fast concurrent queues for x86 processors. In: PPoPP (2013)

[17]

O’Hearn, P.W., Rinetzky, N., Vechev, M.T., Yahav, E., Yorsh, G.: Verifying linearizability with hindsight. In: PODC (2010)

[18]

Owicki SS and Gries D An axiomatic proof technique for parallel programs I Acta Informatica 1976 6 319-340

[19]

Schellhorn G, Derrick J, and Wehrheim H A sound and complete proof technique for linearizability of concurrent data structures ACM TOCL 2014 15 4 31

[20]

Turon, A., Dreyer, D., Birkedal, L.: Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency. In: ICFP (2013)

[21]

Turon, A.J., Thamsborg, J., Ahmed, A., Birkedal, L., Dreyer, D.: Logical relations for fine-grained concurrency. In: POPL (2013)

[22]

Vafeiadis, V.: Modular fine-grained concurrency verification. Ph.D. thesis, University of Cambridge, UK (2008). Technical report UCAM-CL-TR-726

Cited By

Oliveira Vale AWang ZChen YYou PShao Z(2024)Compositionality and Observational Refinement for Linearizability with CrashesProceedings of the ACM on Programming Languages10.1145/36897928:OOPSLA2(2296-2324)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689792
Jayanti PJayanti SYavuz UHernandez LDhulipala LSun Y(2024)Meta-Configuration Tracking for Machine-Certified Correctness of Concurrent Data Structures (Abstract)Proceedings of the 2024 ACM Workshop on Highlights of Parallel Computing10.1145/3670684.3673406(21-22)Online publication date: 17-Jun-2024
https://dl.acm.org/doi/10.1145/3670684.3673406
Oliveira Vale AShao ZChen Y(2024)A Compositional Theory of LinearizabilityJournal of the ACM10.1145/364366871:2(1-107)Online publication date: 27-Jan-2024
https://dl.acm.org/doi/10.1145/3643668
Show More Cited By

Index Terms

Proving Linearizability Using Partial Orders

Index terms have been assigned to the content through auto-classification.

Recommendations

Linearizability: a correctness condition for concurrent objects

A concurrent object is a data object shared by concurrent processes. Linearizability is a correctness condition for concurrent objects that exploits the semantics of abstract data types. It permits a high degree of concurrency, yet it permits programmers ...
Proving linearizability via non-atomic refinement
IFM'07: Proceedings of the 6th international conference on Integrated formal methods

Linearizability is a correctness criterion for concurrent objects. In this paper, we prove linearizability of a concurrent lock-free stack implementation by showing the implementation to be a nonatomic refinement of an abstract stack. To this end, we ...
Using refinement calculus techniques to prove linearizability
Abstract
Stepwise refinement is a method for systematically transforming a high-level program into an efficiently executable one. A sequence of successively refined programs can also serve as a correctness proof, which makes different mechanisms in the ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

Programming Languages and Systems: 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22–29, 2017, Proceedings

Apr 2017

1005 pages

ISBN:978-3-662-54433-4

DOI:10.1007/978-3-662-54434-1

Editor:
Hongseok Yang
Department of Computer Science, University of Oxford, Oxford, UK

© Springer-Verlag GmbH Germany 2017.

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 25 April 2017

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

11
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 12 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Oliveira Vale AWang ZChen YYou PShao Z(2024)Compositionality and Observational Refinement for Linearizability with CrashesProceedings of the ACM on Programming Languages10.1145/36897928:OOPSLA2(2296-2324)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689792
Jayanti PJayanti SYavuz UHernandez LDhulipala LSun Y(2024)Meta-Configuration Tracking for Machine-Certified Correctness of Concurrent Data Structures (Abstract)Proceedings of the 2024 ACM Workshop on Highlights of Parallel Computing10.1145/3670684.3673406(21-22)Online publication date: 17-Jun-2024
https://dl.acm.org/doi/10.1145/3670684.3673406
Oliveira Vale AShao ZChen Y(2024)A Compositional Theory of LinearizabilityJournal of the ACM10.1145/364366871:2(1-107)Online publication date: 27-Jan-2024
https://dl.acm.org/doi/10.1145/3643668
Oliveira Vale AShao ZChen Y(2023)A Compositional Theory of LinearizabilityProceedings of the ACM on Programming Languages10.1145/35712317:POPL(1089-1120)Online publication date: 9-Jan-2023
https://dl.acm.org/doi/10.1145/3571231
Dang HJung JChoi JNguyen DMansky WKang JDreyer DJhala RDillig I(2022)Compass: strong and compositional library specifications in relaxed memory separation logicProceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3519939.3523451(792-808)Online publication date: 9-Jun-2022
https://dl.acm.org/doi/10.1145/3519939.3523451
Patel NKrishna SShasha DWies T(2021)Verifying concurrent multicopy search structuresProceedings of the ACM on Programming Languages10.1145/34854905:OOPSLA(1-32)Online publication date: 15-Oct-2021
https://dl.acm.org/doi/10.1145/3485490
Krishna SPatel NShasha DWies TDonaldson ATorlak E(2020)Verifying concurrent search structure templatesProceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3385412.3386029(181-196)Online publication date: 11-Jun-2020
https://dl.acm.org/doi/10.1145/3385412.3386029
Nanevski ABanerjee ADelbianco GFábregas I(2019)Specifying concurrent programs in separation logic: morphisms and simulationsProceedings of the ACM on Programming Languages10.1145/33605873:OOPSLA(1-30)Online publication date: 10-Oct-2019
https://dl.acm.org/doi/10.1145/3360587
Zou MDing HDu DFu MGu RChen HBrecht TWilliamson C(2019)Using concurrent relational logic with helpers for verifying the AtomFS file systemProceedings of the 27th ACM Symposium on Operating Systems Principles10.1145/3341301.3359644(259-274)Online publication date: 27-Oct-2019
https://dl.acm.org/doi/10.1145/3341301.3359644
Meyer RWolff S(2019)Decoupling lock-free data structures from memory reclamation for static analysisProceedings of the ACM on Programming Languages10.1145/32903713:POPL(1-31)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1145/3290371
Show More Cited By

View Options

View options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents