{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,20]],"date-time":"2026-06-20T09:24:38Z","timestamp":1781947478866,"version":"3.54.5"},"reference-count":77,"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":"Samsung Research Funding & Incubation Center of Samsung Electronics","award":["SRFC-IT2201-06"],"award-info":[{"award-number":["SRFC-IT2201-06"]}]}],"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>\n            Formal verification is an effective method to address the challenge of designing correct and efficient concurrent data structures. But verification efforts often ignore\n            <jats:italic>memory reclamation<\/jats:italic>\n            , which involves nontrivial synchronization between concurrent accesses and reclamation. When incorrectly implemented, it may lead to critical safety errors such as use-after-free and the ABA problem. Semi-automatic safe memory reclamation schemes such as hazard pointers and RCU encapsulate the complexity of manual memory management in modular interfaces. However, this modularity has not been carried over to formal verification.\n          <\/jats:p>\n          <jats:p>\n            We propose modular specifications of hazard pointers and RCU, and formally verify realistic implementations of them in concurrent separation logic. Specifically, we design abstract predicates for hazard pointers that capture the meaning of\n            <jats:italic>validating<\/jats:italic>\n            the protection of nodes, and those for RCU that support\n            <jats:italic>optimistic traversal<\/jats:italic>\n            to possibly retired nodes. We demonstrate that the specifications indeed facilitate modular verification in three criteria: compositional verification, general applicability, and easy integration. In doing so, we present the first formal verification of Harris\u2019s list, the Harris-Michael list, the Chase-Lev deque, and RDCSS with reclamation. We report the Coq mechanization of all our results in the Iris separation logic framework.\n          <\/jats:p>","DOI":"10.1145\/3622827","type":"journal-article","created":{"date-parts":[[2023,10,16]],"date-time":"2023-10-16T15:41:29Z","timestamp":1697470889000},"page":"828-856","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["Modular Verification of Safe Memory Reclamation in Concurrent Separation Logic"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6099-2644","authenticated-orcid":false,"given":"Jaehwang","family":"Jung","sequence":"first","affiliation":[{"name":"KAIST, Daejeon, Republic of Korea"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-0047-7717","authenticated-orcid":false,"given":"Janggun","family":"Lee","sequence":"additional","affiliation":[{"name":"KAIST, Daejeon, Republic of Korea"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2023-6267","authenticated-orcid":false,"given":"Jaemin","family":"Choi","sequence":"additional","affiliation":[{"name":"KAIST, Daejeon, Republic of Korea"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-3800-9879","authenticated-orcid":false,"given":"Jaewoo","family":"Kim","sequence":"additional","affiliation":[{"name":"KAIST, Daejeon, Republic of Korea"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-5380-1969","authenticated-orcid":false,"given":"Sunho","family":"Park","sequence":"additional","affiliation":[{"name":"KAIST, Daejeon, Republic of Korea"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2115-0871","authenticated-orcid":false,"given":"Jeehoon","family":"Kang","sequence":"additional","affiliation":[{"name":"KAIST, Daejeon, Republic of Korea"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"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-642-17653-1_29"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3296957.3177156"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3064176.3064214"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3201897"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454060"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926394"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1047659.1040327"},{"key":"e_1_2_1_8_1","volume-title":"Checking Interference with Fractional Permissions","author":"Boyland John","unstructured":"John Boyland . 2003. Checking Interference with Fractional Permissions . In Static Analysis, Radhia Cousot (Ed.). Springer Berlin Heidelberg , Berlin, Heidelberg . 55\u201372. isbn:978-3-540-44898-3 John Boyland. 2003. Checking Interference with Fractional Permissions. In Static Analysis, Radhia Cousot (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 55\u201372. isbn:978-3-540-44898-3"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2767386.2767436"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1073970.1073974"},{"key":"e_1_2_1_11_1","volume-title":"TaDA: A Logic for Time and Data Abstraction. In ECOOP 2014 \u2013 Object-Oriented Programming, Richard Jones (Ed.). Springer Berlin Heidelberg","author":"da Rocha Pinto Pedro","year":"2014","unstructured":"Pedro da Rocha Pinto , Thomas Dinsdale-Young , and Philippa Gardner . 2014 . TaDA: A Logic for Time and Data Abstraction. In ECOOP 2014 \u2013 Object-Oriented Programming, Richard Jones (Ed.). Springer Berlin Heidelberg , Berlin, Heidelberg. 207\u2013231. isbn:978-3-662-44202-9 Pedro da Rocha Pinto, Thomas Dinsdale-Young, and Philippa Gardner. 2014. TaDA: A Logic for Time and Data Abstraction. In ECOOP 2014 \u2013 Object-Oriented Programming, Richard Jones (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 207\u2013231. isbn:978-3-662-44202-9"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371102"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523451"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-06410-9_15"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/TPDS.2011.159"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30232-2_7"},{"key":"e_1_2_1_17_1","volume-title":"Tackling Real-Life Relaxed Concurrency with FSL++","author":"Doko Marko","unstructured":"Marko Doko and Viktor Vafeiadis . 2017. Tackling Real-Life Relaxed Concurrency with FSL++ . In Programming Languages and Systems, Hongseok Yang (Ed.). Springer Berlin Heidelberg , Berlin, Heidelberg . 448\u2013475. isbn:978-3-662-54434-1 Marko Doko and Viktor Vafeiadis. 2017. Tackling Real-Life Relaxed Concurrency with FSL++. In Programming Languages and Systems, Hongseok Yang (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 448\u2013475. isbn:978-3-662-54434-1"},{"key":"e_1_2_1_18_1","unstructured":"Keir Fraser. 2004. Practical lock-freedom. Ph. D. Dissertation. \t\t\t\t  Keir Fraser. 2004. Practical lock-freedom. Ph. D. Dissertation."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15375-4_27"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_15"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32940-1_19"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2016.6"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/645958.676105"},{"key":"e_1_2_1_24_1","volume-title":"Proceedings of the 16th International Conference on Distributed Computing (DISC \u201902)","author":"Harris Timothy L.","unstructured":"Timothy L. Harris , Keir Fraser , and Ian A. Pratt . 2002. A Practical Multi-Word Compare-and-Swap Operation . In Proceedings of the 16th International Conference on Distributed Computing (DISC \u201902) . Springer-Verlag, Berlin, Heidelberg. 265\u2013279. isbn:3540000739 Timothy L. Harris, Keir Fraser, and Ian A. Pratt. 2002. A Practical Multi-Word Compare-and-Swap Operation. In Proceedings of the 16th International Conference on Distributed Computing (DISC \u201902). Springer-Verlag, Berlin, Heidelberg. 265\u2013279. isbn:3540000739"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jpdc.2007.04.010"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1007912.1007944"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429109"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/78969.78972"},{"key":"e_1_2_1_29_1","unstructured":"Iris Team. 2023. Iris examples. https:\/\/gitlab.mpi-sws.org\/iris\/examples \t\t\t\t  Iris Team. 2023. Iris examples. https:\/\/gitlab.mpi-sws.org\/iris\/examples"},{"key":"e_1_2_1_30_1","unstructured":"Iris Team. 2023. The Iris project website. https:\/\/iris-project.org\/ \t\t\t\t  Iris Team. 2023. The Iris project website. https:\/\/iris-project.org\/"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926417"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-43951-7_19"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3580418"},{"key":"e_1_2_1_34_1","volume-title":"Iris Workshop. https:\/\/people.mpi-sws.org\/~jung\/iris\/talk-iris2019","author":"Jung Ralf","year":"2019","unstructured":"Ralf Jung . 2019 . Logical Atomicity in Iris: the Good, the Bad, and the Ugly . Iris Workshop. https:\/\/people.mpi-sws.org\/~jung\/iris\/talk-iris2019 .pdf Ralf Jung. 2019. Logical Atomicity in Iris: the Good, the Bad, and the Ugly. Iris Workshop. https:\/\/people.mpi-sws.org\/~jung\/iris\/talk-iris2019.pdf"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371113"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2017.17"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3093333.3009850"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385978"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009855"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158125"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17184-1_4"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062352"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1979.1675439"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498672"},{"key":"e_1_2_1_47_1","unstructured":"Paul E. McKenney Maged Michael Jens Maurer Peter Sewell Martin Uecker Hans Boehm Hubert Tong Niall Douglas Thomas Rodgers Will Deacon Michael Wong David Goldblatt Kostya Serebryany and Anthony Williams.. 2021. P2414R1: Pointer lifetime-end zap proposed solutions. https:\/\/wg21.link\/p2414r1 \t\t\t\t  Paul E. McKenney Maged Michael Jens Maurer Peter Sewell Martin Uecker Hans Boehm Hubert Tong Niall Douglas Thomas Rodgers Will Deacon Michael Wong David Goldblatt Kostya Serebryany and Anthony Williams.. 2021. P2414R1: Pointer lifetime-end zap proposed solutions. https:\/\/wg21.link\/p2414r1"},{"key":"e_1_2_1_48_1","unstructured":"P. E. McKenney and J. D. Slingwine. 1998. Read-copy update: Using execution history to solve concurrency problems. In PDCS \u201998. \t\t\t\t  P. E. McKenney and J. D. Slingwine. 1998. Read-copy update: Using execution history to solve concurrency problems. In PDCS \u201998."},{"key":"e_1_2_1_49_1","unstructured":"Paul E. McKenney Michael Wong Maged M. Michael Geoffrey Romer Andrew Hunter Arthur O\u2019Dwyer Daisy Hollman JF Bastien Hans Boehm David Goldblatt Frank Birbacher Erik Rigtorp Tomasz Kami\u0144ski and Jens Maurer. 2023. P2545R4: Read-Copy Update (RCU). https:\/\/wg21.link\/p2545r4 \t\t\t\t  Paul E. McKenney Michael Wong Maged M. Michael Geoffrey Romer Andrew Hunter Arthur O\u2019Dwyer Daisy Hollman JF Bastien Hans Boehm David Goldblatt Frank Birbacher Erik Rigtorp Tomasz Kami\u0144ski and Jens Maurer. 2023. P2545R4: Read-Copy Update (RCU). https:\/\/wg21.link\/p2545r4"},{"key":"e_1_2_1_50_1","volume-title":"Folly: Facebook Open-source Library. https:\/\/github.com\/facebook\/folly","year":"2023","unstructured":"Meta. 2023 . Folly: Facebook Open-source Library. https:\/\/github.com\/facebook\/folly Meta. 2023. Folly: Facebook Open-source Library. https:\/\/github.com\/facebook\/folly"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408978"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563337"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290371"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371136"},{"key":"e_1_2_1_55_1","unstructured":"Maged Michael Maged M. Michael Michael Wong Paul McKenney Andrew Hunter Daisy S. Hollman JF Bastien Hans Boehm David Goldblatt Frank Birbacher and Mathias Stearn. 2023. P2530R3: Hazard Pointers for C++26. https:\/\/wg21.link\/p2530r3 \t\t\t\t  Maged Michael Maged M. Michael Michael Wong Paul McKenney Andrew Hunter Daisy S. Hollman JF Bastien Hans Boehm David Goldblatt Frank Birbacher and Mathias Stearn. 2023. P2530R3: Hazard Pointers for C++26. https:\/\/wg21.link\/p2530r3"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/564870.564881"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1109\/TPDS.2004.8"},{"key":"e_1_2_1_58_1","volume-title":"PODC","author":"Maged","year":"1996","unstructured":"Maged M. Michael and Michael L. Scott. 1996. Simple, Fast, and Practical Non-Blocking and Blocking Concurrent Queue Algorithms . In PODC 1996 . Maged M. Michael and Michael L. Scott. 1996. Simple, Fast, and Practical Non-Blocking and Blocking Concurrent Queue Algorithms. In PODC 1996."},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/3586043"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523432"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/3332466.3374540"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.DISC.2021.60"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190261"},{"key":"e_1_2_1_64_1","volume-title":"Project Snowflake: Non-blocking safe manual memory management in .NET. Microsoft. https:\/\/www.microsoft.com\/en-us\/research\/publication\/project-snowflake-non-blocking-safe-manual-memory-management-net\/","author":"Parkinson Matthew","year":"2017","unstructured":"Matthew Parkinson , Kapil Vaswani , Dimitrios Vytiniotis , Manuel Costa , Pantazis Deligiannis , Aaron Blankstein , Dylan McDermott , and Jonathan Balkind . 2017 . Project Snowflake: Non-blocking safe manual memory management in .NET. Microsoft. https:\/\/www.microsoft.com\/en-us\/research\/publication\/project-snowflake-non-blocking-safe-manual-memory-management-net\/ Matthew Parkinson, Kapil Vaswani, Dimitrios Vytiniotis, Manuel Costa, Pantazis Deligiannis, Aaron Blankstein, Dylan McDermott, and Jonathan Balkind. 2017. Project Snowflake: Non-blocking safe manual memory management in .NET. Microsoft. https:\/\/www.microsoft.com\/en-us\/research\/publication\/project-snowflake-non-blocking-safe-manual-memory-management-net\/"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/3409964.3461817"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/3437801.3441625"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_9"},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737992"},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-23283-1_16"},{"key":"e_1_2_1_70_1","unstructured":"R. K. Treiber. 1986. Systems programming: coping with parallelism. \t\t\t\t  R. K. Treiber. 1986. Systems programming: coping with parallelism."},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660193.2660243"},{"key":"e_1_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_40"},{"key":"e_1_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11319-2_25"},{"key":"e_1_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2011.09.029"},{"key":"e_1_2_1_75_1","volume-title":"Program Verification Under Weak Memory Consistency Using Separation Logic","author":"Vafeiadis Viktor","unstructured":"Viktor Vafeiadis . 2017. Program Verification Under Weak Memory Consistency Using Separation Logic . In Computer Aided Verification, Rupak Majumdar and Viktor Kun\u010dak (Eds.). Springer International Publishing , Cham . 30\u201346. isbn:978-3-319-63387-9 Viktor Vafeiadis. 2017. Program Verification Under Weak Memory Consistency Using Separation Logic. In Computer Aided Verification, Rupak Majumdar and Viktor Kun\u010dak (Eds.). Springer International Publishing, Cham. 30\u201346. isbn:978-3-319-63387-9"},{"key":"e_1_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.1145\/3200691.3178488"},{"key":"e_1_2_1_77_1","doi-asserted-by":"publisher","DOI":"10.24355\/dbbs.084-202108191157-0"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3622827","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3622827","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\/3622827"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,10,16]]},"references-count":77,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2023,10,16]]}},"alternative-id":["10.1145\/3622827"],"URL":"https:\/\/doi.org\/10.1145\/3622827","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"}}]}}