More Web Proxy on the site http://driver.im/

research-article

Open access

Mechanically verified proof obligations for linearizability

Authors:

Gerhard Schellhorn,

Heike WehrheimAuthors Info & Claims

ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 33, Issue 1

Article No.: 4, Pages 1 - 43

https://doi.org/10.1145/1889997.1890001

Published: 25 January 2011 Publication History

Abstract

Concurrent objects are inherently complex to verify. In the late 80s and early 90s, Herlihy and Wing proposed linearizability as a correctness condition for concurrent objects, which, once proven, allows us to reason about concurrent objects using pre- and postconditions only. A concurrent object is linearizable if all of its operations appear to take effect instantaneously some time between their invocation and return.

In this article we define simulation-based proof conditions for linearizability and apply them to two concurrent implementations, a lock-free stack and a set with lock-coupling. Similar to other approaches, we employ a theorem prover (here, KIV) to mechanize our proofs. Contrary to other approaches, we also use the prover to mechanically check that our proof obligations actually guarantee linearizability. This check employs the original ideas of Herlihy and Wing of verifying linearizability via possibilities.

References

[1]

Abrial, I.-R. and Cansell, D. 2005. Formal construction of a non-blocking concurrent queue algorithm (a case study in atomicity). J. Univ. Comput. Sci. 11, 5, 744--770.

[2]

Amit, D., Rinetzky, N., Reps, T. W., Sagiv, M., and Yahav, E. 2007. Comparison under abstraction for verifying linearizability. In Proceedings of the International Conference on Computer Aided Verification. W. Damm and H. Hermanns, Eds. Lecture Notes in Computer Science, vol. 4590, Springer, 477--490.

Digital Library

[3]

Barden, R., Stepney, S., and Cooper, D. 1994. Z in Practice. BCS Practitioner Series. Prentice-Hall.

Digital Library

[4]

Barnett, M., Rustan, K., Leino, M., and Schulte, W. 2004. The Spec&num; programming system: An overview. In Proceedings of the International Conference on Construction and Analysis of Safe, Secure, and Interoperable Smart Devices. Lecture Notes in Computer Science, vol. 3362, Springer, 49--69.

Digital Library

[5]

Bäumler, S., Schellhorn, G., Tofan, B., and Reif, W. 2009. Proving linearizability with temporal logic. Form. Asp. Comput.

[6]

Bayer, R. and Schkolnick, M. 1977. Concurrency of operations on b-trees. Acta Inform. 9, 1--21.

Digital Library

[7]

Calcagno, C., Parkinson, M., and Vafeiadis, V. 2007. Modular safety checking for fine-grained concurrency. In Proceedings of the International Static Analysis Symposium. Lecture Notes in Computer Science, vol. 4634, Springer, 233--238.

Digital Library

[8]

CoFI. 2004. CASL Reference Manual. Lecture Notes in Computer Science, vol. 2960, (IFIP Series). Springer.

[9]

Cohen, E. and Lamport, L. 1998. Reduction in TLA. In Proceedings of the 9th International Conference on Concurrency Theory (CONCUR'98). Springer-Verlag, 317--331.

Digital Library

[10]

Colvin, R., Doherty, S., and Groves, L. 2005. Verifying concurrent data structures by simulation. Electron. Notes Theor. Comput. Sci. 137, 93--110.

Digital Library

[11]

de Roever, W. and Engelhardt, K. 1998. Data Refinement: Model-Oriented Proof Methods and Their Comparison. Cambridge Tracts in Theoretical Computer Science, vol. 47, Cambridge University Press.

[12]

Derrick, J. and Boiten, E. 2001. Refinement in Z and Object-Z: Foundations and Advanced Applications. Springer.

Digital Library

[13]

Derrick, J., Schellhorn, G., and Wehrheim, H. 2007. Proving linearizability via non-atomic refinement. In Proceedings of the 6th International Conference on Integrated Formal Methods. J. Davies and J. Gibbons Eds., Lecture Notes in Computer Science, vol. 4591, Springer, 195--214.

Digital Library

[14]

Derrick, J., Schellhorn, G., and Wehrheim, H. 2008. Mechanizing a correctness proof for a lock-free concurrent stack. In Proceedings of the International Conference on Formal Methods For Open, Object-Based Distributed Systems. G. Barthe and F. de Boer Eds., Lecture Notes in Computer Science, vol. 5051, Springer, 78--95.

Digital Library

[15]

Derrick, J. and Wehrheim, H. 2003. Using coupled simulations in non-atomic refinement. In Proceedings of the 3rd International Conference of B and Z Users: Format Specification and Development in Z and B. Lecture Notes in Computer Science, vol. 2651, Springer, 127--147.

Digital Library

[16]

Derrick, J. and Wehrheim, H. 2005. Non-atomic refinement in Z and CSP. In Proceedings of the 4th International Conference of B and Z Users. Lecture Notes in Computer Science, vol. 3455, Springer.

Digital Library

[17]

Distefano, D., O'Hearn, P., and Yang, H. 2006. A local shape analysis based on separation logic. In Proceedings of the 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'06). Lecture Notes in Computer Science, vol. 3920, Springer, 287--302.

