{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T08:55:05Z","timestamp":1770281705347,"version":"3.49.0"},"reference-count":39,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2024,10,8]],"date-time":"2024-10-08T00:00:00Z","timestamp":1728345600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["2313433, 2019285, 1763399"],"award-info":[{"award-number":["2313433, 2019285, 1763399"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Defense Advanced Research Projects Agency and Naval Information Warfare Center Pacific","award":["N66001-21-C-4018"],"award-info":[{"award-number":["N66001-21-C-4018"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,10,8]]},"abstract":"<jats:p>\n                    Crash-safety is an important property of real systems, as the main functionality of some systems is resilience to crashes. Toward a compositional verification approach for crash-safety under full-system crashes, one observes that crashes propagate instantaneously to all components across all levels of abstraction, even to unspecified components, hindering compositionality. Furthermore, in the presence of concurrency, a correctness criterion that addresses both crashes\n                    <jats:italic toggle=\"yes\">and<\/jats:italic>\n                    concurrency proves necessary. For this, several adaptations of linearizability have been suggested, each featuring different trade-offs between complexity and expressiveness. The recently proposed compositional linearizability framework shows that to achieve compositionality with linearizability, both a locality and observational refinement property are necessary. Despite that, no linearizability criterion with crashes has been proven to support an observational refinement property.\n                  <\/jats:p>\n                  <jats:p>\n                    In this paper, we define a compositional model of concurrent computation with full-system crashes. We use this model to develop a compositional theory of linearizability with crashes, which reveals a criterion,\n                    <jats:italic toggle=\"yes\">crash-aware linearizability<\/jats:italic>\n                    , as its inherent notion of linearizability and supports both locality and observational refinement. We then show that strict linearizability and durable linearizability factor through crash-aware linearizability as two different ways of translating between concurrent computation with and without crashes, enabling simple proofs of locality and observational refinement for a generalization of these two criteria. Then, we show how the theory can be connected with a program logic for durable and crash-aware linearizability, which gives the first program logic that verifies a form of linearizability with crashes. We showcase the advantages of compositionality by verifying a library facilitating programming persistent data structures and a fragment of a transactional interface for a file system.\n                  <\/jats:p>","DOI":"10.1145\/3689792","type":"journal-article","created":{"date-parts":[[2024,10,8]],"date-time":"2024-10-08T03:23:04Z","timestamp":1728357784000},"page":"2296-2324","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Compositionality and Observational Refinement for Linearizability with Crashes"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1091-7560","authenticated-orcid":false,"given":"Arthur","family":"Oliveira Vale","sequence":"first","affiliation":[{"name":"Yale University, New Haven, USA"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-4494-0486","authenticated-orcid":false,"given":"Zhongye","family":"Wang","sequence":"additional","affiliation":[{"name":"Yale University, New Haven, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8659-8493","authenticated-orcid":false,"given":"Yixuan","family":"Chen","sequence":"additional","affiliation":[{"name":"Yale University, New Haven, USA"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-8035-5209","authenticated-orcid":false,"given":"Peixin","family":"You","sequence":"additional","affiliation":[{"name":"Yale University, New Haven, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8184-7649","authenticated-orcid":false,"given":"Zhong","family":"Shao","sequence":"additional","affiliation":[{"name":"Yale University, New Haven, USA"}]}],"member":"320","published-online":{"date-parts":[[2024,10,8]]},"reference":[{"key":"e_1_3_1_2_2","first-page":"1","volume-title":"Computational Logic","author":"Abramsky Samson","year":"1999","unstructured":"Samson Abramsky and Guy McCusker. 1999. Game Semantics. In Computational Logic,Ulrich Berger and Helmut Schwichtenberg (Eds.). Springer Berlin Heidelberg,Berlin, Heidelberg,1\u201355. https:\/\/doi.org\/10.1007\/978-3-642-58622-4_1 10.1007\/978-3-642-58622-4_1"},{"key":"e_1_3_1_3_2","article-title":"Strict linearizability and the power of aborting","author":"Aguilera Marcos K","year":"2003","unstructured":"Marcos K Aguilera and Svend Fr\u00f8lund. 2003. Strict linearizability and the power of aborting. Technical Report HPL-2003-241 (2003).","journal-title":"Technical Report HPL-2003-241"},{"key":"e_1_3_1_4_2","first-page":"41:1","volume-title":"36th International Symposium on Distributed Computing (DISC 2022) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 246),","author":"Ben-David Naama","year":"2022","unstructured":"Naama Ben-David,Michal Friedman, and Yuanhao Wei. 2022. Brief Announcement: Survey of Persistent Memory Correctness Conditions. In 36th International Symposium on Distributed Computing (DISC 2022) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 246), Christian Scheideler (Ed.). Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik,Dagstuhl, Germany,41:1\u201341:4. https:\/\/doi.org\/10.4230\/LIPIcs.DISC.2022.41 10.4230\/LIPIcs.DISC.2022.41"},{"key":"e_1_3_1_5_2","first-page":"20:1","volume-title":"19th International Conference on Principles of Distributed Systems (OPODIS 2015) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 46)","author":"Berryhill Ryan","year":"2016","unstructured":"Ryan Berryhill,Wojciech Golab, and Mahesh Tripunitara. 2016. Robust Shared Objects for Non-Volatile Main Memory. In 19th International Conference on Principles of Distributed Systems (OPODIS 2015) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 46),Emmanuelle Anceaume,Christian Cachin, and Maria Potop-Butucaru (Eds.). Schloss Dagstuhl,Dagstuhl, Germany,20:1\u201320:17. https:\/\/doi.org\/10.4230\/LIPIcs.OPODIS.2015.20 10.4230\/LIPIcs.OPODIS.2015.20"},{"key":"e_1_3_1_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-50521-8_2"},{"key":"e_1_3_1_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/164051.164056"},{"key":"e_1_3_1_8_2","first-page":"420","volume-title":"Proceedings of the 29th International Symposium on Distributed Computing - Volume 9363(DISC 2015)","author":"Casta\u00f1eda Armando","year":"2015","unstructured":"Armando Casta\u00f1eda,Sergio Rajsbaum, and Michel Raynal. 2015. Specifying Concurrent Problems: Beyond Linearizability and up to Tasks. In Proceedings of the 29th International Symposium on Distributed Computing - Volume 9363 (Tokyo, Japan) (DISC 2015). Springer-Verlag,Berlin, Heidelberg,420\u2013435. https:\/\/doi.org\/10.1007\/978-3-662-48653-5_28 10.1007\/978-3-662-48653-5_28"},{"key":"e_1_3_1_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314585"},{"key":"e_1_3_1_10_2","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359632"},{"key":"e_1_3_1_11_2","first-page":"423","volume-title":"15th USENIX Symposium on Operating Systems Design and Implementation (OSDI 21)","author":"Chajed Tej","year":"2021","unstructured":"Tej Chajed,Joseph Tassarotti,Mark Theng,Ralf Jung,M. Frans Kaashoek, and Nickolai Zeldovich. 2021. GoJournal: a verified, concurrent, crash-safe journaling system. In 15th USENIX Symposium on Operating Systems Design and Implementation (OSDI 21). USENIX Association,423\u2013439."},{"key":"e_1_3_1_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815402"},{"key":"e_1_3_1_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14107-2_24"},{"key":"e_1_3_1_14_2","first-page":"27","article-title":"The Path to Durable Linearizability","volume":"7","author":"D\u2019Osualdo Emanuele","year":"2023","unstructured":"Emanuele D\u2019Osualdo,Azalea Raad, and Viktor Vafeiadis. 2023. The Path to Durable Linearizability. Proc. ACM Program. Lang. 7,POPL,Article 26 (jan 2023),27 pages. https:\/\/doi.org\/10.1145\/3571219 10.1145\/3571219","journal-title":"Proc. ACM Program. Lang."},{"key":"e_1_3_1_15_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2010.09.021"},{"key":"e_1_3_1_16_2","unstructured":"Dan R. Ghica. 2019. The far side of the cube. CoRR abs\/1908.04291 (2019). arXiv:1908.04291 http:\/\/arxiv.org\/abs\/1908.04291"},{"key":"e_1_3_1_17_2","doi-asserted-by":"crossref","first-page":"211","DOI":"10.1007\/978-3-540-24727-2_16","volume-title":"Foundations of Software Science and Computation Structures","author":"Ghica Dan R.","year":"2004","unstructured":"Dan R. Ghica and Andrzej S. Murawski. 2004. Angelic Semantics of Fine-Grained Concurrency. In Foundations of Software Science and Computation Structures,Igor Walukiewicz (Ed.). Springer Berlin Heidelberg,Berlin, Heidelberg,211\u2013225. https:\/\/doi.org\/10.1016\/j.apal.2007.10.005 10.1016\/j.apal.2007.10.005"},{"key":"e_1_3_1_18_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2012.08.013"},{"key":"e_1_3_1_19_2","first-page":"28:1","volume-title":"22nd International Conference on Principles of Distributed Systems (OPODIS 2018) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 125)","author":"Goubault \u00c9ric","year":"2018","unstructured":"\u00c9ric Goubault,J\u00e9r\u00e9my Ledent, and Samuel Mimram. 2018. Concurrent Specifications Beyond Linearizability. In 22nd International Conference on Principles of Distributed Systems (OPODIS 2018) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 125),Jiannong Cao,Faith Ellen,Luis Rodrigues, and Bernardo Ferreira (Eds.). Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik,Dagstuhl, Germany,28:1\u201328:16. https:\/\/doi.org\/10.4230\/LIPIcs.OPODIS.2018.28 10.4230\/LIPIcs.OPODIS.2018.28"},{"key":"e_1_3_1_20_2","doi-asserted-by":"publisher","DOI":"10.5555\/977400.978019"},{"key":"e_1_3_1_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/78969.78972"},{"key":"e_1_3_1_22_2","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1017\/CBO9780511526619.005","volume-title":"Semantics and Logics of Computation","author":"Hyland Martin","year":"1997","unstructured":"Martin Hyland. 1997. Game Semantics. In Semantics and Logics of Computation,Andrew M. Pitts and P. Editors Dybjer (Eds.). Cambridge University Press,Cambridge, UK,131\u2013184. https:\/\/doi.org\/10.1017\/CBO9780511526619.005 10.1017\/CBO9780511526619.005"},{"key":"e_1_3_1_23_2","doi-asserted-by":"crossref","first-page":"313","DOI":"10.1007\/978-3-662-53426-7_23","volume-title":"Distributed Computing","author":"Izraelevitz Joseph","year":"2016","unstructured":"Joseph Izraelevitz,Hammurabi Mendes, and Michael L. Scott. 2016. Linearizability of Persistent Memory Objects Under a Full-System-Crash Failure Model. In Distributed Computing,Cyril Gavoille and David Ilcinkas (Eds.). Springer Berlin Heidelberg,Berlin, Heidelberg,313\u2013327. https:\/\/doi.org\/10.1007\/978-3-662-53426-7_23 10.1007\/978-3-662-53426-7_23"},{"key":"e_1_3_1_24_2","doi-asserted-by":"crossref","first-page":"639","DOI":"10.1007\/978-3-662-54434-1_24","volume-title":"Programming Languages and Systems: 26th European Symposium on Programming, ESOP 2017","author":"Khyzha Artem","year":"2017","unstructured":"Artem Khyzha,Mike Dodds,Alexey Gotsman, and Matthew Parkinson. 2017. Proving Linearizability Using Partial Orders. In Programming Languages and Systems: 26th European Symposium on Programming, ESOP 2017 (Uppsala, Sweden). Springer-Verlag,Berlin, Heidelberg,639\u2013667. https:\/\/doi.org\/10.1007\/978-3-662-54434-1_24 10.1007\/978-3-662-54434-1_24"},{"key":"e_1_3_1_25_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99336-8_10"},{"key":"e_1_3_1_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/3373718.3394799"},{"key":"e_1_3_1_27_2","doi-asserted-by":"crossref","first-page":"459","DOI":"10.1145\/2491956.2462189","volume-title":"Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation(PLDI\u201913)","author":"Liang Hongjin","year":"2013","unstructured":"Hongjin Liang and Xinyu Feng. 2013. Modular verification of linearizability with non-fixed linearization points. In Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation (Seattle, Washington, USA) (PLDI\u201913). Association for Computing Machinery,New York, NY, USA,459\u2013470. https:\/\/doi.org\/10.1145\/2491956.2462189 10.1145\/2491956.2462189"},{"key":"e_1_3_1_28_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0060"},{"key":"e_1_3_1_29_2","first-page":"30","article-title":"Categorical Combinatorics of Scheduling and Synchronization in Game Semantics","volume":"3","author":"Mellies Paul-Andr\u00e9","year":"2019","unstructured":"Paul-Andr\u00e9 Mellies. 2019. Categorical Combinatorics of Scheduling and Synchronization in Game Semantics. Proc. ACM Program. Lang. 3,POPL,Article 23 (jan 2019),30 pages. https:\/\/doi.org\/10.1145\/3290336 10.1145\/3290336","journal-title":"Proc. ACM Program. Lang."},{"key":"e_1_3_1_30_2","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676970"},{"key":"e_1_3_1_31_2","first-page":"32","article-title":"Layered and Object-Based Game Semantics","volume":"6","author":"Oliveira Vale Arthur","year":"2022","unstructured":"Arthur Oliveira Vale,Paul-Andr\u00e9 Melli\u00e8s,Zhong Shao,J\u00e9r\u00e9mie Koenig, and L\u00e9o Stefanesco. 2022. Layered and Object-Based Game Semantics. Proc. ACM Program. Lang. 6,POPL,Article 42 (jan 2022),32 pages. https:\/\/doi.org\/10.1145\/3498703 10.1145\/3498703","journal-title":"Proc. ACM Program. Lang."},{"key":"e_1_3_1_32_2","first-page":"32","article-title":"A Compositional Theory of Linearizability","volume":"7","author":"Oliveira Vale Arthur","year":"2023","unstructured":"Arthur Oliveira Vale,Zhong Shao, and Yixuan Chen. 2023. A Compositional Theory of Linearizability. Proc. ACM Program. Lang. 7,POPL,Article 38 (jan 2023),32 pages. https:\/\/doi.org\/10.1145\/3571231 10.1145\/3571231","journal-title":"Proc. ACM Program. Lang."},{"issue":"2","key":"e_1_3_1_33_2","first-page":"107","article-title":"A Compositional Theory of Linearizability","volume":"71","author":"Oliveira Vale Arthur","year":"2024","unstructured":"Arthur Oliveira Vale,Zhong Shao, and Yixuan Chen. 2024. A Compositional Theory of Linearizability. J. ACM 71,2,Article 14 (apr 2024),107 pages. https:\/\/doi.org\/10.1145\/3643668 10.1145\/3643668","journal-title":"J. ACM"},{"key":"e_1_3_1_34_2","doi-asserted-by":"crossref","unstructured":"Arthur Oliveira Vale Zhongye Wang Yixuan Chen Peixin You and Zhong Shao. 2024. Compositionality and Observational Refinement for Linearizability with Crashes. Technical Report YALEU\/DCS\/TR-1570. Yale Univ. https:\/\/flint.cs.yale.edu\/publications\/crashlin.html","DOI":"10.1145\/3689792"},{"key":"e_1_3_1_35_2","first-page":"31","article-title":"Persistency Semantics of the Intel-X86 Architecture","volume":"4","author":"Raad Azalea","year":"2019","unstructured":"Azalea Raad,John Wickerson,Gil Neiger, and Viktor Vafeiadis. 2019. Persistency Semantics of the Intel-X86 Architecture. Proc. ACM Program. Lang. 4,POPL,Article 11 (dec 2019),31 pages. https:\/\/doi.org\/10.1145\/3371079 10.1145\/3371079","journal-title":"Proc. ACM Program. Lang."},{"key":"e_1_3_1_36_2","first-page":"27","article-title":"Weak Persistency Semantics from the Ground up: Formalising the Persistency Semantics of ARMv8 and Transactional Models","volume":"3","author":"Raad Azalea","year":"2019","unstructured":"Azalea Raad,John Wickerson, and Viktor Vafeiadis. 2019. Weak Persistency Semantics from the Ground up: Formalising the Persistency Semantics of ARMv8 and Transactional Models. Proc. ACM Program. Lang. 3,OOPSLA,Article 135 (oct 2019),27 pages. https:\/\/doi.org\/10.1145\/3360561 10.1145\/3360561","journal-title":"Proc. ACM Program. Lang."},{"key":"e_1_3_1_37_2","unstructured":"Uday S. Reddy. 1993. A Linear Logic Model of State. Technical Report. Dept. of Computer Science UIUC Urbana IL."},{"issue":"1","key":"e_1_3_1_38_2","first-page":"7","article-title":"Global State Considered Unnecessary: An Introduction to Object-Based Semantics","volume":"9","author":"Reddy Uday S.","year":"1996","unstructured":"Uday S. Reddy. 1996. Global State Considered Unnecessary: An Introduction to Object-Based Semantics. LISP Symb. Comput. 9,1 (1996),7\u201376. https:\/\/doi.org\/10.1007\/978-1-4757-3851-3_9 10.1007\/978-1-4757-3851-3_9","journal-title":"LISP Symb. Comput."},{"key":"e_1_3_1_39_2","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1007\/978-3-642-54833-8_9","volume-title":"Programming Languages and Systems","author":"Svendsen Kasper","year":"2014","unstructured":"Kasper Svendsen and Lars Birkedal. 2014. Impredicative Concurrent Abstract Predicates. In Programming Languages and Systems,Zhong Shao (Ed.). Springer Berlin Heidelberg,Berlin, Heidelberg,149\u2013168. https:\/\/doi.org\/10.1007\/978-3-642-54833-8_9 10.1007\/978-3-642-54833-8_9"},{"key":"e_1_3_1_40_2","first-page":"309","volume-title":"Proceedings of the 27th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming(PPoPP\u201922)","author":"Wei Yuanhao","year":"2022","unstructured":"Yuanhao Wei,Naama Ben-David,Michal Friedman,Guy E. Blelloch, and Erez Petrank. 2022. FliT: a library for simple and efficient persistent algorithms. In Proceedings of the 27th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (Seoul, Republic of Korea) (PPoPP\u201922). Association for Computing Machinery,New York, NY, USA,309\u2013321. https:\/\/doi.org\/10.1145\/3503221.3508436 10.1145\/3503221.3508436"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3689792","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3689792","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T09:11:17Z","timestamp":1770196277000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3689792"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,8]]},"references-count":39,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2024,10,8]]}},"alternative-id":["10.1145\/3689792"],"URL":"https:\/\/doi.org\/10.1145\/3689792","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,10,8]]},"assertion":[{"value":"2024-04-06","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-08-18","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-10-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}