{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T03:23:41Z","timestamp":1779074621957,"version":"3.51.4"},"reference-count":56,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2023,1,9]],"date-time":"2023-01-09T00:00:00Z","timestamp":1673222400000},"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":["2019285, 1763399, 2118851"],"award-info":[{"award-number":["2019285, 1763399, 2118851"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"name":"DARPA and NIWC 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":[[2023,1,9]]},"abstract":"<jats:p>Compositionality is at the core of programming languages research and has become an important goal toward scalable verification of large systems. Despite that, there is no compositional account of linearizability, the gold standard of correctness for concurrent objects.<\/jats:p><jats:p>In this paper, we develop a compositional semantics for linearizable concurrent objects. We start by showcasing a common issue, which is independent of linearizability, in the construction of compositional models of concurrent computation: interaction with the neutral element for composition can lead to emergent behaviors, a hindrance to compositionality. Category theory provides a solution for the issue in the form of the Karoubi envelope. Surprisingly, and this is the main discovery of our work, this abstract construction is deeply related to linearizability and leads to a novel formulation of it. Notably, this new formulation neither relies on atomicity nor directly upon happens-before ordering and is only possible because of compositionality, revealing that linearizability and compositionality are intrinsically related to each other.<\/jats:p><jats:p>We use this new, and compositional, understanding of linearizability to revisit much of the theory of linearizability, providing novel, simple, algebraic proofs of the locality property and of an analogue of the equivalence with observational refinement. We show our techniques can be used in practice by connecting our semantics with a simple program logic that is nonetheless sound concerning this generalized linearizability.<\/jats:p>","DOI":"10.1145\/3571231","type":"journal-article","created":{"date-parts":[[2023,1,11]],"date-time":"2023-01-11T21:58:14Z","timestamp":1673474294000},"page":"1089-1120","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["A Compositional Theory of Linearizability"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1091-7560","authenticated-orcid":false,"given":"Arthur","family":"Oliveira Vale","sequence":"first","affiliation":[{"name":"Yale University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8184-7649","authenticated-orcid":false,"given":"Zhong","family":"Shao","sequence":"additional","affiliation":[{"name":"Yale University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8659-8493","authenticated-orcid":false,"given":"Yixuan","family":"Chen","sequence":"additional","affiliation":[{"name":"Yale University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,1,11]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.2930"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-58622-4_1"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1999.782638"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473586"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(92)90073-9"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-48653-5_28"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-13(3:35)2017"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-43951-7_9"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44202-9_9"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14107-2_24"},{"key":"e_1_2_1_11_1","volume-title":"Programming Languages and Systems","author":"Feng Xinyu","unstructured":"Xinyu Feng , Rodrigo Ferreira , and Zhong Shao . 2007. On the Relationship Between Concurrent Separation Logic and Assume-Guarantee Reasoning . In Programming Languages and Systems , Rocco De Nicola (Ed.). Springer Berlin Heidelberg , Berlin, Heidelberg . 173\u2013188. isbn:978-3-540-71316-6 https:\/\/doi.org\/10.5555\/1762174.1762193 10.5555\/1762174.1762193 Xinyu Feng, Rodrigo Ferreira, and Zhong Shao. 2007. On the Relationship Between Concurrent Separation Logic and Assume-Guarantee Reasoning. In Programming Languages and Systems, Rocco De Nicola (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 173\u2013188. isbn:978-3-540-71316-6 https:\/\/doi.org\/10.5555\/1762174.1762193"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2010.09.021"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15375-4_27"},{"key":"e_1_2_1_14_1","volume-title":"LXI, 2","author":"Gaucher Philippe","year":"2020","unstructured":"Philippe Gaucher . 2020. Flows revisited: the model category structure and its left determinedness. Cahiers de topologie et g\u00e9om\u00e9trie diff\u00e9rentielle cat\u00e9goriques , LXI, 2 ( 2020 ), 208\u2013226. https:\/\/hal.archives-ouvertes.fr\/hal-01919037 Philippe Gaucher. 2020. Flows revisited: the model category structure and its left determinedness. Cahiers de topologie et g\u00e9om\u00e9trie diff\u00e9rentielle cat\u00e9goriques, LXI, 2 (2020), 208\u2013226. https:\/\/hal.archives-ouvertes.fr\/hal-01919037"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38164-5_5"},{"key":"e_1_2_1_16_1","volume-title":"The far side of the cube. CoRR, abs\/1908.04291","author":"Ghica Dan R.","year":"2019","unstructured":"Dan R. Ghica . 2019. The far side of the cube. CoRR, abs\/1908.04291 ( 2019 ), arXiv:1908.04291. arxiv:1908.04291 Dan R. Ghica. 2019. The far side of the cube. CoRR, abs\/1908.04291 (2019), arXiv:1908.04291. arxiv:1908.04291"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2007.10.005"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.OPODIS.2018.28"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676975"},{"key":"e_1_2_1_20_1","volume-title":"Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation (OSDI\u201916)","author":"Gu Ronghui","year":"2016","unstructured":"Ronghui Gu , Zhong Shao , Hao Chen , Xiongnan Wu , Jieung Kim , Vilhelm Sj\u00f6berg , and David Costanzo . 2016 . CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels . In Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation (OSDI\u201916) . USENIX Association, USA. 653\u2013669. isbn:978 1931971331 Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan Wu, Jieung Kim, Vilhelm Sj\u00f6berg, and David Costanzo. 2016. CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. In Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation (OSDI\u201916). USENIX Association, USA. 653\u2013669. isbn:9781931971331"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192381"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-09581-3_5"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2016.6"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(85)90062-3"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-48653-5_25"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/78969.78972"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1017\/S096012950000061X"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.2917"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511526619.005"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.04.024"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371113"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2775051.2676980"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_24"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-48989-6_26"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373718.3394799"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3527324"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837635"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290336"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74407-8_27"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373718.3394762"},{"key":"e_1_2_1_43_1","first-page":"163","article-title":"On regular presheaves and regular semi-categories","volume":"43","author":"Moens M.-A.","year":"2002","unstructured":"M.-A. Moens , U. Berni-Canani , and Francis Borceux . 2002 . On regular presheaves and regular semi-categories . Cahiers de Topologie et G\u00e9om\u00e9trie Diff\u00e9rentielle Cat\u00e9goriques , 43 , 3 (2002), 163 \u2013 190 . http:\/\/www.numdam.org\/item\/CTGDC_2002__43_3_163_0\/ M.-A. Moens, U. Berni-Canani, and Francis Borceux. 2002. On regular presheaves and regular semi-categories. Cahiers de Topologie et G\u00e9om\u00e9trie Diff\u00e9rentielle Cat\u00e9goriques, 43, 3 (2002), 163\u2013190. http:\/\/www.numdam.org\/item\/CTGDC_2002__43_3_163_0\/","journal-title":"Cahiers de Topologie et G\u00e9om\u00e9trie Diff\u00e9rentielle Cat\u00e9goriques"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2019.01.002"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_16"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/197917.198176"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498703"},{"key":"e_1_2_1_48_1","doi-asserted-by":"crossref","unstructured":"Arthur Oliveira Vale Zhong Shao and Yixuan Chen. 2022. A Compositional Theory of Linearizability. Yale Univ.. https:\/\/flint.cs.yale.edu\/publications\/ctlinear.html Arthur Oliveira Vale Zhong Shao and Yixuan Chen. 2022. A Compositional Theory of Linearizability. Yale Univ.. https:\/\/flint.cs.yale.edu\/publications\/ctlinear.html","DOI":"10.1145\/3571231"},{"key":"e_1_2_1_50_1","volume-title":"A Linear Logic Model of State. Dept. of Computer Science","author":"Reddy Uday S.","unstructured":"Uday S. Reddy . 1993. A Linear Logic Model of State. Dept. of Computer Science , UIUC , Urbana, IL . Uday S. Reddy. 1993. A Linear Logic Model of State. Dept. of Computer Science, UIUC, Urbana, IL."},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-3851-3_9"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2011.13"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/2629496"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_9"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500600"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/1122971.1122992"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74407-8_18"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3571231","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3571231","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T18:08:22Z","timestamp":1750183702000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3571231"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,9]]},"references-count":56,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2023,1,9]]}},"alternative-id":["10.1145\/3571231"],"URL":"https:\/\/doi.org\/10.1145\/3571231","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,1,9]]},"assertion":[{"value":"2023-01-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}