{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T08:55:17Z","timestamp":1770281717787,"version":"3.49.0"},"reference-count":48,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T00:00:00Z","timestamp":1718841600000},"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":[[2024,6,20]]},"abstract":"<jats:p>\n            Linearizability is the de facto standard for correctness of concurrent objects\u2013it essentially says that all the object\u2019s operations behave as if they were atomic. There have been a number of recent advances in developing increasingly strong linearizability specifications for relaxed memory consistency (RMC), but scalable\n            <jats:italic toggle=\"yes\">proof methods<\/jats:italic>\n            for these specifications do not exist due to the challenges arising from out-of-order executions (requiring event reordering) and selected synchronization (requiring tracking of view transfers).\n          <\/jats:p>\n          <jats:p>\n            We propose a proof recipe for the\n            <jats:italic toggle=\"yes\">linearizable history specifications<\/jats:italic>\n            by\n            <jats:xref ref-type=\"bibr\">Dang et al<\/jats:xref>\n            . in the Iris-based iRC11 concurrent separation logic in Coq. Key to our proof recipe is the notion of\n            <jats:italic toggle=\"yes\">object modification order (OMO)<\/jats:italic>\n            , which generalizes the modification order of the C11 memory model to an object-local setting. Using OMO we minimize the conditions that need to be proved for event reordering. To enable proof reuse for concurrent libraries that are built on top of others, OMO provides the novel notion of a\n            <jats:italic toggle=\"yes\">commit-with relation<\/jats:italic>\n            that connects the linearization points of the lower and upper libraries. Using our recipe, we verify the linearizability of the Michael\u2013Scott queue, the elimination stack, and Folly\u2019s MPMC queue in RMC for the first time; and verify stronger specifications of a spinlock and atomic reference counting in RMC than prior work.\n          <\/jats:p>","DOI":"10.1145\/3656384","type":"journal-article","created":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T16:27:20Z","timestamp":1718900840000},"page":"175-198","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["A Proof Recipe for Linearizability in Relaxed Memory Separation Logic"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0009-0000-5380-1969","authenticated-orcid":false,"given":"Sunho","family":"Park","sequence":"first","affiliation":[{"name":"KAIST, Daejeon, South Korea"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-3800-9879","authenticated-orcid":false,"given":"Jaewoo","family":"Kim","sequence":"additional","affiliation":[{"name":"KAIST, Daejeon, South Korea"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9926-9736","authenticated-orcid":false,"given":"Ike","family":"Mulder","sequence":"additional","affiliation":[{"name":"Radboud University Nijmegen, Nijmegan, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6099-2644","authenticated-orcid":false,"given":"Jaehwang","family":"Jung","sequence":"additional","affiliation":[{"name":"KAIST, Daejeon, South Korea"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-0047-7717","authenticated-orcid":false,"given":"Janggun","family":"Lee","sequence":"additional","affiliation":[{"name":"KAIST, Daejeon, South Korea"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1185-5237","authenticated-orcid":false,"given":"Robbert","family":"Krebbers","sequence":"additional","affiliation":[{"name":"Radboud University Nijmegen, Nijmegan, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2115-0871","authenticated-orcid":false,"given":"Jeehoon","family":"Kang","sequence":"additional","affiliation":[{"name":"KAIST, Daejeon, South Korea"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,6,20]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2480359.2429099"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926394"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","unstructured":"John Bender and Jens Palsberg. 2019. A formalization of Java\u2019s concurrent access modes. PACMPL 3 OOPSLA Article 142 (2019). https:\/\/doi.org\/10.1145\/3360568 10.1145\/3360568","DOI":"10.1145\/3360568"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473586"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","unstructured":"Stephen D. Brookes. 2004. A Semantics for Concurrent Separation Logic. In CONCUR (LNCS Vol. 3170). 16-34. https:\/\/doi.org\/10.1007\/978-3-540-28644-8_2 10.1007\/978-3-540-28644-8_2","DOI":"10.1007\/978-3-540-28644-8_2"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","unstructured":"Stephen D. Brookes and William C. Rounds. 1983. Behavioural equivalence relations induced by programming logics. In ICALP (LNCS Vol. 154). 97-108. https:\/\/doi.org\/10.1007\/BFB0036900 10.1007\/BFB0036900","DOI":"10.1007\/BFB0036900"},{"key":"e_1_3_1_8_1","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-231. https:\/\/doi.org\/10.1007\/978-3-662-44202-9_9 10.1007\/978-3-662-44202-9_9","DOI":"10.1007\/978-3-662-44202-9_9"},{"key":"e_1_3_1_9_1","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). https:\/\/doi.org\/10.1145\/3371102 10.1145\/3371102","DOI":"10.1145\/3371102"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523451"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","unstructured":"Marko Doko and Viktor Vafeiadis. 2016. A Program Logic for C11 Memory Fences. In VMCAI (LNCS Vol. 9583). 413-430 https:\/\/doi.org\/10.1007\/978-3-662-49122-5_20 10.1007\/978-3-662-49122-5_20","DOI":"10.1007\/978-3-662-49122-5_20"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_17"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192421"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","unstructured":"Brijesh Dongol Radha Jagadeesan James Riely and Alasdair Armstrong. 2018. On abstraction and compositionality for weak-memory linearisability. In VMCAI (LNCS Vol. 10747). 183-204. https:\/\/doi.org\/10.1007\/978-3-319-73721-8_9 10.1007\/978-3-319-73721-8_9","DOI":"10.1007\/978-3-319-73721-8_9"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2010.09.021"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","unstructured":"Danny Hendler Nir Shavit and Lena Yerushalmi. 2004. A scalable lock-free stack algorithm. In SPAA. 206-215. https:\/\/doi.org\/10.1145\/1007912.1007944 10.1145\/1007912.1007944","DOI":"10.1145\/1007912.1007944"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","unstructured":"Maurice P. Herlihy and Jeannette M. Wing. 1990. Linearizability: A Correctness Condition for Concurrent Objects. TOPLAS 12 3 (1990) 463-492. https:\/\/doi.org\/10.1145\/78969.78972 10.1145\/78969.78972","DOI":"10.1145\/78969.78972"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","unstructured":"Ralf Jung Robbert Krebbers Lars Birkedal and Derek Dreyer. 2016. Higher-order ghost state. In ICFP. 256-269. https:\/\/doi.org\/10.1145\/2951913.2951943 10.1145\/2951913.2951943","DOI":"10.1145\/2951913.2951943"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_1_20_1","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). https:\/\/doi.org\/10.1145\/3371113 10.1145\/3371113","DOI":"10.1145\/3371113"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2775051.2676980"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3093333.3009850"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314609"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","unstructured":"Robbert Krebbers Jacques-Henri Jourdan Ralf Jung Joseph Tassarotti Jan-Oliver Kaiser Amin Timany Arthur Chargu\u00e9raud and Derek Dreyer. 2018. MoSeL: a general extensible modal framework for interactive proofs in separation logic. PACMPL 2 ICFP (2018) 77:1-77:30. https:\/\/doi.org\/10.1145\/3236772 10.1145\/3236772","DOI":"10.1145\/3236772"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","unstructured":"Robbert Krebbers Ralf Jung Ales Bizjak Jacques-Henri Jourdan Derek Dreyer and Lars Birkedal. 2017a. The Essence of Higher-Order Concurrent Separation Logic. In ESOP (LNCS Vol. 10201). 696-723. https:\/\/doi.org\/10.1007\/978-3-662-54434-1_26 10.1007\/978-3-662-54434-1_26","DOI":"10.1007\/978-3-662-54434-1_26"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009855"},{"key":"e_1_3_1_27_1","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). https:\/\/doi.org\/10.1145\/3158125 10.1145\/3158125","DOI":"10.1145\/3158125"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062352"},{"key":"e_1_3_1_29_1","unstructured":"Meta. 2023. Folly: Facebook Open-source Library. https:\/\/github.com\/facebook\/folly"},{"key":"e_1_3_1_30_1","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). https:\/\/doi.org\/10.1145\/3473571 10.1145\/3473571","DOI":"10.1145\/3473571"},{"key":"e_1_3_1_31_1","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). https:\/\/doi.org\/10.1145\/3408978 10.1145\/3408978","DOI":"10.1145\/3408978"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","unstructured":"Roland Meyer Thomas Wies and Sebastian Wolff. 2022. A Concurrent Program Logic with a Future and History. PACMPL 6 OOPSLA2 Article 174 (2022). https:\/\/doi.org\/10.1145\/3563337 10.1145\/3563337","DOI":"10.1145\/3563337"},{"key":"e_1_3_1_33_1","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). https:\/\/doi.org\/10.1145\/3591296 10.1145\/3591296","DOI":"10.1145\/3591296"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/248052.248106"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","unstructured":"Ike Mulder and Robbert Krebbers. 2023. Proof Automation for Linearizability in Separation Logic. PACMPL 7 OOPSLA1 (2023) 91:462-91:491. https:\/\/doi.org\/10.1145\/3586043 10.1145\/3586043","DOI":"10.1145\/3586043"},{"key":"e_1_3_1_36_1","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-824. https:\/\/doi.org\/10.1145\/3519939.3523432 10.1145\/3519939.3523432","DOI":"10.1145\/3519939.3523432"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","unstructured":"Peter M\u00fcller Malte Schwerhoff and Alexander J. Summers. 2017. Viper: A verification infrastructure for permission-based reasoning. 104-125. https:\/\/doi.org\/10.3233\/978-1-61499-810-5-104 10.3233\/978-1-61499-810-5-104","DOI":"10.3233\/978-1-61499-810-5-104"},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","unstructured":"Peter W. O\u2019Hearn. 2004. Resources Concurrency and Local Reasoning. In CONCUR (LNCS Vol. 3170). 49-67. https:\/\/doi.org\/10.1007\/978-3-540-28644-8_4 10.1007\/978-3-540-28644-8_4","DOI":"10.1007\/978-3-540-28644-8_4"},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.10933398"},{"key":"e_1_3_1_40_1","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). https:\/\/doi.org\/10.1145\/3290381 10.1145\/3290381","DOI":"10.1145\/3290381"},{"key":"e_1_3_1_41_1","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). https:\/\/doi.org\/10.1145\/3571246 10.1145\/3571246","DOI":"10.1145\/3571246"},{"key":"e_1_3_1_42_1","doi-asserted-by":"publisher","unstructured":"Graeme Smith Kirsten Winter and Robert J. Colvin. 2020. Linearizability on Hardware Weak Memory Models. Form. Asp. Comput. 32 1 (2020) 1-32. https:\/\/doi.org\/10.1007\/s00165-019-00499-8 10.1007\/s00165-019-00499-8","DOI":"10.1007\/s00165-019-00499-8"},{"key":"e_1_3_1_43_1","doi-asserted-by":"publisher","unstructured":"Alexander J. Summers and Peter M\u00fcller. 2018. Automating Deductive Verification for Weak-Memory Programs. In TACAS (LNCS Vol. 10805). 190-209. https:\/\/doi.org\/10.1007\/978-3-319-89960-2_11 10.1007\/978-3-319-89960-2_11","DOI":"10.1007\/978-3-319-89960-2_11"},{"key":"e_1_3_1_44_1","volume-title":"Systems Programming: Coping with Parallelism","author":"Treiber R.K.","year":"1986","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_1_45_1","doi-asserted-by":"publisher","unstructured":"Viktor Vafeiadis. 2010. Automatically Proving Linearizability. In CAV (LNCS Vol. 6174). 450-464. https:\/\/doi.org\/10.1007\/978-3-642-14295-6_40 10.1007\/978-3-642-14295-6_40","DOI":"10.1007\/978-3-642-14295-6_40"},{"key":"e_1_3_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509532"},{"key":"e_1_3_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3437992.3439930"},{"key":"e_1_3_1_48_1","doi-asserted-by":"publisher","unstructured":"Felix A. Wolf Malte Schwerhoff and Peter M\u00fcller. 2021. Concise Outlines for a Complex Logic: A Proof Outline Checker for TaDA. In FM (LNCS Vol. 13047). 407-426. https:\/\/doi.org\/10.1007\/978-3-030-90870-6_22 10.1007\/978-3-030-90870-6_22","DOI":"10.1007\/978-3-030-90870-6_22"},{"key":"e_1_3_1_49_1","doi-asserted-by":"publisher","unstructured":"He Zhu Gustavo Petri and Suresh Jagannathan. 2015. Poling: SMT Aided Linearizability Proofs. In CAV (LNCS Vol. 9207). 3-19. https:\/\/doi.org\/10.1007\/978-3-319-21668-3_1 10.1007\/978-3-319-21668-3_1","DOI":"10.1007\/978-3-319-21668-3_1"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656384","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3656384","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:43:44Z","timestamp":1751661824000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656384"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,6,20]]},"references-count":48,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2024,6,20]]}},"alternative-id":["10.1145\/3656384"],"URL":"https:\/\/doi.org\/10.1145\/3656384","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,6,20]]},"assertion":[{"value":"2024-06-20","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}