{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,24]],"date-time":"2026-08-24T17:24:36Z","timestamp":1787592276758,"version":"build-2736575974"},"reference-count":45,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T00:00:00Z","timestamp":1744156800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"funder":[{"name":"Samsung Research Funding Center of Samsung Electronics","award":["SRFC-IT2102-03"],"award-info":[{"award-number":["SRFC-IT2102-03"]}]},{"DOI":"10.13039\/501100003725","name":"National Research Foundation of Korea","doi-asserted-by":"publisher","award":["RS-2024-00347786"],"award-info":[{"award-number":["RS-2024-00347786"]}],"id":[{"id":"10.13039\/501100003725","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,4,9]]},"abstract":"<jats:p>Concurrent separation logic (CSL) has excelled in verifying safety properties across various applications, yet its application to liveness properties remains limited. While existing approaches like TaDA Live and Fair Operational Semantics (FOS) have made significant strides, they still face limitations. TaDA Live struggles to verify certain classes of programs, particularly concurrent objects with non-local linearization points, and lacks support for general liveness properties such as \u201cgood things happen infinitely often\u201d. On the other hand, FOS's scalability is hindered by the absence of thread modular reasoning principles and modular specifications.<\/jats:p>\n                  <jats:p>This paper introduces Lilo, a higher-order, relational CSL designed to overcome these limitations. Our core observation is that FOS helps us to maintain simple primitives for our logic, which enable us to explore design space with fewer restrictions. As a result, Lilo adapts various successful techniques from literature. It supports reasoning about non-terminating programs by supporting refinement proofs, and also provides Iris-style invariants and modular specifications to facilitate modular verification. To support higher-order reasoning without relying on step-indexing, we develop a technique called stratified propositions inspired by Nola. In particular, we develop novel abstractions for liveness reasoning that bring these techniques together in a uniform way. We show Lilo\u2019s scalability through case studies, including the first termination-guaranteeing modular verification of the elimination stack. Lilo and examples in this paper are mechanized in Coq.<\/jats:p>","DOI":"10.1145\/3720525","type":"journal-article","created":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T13:48:26Z","timestamp":1744206506000},"page":"1267-1294","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Lilo: A Higher-Order, Relational Concurrent Separation Logic for Liveness"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2576-1220","authenticated-orcid":false,"given":"Dongjae","family":"Lee","sequence":"first","affiliation":[{"name":"MIT, CSAIL, Cambridge, USA"},{"name":"Seoul National University, Seoul, 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-0035-4077","authenticated-orcid":false,"given":"Taeyoung","family":"Yoon","sequence":"additional","affiliation":[{"name":"Seoul National University, Seoul, Republic of Korea"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6684-0921","authenticated-orcid":false,"given":"Minki","family":"Cho","sequence":"additional","affiliation":[{"name":"Seoul National University, Seoul, Republic of Korea"},{"name":"FuriosaAI, Seoul, 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"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1656-0913","authenticated-orcid":false,"given":"Chung-Kil","family":"Hur","sequence":"additional","affiliation":[{"name":"Seoul National University, Seoul, Republic of Korea"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,4,9]]},"reference":[{"key":"e_1_3_1_2_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01782772"},{"key":"e_1_3_1_3_2","volume-title":"Modelling, Controlling and Reasoning About State, Proceedings of Dagstuhl Seminar 10351 (modelling, controlling and reasoning about state, proceedings of dagstuhl seminar 10351","author":"Benton Nick","year":"2010","unstructured":"Nick Benton and Chung-Kil Hur. 2010. Step-Indexing: The good, the bad and the Ugly. In Modelling, Controlling and Reasoning About State, Proceedings of Dagstuhl Seminar 10351 (modelling, controlling and reasoning about state, proceedings of dagstuhl seminar 10351 ed.). Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany. https:\/\/www.microsoft.com\/en-us\/research\/publication\/step-indexing-the-good-the-bad-and-the-ugly\/ An earlier version of this work was presented at the Workshop on Syntax and Semantics of Low-Level Languages (LOLA) in July 2010."},{"key":"e_1_3_1_4_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.034"},{"key":"e_1_3_1_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411226"},{"key":"e_1_3_1_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/3622857"},{"key":"e_1_3_1_7_2","unstructured":"Pedro da Rocha Pinto. 2016. Reasoning with time and data abstractions. Ph. D. Dissertation. Imperial College London UK."},{"key":"e_1_3_1_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44202-9_9"},{"key":"e_1_3_1_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523451"},{"key":"e_1_3_1_10_2","doi-asserted-by":"publisher","DOI":"10.1145\/3477082"},{"key":"e_1_3_1_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/3428224"},{"key":"e_1_3_1_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209174"},{"key":"e_1_3_1_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/3498689"},{"key":"e_1_3_1_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/3498689"},{"key":"e_1_3_1_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/1007912.1007944"},{"key":"e_1_3_1_16_2","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926402"},{"key":"e_1_3_1_17_2","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103666"},{"key":"e_1_3_1_18_2","unstructured":"Iris Team. 2024. Iris examples. https:\/\/gitlab.mpi-sws.org\/iris\/examples"},{"key":"e_1_3_1_19_2","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"},{"key":"e_1_3_1_20_2","doi-asserted-by":"publisher","DOI":"10.1145\/3158154"},{"key":"e_1_3_1_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951943"},{"key":"e_1_3_1_22_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_1_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/3371113"},{"key":"e_1_3_1_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/2775051.2676980"},{"key":"e_1_3_1_25_2","doi-asserted-by":"publisher","unstructured":"Bernhard Kragl and Shaz Qadeer. 2021. The Civl Verifier. In 2021 Formal Methods in Computer Aided Design (FMCAD). 143-152. doi:10.34727\/2021\/isbn.978-3-85448-046-4_23","DOI":"10.34727\/2021\/isbn.978-3-85448-046-4_23"},{"key":"e_1_3_1_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009855"},{"key":"e_1_3_1_27_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-44914-8_13"},{"key":"e_1_3_1_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/3591253"},{"key":"e_1_3_1_29_2","doi-asserted-by":"publisher","unstructured":"Dongjae Lee Janggun Lee Taeyoung Yoon Minki Cho Jeehoon Kang and Chung-Kil Hur. 2025. Artifact for Lilo: A Higher-Order Relational Concurrent Separation Logic for Liveness. doi:10.5281\/zenodo.14927742","DOI":"10.5281\/zenodo.14927742"},{"key":"e_1_3_1_30_2","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837635"},{"key":"e_1_3_1_31_2","doi-asserted-by":"publisher","DOI":"10.1145\/3158108"},{"key":"e_1_3_1_32_2","unstructured":"Yusuke Matsushita. 2023. Non-Step-Indexed Separation Logic with Invariants and Rust-Style Borrows. Ph. D. Dissertation. University of Tokyo."},{"key":"e_1_3_1_33_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17184-1_1"},{"key":"e_1_3_1_34_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.035"},{"key":"e_1_3_1_35_2","doi-asserted-by":"publisher","DOI":"10.1145\/3656384"},{"key":"e_1_3_1_36_2","doi-asserted-by":"publisher","DOI":"10.1145\/960116.54010"},{"key":"e_1_3_1_37_2","doi-asserted-by":"publisher","DOI":"10.1145\/3427761.3428345"},{"key":"e_1_3_1_38_2","doi-asserted-by":"publisher","DOI":"10.1145\/3600006.3613172"},{"key":"e_1_3_1_39_2","doi-asserted-by":"publisher","DOI":"10.1145\/3571232"},{"key":"e_1_3_1_40_2","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454031"},{"key":"e_1_3_1_41_2","doi-asserted-by":"publisher","DOI":"10.1145\/3547631"},{"key":"e_1_3_1_42_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_9"},{"key":"e_1_3_1_43_2","doi-asserted-by":"crossref","unstructured":"Kasper Svendsen Lars Birkedal and Matthew J. Parkinson. 2013. Modular Reasoning about Separation for Concurrent Data Structures. In Proceedings of ESOP (proceedings of esop ed.). https:\/\/www.microsoft.com\/en-us\/research\/publication\/modular-reasoning-about-separation-for-concurrent-data-structures\/","DOI":"10.1007\/978-3-642-37036-6_11"},{"key":"e_1_3_1_44_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_34"},{"key":"e_1_3_1_45_2","doi-asserted-by":"publisher","DOI":"10.1145\/3632851"},{"key":"e_1_3_1_46_2","unstructured":"R. K. Treiber. 1986. Systems programming: coping with parallelism."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3720525","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3720525","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,8,24]],"date-time":"2026-08-24T16:29:44Z","timestamp":1787588984000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3720525"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,4,9]]},"references-count":45,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2025,4,9]]}},"alternative-id":["10.1145\/3720525"],"URL":"https:\/\/doi.org\/10.1145\/3720525","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,4,9]]},"assertion":[{"value":"2024-10-16","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-02-18","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-04-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}