skip to main content
research-article
Open access

Sound, complete, and tractable linearizability monitoring for concurrent collections

Published: 27 December 2017 Publication History

Abstract

While many program properties like the validity of assertions and in-bounds array accesses admit nearly-trivial monitoring algorithms, the standard correctness criterion for concurrent data structures does not. Given an implementation of an arbitrary abstract data type, checking whether the operations invoked in one single concurrent execution are linearizable, i.e., indistinguishable from an execution where the same operations are invoked atomically, requires exponential time in the number of operations.
In this work we identify a class of collection abstract data types which admit polynomial-time linearizability monitors. Collections capture the majority of concurrent data structures available in practice, including stacks, queues, sets, and maps. Although monitoring executions of arbitrary abstract data types requires enumerating exponentially-many possible linearizations, collections enjoy combinatorial properties which avoid the enumeration. We leverage these properties to reduce linearizability to Horn satisfiability. As far as we know, ours is the first sound, complete, and tractable algorithm for monitoring linearizability for types beyond single-value registers.

Supplementary Material

WEBM File (soundcompleteandtractablelinearizability.webm)

References

[1]
Parosh Aziz Abdulla, Frédéric Haziza, Lukás Holík, Bengt Jonsson, and Ahmed Rezine. 2013. An Integrated Specification and Verification Technique for Highly Concurrent Data Structures. In Tools and Algorithms for the Construction and Analysis of Systems - 19th International Conference, TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings (Lecture Notes in Computer Science), Nir Piterman and Scott A. Smolka (Eds.), Vol. 7795. Springer, 324–338.
[2]
Rajeev Alur, Kenneth L. McMillan, and Doron A. Peled. 2000. Model-Checking of Correctness Conditions for Concurrent Objects. Inf. Comput. 160, 1-2 (2000), 167–188.
[3]
Daphna Amit, Noam Rinetzky, Thomas W. Reps, Mooly Sagiv, and Eran Yahav. 2007. Comparison Under Abstraction for Verifying Linearizability. In Computer Aided Verification, 19th International Conference, CAV 2007, Berlin, Germany, July 3-7, 2007, Proceedings (Lecture Notes in Computer Science), Werner Damm and Holger Hermanns (Eds.), Vol. 4590. Springer, 477–490.
[4]
Ahmed Bouajjani, Michael Emmi, Constantin Enea, and Jad Hamza. 2013. Verifying Concurrent Programs against Sequential Specifications. In Programming Languages and Systems - 22nd European Symposium on Programming, ESOP 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings (Lecture Notes in Computer Science), Matthias Felleisen and Philippa Gardner (Eds.), Vol. 7792. Springer, 290–309.
[5]
Ahmed Bouajjani, Michael Emmi, Constantin Enea, and Jad Hamza. 2015a. On Reducing Linearizability to State Reachability. In Automata, Languages, and Programming - 42nd International Colloquium, ICALP 2015, Kyoto, Japan, July 6-10, 2015, Proceedings, Part II (Lecture Notes in Computer Science), Magnús M. Halldórsson, Kazuo Iwama, Naoki Kobayashi, and Bettina Speckmann (Eds.), Vol. 9135. Springer, 95–107.
[6]
Ahmed Bouajjani, Michael Emmi, Constantin Enea, and Jad Hamza. 2015b. Tractable Refinement Checking for Concurrent Objects. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015, Sriram K. Rajamani and David Walker (Eds.). ACM, 651–662.
[7]
Eric A. Brewer. 2000. Towards robust distributed systems (abstract). In Proceedings of the Nineteenth Annual ACM Symposium on Principles of Distributed Computing, July 16-19, 2000, Portland, Oregon, USA., Gil Neiger (Ed.). ACM, 7.
[8]
Sebastian Burckhardt, Chris Dern, Madanlal Musuvathi, and Roy Tan. 2010. Line-up: a complete and automatic linearizability checker. In Proceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2010, Toronto, Ontario, Canada, June 5-10, 2010, Benjamin G. Zorn and Alexander Aiken (Eds.). ACM, 330–340.
[9]
Jacob Burnim, George C. Necula, and Koushik Sen. 2011. Specifying and checking semantic atomicity for multithreaded programs. In Proceedings of the 16th International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2011, Newport Beach, CA, USA, March 5-11, 2011, Rajiv Gupta and Todd C. Mowry (Eds.). ACM, 79–90.
[10]
Austin T. Clements, M. Frans Kaashoek, Nickolai Zeldovich, Robert Tappan Morris, and Eddie Kohler. 2015. The Scalable Commutativity Rule: Designing Scalable Software for Multicore Processors. ACM Trans. Comput. Syst. 32, 4 (2015), 10:1–10:47.
[11]
Mike Dodds, Andreas Haas, and Christoph M. Kirsch. 2015. A Scalable, Correct Time-Stamped Stack. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015, Sriram K. Rajamani and David Walker (Eds.). ACM, 233–246.
[12]
William F. Dowling and Jean H. Gallier. 1984. Linear-Time Algorithms for Testing the Satisfiability of Propositional Horn Formulae. J. Log. Program. 1, 3 (1984), 267–284.
[13]
Cezara Dragoi, Ashutosh Gupta, and Thomas A. Henzinger. 2013. Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates. In Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings (Lecture Notes in Computer Science), Natasha Sharygina and Helmut Veith (Eds.), Vol. 8044. Springer, 174–190.
[14]
Michael Emmi and Constantin Enea. 2016. Symbolic abstract data type inference. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 -22, 2016, Rastislav Bodík and Rupak Majumdar (Eds.). ACM, 513–525.
[15]
Michael Emmi and Constantin Enea. 2017. Exposing Non-Atomic Methods of Concurrent Objects. CoRR abs/1706.09305 (2017). arXiv: 1706.09305 http://arxiv.org/abs/1706.09305
[16]
Michael Emmi, Constantin Enea, and Jad Hamza. 2015. Monitoring refinement via symbolic reasoning. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, June 15-17, 2015, David Grove and Steve Blackburn (Eds.). ACM, 260–269.
[17]
Phillip B. Gibbons and Ephraim Korach. 1997. Testing Shared Memories. SIAM J. Comput. 26, 4 (1997), 1208–1244.
[18]
Jad Hamza. 2015. On the Complexity of Linearizability. In Networked Systems - Third International Conference, NETYS 2015, Agadir, Morocco, May 13-15, 2015, Revised Selected Papers (Lecture Notes in Computer Science), Ahmed Bouajjani and Hugues Fauconnier (Eds.), Vol. 9466. Springer, 308–321.
[19]
Klaus Havelund and Grigore Rosu. 2004. Efficient monitoring of safety properties. STTT 6, 2 (2004), 158–173.
[20]
Thomas A. Henzinger, Ali Sezgin, and Viktor Vafeiadis. 2013. Aspect-Oriented Linearizability Proofs. In CONCUR 2013 -Concurrency Theory - 24th International Conference, CONCUR 2013, Buenos Aires, Argentina, August 27-30, 2013. Proceedings (Lecture Notes in Computer Science), Pedro R. D’Argenio and Hernán C. Melgratti (Eds.), Vol. 8052. Springer, 242–256.
[21]
Maurice Herlihy and Nir Shavit. 2008. The art of multiprocessor programming. Morgan Kaufmann.
[22]
Maurice Herlihy and Jeannette M. Wing. 1990. Linearizability: A Correctness Condition for Concurrent Objects. ACM Trans. Program. Lang. Syst. 12, 3 (1990), 463–492.
[23]
C. A. R. Hoare. 1969. An Axiomatic Basis for Computer Programming. Commun. ACM 12, 10 (1969), 576–580.
[24]
Alex Horn and Daniel Kroening. 2015. Faster Linearizability Checking via P-Compositionality. In Formal Techniques for Distributed Objects, Components, and Systems - 35th IFIP WG 6.1 International Conference, FORTE 2015, Held as Part of the 10th International Federated Conference on Distributed Computing Techniques, DisCoTec 2015, Grenoble, France, June 2-4, 2015, Proceedings (Lecture Notes in Computer Science), Susanne Graf and Mahesh Viswanathan (Eds.), Vol. 9039. Springer, 50–65.
[25]
Artem Khyzha, Alexey Gotsman, and Matthew J. Parkinson. 2016. A Generic Logic for Proving Linearizability. In FM 2016: Formal Methods - 21st International Symposium, Limassol, Cyprus, November 9-11, 2016, Proceedings (Lecture Notes in Computer Science), John S. Fitzgerald, Constance L. Heitmeyer, Stefania Gnesi, and Anna Philippou (Eds.), Vol. 9995. 426–443.
[26]
Hongjin Liang and Xinyu Feng. 2013. Modular verification of linearizability with non-fixed linearization points. In ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’13, Seattle, WA, USA, June 16-19, 2013, Hans-Juergen Boehm and Cormac Flanagan (Eds.). ACM, 459–470.
[27]
Barbara Liskov and Stephen N. Zilles. 1974. Programming with Abstract Data Types. SIGPLAN Notices 9, 4 (1974), 50–59.
[28]
Yang Liu, Wei Chen, Yanhong A. Liu, and Jun Sun. 2009. Model Checking Linearizability via Refinement. In FM 2009: Formal Methods, Second World Congress, Eindhoven, The Netherlands, November 2-6, 2009. Proceedings (Lecture Notes in Computer Science), Ana Cavalcanti and Dennis Dams (Eds.), Vol. 5850. Springer, 321–337.
[29]
Gavin Lowe. 2017. Testing for linearizability. Concurrency and Computation: Practice and Experience 29, 4 (2017).
[30]
Maged M. Michael. 2004. ABA Prevention Using Single-Word Instructions. Technical Report RC 23089. IBM Thomas J. Watson Research Center.
[31]
Mark Moir and Nir Shavit. 2004. Concurrent Data Structures. In Handbook of Data Structures and Applications., Dinesh P. Mehta and Sartaj Sahni (Eds.). Chapman and Hall/CRC.
[32]
Peter W. O’Hearn, Noam Rinetzky, Martin T. Vechev, Eran Yahav, and Greta Yorsh. 2010. Verifying linearizability with hindsight. In Proceedings of the 29th Annual ACM Symposium on Principles of Distributed Computing, PODC 2010, Zurich, Switzerland, July 25-28, 2010, Andréa W. Richa and Rachid Guerraoui (Eds.). ACM, 85–94.
[33]
Gerhard Schellhorn, Heike Wehrheim, and John Derrick. 2012. How to Prove Algorithms Linearisable. In Computer Aided Verification - 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings (Lecture Notes in Computer Science), P. Madhusudan and Sanjit A. Seshia (Eds.), Vol. 7358. Springer, 243–259.
[34]
Ilya Sergey, Aleksandar Nanevski, and Anindya Banerjee. 2015a. Mechanized verification of fine-grained concurrent programs. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, June 15-17, 2015, David Grove and Steve Blackburn (Eds.). ACM, 77–87.
[35]
Ilya Sergey, Aleksandar Nanevski, and Anindya Banerjee. 2015b. Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity. In Programming Languages and Systems - 24th European Symposium on Programming, ESOP 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings (Lecture Notes in Computer Science), Jan Vitek (Ed.), Vol. 9032. Springer, 333–358.
[36]
Ohad Shacham, Nathan Grasso Bronson, Alex Aiken, Mooly Sagiv, Martin T. Vechev, and Eran Yahav. 2011. Testing atomicity of composed concurrent operations. In Proceedings of the 26th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2011, part of SPLASH 2011, Portland, OR, USA, October 22 -27, 2011, Cristina Videira Lopes and Kathleen Fisher (Eds.). ACM, 51–64.
[37]
Viktor Vafeiadis. 2010. Automatically Proving Linearizability. In Computer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings (Lecture Notes in Computer Science), Tayssir Touili, Byron Cook, and Paul B. Jackson (Eds.), Vol. 6174. Springer, 450–464.
[38]
Jeannette M. Wing and C. Gong. 1993. Testing and Verifying Concurrent Objects. J. Parallel Distrib. Comput. 17, 1-2 (1993), 164–182.
[39]
Lu Zhang, Arijit Chattopadhyay, and Chao Wang. 2015. Round-Up: Runtime Verification of Quasi Linearizability for Concurrent Data Structures. IEEE Trans. Software Eng. 41, 12 (2015), 1202–1216.
[40]
Shao Jie Zhang. 2011. Scalable automatic linearizability checking. In Proceedings of the 33rd International Conference on Software Engineering, ICSE 2011, Waikiki, Honolulu, HI, USA, May 21-28, 2011, Richard N. Taylor, Harald C. Gall, and Nenad Medvidovic (Eds.). ACM, 1185–1187.

