{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T11:06:06Z","timestamp":1784199966707,"version":"3.55.0"},"reference-count":54,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","funder":[{"name":"National Research Foundation of Kore","award":["RS-2024-00347786"],"award-info":[{"award-number":["RS-2024-00347786"]}]},{"name":"Institute of Information & communications Technology Planning & Evaluation","award":["IITP-2025-RS-2023-00256472"],"award-info":[{"award-number":["IITP-2025-RS-2023-00256472"]}]},{"name":"Institute of Information & Communications Technology Planning & Evaluation(IITP)-ITR","award":["IITP-2025-RS-2020-II201795"],"award-info":[{"award-number":["IITP-2025-RS-2020-II201795"]}]}],"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>\n                    We report the first formal verification of a lock-free list, skiplist, and a skiplist-based priority queue against a strong specification in relaxed memory consistency (RMC). RMC allows relaxed behaviors in which memory accesses may be reordered with other operations, posing two significant challenges for the verification of lock-free traversals.\n                    <jats:bold>(1)<\/jats:bold>\n                    <jats:italic toggle=\"yes\">Specification challenge<\/jats:italic>\n                    : formulating a specification that is flexible enough to capture relaxed behaviors, yet simple enough to be easily understood and used. We address this challenge by proposing the\n                    <jats:italic toggle=\"yes\">per-key linearizable history specification<\/jats:italic>\n                    that enforces a total order of operations for each key that respects causality, rather than a total order of all operations.\n                    <jats:bold>(2)<\/jats:bold>\n                    <jats:italic toggle=\"yes\">Verification challenge<\/jats:italic>\n                    : devising verification techniques for reasoning about the reachability of edges for traversing threads, which can read stale edges due to relaxed behaviors. We address this challenge by introducing the\n                    <jats:italic toggle=\"yes\">shadowed-by relation<\/jats:italic>\n                    that formalizes the notion of outdated edges. This relation enables us to establish a total order of edges and thus their associated operations for each key, required to satisfy the strong specification. All our proofs are mechanized on the iRC11 relaxed memory separation logic, built on the Iris framework in Rocq.\n                  <\/jats:p>","DOI":"10.1145\/3729248","type":"journal-article","created":{"date-parts":[[2025,6,13]],"date-time":"2025-06-13T16:02:27Z","timestamp":1749830547000},"page":"48-72","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Verifying Lock-Free Traversals in Relaxed Memory Separation Logic"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0009-0000-5380-1969","authenticated-orcid":false,"given":"Sunho","family":"Park","sequence":"first","affiliation":[{"name":"KAIST, Daejeon, Republic of Korea"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6099-2644","authenticated-orcid":false,"given":"Jaehwang","family":"Jung","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\/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","unstructured":"Kapil Kumar Attinagaramu and Praveen Alapati. 2024. CAA: A Concurrent AA Tree via Logical ordering. In 2024 23rd International Symposium on Parallel and Distributed Computing (ISPDC). 1\u20138. doi:10.1109\/ISPDC62236.2024.10705402","DOI":"10.1109\/ISPDC62236.2024.10705402"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","unstructured":"Mark Batty Mike Dodds and Alexey Gotsman. 2013. Library abstraction for C\/C++ concurrency. In The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages POPL \u201913 Rome Italy - January 23-25 2013. ACM 235\u2013248. doi:10.1145\/2429069.2429099","DOI":"10.1145\/2429069.2429099"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1145\/3473586"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44202-9_9"},{"key":"e_1_3_2_6_2","unstructured":"Sadegh Dalvandi and Brijesh Dongol. 2021. Verifying C11-Style Weak Memory Libraries via Refinement. CoRR abs\/2108.06944 (2021). arXiv:2108.06944 https:\/\/arxiv.org\/abs\/2108.06944"},{"key":"e_1_3_2_7_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_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/3371102"},{"key":"e_1_3_2_9_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_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_20"},{"key":"e_1_3_2_11_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_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/2555243.2555269"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/3428196"},{"key":"e_1_3_2_14_2","unstructured":"Keir Fraser. 2004. Practical lock-freedom. Ph. D. Dissertation."},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2738006"},{"key":"e_1_3_2_16_2","first-page":"300","volume-title":"Proceedings of the 15th International Conference on Distributed Computing (DISC \u201901)","author":"Timothy L. Harris","year":"2001","unstructured":"Timothy L. Harris. 2001. A Pragmatic Implementation of Non-Blocking Linked-Lists. In Proceedings of the 15th International Conference on Distributed Computing (DISC \u201901). Springer-Verlag, Berlin, Heidelberg, 300\u2013314."},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1145\/78969.78972"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/3622827"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","unstructured":"Jaehwang Jung Sunho Park Janggun Lee and Jeehoon Kang. 2025. Verifying General-Purpose RCU for Reclamation in Relaxed Memory Separation Logic. Proc. ACM Program. Lang. PLDI (2025). doi:10.1145\/3729246","DOI":"10.1145\/3729246"},{"key":"e_1_3_2_20_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_21_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_22_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_23_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2017.17"},{"key":"e_1_3_2_24_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_25_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_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386029"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","unstructured":"Siddharth Krishna Dennis Shasha and Thomas Wies. 2018. Go with the Flow: Compositional Abstractions for Concurrent Data Structures. PACMPL 2 POPL Article 37 (2018). doi:10.1145\/3158125","DOI":"10.1145\/3158125"},{"key":"e_1_3_2_28_2","doi-asserted-by":"crossref","first-page":"308","DOI":"10.1007\/978-3-030-44914-8_12","volume-title":"Programming Languages and Systems","author":"Siddharth Krishna","year":"2020","unstructured":"Siddharth Krishna, Alexander J. Summers, and Thomas Wies. 2020. Local Reasoning for Global Graph Properties. In Programming Languages and Systems, Peter M\u00fcller (Ed.). Springer International Publishing, Cham, 308\u2013335."},{"key":"e_1_3_2_29_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_30_2","doi-asserted-by":"publisher","DOI":"10.1145\/3492545"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","unstructured":"Sung-Hwan Lee Minki Cho Roy Margalit Chung-Kil Hur and Ori Lahav. 2023. Putting Weak Memory in Order via a Promising Intermediate Representation. Proc. ACM Program. Lang. 7 PLDI Article 183 (jun 2023) 24 pages. doi:10.1145\/3591297","DOI":"10.1145\/3591297"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","unstructured":"Jean-Marie Madiot and Fran\u00e7ois Pottier. 2022. A Separation Logic for Heap Space under Garbage Collection. Proc. ACM Program. Lang. 6 POPL Article 11 (jan 2022) 28 pages. doi:10.1145\/3498672","DOI":"10.1145\/3498672"},{"key":"e_1_3_2_33_2","unstructured":"P. E. McKenney and J. D. Slingwine. 1998. Read-copy update: Using execution history to solve concurrency problems. In PDCS \u201998."},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","unstructured":"Glen M\u00e9vel and Jacques-Henri Jourdan. 2021. Formal Verification of a Concurrent Bounded Queue in a Weak Memory Model. PACMPL 5 ICFP Article 66 (2021). doi:10.1145\/3473571","DOI":"10.1145\/3473571"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","unstructured":"Roland Meyer Thomas Wies and Sebastian Wolff. 2023. Embedding Hindsight Reasoning in Separation Logic. PACMPL 7 PLDI Article 182 (2023). doi:10.1145\/3591296","DOI":"10.1145\/3591296"},{"key":"e_1_3_2_36_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 \u201902). 73\u201382. doi:10.1145\/564870.564881","DOI":"10.1145\/564870.564881"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","unstructured":"Ike Mulder and Robbert Krebbers. 2023. Proof Automation for Linearizability in Separation Logic. PACMPL 7 OOPSLA1 (2023) 91:462\u201391:491. doi:10.1145\/3586043","DOI":"10.1145\/3586043"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","unstructured":"Ike Mulder Robbert Krebbers and Herman Geuvers. 2022. Diaframe: Automated Verification of Fine-Grained Concurrent Programs in Iris (PLDI). 809\u2013824. doi:10.1145\/3519939.3523432","DOI":"10.1145\/3519939.3523432"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","DOI":"10.1145\/1835698.1835722"},{"key":"e_1_3_2_40_2","unstructured":"Oracle. 2024. java.util.concurrent.ConcurrentMap. https:\/\/docs.oracle.com\/en\/java\/javase\/22\/docs\/api\/java.base\/java\/util\/concurrent\/ConcurrentMap.html."},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","unstructured":"Sunho Park Jaehwang Jung Janggun Lee and Jeehoon Kang. 2025. Artifact for \"Verifying Lock-Free Traversals in Relaxed Memory Separation Logic\" PLDI 2025. doi:10.5281\/zenodo.15004020","DOI":"10.5281\/zenodo.15004020"},{"key":"e_1_3_2_42_2","doi-asserted-by":"crossref","unstructured":"Sunho Park Jaehwang Jung Janggun Lee and Jeehoon Kang. 2025. Verifying Lock-Free Traversals in Relaxed Memory Separation Logic (Extended Version). https:\/\/cp.kaist.ac.kr","DOI":"10.1145\/3729248"},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","unstructured":"Sunho Park Jaewoo Kim Ike Mulder Jaehwang Jung Janggun Lee Robbert Krebbers and Jeehoon Kang. 2024. A Proof Recipe for Linearizability in Relaxed Memory Separation Logic. Proc. ACM Program. Lang. 8 PLDI Article 154 (jun 2024) 24 pages. doi:10.1145\/3656384","DOI":"10.1145\/3656384"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","unstructured":"Nisarg Patel Siddharth Krishna Dennis Shasha and Thomas Wies. 2021. Verifying concurrent multicopy search structures. Proc. ACM Program. Lang. 5 OOPSLA Article 113 (oct 2021) 32 pages. doi:10.1145\/3485490","DOI":"10.1145\/3485490"},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2024.30"},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","unstructured":"Azalea Raad Marko Doko Lovro Ro\u017ei\u0107 Ori Lahav and Viktor Vafeiadis. 2019. On Library Correctness under Weak Memory Consistency: Specifying and Verifying Concurrent Libraries under Declarative Consistency Models. PACMPL 3 POPL Article 68 (2019). doi:10.1145\/3290381","DOI":"10.1145\/3290381"},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","unstructured":"Peter Sewell Susmit Sarkar Scott Owens Francesco Zappa Nardelli and Magnus O. Myreen. 2010. x86-TSO: a rigorous and usable programmer\u2019s model for x86 multiprocessors. Commun. ACM 53 7 (jul 2010) 89\u201397. doi:10.1145\/1785414.1785443","DOI":"10.1145\/1785414.1785443"},{"key":"e_1_3_2_48_2","doi-asserted-by":"publisher","DOI":"10.1145\/42201.42204"},{"key":"e_1_3_2_49_2","unstructured":"Nir N Shavit Yosef Lev and Maurice P Herlihy. 2011. Concurrent lock-free skiplist with wait-free contains operator. https:\/\/patentcenter.uspto.gov\/applications\/12191008 US Patent 7 937 378."},{"key":"e_1_3_2_50_2","doi-asserted-by":"publisher","unstructured":"Abhishek Kr Singh and Ori Lahav. 2023. An Operational Approach to Library Abstraction under Relaxed Memory Concurrency. PACMPL 7 POPL Article 53 (2023). doi:10.1145\/3571246","DOI":"10.1145\/3571246"},{"key":"e_1_3_2_51_2","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737992"},{"key":"e_1_3_2_52_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_53_2","doi-asserted-by":"publisher","DOI":"10.1145\/2660193.2660243"},{"key":"e_1_3_2_54_2","doi-asserted-by":"publisher","unstructured":"Viktor Vafeiadis and Chinmay Narayan. 2013. Relaxed Separation Logic: A Program Logic for C11 Concurrency. In OOPSLA. 867\u2013884. doi:10.1145\/2509136.2509532","DOI":"10.1145\/2509136.2509532"},{"key":"e_1_3_2_55_2","doi-asserted-by":"crossref","first-page":"964","DOI":"10.1007\/978-3-662-54434-1_36","volume-title":"Programming Languages and Systems","author":"Shale Xiong","year":"2017","unstructured":"Shale Xiong, Pedro da Rocha Pinto, Gian Ntzik, and Philippa Gardner. 2017. Abstract Specifications for Concurrent Maps. In Programming Languages and Systems, Hongseok Yang (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 964\u2013990."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3729248","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T10:07:04Z","timestamp":1784196424000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3729248"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,10]]},"references-count":54,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2025,6,10]]}},"alternative-id":["10.1145\/3729248"],"URL":"https:\/\/doi.org\/10.1145\/3729248","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,6,10]]},"assertion":[{"value":"2024-11-14","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"}}]}}