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

research-article

Open access

Spirea: A Mechanized Concurrent Separation Logic for Weak Persistent Memory

Authors:

Simon Friis Vindum,

Lars BirkedalAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 7, Issue OOPSLA2

Article No.: 244, Pages 632 - 657

https://doi.org/10.1145/3622820

Published: 16 October 2023 Publication History

Abstract

Weak persistent memory (a.k.a. non-volatile memory) is an emerging technology that offers fast byte-addressable durable main memory. A wealth of algorithms and libraries has been developed to explore this exciting technology. As noted by others, this has led to a significant verification gap. Towards closing this gap, we present Spirea, the first concurrent separation logic for verification of programs under a weak persistent memory model. Spirea is based on the Iris and Perennial verification frameworks, and by combining features from these logics with novel techniques it supports high-level modular reasoning about crash-safe and thread-safe programs and libraries. Spirea is fully mechanized in the Coq proof assistant and allows for interactive development of proofs with the Iris Proof Mode. We use Spirea to verify several challenging examples with modular specifications. We show how our logic can verify thread-safety and crash-safety of non-blocking durable data structures with null-recovery, in particular the Treiber stack and the Michael-Scott queue adapted to persistent memory. This is the first time durable data structures have been verified with a program logic.

References

[1]

Eleni Vafeiadi Bila, Brijesh Dongol, Ori Lahav, Azalea Raad, and John Wickerson. 2022. View-Based Owicki-Gries Reasoning for Persistent x86-TSO. In Programming Languages and Systems - 31st European Symposium on Programming, ESOP 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Ilya Sergey (Ed.) (Lecture Notes in Computer Science, Vol. 13240). Springer, 234–261. https://doi.org/10.1007/978-3-030-99336-8_9

Digital Library

[2]

Lars Birkedal and Aleš Bizjak. 2020. Lecture Notes on Iris: Higher-Order Concurrent Separation Logic. https://iris-project.org/tutorial-material.html

[3]

Wentao Cai, Haosen Wen, H. Alan Beadle, Chris Kjellqvist, Mohammad Hedayati, and Michael L. Scott. 2020. Understanding and optimizing persistent memory allocation. In ISMM ’20: 2020 ACM SIGPLAN International Symposium on Memory Management, ISMM 2020, virtual [London, UK], June 16, 2020, Chen Ding and Martin Maas (Eds.). ACM, 60–73. isbn:978-1-4503-7566-5 https://doi.org/10.1145/3381898.3397212

Digital Library

[4]

Wentao Cai, Haosen Wen, Vladimir Maksimovski, Mingzhe Du, Rafaello Sanna, Shreif Abdallah, and Michael L. Scott. 2021. Fast Nonblocking Persistence for Concurrent Data Structures. In 35th International Symposium on Distributed Computing, DISC 2021, October 4-8, 2021, Freiburg, Germany (Virtual Conference), Seth Gilbert (Ed.) (LIPIcs, Vol. 209). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 14:1–14:20. isbn:978-3-95977-210-5 https://doi.org/10.4230/LIPIcs.DISC.2021.14

[5]

Tej Chajed. 2022. Verifying a concurrent, crash-safe file system with sequential reasoning. Ph. D. Dissertation. Machetutes Institute of Technology.

[6]

Tej Chajed, Joseph Tassarotti, M. Frans Kaashoek, and Nickolai Zeldovich. 2019. Verifying concurrent, crash-safe systems with Perennial. In Proceedings of the 27th ACM Symposium on Operating Systems Principles, SOSP 2019, Huntsville, ON, Canada, October 27-30, 2019, Tim Brecht and Carey Williamson (Eds.). ACM, 243–258. isbn:978-1-4503-6873-5 https://doi.org/10.1145/3341301.3359632

Digital Library

[7]

Tej Chajed, Joseph Tassarotti, Mark Theng, Ralf Jung, M. Frans Kaashoek, and Nickolai Zeldovich. 2021. GoJournal: a verified, concurrent, crash-safe journaling system. In 15th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2021, July 14-16, 2021, Angela Demke Brown and Jay R. Lorch (Eds.). USENIX Association, 423–439. https://www.usenix.org/conference/osdi21/presentation/chajed

[8]

Haogang Chen, Daniel Ziegler, Tej Chajed, Adam Chlipala, M. Frans Kaashoek, and Nickolai Zeldovich. 2016. Using Crash Hoare Logic for Certifying the FSCQ File System. In 2016 USENIX Annual Technical Conference, USENIX ATC 2016, Denver, CO, USA, June 22-24, 2016, Ajay Gulati and Hakim Weatherspoon (Eds.). USENIX Association. https://www.usenix.org/conference/atc16/technical-sessions/presentation/chen_haogang