Cited By

View all
  • (2024)Automated Robustness Verification of Concurrent Data Structure Libraries against Relaxed Memory ModelsProceedings of the ACM on Programming Languages10.1145/36898028:OOPSLA2(2578-2605)Online publication date: 8-Oct-2024
  • (2023)Asynchronous Wait-Free Runtime Verification and Enforcement of LinearizabilityProceedings of the 2023 ACM Symposium on Principles of Distributed Computing10.1145/3583668.3594563(90-101)Online publication date: 19-Jun-2023
  • (2023)VeriLin: A Linearizability Checker for Large-Scale Concurrent ObjectsTheoretical Aspects of Software Engineering10.1007/978-3-031-35257-7_12(202-220)Online publication date: 27-Jun-2023
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages
Proceedings of the ACM on Programming Languages  Volume 2, Issue POPL
January 2018
1961 pages
EISSN:2475-1421
DOI:10.1145/3177123
Issue’s Table of Contents
Permission to make digital or hard copies of part or all 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 third-party components of this work must be honored. For all other uses, contact the Owner/Author.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 27 December 2017
Published in PACMPL Volume 2, Issue POPL

Check for updates

Author Tags

  1. Concurrent Objects
  2. Linearizability
  3. Runtime Veri cation

Qualifiers

  • Research-article