Digital Library

[18]

Doherty, S., Groves, L., Luchangco, V., and Moir, M. 2004. Formal verification of a practical lock-free queue algorithm. In Proceedings of the 12th International Conference on Formal Techniques for Networked and Distributed Systems. Lecture Notes in Computer Science, vol. 3235, Springer, 97--114.

[19]

Farmer, W. M. 1994. Theory interpretation in simple type theory. In Proceedings of the 1st International Workshop on Higher-Order Algebra, Logic, and Term Rewriting. J. Heering et al. Eds., Lecture Notes in Computer Science, vol. 816, Springer.

Digital Library

[20]

Feng, X., Ferheira, R., and Shao, Z. 2007. On the relationship between concurrent separation logic and assume-guarantee reasoning. In Proceedings of the 16th European Symposium on Programming. Springer, 173--188.

Digital Library

[21]

Flanagan, C. and Qadeer, S. 2003. Thread-modular model checking. In Proceedings of the Spin Workshop. Lecture Notes in Computer Science, vol. 2648, Springer, 213--224.

Digital Library

[22]

Gao, H. and Hesselink, W. H. 2007. A general lock-free algorithm using compare-and-swap.Inform. Comput. 205, 2, 225--241.

Digital Library

[23]

Groves, L. and Colvin, R. 2007. Derivation of a scalable lock-free stack algorithm. Electron. Notes Theor. Comput Sci. 187, 55--74.

Digital Library

[24]