[9]

Youmin Chen, Youyou Lu, Fan Yang, Qing Wang, Yang Wang, and Jiwu Shu. 2020. FlatStore: An Efficient Log-Structured Key-Value Storage Engine for Persistent Memory. In ASPLOS ’20: Architectural Support for Programming Languages and Operating Systems, Lausanne, Switzerland, March 16-20, 2020, James R. Larus, Luis Ceze, and Karin Strauss (Eds.). ACM, 1077–1091. isbn:978-1-4503-7102-5 https://doi.org/10.1145/3373376.3378515 ASPLOS 2020 was canceled because of COVID-19.

Digital Library

[10]

Kyeongmin Cho, Sung Hwan Lee, Azalea Raad, and Jeehoon Kang. 2021. Revamping hardware persistency models: view-based and axiomatic persistency models for Intel-x86 and Armv8. In PLDI ’21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Virtual Event, Canada, June 20-25, 20211, Stephen N. Freund and Eran Yahav (Eds.). ACM, 16–31. isbn:978-1-4503-8391-2 https://doi.org/10.1145/3453483.3454027

Digital Library

[11]

Hoang-Hai Dang, Jacques-Henri Jourdan, Jan-Oliver Kaiser, and Derek Dreyer. 2020. RustBelt meets relaxed memory. Proc. ACM Program. Lang., 4, POPL (2020), 34:1–34:29. https://doi.org/10.1145/3371102

Digital Library

[12]

Hoang-Hai Dang, Jaehwang Jung, Jaemin Choi, Duc-Than Nguyen, William Mansky, Jeehoon Kang, and Derek Dreyer. 2022. Compass: strong and compositional library specifications in relaxed memory separation logic. In PLDI ’22: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, San Diego, CA, USA, June 13 - 17, 2022, Ranjit Jhala and Isil Dillig (Eds.). ACM, 792–808. isbn:978-1-4503-9265-5 https://doi.org/10.1145/3519939.3523451

Digital Library

[13]

Marko Doko and Viktor Vafeiadis. 2016. A Program Logic for C11 Memory Fences. In Verification, Model Checking, and Abstract Interpretation - 17th International Conference, VMCAI 2016, St. Petersburg, FL, USA, January 17-19, 2016. Proceedings, Barbara Jobstmann and K. Rustan M. Leino (Eds.) (Lecture Notes in Computer Science, Vol. 9583). Springer, 413–430. isbn:978-3-662-49121-8 https://doi.org/10.1007/978-3-662-49122-5_20

Digital Library

[14]

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 Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2020, London, UK, June 15-20, 2020, Alastair F. Donaldson and Emina Torlak (Eds.). ACM, 377–392. isbn:978-1-4503-7613-6 https://doi.org/10.1145/3385412.3386031

Digital Library

[15]

Michal Friedman, Maurice Herlihy, Virendra J. 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, PPoPP 2018, Vienna, Austria, February 24-28, 2018, Andreas Krall and Thomas R. Gross (Eds.). ACM, 28–40. isbn:978-1-4503-4982-6 https://doi.org/10.1145/3178487.3178490

Digital Library

[16]

Jerrin Shaji George, Mohit Verma, Rajesh Venkatasubramanian, and Pratap Subrahmanyam. 2020. go-pmem: Native Support for Programming Persistent Memory in Go. In 2020 USENIX Annual Technical Conference, USENIX ATC 2020, July 15-17, 2020, Ada Gavrilovska and Erez Zadok (Eds.). USENIX Association, 859–872. isbn:978-1-939133-14-4 https://www.usenix.org/conference/atc20/presentation/george

[17]

Joseph Izraelevitz, Hammurabi Mendes, and Michael L. Scott. 2016. Linearizability of Persistent Memory Objects Under a Full-System-Crash Failure Model. In Distributed Computing - 30th International Symposium, DISC 2016, Paris, France, September 27-29, 2016. Proceedings, Cyril Gavoille and David Ilcinkas (Eds.) (Lecture Notes in Computer Science, Vol. 9888). Springer, 313–327. https://doi.org/10.1007/978-3-662-53426-7_23

[18]

Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Ales Bizjak, Lars Birkedal, and Derek Dreyer. 2018. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. J. Funct. Program., 28 (2018), e20. https://doi.org/10.1017/S0956796818000151

