[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ skip to main content
research-article
Open access

The Path to Durable Linearizability

Published: 11 January 2023 Publication History

Abstract

There is an increasing body of literature proposing new and efficient persistent versions of concurrent data structures ensuring that a consistent state can be recovered after a power failure or a crash. Their correctness is typically stated in terms of durable linearizability (DL), which requires that individual library operations appear to be executed atomically in a sequence consistent with the real-time order and, moreover, that recovering from a crash return a state corresponding to a prefix of that sequence. Sadly, however, there are hardly any formal DL proofs, and those that do exist cover the correctness of rather simple persistent algorithms on specific (simplified) persistency models. In response, we propose a general, powerful, modular, and incremental proof technique that can be used to guide the development and establish DL. Our technique is (1) general, in that it is not tied to a specific persistency and/or consistency model, (2) powerful, in that it can handle the most advanced persistent algorithms in the literature, (3) modular, in that it allows the reuse of an existing linearizability argument, and (4) incremental, in that the additional requirements for establishing DL depend on the complexity of the algorithm to be verified. We illustrate this technique on various versions of a persistent set, leading to the link-free set of Zuriel et al.

References

[1]
Marcos K. Aguilera and Svend Frolund. 2003. Strict Linearizability and the Power of Aborting. https://www.hpl.hp.com/ techreports/2003/HPL-2003-241.html
[2]
Jade Alglave. 2012. A formal hierarchy of weak memory models. Formal Methods Syst. Des. 41, 2 ( 2012 ), 178-210. https: //doi.org/10.1007/S10703-012-0161-5
[3]
Mark Batty, Mike Dodds, and Alexey Gotsman. 2013. Library abstraction for C/C++ concurrency. In POPL 2013. ACM, New York, NY, USA, 235-248. https://doi.org/10.1145/2429069.2429099
[4]
Mark Batty, Scott Owens, Susmit Sarkar, Peter Sewell, and Tjark Weber. 2011. Mathematizing C+ + Concurrency. In Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Austin, Texas, USA) ( POPL '11). Association for Computing Machinery, New York, NY, USA, 55-66. https://doi.org/10.1145/1926385.1926394
[5]
Sebastian Burckhardt, Alexey Gotsman, Madanlal Musuvathi, and Hongseok Yang. 2012. Concurrent Library Correctness on the TSO Memory Model. In ESOP 2012 (LNCS, Vol. 7211 ). Springer, Heidelberg, Germany, 87-107. https://doi.org/10. 1007/978-3-642-28869-2_5
[6]
Nachshon Cohen, Rachid Guerraoui, and Igor Zablotchi. 2018. The Inherent Cost of Remembering Consistently. In SPAA. ACM, 259-269. https://doi.org/10.1145/3210377.3210400
[7]
John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, and Heike Wehrheim. 2021. Verifying correctness of persistent concurrent data structures: a sound and complete method. Formal Aspects Comput. 33, 4-5 ( 2021 ), 547-573. https://doi.org/10.1007/s00165-021-00541-8
[8]
Emanuele D'Osualdo, Azalea Raad, and Viktor Vafeiadis. 2022. The Path to Durable Linearizability (Extended Version). CoRR arxiv:2211.07631 ( 2022 ). https://doi.org/10.48550/arxiv.2211.07631
[9]
Michal Friedman, Naama Ben-David, Yuanhao Wei, Guy E. Blelloch, and Erez Petrank. 2020. NVTraverse: in NVRAM data structures, the destination is more important than the journey. In PLDI. ACM, 377-392. https://doi.org/10.1145/3385412. 3386031
[10]
Michal Friedman, Maurice Herlihy, Virendra Marathe, and Erez Petrank. 2018. A Persistent Lock-Free Queue for Non-Volatile Memory. In Proceedings of the 23rd ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (Vienna, Austria) ( PPoPP '18). Association for Computing Machinery, New York, NY, USA, 28-40. https://doi.org/10.1145/3178487. 3178490
[11]
Michal Friedman, Erez Petrank, and Pedro Ramalhete. 2021. Mirror: making lock-free data structures persistent. In PLDI. ACM, 1218-1232. https://doi.org/10.1145/3453483.3454105
[12]
Timothy L. Harris. 2001. A Pragmatic Implementation of Non-blocking Linked-Lists. In DISC (Lecture Notes in Computer Science, Vol. 2180 ). Springer, 300-314. https://doi.org/10.1007/3-540-45414-4_21
[13]
Maurice Herlihy and Jeannette M. Wing. 1990. Linearizability: A correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst. 12, 3 ( 1990 ), 463-492. https://doi.org/10.1145/78969.78972
[14]
Intel. 2015. Persistent Memory Programming. http://pmem.io/
[15]
Joseph Izraelevitz, Hammurabi Mendes, and Michael L. Scott. 2016. Linearizability of Persistent Memory Objects Under a Full-System-Crash Failure Model. In DISC (Lecture Notes in Computer Science, Vol. 9888 ), Cyril Gavoille and David Ilcinkas (Eds.). 313-327. https://doi.org/10.1007/978-3-662-53426-7_23
[16]
Takayuki Kawahara, Kenchi Ito, Riichiro Takemura, and Hideo Ohno. 2012. Spin-transfer torque RAM technology: Review and prospect. Microelectron. Reliab. 52, 4 ( 2012 ), 613-627. https://doi.org/10.1016/J.MICROREL. 2011. 09.028
[17]
Leslie Lamport. 1979. How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Computers 28, 9 (Sept. 1979 ), 690-691. https://doi.org/10.1109/TC. 1979.1675439
[18]
Benjamin C. Lee, Engin Ipek, Onur Mutlu, and Doug Burger. 2009. Architecting phase change memory as a scalable DRAM alternative. In ISCA. ACM, 2-13. https://doi.org/10.1145/1555754.1555758
[19]
Maged M. Michael and Michael L. Scott. 1996. Simple, Fast, and Practical Non-blocking and Blocking Concurrent Queue Algorithms. In Proceedings of the Fifteenth Annual ACM Symposium on Principles of Distributed Computing (Philadelphia, Pennsylvania, USA) ( PODC '96). ACM, New York, NY, USA, 267-275. https://doi.org/10.1145/248052.248106
[20]
Peter W. O'Hearn, Noam Rinetzky, Martin T. Vechev, Eran Yahav, and Greta Yorsh. 2010. Verifying linearizability with hindsight. In PODC. 85-94. https://doi.org/10.1145/1835698.1835722
[21]
Steven Pelley, Peter M. Chen, and Thomas F. Wenisch. 2014. Memory persistency. In ISCA. IEEE Computer Society, 265-276. https://doi.org/10.1109/ISCA. 2014.6853222
[22]
Azalea Raad, Marko Doko, Lovro Rožić, Ori Lahav, and Viktor Vafeiadis. 2019a. On Library Correctness under Weak Memory Consistency: Specifying and Verifying Concurrent Libraries under Declarative Consistency Models. 3, POPL ( 2019 ). https://doi.org/10.1145/3290381
[23]
Azalea Raad and Viktor Vafeiadis. 2018. Persistence Semantics for Weak Memory: Integrating Epoch Persistency with the TSO Memory Model. Proc. ACM Program. Lang. 2, OOPSLA, Article 137 (Oct. 2018 ), 27 pages. https://doi.org/10.1145/3276507
[24]
Azalea Raad, John Wickerson, Gil Neiger, and Viktor Vafeiadis. 2020. Persistency semantics of the Intel-x86 architecture. Proc. ACM Program. Lang. 4, POPL ( 2020 ), 11 : 1-11 : 31. https://doi.org/10.1145/3371079
[25]
Azalea Raad, John Wickerson, and Viktor Vafeiadis. 2019b. Weak Persistency Semantics from the Ground Up: Formalising the Persistency Semantics of ARMv8 and Transactional Models. Proc. ACM Program. Lang. 3, OOPSLA, Article 135, 27 pages. https://doi.org/10.1145/3360561
[26]
Gerhard Schellhorn, John Derrick, and Heike Wehrheim. 2014. A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures. ACM Trans. Comput. Log. 15, 4 ( 2014 ), 31 : 1-31 : 37. https://doi.org/10.1145/2629496
[27]
Peter Sewell, Susmit Sarkar, Scott Owens, Francesco Zappa Nardelli, and Magnus O. Myreen. 2010. X86-TSO: A Rigorous and Usable Programmer's Model for X86 Multiprocessors. Commun. ACM 53, 7 (jul 2010 ), 89-97. https://doi.org/10. 1145/1785414.1785443
[28]
Storage Networking Industry Association (SNIA). 2017. NVM Programming Model (NPM). SNIA Technical Position. https://www.snia.org/sites/default/files/technical_work/final/NVMProgrammingModel_v1.2.pdf Version 1.2.
[29]
Dmitri B Strukov, Gregory S Snider, Duncan R Stewart, and R Stanley Williams. 2008. The missing memristor found. Nature 453, 7191 ( 2008 ), 80-83. https://doi.org/10.1109/IOLTS. 2019.8854427
[30]
Yuanhao Wei, Naama Ben-David, Michal Friedman, Guy E. Blelloch, and Erez Petrank. 2022. FliT: a library for simple and eficient persistent algorithms. In PPoPP. ACM, 309-321. https://doi.org/10.1145/3503221.3508436
[31]
Yoav Zuriel, Michal Friedman, Gali Shefi, Nachshon Cohen, and Erez Petrank. 2019. Eficient lock-free durable sets. Proc. ACM Program. Lang. 3, OOPSLA ( 2019 ), 128 : 1-128 : 26. https://doi.org/10.1145/3360554

Cited By

View all
  • (2024)BonsaiKV: Towards Fast, Scalable, and Persistent Key-Value Stores with Tiered, Heterogeneous Memory SystemProceedings of the VLDB Endowment10.14778/3636218.363622817:4(726-739)Online publication date: 5-Mar-2024
  • (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
  • (2024)A verified durable transactional mutex lock for persistent x86-TSOFormal Methods in System Design10.1007/s10703-024-00462-1Online publication date: 31-Jul-2024
  • Show More Cited By

Recommendations

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages
Proceedings of the ACM on Programming Languages  Volume 7, Issue POPL
January 2023
2196 pages
EISSN:2475-1421
DOI:10.1145/3554308
  • Editor:
Issue’s Table of Contents
This work is licensed under a Creative Commons Attribution 4.0 International License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 11 January 2023
Published in PACMPL Volume 7, Issue POPL

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. Concurrency
  2. Linearizability
  3. Non-Volatile Memory
  4. Persistency
  5. Px86
  6. Weak Memory Models

Qualifiers

  • Research-article

Funding Sources

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)197
  • Downloads (Last 6 weeks)9
Reflects downloads up to 21 Dec 2024

Other Metrics

Citations

Cited By

View all
  • (2024)BonsaiKV: Towards Fast, Scalable, and Persistent Key-Value Stores with Tiered, Heterogeneous Memory SystemProceedings of the VLDB Endowment10.14778/3636218.363622817:4(726-739)Online publication date: 5-Mar-2024
  • (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
  • (2024)A verified durable transactional mutex lock for persistent x86-TSOFormal Methods in System Design10.1007/s10703-024-00462-1Online publication date: 31-Jul-2024
  • (2024)A Fully Verified Persistency LibraryVerification, Model Checking, and Abstract Interpretation10.1007/978-3-031-50521-8_2(26-47)Online publication date: 15-Jan-2024

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