Hendler, D., Shavit, N., and Yerushalmi, L. 2004. A scalable lock-free stack algorithm. In Proceedings of the Annual ACM Symposium on Parallelism in Algorithms and Architectures(SPAA'04). ACM Press, New York, NY, 206--215.

Digital Library

[25]

Herlihy, M. and Wing, J. 1987. Axioms for concurrent objects. In Proceedings of the ACM Symposium on Principles of Programming Languages. ACM Press, 13--26.

Digital Library

[26]

Herlihy, M. and Wing, J. M. 1990. Linearizability: A correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst. 12, 3, 463--492.

Digital Library

[27]

Hesselink, W. H. 2004. Using eternity variables to specify and prove a serializable database interface. Sci. Comput. Program. 51, 1--2, 47--85.

Digital Library

[28]

Hesselink, W. H. 2005. Eternity variables to prove simulation of specifications. ACM Trans. Comput. Logic 6, 1, 175--201.

Digital Library

[29]

Hesselink, W. H. 2006. Refinement verification of the lazy caching algorithm. Acta Inform. 43, 3, 195--222.

Digital Library

[30]

Hesselink, W. H. 2007. A criterion for atomicity revisited. Acta Inform. 44, 2, 123--151.

Digital Library

[31]

Jacobs, B., Smans, J., Piessens, F., and Schulte, W. 2006. A statically verifiable programming model for concurrent object-oriented programs. In Proceedings of the 8th International Conference on Formal Engineering Methods (ICFEM'06). Z. Liu and J. He Eds., Lecture Notes in Computer Science, vol. 4260, Springer, 420--439.

Digital Library

[32]

Jones, C. B. 1983. Specification and design of (parallel) programs. InProceedings of the International Federation for Information Processing (IFIP'83). North-Holland, 321--332.

[33]

KIV. 2009. Web presentation of the linearization case study in KIV. http://www.informatik.uni-augsburg.de/swt/projects/linearizability2.html.

[34]

Lamport, L. 1994. The temporal logic of actions. ACM Trans. Program. Lang. Syst. 16, 3, 872--923.

Digital Library

[35]

Lamport, L. and Schneider, F. B. 1989. Pretending atomicity. Tech. rep. TR89-1005, SRC Digital.

Digital Library

[36]

Lipton, R. J. 1975. Reduction: A method of proving properties of parallel programs. Comm. ACM 18, 12, 717--72l.

Digital Library

[37]

Liu, Y., Chen, W., Liu, Y. A., and Sun, J. 2009. Model checking linearizability via refinement. In Proceedings of the 2nd World Congress on Formal Methods. A. Cavalcanti and D. Dams Eds., Lecture Notes in Computer Science, vol. 5850, Springer, 321--337.

Digital Library

[38]

Michael, M. M. and Scott, M. L. 1998. Nonblocking algorithms and preemption-safe locking on multi programmed shared - memory multiprocessors. J. Parall. Distrib. Comput. 51, 1, 1--26.

Digital Library

[39]

Misra, J. 2003. A reduction theorem for concurrent object-oriented programs. In Programming Methodology. A. McIver and C. Morgan Eds., Springer-Verlag, 69--92.

Digital Library

[40]

Owicki, S. S. and Gries, D. 1976. An axiomatic proof technique for parallel programs I. Acta Inform. 6, 319--340.

Digital Library

[41]

Parkinson, M., Bornat, R., and O'Hearn, P. 2007. Modular verification of a non-blocking stack. In Proceedings of the 34th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'07). ACM, New York, NY, 297--302.

Digital Library

[42]

Reif, W., Schellhorn, G., Stenzel, K., and Balser, M. 1998. Structured specifications and interactive proofs with KIV. In Automated Deduction—A Basis for Applications, Vol. II: Systems and Implementation Techniques, W. Bibel and P. Schmitt Eds., Kluwer Academic Publishers, Dordrecht, Chapter 1, 13--39.

[43]

Reynolds, J. C. 2002. Separation logic: A logic for shared mutable data structures. In Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science. 55--74.

Digital Library

[44]

Spivey, J. 1992. The Z Notation: A Reference Manual. Prentice Hall.

Digital Library

[45]

Vafeiadis, V. 2008. Modular fine-grained concurrency verification. Tech. rep. UCAM-CL-TR726, Computer Laboratory, University of Cambridge.

[46]

Vafeiadis, V., Herlihy, M., Hoare, T., and Shapiro, M. 2006. Proving correctness of highly concurrent linearisable objects. In Proceedings of the 11th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP'06). ACM, New York, NY, 129--136.

Digital Library

[47]

Vafeiadis, V. and Parkinson, M. J. 2007. A marriage of rely/guarantee and separation logic. In Proceedings of the 18th International Conference on Concurrency Theory, (CONCUR'07). L. Caires and V. T. Vasconcelos Eds., Lecture Notes in Computer Science, vol. 4703, Springer, 256--27l.

Digital Library

[48]

Vechev, M. and Yahav, E. 2008. Deriving linearizable fine-grained concurrent objects. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'08). ACM, New York, NY, 125--135.

Digital Library

[49]

Wang, L. and Stoller, S. D. 2004. Automated verification of programs with non-blocking synchronization. Tech. rep. DAR-04-17, Computer Science Department, SUNY at Stony BroDk. http://www.cs.sunysb.edu/~liqiang/lockfree.html.

[50]

Wang, L. and Stoller, S. D. 2004, 2005. Static analysis for programs with non-blocking synchronization. In Proceedings of the ACM SIGPLAN Symposium on Principles and Practice of Parallel. Programming (PPoPP'05). ACM Press, New York, NY.

Digital Library

[51]

Woodcock, J. C. P. and Davies, J. 1996. Using Z: Specification, Refinement, and Proof. Prentice Hall.

Digital Library

Cited By

Wen TPeng JXue JYou ZSong L(2021)Strict Linearizability and Abstract AtomicityInternational Journal of Foundations of Computer Science10.1142/S012905412150001532:01(1-35)Online publication date: 6-Jan-2021
https://doi.org/10.1142/S0129054121500015
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
Show More Cited By

Index Terms

Mechanically verified proof obligations for linearizability

Recommendations

A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures

Efficient implementations of data structures such as queues, stacks or hash-tables allow for concurrent access by many processes at the same time. To increase concurrency, these algorithms often completely dispose with locking, or only lock small parts ...
Mechanizing a Correctness Proof for a Lock-Free Concurrent Stack
FMOODS '08: Proceedings of the 10th IFIP WG 6.1 international conference on Formal Methods for Open Object-Based Distributed Systems

Distributed algorithms are inherently complex to verify. In this paper we show how to verify that a concurrent lock-free implementation of a stack is correct by mechanizing the proof that it is linearizable, linearizability being a correctness notion ...
Verifying Linearizability via Optimized Refinement Checking

Linearizability is an important correctness criterion for implementations of concurrent objects. Automatic checking of linearizability is challenging because it requires checking that: 1) All executions of concurrent operations are serializable, and 2) ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Programming Languages and Systems

ACM Transactions on Programming Languages and Systems Volume 33, Issue 1

January 2011

218 pages

ISSN:0164-0925

EISSN:1558-4593

DOI:10.1145/1889997

Issue’s Table of Contents

Copyright © 2011 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 25 January 2011

Accepted: 01 February 2010

Revised: 01 December 2009

Received: 01 January 2009

Published in TOPLAS Volume 33, Issue 1

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

42
Total Citations
View Citations
689
Total Downloads

Downloads (Last 12 months)92
Downloads (Last 6 weeks)34

Reflects downloads up to 27 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Wen TPeng JXue JYou ZSong L(2021)Strict Linearizability and Abstract AtomicityInternational Journal of Foundations of Computer Science10.1142/S012905412150001532:01(1-35)Online publication date: 6-Jan-2021
https://doi.org/10.1142/S0129054121500015
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
Winter KSmith GDerrick J(2019)Modelling concurrent objects running on the TSO and ARMv8 memory modelsScience of Computer Programming10.1016/j.scico.2019.102308(102308)Online publication date: Sep-2019
https://doi.org/10.1016/j.scico.2019.102308
Murawski ATzevelekos N(2019)Higher-Order LinearisabilityJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2019.01.002Online publication date: Jan-2019
https://doi.org/10.1016/j.jlamp.2019.01.002
Zakowski YCachera DDemange DPichardie DHaddad HWainwright RChbeir R(2018)Verified compilation of linearizable data structuresProceedings of the 33rd Annual ACM Symposium on Applied Computing10.1145/3167132.3167333(1881-1890)Online publication date: 9-Apr-2018
https://dl.acm.org/doi/10.1145/3167132.3167333
Winter KSmith GDerrick J(2018)Observational Models for Linearizability Checking on Weak Memory Models2018 International Symposium on Theoretical Aspects of Software Engineering (TASE)10.1109/TASE.2018.00021(100-107)Online publication date: Aug-2018
https://doi.org/10.1109/TASE.2018.00021
Smith GWinter K(2017)Relating trace refinement and linearizabilityFormal Aspects of Computing10.1007/s00165-017-0418-229:6(935-950)Online publication date: 1-Nov-2017
https://dl.acm.org/doi/10.1007/s00165-017-0418-2
Kim JSjöberg VGu RShao Z(2017)Safety and Liveness of MCS Lock—Layer by LayerProgramming Languages and Systems10.1007/978-3-319-71237-6_14(273-297)Online publication date: 19-Nov-2017
https://doi.org/10.1007/978-3-319-71237-6_14
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

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 Article

Media

Figures

Other

Tables

View Issue’s Table of Contents