{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T11:06:15Z","timestamp":1784199975826,"version":"3.55.0"},"reference-count":54,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","funder":[{"name":"IITP","award":["RS-2024-00459026, IITP-2025-RS-2023-00256472, IITP-2025-RS-2020-II201795"],"award-info":[{"award-number":["RS-2024-00459026, IITP-2025-RS-2023-00256472, 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                    Hazard pointers (HP) is one of the earliest manual memory reclamation algorithms for concurrent data structures. It is widely used for its robustness: memory overhead is bounded (\n                    <jats:italic toggle=\"yes\">e.g<\/jats:italic>\n                    ., by the number of threads). To access a node, threads first announce the protection of\n                    <jats:italic toggle=\"yes\">each<\/jats:italic>\n                    to-be-accessed node, which prevents its reclamation. After announcement, they validate the node\u2019s reachability from the root to ensure that no threads have missed the announcement and reclaimed it. Traversal-based data structures typically use a marking-based validation strategy. This strategy uses a node\u2019s mark to indicate whether the node is to be detached. Unmarked nodes are considered safe to traverse as both the node and its successors are still reachable, while marked nodes are considered unsafe. However, this strategy is inapplicable to the efficient\n                    <jats:italic toggle=\"yes\">optimistic traversal<\/jats:italic>\n                    strategy that skips over marked nodes.\n                  <\/jats:p>\n                  <jats:p>\n                    We propose a new validation strategy for HP that supports lock-free data structures with optimistic traversal, such as lists, trees, and skip lists. The key idea is to exploit the\n                    <jats:italic toggle=\"yes\">immutability<\/jats:italic>\n                    of marked nodes, and validate their reachability at once by checking the reachability of the\n                    <jats:italic toggle=\"yes\">most recent unmarked node<\/jats:italic>\n                    . To ensure correctness, we prove the safety of Harris\u2019s list protected with the new strategy in Rocq using the Iris separation logic framework. We show that the new strategy\u2019s performance is competitive with state-of-the-art reclamation algorithms when applied to data structures with optimistic traversal, while remaining simple and robust.\n                  <\/jats:p>","DOI":"10.1145\/3729247","type":"journal-article","created":{"date-parts":[[2025,6,13]],"date-time":"2025-06-13T16:02:27Z","timestamp":1749830547000},"page":"26-47","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Leveraging Immutability to Validate Hazard Pointers for Optimistic Traversals"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0009-0002-0047-7717","authenticated-orcid":false,"given":"Janggun","family":"Lee","sequence":"first","affiliation":[{"name":"KAIST, Daejeon, Republic of Korea"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-7070-3578","authenticated-orcid":false,"given":"Jeonghyeon","family":"Kim","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\/3453483.3454060"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523730"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","unstructured":"TrevorBrown FaithEllen and EricRuppert.2014. A General Technique for Non-Blocking Trees. SIGPLAN Not. 49 8 (feb 2014) 329\u2013342. doi:10.1145\/2692916.2555267","DOI":"10.1145\/2692916.2555267"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/2767386.2767436"},{"key":"e_1_3_2_6_2","unstructured":"Windows Dev Center. 2025. FlushProcessWriteBuffers function. https:\/\/docs.microsoft.com\/en-us\/windows\/desktop\/api\/processthreadsapi\/nf-processthreadsapi-flushprocesswritebuffers"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/2814270.2814298"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1109\/TPDS.2011.159"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/2926697.2926699"},{"key":"e_1_3_2_10_2","unstructured":"DaveDice HuiHuang and MingyaoYang.2001. Asymmetric Dekker Synchronization. http:\/\/web.archive.org\/web\/20080220051535\/http:\/\/blogs.sun.com\/dave\/resource\/Asymmetric-Dekker-Synchronization.txt"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","unstructured":"DanaDrachsler MartinVechev and EranYahav.2014. Practical Concurrent Binary Search Trees via Logical Ordering. SIGPLAN Not. 49 8 (feb 2014) 343\u2013356. doi:10.1145\/2692916.2555269","DOI":"10.1145\/2692916.2555269"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/2611462.2611486"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/1835698.1835736"},{"key":"e_1_3_2_14_2","unstructured":"JasonEvans.2006. A scalable concurrent malloc (3) implementation for FreeBSD."},{"key":"e_1_3_2_15_2","unstructured":"KeirFraser.2004. Practical lock-freedom. Ph. D. Dissertation. University of Cambridge Computer Laboratory."},{"key":"e_1_3_2_16_2","unstructured":"DavidGoldblatt.2022.P1202R5: Asymmetric Fences. https:\/\/wg21.link\/p1202r5."},{"key":"e_1_3_2_17_2","first-page":"300","volume-title":"In Proceedings of the 15th International Conference on Distributed Computing (DISC\u201901)","author":"Timothy L.Harris","year":"2001","unstructured":"TimothyL.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_18_2","doi-asserted-by":"crossref","first-page":"313","DOI":"10.1007\/978-3-642-25873-2_22","volume-title":"In Principles of Distributed Systems","author":"Maurice Herlihy","year":"2011","unstructured":"MauriceHerlihyand NirShavit.2011. On the Nature of Progress. In Principles of Distributed Systems, AntonioFern\u00e0ndez Anta,GiuseppeLipari,and MatthieuRoy(Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 313\u2013328."},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","unstructured":"MauriceP.Herlihyand JeannetteM.Wing. 1990. Linearizability: A Correctness Condition for Concurrent Objects. ACM Trans. Program. Lang. Syst. 12 3 (July 1990) 463\u2013492. doi:10.1145\/78969.78972","DOI":"10.1145\/78969.78972"},{"key":"e_1_3_2_20_2","volume-title":"Lock-free internal binary search trees with memory management","author":"Shane V.Howley","year":"2012","unstructured":"ShaneV.Howley. 2012. Lock-free internal binary search trees with memory management. Ph. D. Dissertation. Trinity CollegeDublin, Ireland. https:\/\/hdl.handle.net\/2262\/77623"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/2312005.2312036"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","unstructured":"JaehwangJung JeonghyeonKim MatthewJ.Parkinson and JeehoonKang.2024. Concurrent Immediate Reference Counting. Proc. ACM Program. Lang. 8 PLDI Article 153 (June 2024) 24 pages. doi:10.1145\/3656383","DOI":"10.1145\/3656383"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","unstructured":"JaehwangJung JanggunLee JaeminChoi JaewooKim SunhoPark and JeehoonKang.2023. Modular Verification of Safe Memory Reclamation in Concurrent Separation Logic. Proc. ACM Program. Lang. 7 OOPSLA2 Article 251(oct 2023) 29 pages. doi:10.1145\/3622827","DOI":"10.1145\/3622827"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/3558481.3591102"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","unstructured":"RalfJung RobbertKrebbers Jacques-HenriJourdan AlesBizjak LarsBirkedal and DerekDreyer.2018. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. f. Funct. Program. 28(2018) e20. doi:10.1017\/S0956796818000151","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","unstructured":"RalfJung DavidSwasey FilipSieczkowski KasperSvendsen AaronTuron LarsBirkedal and DerekDreyer.2015. Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages POPL 2015 Mumbai India January 15-17 2015. ACM 637\u2013650. doi:10.1145\/2676726.2676980","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385978"},{"key":"e_1_3_2_28_2","unstructured":"MaxKhizhinsky.2024.CDS C++ library. https:\/\/github.com\/khizmax\/libcds."},{"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":"RobbertKrebbers AminTimany and LarsBirkedal.2017. Interactive proofs in higher-order concurrent separation logic. SIGPLAN Not. 52 1 (Jan. 2017) 205\u2013217. doi:10.1145\/3093333.3009855","DOI":"10.1145\/3093333.3009855"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","unstructured":"JanggunLee JeonghyeonKim and JeehoonKang.2025. Leveraging Immutability to Validate Hazard Pointers for Optimistic Traversals (artifact and appendix). doi:10.5281\/zenodo. 15183251 Project webpage: https:\/\/cp.kaist.ac.kr\/gc.","DOI":"10.5281\/zenodo"},{"key":"e_1_3_2_32_2","unstructured":"Linux Programmer\u2019s Manual. 2025.membarrier(2) - Linux manual page. http:\/\/man7.org\/linux\/man-pages\/man2\/membarrier.2.html"},{"key":"e_1_3_2_33_2","unstructured":"Linux Programmer\u2019s Manual. 2025. signal(7) - Linux manual page. https:\/\/man7.org\/linux\/man-pages\/man7\/signal.7.html"},{"key":"e_1_3_2_34_2","unstructured":"P. E.McKenneyand J. D.Slingwine.1998. Read-copy update: Using execution history to solve concurrency problems. In PDCS\u201998."},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1145\/564870.564881"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1145\/571825.571829"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","unstructured":"MagedM. Michael.2004. Hazard Pointers: Safe Memory Reclamation for Lock-Free Objects. IEEE Trans. Parallel Distrib. Syst. 15 6 (June 2004) 491\u2013504. doi:10.1109\/TPDS.2004.8","DOI":"10.1109\/TPDS.2004.8"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1145\/3382734.3405738"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","DOI":"10.1145\/248052.248106"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.1145\/2555243.2555256"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","unstructured":"AravindNatarajan ArunmoezhiRamachandran and NeerajMittal.2020. FEAST: A Lightweight Lock-free Concurrent Binary Search Tree. ACM Trans. Parallel Comput. 7 2 Article 10 (May 2020) 64 pages. doi:10.1145\/3391438","DOI":"10.1145\/3391438"},{"key":"e_1_3_2_42_2","doi-asserted-by":"crossref","unstructured":"RuslanNikolaevand BinoyRavindran.2020. Universal Wait-Free Memory Reclamation. Association for Computing Machinery New York NY USA 130\u2013143. https:\/\/doi.org\/10.1145\/3332466.3374540","DOI":"10.1145\/3332466.3374540"},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","unstructured":"RuslanNikolaevand BinoyRavindran.2021. Snapshot-Free Transparent and Robust Memory Reclamation for LockFree Data Structures. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (Virtual Canada) (PLDI 2021). Association for Computing Machinery New York NY USA 987\u20131002. doi:10.1145\/3453483.3454090","DOI":"10.1145\/3453483.3454090"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","unstructured":"RuslanNikolaevand BinoyRavindran.2024. A Family of Fast and Memory Efficient Lock- and Wait-Free Reclamation. Proc. ACM Program. Lang. 8 PLDI Article 235 (June 2024) 25 pages. doi:10.1145\/3658851","DOI":"10.1145\/3658851"},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","unstructured":"MatthewParkinson DimitriosVytiniotis KapilVaswani ManuelCosta PantazisDeligiannis DylanMcDermott AaronBlankstein and JonathanBalkind.2017. Project Snowflake: Non-Blocking Safe Manual Memory Management in.NET. Proc. ACM Program. Lang. 1 OOPSLA Article 95 (oct 2017) 25 pages.doi:10.1145\/3141879","DOI":"10.1145\/3141879"},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","DOI":"10.1145\/2684464.2684472"},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","DOI":"10.1145\/3087556.3087588"},{"key":"e_1_3_2_48_2","unstructured":"NirN Shavit YosefLev and MauriceP Herlihy.2011. Concurrent lock-free skiplist with wait-free contains operator. https:\/\/patentcenter.uspto.gov\/applications\/12191008USPatent7 937 378."},{"key":"e_1_3_2_49_2","doi-asserted-by":"publisher","unstructured":"GaliSheffi MauriceHerlihy and ErezPetrank.2021. VBR: Version Based Reclamation. In 35th International Symposium on Distributed Computing (DISC 2021) (Leibniz International Proceedings in Informatics (LIPIcs) Vol. 209) SethGilbert(Ed.). Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik Dagstuhl Germany 35:1\u201335:18. doi:10.4230\/LIPIcs.DISC.2021.35","DOI":"10.4230\/LIPIcs.DISC.2021.35"},{"key":"e_1_3_2_50_2","unstructured":"GaliSheffiand ErezPetrank.2022. The ERA Theorem for Safe Memory Reclamation. arXiv:2211.04351[cs.DC]https:\/\/arxiv.org\/abs\/2211.04351"},{"key":"e_1_3_2_51_2","doi-asserted-by":"publisher","DOI":"10.1145\/3583668.3594564"},{"key":"e_1_3_2_52_2","doi-asserted-by":"publisher","DOI":"10.1145\/3437801.3441625"},{"key":"e_1_3_2_53_2","doi-asserted-by":"publisher","DOI":"10.1145\/3503221.3508441"},{"key":"e_1_3_2_54_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_55_2","doi-asserted-by":"publisher","DOI":"10.1145\/3178487.3178488"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3729247","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T10:07:16Z","timestamp":1784196436000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3729247"}},"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\/3729247"],"URL":"https:\/\/doi.org\/10.1145\/3729247","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,6,10]]},"assertion":[{"value":"2024-11-13","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"}}]}}