{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T11:06:21Z","timestamp":1784199981350,"version":"3.55.0"},"reference-count":51,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","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":[[2025,6,10]]},"abstract":"<jats:p>Read-Copy-Update (RCU) is a critical synchronization mechanism for concurrent data structures, enabling efficient deferred memory reclamation. However, implementing and using RCU correctly is challenging due to its inherent concurrency complexities. While previous work verified RCU, they either relied on unrealistic assumptions of sequentially consistent (SC) memory model or lacked three key features of general-purpose RCU libraries: modular specification, switchable critical sections, and concurrent writer support.<\/jats:p>\n                  <jats:p>\n                    We present the first formal verification of a general-purpose RCU in realistic\n                    <jats:italic toggle=\"yes\">relaxed memory consistency<\/jats:italic>\n                    (RMC), addressing the challenges posed by these features. To achieve modular specification that encompasses relaxed behaviors, we extend existing SC specifications to account for explicit synchronization. To support switchable critical sections, which require read-after-write (RAW) synchronization, we introduce a reasoning principle for RAW-synchronizing\n                    <jats:italic toggle=\"yes\">SC fences<\/jats:italic>\n                    . Using this principle, we also present the first formal verification of Peterson's mutex in RMC. To support concurrent writers performing partially ordered writes, we avoid assuming a total order of links and instead formulate invariants based on per-node incoming link histories. Our proofs are mechanized in the iRC11 relaxed memory separation logic, built upon Iris, in Rocq.\n                  <\/jats:p>","DOI":"10.1145\/3729246","type":"journal-article","created":{"date-parts":[[2025,6,13]],"date-time":"2025-06-13T16:02:27Z","timestamp":1749830547000},"page":"1-25","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Verifying General-Purpose RCU for Reclamation in Relaxed Memory Separation Logic"],"prefix":"10.1145","volume":"9","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-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\/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\/0009-0000-7000-6836","authenticated-orcid":false,"given":"Jeho","family":"Yeon","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":[[2025,6,13]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009883"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1145\/3173162.3177156"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926442"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378819"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","unstructured":"Pedro da Rocha Pinto Thomas Dinsdale-Young and Philippa Gardner. 2014. TaDA: A Logic for Time and Data Abstraction. In ECOOP (LNCS Vol. 8586). 207\u2013231. doi:10.1007\/978-3-662-44202-9_9","DOI":"10.1007\/978-3-662-44202-9_9"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2020.11"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","unstructured":"Hoang Hai Dang. 2024. Scaling up relaxed memory verification with separation logics. doi:10.22028\/D291-43142","DOI":"10.22028\/D291-43142"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","unstructured":"Hoang-Hai Dang Jacques-Henri Jourdan Jan-Oliver Kaiser and Derek Dreyer. 2020. RustBelt Meets Relaxed Memory. PACMPL 4 POPL Article 34 (2020). doi:10.1145\/3371102","DOI":"10.1145\/3371102"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","unstructured":"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. 792\u2013808. doi:10.1145\/3519939.3523451","DOI":"10.1145\/3519939.3523451"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1109\/TPDS.2011.159"},{"key":"e_1_3_2_12_2","unstructured":"Crossbeam Developers. 2023. Crossbeam. https:\/\/github.com\/crossbeam-rs\/crossbeam"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","unstructured":"Marko Doko and Viktor Vafeiadis. 2016. A Program Logic for C11 Memory Fences. In VMCAI (LNCS Vol. 9583). 413\u2013430. doi:10.1007\/978-3-662-49122-5_20","DOI":"10.1007\/978-3-662-49122-5_20"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","unstructured":"Marko Doko and Viktor Vafeiadis. 2017. Tackling Real-Life Relaxed Concurrency with FSL++. In ESOP (LNCS). 448\u2013475. doi:10.1007\/978-3-662-54434-1_17","DOI":"10.1007\/978-3-662-54434-1_17"},{"key":"e_1_3_2_15_2","unstructured":"Keir Fraser. 2004. Practical lock-freedom. Ph. D. Dissertation."},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15375-4_27"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2738006"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_15"},{"key":"e_1_3_2_19_2","doi-asserted-by":"crossref","unstructured":"Timothy L. Harris. 2001. A Pragmatic Implementation of Non-Blocking Linked-Lists. In Proceedings of the 15th International Conference on Distributed Computing (DISC '01). Springer-Verlag Berlin Heidelberg 300\u2013314.","DOI":"10.1007\/3-540-45414-4_21"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.5555\/2385452"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/3622827"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","unstructured":"Jaehwang Jung Sunho Park Janggun Lee Jeho Yeon and Jeehoon Kang. 2025. Artifact for Verifying General-Purpose RCU for Reclamation in Relaxed Memory Separation Logic PLDI 2025. doi:10.5281\/zenodo.15167032","DOI":"10.5281\/zenodo.15167032"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","unstructured":"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. JFP 28 (2018) e20. doi:10.1017\/S0956796818000151","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","unstructured":"Ralf Jung Rodolphe Lepigre Gaurav Parthasarathy Marianna Rapoport Amin Timany Derek Dreyer and Bart Jacobs. 2020. The future is ours: prophecy variables in separation logic. PACMPL 4 POPL Article 45 (2020). doi:10.1145\/3371113","DOI":"10.1145\/3371113"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","unstructured":"Ralf Jung David Swasey Filip Sieczkowski Kasper Svendsen Aaron Turon Lars Birkedal and Derek Dreyer. 2015. Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning. In POPL. 637\u2013650. doi:10.1145\/2775051.2676980","DOI":"10.1145\/2775051.2676980"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","unstructured":"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) (Leibniz International Proceedings in Informatics (LIPIcs) Vol. 74). 17:1-17:29. doi:10.4230\/LIPIcs.ECOOP.2017.17","DOI":"10.4230\/LIPIcs.ECOOP.2017.17"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","unstructured":"Jeehoon Kang Chung-Kil Hur Ori Lahav Viktor Vafeiadis and Derek Dreyer. 2017. A Promising Semantics for Relaxed-Memory Concurrency. In POPL. 175\u2013189. doi:10.1145\/3093333.3009850","DOI":"10.1145\/3093333.3009850"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_10"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1145\/3626183.3659941"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","unstructured":"Robbert Krebbers Amin Timany and Lars Birkedal. 2017. Interactive proofs in higher-order concurrent separation logic. In POPL. 205\u2013217. doi:10.1145\/3009837.3009855","DOI":"10.1145\/3009837.3009855"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","unstructured":"Ori Lahav Viktor Vafeiadis Jeehoon Kang Chung-Kil Hur and Derek Dreyer. 2017. Repairing Sequential Consistency in C\/C++11. In PLDI. 618\u2013632. doi:10.1145\/3062341.3062352","DOI":"10.1145\/3062341.3062352"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1145\/3498672"},{"key":"e_1_3_2_33_2","unstructured":"Paul E. McKenney. 2004. Exploiting Deferred Destruction: An Analysis of Read-Copy-Update Techniques in Operating System Kernels. Ph. D. Dissertation. OGI School of Science and Engineering at Oregon Health and Sciences University."},{"key":"e_1_3_2_34_2","unstructured":"P. E. McKenney and J. D. Slingwine. 1998. Read-copy update: Using execution history to solve concurrency problems. In PDCS '98."},{"key":"e_1_3_2_35_2","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."},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","unstructured":"Glen M\u00e9vel Jacques-Henri Jourdan and Fran\u00e7ois Pottier. 2020. Cosmo: A Concurrent Separation Logic for Multicore OCaml. PACMPL 4 ICFP Article 96 (2020). doi:10.1145\/3408978","DOI":"10.1145\/3408978"},{"key":"e_1_3_2_37_2","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."},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","unstructured":"Maged M. Michael. 2002. High Performance Dynamic Lock-Free Hash Tables and List-Based Sets. In Proceedings of the Fourteenth Annual ACM Symposium on Parallel Algorithms and Architectures (SPAA '02). 73\u201382. doi:10.1145\/564870.564881","DOI":"10.1145\/564870.564881"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","DOI":"10.1109\/TPDS.2004.8"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","unstructured":"Maged M. Michael and Michael L. Scott. 1996. Simple Fast and Practical Non-Blocking and Blocking Concurrent Queue Algorithms. In PODC. 267\u2013275. doi:10.1145\/248052.248106","DOI":"10.1145\/248052.248106"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1145\/3656384"},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190261"},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","DOI":"10.1145\/3141879"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(81)90106-X"},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-47115-5_17"},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","DOI":"10.1145\/1785414.1785443"},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737992"},{"key":"e_1_3_2_48_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-23283-1_16"},{"key":"e_1_3_2_49_2","unstructured":"R.K. Treiber. 1986. Systems Programming: Coping with Parallelism. International Business Machines Incorporated Thomas J. Watson Research Center. https:\/\/books.google.co.kr\/books?id=YQg3HAAACAAJ"},{"key":"e_1_3_2_50_2","doi-asserted-by":"publisher","DOI":"10.1145\/2660193.2660243"},{"key":"e_1_3_2_51_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63387-9_2"},{"key":"e_1_3_2_52_2","doi-asserted-by":"publisher","DOI":"10.1145\/3437992.3439930"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3729246","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T10:07:25Z","timestamp":1784196445000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3729246"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,10]]},"references-count":51,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2025,6,10]]}},"alternative-id":["10.1145\/3729246"],"URL":"https:\/\/doi.org\/10.1145\/3729246","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,6,10]]},"assertion":[{"value":"2024-11-15","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-03-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-06-13","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}