[19]

Jan-Oliver Kaiser, Hoang-Hai Dang, Derek Dreyer, Ori Lahav, and Viktor Vafeiadis. 2017. Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris. In 31st European Conference on Object-Oriented Programming, ECOOP 2017, June 19-23, 2017, Barcelona, Spain, Peter Müller (Ed.) (LIPIcs, Vol. 74). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 17:1–17:29. https://doi.org/10.4230/LIPIcs.ECOOP.2017.17

[20]

Olzhas Kaiyrakhmet, Songyi Lee, Beomseok Nam, Sam H. Noh, and Young-ri Choi. 2019. SLM-DB: Single-Level Key-Value Store with Persistent Memory. 191–205. https://www.usenix.org/conference/fast19/presentation/kaiyrakhmet

[21]

Artem Khyzha and Ori Lahav. 2021. Taming x86-TSO persistency. Proc. ACM Program. Lang., 5, POPL (2021), 1–29. https://doi.org/10.1145/3434328

Digital Library

[22]

Robbert Krebbers, Amin Timany, and Lars Birkedal. 2017. Interactive proofs in higher-order concurrent separation logic. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, Giuseppe Castagna and Andrew D. Gordon (Eds.). ACM, 205–217. https://doi.org/10.1145/3009837.3009855

Digital Library

[23]

2019. 17th USENIX Conference on File and Storage Technologies, FAST 2019, Boston, MA, February 25-28, 2019, Arif Merchant and Hakim Weatherspoon (Eds.). USENIX Association. https://www.usenix.org/conference/fast19

[24]

Glen Mével and Jacques-Henri Jourdan. 2021. Formal verification of a concurrent bounded queue in a weak memory model. Proc. ACM Program. Lang., 5, ICFP (2021), 1–29. https://doi.org/10.1145/3473571

Digital Library

[25]

Steven Pelley, Peter M. Chen, and Thomas F. Wenisch. 2014. Memory persistency. In ACM/IEEE 41st International Symposium on Computer Architecture, ISCA 2014, Minneapolis, MN, USA, June 14-18, 2014. IEEE Computer Society, 265–276. isbn:978-1-4799-4396-8 https://doi.org/10.1109/ISCA.2014.6853222

[26]

Azalea Raad, Ori Lahav, and Viktor Vafeiadis. 2020. Persistent Owicki-Gries reasoning: a program logic for reasoning about persistent programs on Intel-x86. Proc. ACM Program. Lang., 4, OOPSLA (2020), 151:1–151:28. https://doi.org/10.1145/3428219

Digital Library

[27]

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

Digital Library

[28]

Azalea Raad, John Wickerson, and Viktor Vafeiadis. 2019. Weak persistency semantics from the ground up: formalising the persistency semantics of ARMv8 and transactional models. Proc. ACM Program. Lang., 3, OOPSLA (2019), 135:1–135:27. https://doi.org/10.1145/3360561

Digital Library

[29]

Pedro Ramalhete, Andreia Correia, and Pascal Felber. 2021. Efficient algorithms for persistent transactional memory. In PPoPP ’21: 26th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, Virtual Event, Republic of Korea, February 27- March 3, 2021, Jaejin Lee and Erez Petrank (Eds.). ACM, 1–15. isbn:978-1-4503-8294-6 https://doi.org/10.1145/3437801.3441586

Digital Library

[30]

David Schwalb, Tim Berning, Martin Faust, Markus Dreseler, and Hasso Plattner. 2015. nvm malloc: Memory Allocation for NVRAM. In International Workshop on Accelerating Data Management Systems Using Modern Processor and Storage Architectures - ADMS 2015, Kohala Coast, Hawaii, USA, August 31, 2015, Rajesh Bordawekar, Tirthankar Lahiri, Bugra Gedik, and Christian A. Lang (Eds.). 61–72. http://www.adms-conf.org/2015/adms15_schwalb.pdf

[31]

Aaron Turon, Viktor Vafeiadis, and Derek Dreyer. 2014. GPS: navigating weak memory with ghosts, protocols, and separation. In Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA 2014, part of SPLASH 2014, Portland, OR, USA, October 20-24, 2014, Andrew P. Black and Todd D. Millstein (Eds.). ACM, 691–707. https://doi.org/10.1145/2660193.2660243

Digital Library

[32]

