Document Open Access Logo

Toward Linearizability Testing for Multi-Word Persistent Synchronization Primitives

Authors Diego Cepeda, Sakib Chowdhury, Nan Li, Raphael Lopez, Xinzhe Wang, Wojciech Golab

PDF
Thumbnail PDF

File

LIPIcs.OPODIS.2019.19.pdf
  • Filesize: 0.89 MB
  • 17 pages

Document Identifiers

Author Details

Diego Cepeda
  • Department of Electrical and Computer Engineering, University of Waterloo, Canada
Sakib Chowdhury
  • Department of Electrical and Computer Engineering, University of Waterloo, Canada
Nan Li
  • Department of Electrical and Computer Engineering, University of Waterloo, Canada
Raphael Lopez
  • Department of Mechanical and Mechatronics Engineering, University of Waterloo, Canada
Xinzhe Wang
  • Department of Electrical and Computer Engineering, University of Waterloo, Canada
Wojciech Golab
  • Department of Electrical and Computer Engineering, University of Waterloo, Canada

Funding

  • Cepeda, Diego: Consejo Nacional de Ciencia y Tecnología
  • Lopez, Raphael: University of Waterloo President’s Research Award
  • Wang, Xinzhe: University of Waterloo President’s Research Award
  • Golab, Wojciech: Natural Sciences and Engineering Research Council (NSERC) of Canada, Discovery Grants Program; Ontario Early Researcher Award; Google Faculty Research Award

Cite AsGet BibTex