Funding Sources

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)186
  • Downloads (Last 6 weeks)27
Reflects downloads up to 07 Jan 2025

Other Metrics

Citations

Cited By

View all
  • (2024)Automated Robustness Verification of Concurrent Data Structure Libraries against Relaxed Memory ModelsProceedings of the ACM on Programming Languages10.1145/36898028:OOPSLA2(2578-2605)Online publication date: 8-Oct-2024
  • (2023)Asynchronous Wait-Free Runtime Verification and Enforcement of LinearizabilityProceedings of the 2023 ACM Symposium on Principles of Distributed Computing10.1145/3583668.3594563(90-101)Online publication date: 19-Jun-2023
  • (2023)VeriLin: A Linearizability Checker for Large-Scale Concurrent ObjectsTheoretical Aspects of Software Engineering10.1007/978-3-031-35257-7_12(202-220)Online publication date: 27-Jun-2023
  • (2023)Efficient linearizability checking for actor‐based systemsSoftware: Practice and Experience10.1002/spe.325153:11(2163-2199)Online publication date: 22-Aug-2023
  • (2022)Checking causal consistency of distributed databasesComputing10.1007/s00607-021-00911-3104:10(2181-2201)Online publication date: 1-Oct-2022
  • (2021)Concurrent Correctness in Vector SpaceVerification, Model Checking, and Abstract Interpretation10.1007/978-3-030-67067-2_8(151-173)Online publication date: 12-Jan-2021
  • (2020)Root Causing Linearizability ViolationsComputer Aided Verification10.1007/978-3-030-53288-8_17(350-375)Online publication date: 14-Jul-2020
  • (2019)On the complexity of checking transactional consistencyProceedings of the ACM on Programming Languages10.1145/33605913:OOPSLA(1-28)Online publication date: 10-Oct-2019
  • (2019)Checking linearizability using hitting familiesProceedings of the 24th Symposium on Principles and Practice of Parallel Programming10.1145/3293883.3295726(366-377)Online publication date: 16-Feb-2019
  • (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
  • Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Full Access

Media

Figures

Other

Tables

Share

Share

Share this Publication link

Share on social media