Viktor Vafeiadis and Chinmay Narayan. 2013. Relaxed separation logic: a program logic for C11 concurrency. In Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA 2013, part of SPLASH 2013, Indianapolis, IN, USA, October 26-31, 2013, Antony L. Hosking, Patrick Th. Eugster, and Cristina V. Lopes (Eds.). ACM, 867–884. isbn:978-1-4503-2374-1 https://doi.org/10.1145/2509136.2509532

Digital Library

[33]

Simon Friis Vindum and Lars Birkedal. 2023. Artifact for the paper "Spirea: A Mechanized Concurrent Separation Logic for Weak Persistent Memory" in OOPSLA23. https://doi.org/10.5281/zenodo.8314888

Digital Library

[34]

Simon Friis Vindum and Lars Birkedal. 2023. Spirea: A Mechanized Concurrent Separation Logic for Weak Persistent Memory (Extended With Appendix). Sept., https://iris-project.org/pdfs/2023-oopsla-spirea.pdf

[35]

Haris Volos, Andres Jaan Tack, and Michael M. Swift. 2011. Mnemosyne: lightweight persistent memory. 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, 91–104. isbn:978-1-4503-0266-1 https://doi.org/10.1145/1950365.1950379

Digital Library

Cited By

Vindum SGeorges ABirkedal LStark KTimany ABlazy STabareau N(2025)The Nextgen Modality: A Modality for Non-Frame-Preserving Updates in Separation LogicProceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3703595.3705876(83-97)Online publication date: 10-Jan-2025
https://dl.acm.org/doi/10.1145/3703595.3705876
Vafeiadi Bila EDongol B(2024)A verified durable transactional mutex lock for persistent x86-TSOFormal Methods in System Design10.1007/s10703-024-00462-164:1-3(237-282)Online publication date: 31-Jul-2024
https://doi.org/10.1007/s10703-024-00462-1
Bargmann LDongol BWehrheim H(2024)Unifying Weak Memory Verification Using PotentialsFormal Methods10.1007/978-3-031-71162-6_27(519-537)Online publication date: 9-Sep-2024
https://dl.acm.org/doi/10.1007/978-3-031-71162-6_27

Index Terms

Spirea: A Mechanized Concurrent Separation Logic for Weak Persistent Memory
1. Theory of computation
  1. Logic
    1. Logic and verification
    2. Separation logic

Recommendations

Persistent Owicki-Gries reasoning: a program logic for reasoning about persistent programs on Intel-x86

The advent of non-volatile memory (NVM) technologies is expected to transform how software systems are structured fundamentally, making the task of correct programming significantly harder. This is because ensuring that memory stores persist in the ...
Failure-Atomic Persistent Memory Updates via JUSTDO Logging
ASPLOS'16

Persistent memory invites applications to manipulate persistent data via load and store instructions. Because failures during updates may destroy transient data (e.g., in CPU registers), preserving data integrity in the presence of failures requires ...
Persistence semantics for weak memory: integrating epoch persistency with the TSO memory model

Emerging non-volatile memory (NVM) technologies promise the durability of disks with the performance of volatile memory (RAM). To describe the persistency guarantees of NVM, several memory persistency models have been proposed in the literature. However, ...

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 OOPSLA2

October 2023

2250 pages

EISSN:2475-1421

DOI:10.1145/3554312

Editor:
Michael Hicks
Amazon, USA

Issue’s Table of Contents

Copyright © 2023 Owner/Author.

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: 16 October 2023

Published in PACMPL Volume 7, Issue OOPSLA2

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Funding Sources

Villum Foundation

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
378
Total Downloads

Downloads (Last 12 months)222
Downloads (Last 6 weeks)21

Reflects downloads up to 17 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Vindum SGeorges ABirkedal LStark KTimany ABlazy STabareau N(2025)The Nextgen Modality: A Modality for Non-Frame-Preserving Updates in Separation LogicProceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3703595.3705876(83-97)Online publication date: 10-Jan-2025
https://dl.acm.org/doi/10.1145/3703595.3705876
Vafeiadi Bila EDongol B(2024)A verified durable transactional mutex lock for persistent x86-TSOFormal Methods in System Design10.1007/s10703-024-00462-164:1-3(237-282)Online publication date: 31-Jul-2024
https://doi.org/10.1007/s10703-024-00462-1
Bargmann LDongol BWehrheim H(2024)Unifying Weak Memory Verification Using PotentialsFormal Methods10.1007/978-3-031-71162-6_27(519-537)Online publication date: 9-Sep-2024
https://dl.acm.org/doi/10.1007/978-3-031-71162-6_27

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