Diego Cepeda, Sakib Chowdhury, Nan Li, Raphael Lopez, Xinzhe Wang, and Wojciech Golab. Toward Linearizability Testing for Multi-Word Persistent Synchronization Primitives. In 23rd International Conference on Principles of Distributed Systems (OPODIS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 153, pp. 19:1-19:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.OPODIS.2019.19

Abstract

Persistent memory makes it possible to recover in-memory data structures following a failure instead of rebuilding them from state saved in slow secondary storage. Implementing such recoverable data structures correctly is challenging as their underlying algorithms must deal with both parallelism and failures, which makes them especially susceptible to programming errors. Traditional proofs of correctness should therefore be combined with other methods, such as model checking or software testing, to minimize the likelihood of uncaught defects. This research focuses specifically on the algorithmic principles of software testing, particularly linearizability analysis, for multi-word persistent synchronization primitives such as conditional swap operations. We describe an efficient decision procedure for linearizability in this context, and discuss its practical applications in detecting previously-unknown bugs in implementations of multi-word persistent primitives.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Synchronization
  • Theory of computation → Shared memory algorithms
  • Computer systems organization → Reliability
Keywords
  • Shared memory
  • persistent memory
  • synchronization
  • multi-word primitives
  • concurrency
  • correctness
  • software testing

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Kiran Adhikari, James Street, Chao Wang, Yang Liu, and Shao Jie Zhang. Verifying a quantitative relaxation of linearizability via refinement. STTT, 18(4):393-407, 2016. Google Scholar
  2. Marcos Aguilera and Svend Frølund. Strict linearizability and the power of aborting. HP Labs Tech. Rep. HPL-2003-241, 2003. Google Scholar
  3. Eric Anderson, Xiaozhou Li, Mehul A. Shah, Joseph Tucek, and Jay J. Wylie. What Consistency Does Your Key-Value Store Actually Provide? In Proc. of the Sixth Workshop on Hot Topics in System Dependability (HotDep), 2010. Google Scholar
  4. Hagit Attiya, Ohad Ben-Baruch, and Danny Hendler. Nesting-Safe Recoverable Linearizability: Modular Constructions for Non-Volatile Memory. In Proc. of the 37th ACM Symposium on Principles of Distributed Computing (PODC), pages 7-16, 2018. Google Scholar
  5. Peter Bailis, Shivaram Venkataraman, Michael J. Franklin, Joseph M. Hellerstein, and Ion Stoica. Probabilistically Bounded Staleness for Practical Partial Quorums. PVLDB, 5(8):776-787, 2012. Google Scholar
  6. Philip A. Bernstein, Vassos Hadzilacos, and Nathan Goodman. Concurrency Control and Recovery in Database Systems. Addison-Wesley, 1987. Google Scholar
  7. Ryan Berryhill, Wojciech M. Golab, and Mahesh Tripunitara. Robust Shared Objects for Non-Volatile Main Memory. In Proc. of the 19th International Conference on Principles of Distributed Systems (OPODIS), pages 20:1-20:17, 2015. Google Scholar
  8. Ahmed Bouajjani, Michael Emmi, Constantin Enea, and Jad Hamza. On Reducing Linearizability to State Reachability. Inf. Comput., 261(Part 2):383-400, 2018. Google Scholar
  9. Sebastian Burckhardt, Chris Dern, Madanlal Musuvathi, and Roy Tan. Line-up: a complete and automatic linearizability checker. In Proc. of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 330-340, 2010. Google Scholar
  10. Pavol Cerný, Arjun Radhakrishna, Damien Zufferey, Swarat Chaudhuri, and Rajeev Alur. Model Checking of Linearizability of Concurrent List Implementations. In Proc. of the 22nd International Conference on Computer Aided Verification (CAV), pages 465-479, 2010. Google Scholar
  11. Michael Emmi and Constantin Enea. Sound, Complete, and Tractable Linearizability Monitoring for Concurrent Collections. Proc. ACM Program. Lang., 2(POPL):25:1-25:27, 2017. Google Scholar
  12. Steven D. Feldman, Pierre LaBorde, and Damian Dechev. A Wait-Free Multi-Word Compare-and-Swap Operation. International Journal of Parallel Programming, 43(4):572-596, 2015. Google Scholar
  13. Yotam M. Y. Feldman, Constantin Enea, Adam Morrison, Noam Rinetzky, and Sharon Shoham. Order out of Chaos: Proving Linearizability Using Local Views. In Proc. of the 32nd International Symposium on Distributed Computing (DISC), pages 23:1-23:21, 2018. Google Scholar
  14. Michal Friedman, Maurice Herlihy, Virendra Marathe, and Erez Petrank. A Persistent Lock-free Queue for Non-volatile Memory. In Proc. of the 23rd ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP), pages 28-40, 2018. Google Scholar
  15. Phillip B. Gibbons and Ephraim Korach. Testing Shared Memories. SIAM J. Comput., 26(4):1208-1244, 1997. Google Scholar
  16. Wojciech Golab, Xiaozhou Li, and Mehul A. Shah. Analyzing consistency properties for fun and profit. In Proc. ACM SIGACT-SIGOPS Symposium on Principles of Distributed Computing (PODC), pages 197-206, 2011. Google Scholar
  17. Rachid Guerraoui and Ron R Levy. Robust emulations of shared memory in a crash-recovery model. In Proc. of the 24th International Conference on Distributed Computing Systems (DISC), pages 400-407, 2004. Google Scholar
  18. Timothy L. Harris, Keir Fraser, and Ian A. Pratt. A Practical Multi-word Compare-and-Swap Operation. In Proc. of the 16th International Conference on Distributed Computing (DISC), pages 265-279, 2002. Google Scholar
  19. Maurice P. Herlihy and Jeannette M. Wing. Linearizability: A Correctness Condition for Concurrent Objects. ACM Trans. Program. Lang. Syst., 12(3):463-492, 1990. Google Scholar
  20. Alex Horn and Daniel Kroening. Faster Linearizability Checking via P-Compositionality. In Proc. of the International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE), pages 50-65, 2015. Google Scholar
  21. Joseph Izraelevitz, Hammurabi Mendes, and Michael L. Scott. Linearizability of Persistent Memory Objects Under a Full-System-Crash Failure Model. In Proc. of the 30th International Symposium on Distributed Computing (DISC), pages 313-327, 2016. Google Scholar
  22. Leslie Lamport. On Interprocess Communication, Part I: Basic Formalism and Part II: Algorithms. Distributed Computing, 1(2):77-101, 1986. Google Scholar
  23. Leslie Lamport. Specifying systems: the TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, 2002. Google Scholar
  24. Leslie Lamport. The PlusCal Algorithm Language. In Proc. of the 6th International Colloquium on Theoretical Aspects of Computing (ICTAC), pages 36-60, 2009. Google Scholar
  25. Gavin Lowe. Testing for linearizability. Concurrency and Computation: Practice and Experience, 29(4), 2017. Google Scholar
  26. J. Misra. Axioms for Memory Access in Asynchronous Hardware Systems. ACM Trans. Program. Lang. Syst., 8(1):142-153, 1986. Google Scholar
  27. Burcu Kulahcioglu Ozkan, Rupak Majumdar, and Filip Niksic. Checking Linearizability Using Hitting Families. In Proc. of the 24th Symposium on Principles and Practice of Parallel Programming (PPoPP), pages 366-377, 2019. Google Scholar
  28. Viktor Vafeiadis. Automatically Proving Linearizability. In Proc. of the 22nd International Conference on Computer Aided Verification (CAV), pages 450-464, 2010. Google Scholar
  29. Martin T. Vechev, Eran Yahav, and Greta Yorsh. Experience with Model Checking Linearizability. In Proc. of the 16th International Workshop on Model Checking Software (SPIN), pages 261-278, 2009. Google Scholar
  30. Tianzheng Wang, Justin J. Levandoski, and Per-Åke Larson. Easy Lock-Free Indexing in Non-Volatile Memory. In Proc. of the 34th IEEE International Conference on Data Engineering (ICDE), pages 461-472, 2018. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact