{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,20]],"date-time":"2026-03-20T16:57:05Z","timestamp":1774025825586,"version":"3.50.1"},"reference-count":35,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2023,10,16]],"date-time":"2023-10-16T00:00:00Z","timestamp":1697414400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"Villum Foundation","award":["25804"],"award-info":[{"award-number":["25804"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2023,10,16]]},"abstract":"<jats:p>Weak persistent memory (a.k.a. non-volatile memory) is an emerging technology that offers fast byte-addressable durable main memory.  \nA wealth of algorithms and libraries has been developed to explore this exciting technology.  \nAs noted by others, this has led to a significant verification gap.  \nTowards closing this gap, we present Spirea, the first concurrent separation logic for verification of programs under a weak persistent memory model.  \nSpirea 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.  \nSpirea is fully mechanized in the Coq proof assistant and allows for interactive development of proofs with the Iris Proof Mode.  \nWe use Spirea to verify several challenging examples with modular specifications.  \nWe show how our logic can verify thread-safety and crash-safety of non-blocking durable data structures with null-recovery,  \nin particular the Treiber stack and the Michael-Scott queue adapted to persistent memory.  \nThis is the first time durable data structures have been verified with a program logic.<\/jats:p>","DOI":"10.1145\/3622820","type":"journal-article","created":{"date-parts":[[2023,10,16]],"date-time":"2023-10-16T15:41:29Z","timestamp":1697470889000},"page":"632-657","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Spirea: A Mechanized Concurrent Separation Logic for Weak Persistent Memory"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4617-4976","authenticated-orcid":false,"given":"Simon Friis","family":"Vindum","sequence":"first","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1320-0098","authenticated-orcid":false,"given":"Lars","family":"Birkedal","sequence":"additional","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,10,16]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99336-8_9"},{"key":"e_1_2_1_2_1","unstructured":"Lars Birkedal and Ale\u0161 Bizjak. 2020. Lecture Notes on Iris: Higher-Order Concurrent Separation Logic. https:\/\/iris-project.org\/tutorial-material.html \t\t\t\t  Lars Birkedal and Ale\u0161 Bizjak. 2020. Lecture Notes on Iris: Higher-Order Concurrent Separation Logic. https:\/\/iris-project.org\/tutorial-material.html"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3381898.3397212"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.DISC.2021.14"},{"key":"e_1_2_1_5_1","volume-title":"Verifying a concurrent, crash-safe file system with sequential reasoning. Ph. D. Dissertation","author":"Chajed Tej","unstructured":"Tej Chajed . 2022. Verifying a concurrent, crash-safe file system with sequential reasoning. Ph. D. Dissertation . Machetutes Institute of Technology . Tej Chajed. 2022. Verifying a concurrent, crash-safe file system with sequential reasoning. Ph. D. Dissertation. Machetutes Institute of Technology."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359632"},{"key":"e_1_2_1_7_1","volume-title":"15th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2021","author":"Chajed Tej","year":"2021","unstructured":"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\u2013439. https:\/\/www.usenix.org\/conference\/osdi21\/presentation\/chajed 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\u2013439. https:\/\/www.usenix.org\/conference\/osdi21\/presentation\/chajed"},{"key":"e_1_2_1_8_1","volume-title":"Using Crash Hoare Logic for Certifying the FSCQ File System. In 2016 USENIX Annual Technical Conference, USENIX ATC 2016","author":"Chen Haogang","year":"2016","unstructured":"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 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"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373376.3378515"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454027"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371102"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523451"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_20"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386031"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3178487.3178490"},{"key":"e_1_2_1_16_1","volume-title":"2020 USENIX Annual Technical Conference, USENIX ATC 2020","author":"George Jerrin Shaji","year":"2020","unstructured":"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\u2013872. isbn:978-1-939133-14-4 https:\/\/www.usenix.org\/conference\/atc20\/presentation\/george 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\u2013872. isbn:978-1-939133-14-4 https:\/\/www.usenix.org\/conference\/atc20\/presentation\/george"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-53426-7_23"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2017.17"},{"key":"e_1_2_1_20_1","unstructured":"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\u2013205. https:\/\/www.usenix.org\/conference\/fast19\/presentation\/kaiyrakhmet \t\t\t\t  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\u2013205. https:\/\/www.usenix.org\/conference\/fast19\/presentation\/kaiyrakhmet"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434328"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009855"},{"key":"e_1_2_1_23_1","volume-title":"17th USENIX Conference on File and Storage Technologies, FAST 2019","year":"2019","unstructured":"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 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"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473571"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISCA.2014.6853222"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428219"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371079"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360561"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3437801.3441586"},{"key":"e_1_2_1_30_1","volume-title":"International Workshop on Accelerating Data Management Systems Using Modern Processor and Storage Architectures - ADMS 2015","author":"Schwalb David","year":"2015","unstructured":"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\u201372. http:\/\/www.adms-conf.org\/2015\/adms15_schwalb.pdf 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\u201372. http:\/\/www.adms-conf.org\/2015\/adms15_schwalb.pdf"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660193.2660243"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509532"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.8314888"},{"key":"e_1_2_1_34_1","volume-title":"Spirea: A Mechanized Concurrent Separation Logic for Weak Persistent Memory (Extended With Appendix). Sept., https:\/\/iris-project.org\/pdfs\/2023-oopsla-spirea.pdf","author":"Vindum Simon Friis","year":"2023","unstructured":"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 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"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1950365.1950379"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3622820","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3622820","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:37:04Z","timestamp":1750178224000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3622820"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,10,16]]},"references-count":35,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2023,10,16]]}},"alternative-id":["10.1145\/3622820"],"URL":"https:\/\/doi.org\/10.1145\/3622820","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,10,16]]},"assertion":[{"value":"2023-10-16","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}