{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T08:55:53Z","timestamp":1770281753472,"version":"3.49.0"},"reference-count":59,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2024,4,12]],"date-time":"2024-04-12T00:00:00Z","timestamp":1712880000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"NSF","award":["GS100000001, 2019285 GS100000001, 1763399 GS100000001, 2313433 GS100000001, 2118851 GS100000001"],"award-info":[{"award-number":["GS100000001, 2019285 GS100000001, 1763399 GS100000001, 2313433 GS100000001, 2118851 GS100000001"]}]},{"name":"Defense Advanced Research Projects Agency (DARPA) and Naval Information Warfare Center Pacific","award":["GS100000005, N66001-21-C-4018, GS100000005"],"award-info":[{"award-number":["GS100000005, N66001-21-C-4018, GS100000005"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["J. ACM"],"published-print":{"date-parts":[[2024,4,30]]},"abstract":"<jats:p>\n            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\n            <jats:italic>linearizability<\/jats:italic>\n            , the gold standard of correctness for concurrent objects.\n          <\/jats:p>\n          <jats:p>\n            In this article, 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\n            <jats:italic>because<\/jats:italic>\n            of compositionality, revealing that linearizability and compositionality are intrinsically related to each other.\n          <\/jats:p>\n          <jats:p>\n            We use this new, and compositional, understanding of linearizability to revisit much of the theory of linearizability, providing novel, simple, algebraic proofs of the\n            <jats:italic>locality<\/jats:italic>\n            property and of an analogue of the equivalence with\n            <jats:italic>observational refinement<\/jats:italic>\n            . 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.\n          <\/jats:p>","DOI":"10.1145\/3643668","type":"journal-article","created":{"date-parts":[[2024,1,27]],"date-time":"2024-01-27T12:48:30Z","timestamp":1706359710000},"page":"1-107","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["A Compositional Theory of Linearizability"],"prefix":"10.1145","volume":"71","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"}],"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, New Haven, 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, New Haven, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,4,12]]},"reference":[{"key":"e_1_3_3_2_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.2930"},{"key":"e_1_3_3_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-58622-4_1"},{"key":"e_1_3_3_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1999.782638"},{"key":"e_1_3_3_5_1","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.","journal-title":"Technical Report HPL-2003-241."},{"key":"e_1_3_3_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473586"},{"key":"e_1_3_3_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(92)90073-9"},{"key":"e_1_3_3_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-48653-5_28"},{"key":"e_1_3_3_9_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-13(3:35)2017"},{"key":"e_1_3_3_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-43951-7_9"},{"key":"e_1_3_3_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44202-9_9"},{"key":"e_1_3_3_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14107-2_24"},{"key":"e_1_3_3_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/1762174.1762193"},{"key":"e_1_3_3_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2010.09.021"},{"key":"e_1_3_3_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15375-4_27"},{"issue":"2","key":"e_1_3_3_16_1","first-page":"208","article-title":"Flows revisited: The model category structure and its left determinedness","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. Retrieved from https:\/\/hal.archives-ouvertes.fr\/hal-01919037","journal-title":"Cahiers de Topologie et G\u00e9om\u00e9trie Diff\u00e9rentielle Cat\u00e9goriques"},{"key":"e_1_3_3_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38164-5_5"},{"key":"e_1_3_3_18_1","doi-asserted-by":"publisher","unstructured":"Dan R. Ghica. 2023. The far side of the cube. In Samson Abramsky on Logic and Structure in Computer Science and Beyond Alessandra Palmigiano and Mehrnoosh Sadrzadeh (Eds.). Springer International Publishing Cham 219\u2013250. DOI:10.1007\/978-3-031-24117-8_6","DOI":"10.1007\/978-3-031-24117-8_6"},{"key":"e_1_3_3_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2007.10.005"},{"key":"e_1_3_3_20_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.OPODIS.2018.28"},{"key":"e_1_3_3_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676975"},{"key":"e_1_3_3_22_1","first-page":"653","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."},{"key":"e_1_3_3_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192381"},{"key":"e_1_3_3_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-09581-3_5"},{"key":"e_1_3_3_25_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2016.6"},{"key":"e_1_3_3_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(85)90062-3"},{"key":"e_1_3_3_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-48653-5_25"},{"key":"e_1_3_3_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/78969.78972"},{"key":"e_1_3_3_29_1","doi-asserted-by":"publisher","DOI":"10.1017\/S096012950000061X"},{"key":"e_1_3_3_30_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511526619.005"},{"key":"e_1_3_3_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.04.024"},{"key":"e_1_3_3_32_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.2917"},{"key":"e_1_3_3_33_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_3_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371113"},{"key":"e_1_3_3_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2775051.2676980"},{"key":"e_1_3_3_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_24"},{"key":"e_1_3_3_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-48989-6_26"},{"key":"e_1_3_3_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373718.3394799"},{"key":"e_1_3_3_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)80965-4"},{"key":"e_1_3_3_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_3_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3527324"},{"key":"e_1_3_3_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837635"},{"key":"e_1_3_3_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/2576235"},{"key":"e_1_3_3_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74407-8_27"},{"key":"e_1_3_3_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373718.3394762"},{"issue":"3","key":"e_1_3_3_46_1","first-page":"163","article-title":"On regular presheaves and regular semi-categories","volume":"43","author":"Moens Marie-Anne","year":"2002","unstructured":"Marie-Anne Moens, Ugo 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. Retrieved from 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_3_3_47_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2019.01.002"},{"key":"e_1_3_3_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_16"},{"key":"e_1_3_3_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/197917.198176"},{"key":"e_1_3_3_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498703"},{"key":"e_1_3_3_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571231"},{"key":"e_1_3_3_52_1","volume-title":"Picturing Resources in Concurrency","author":"Piedeleu Robin","year":"2019","unstructured":"Robin Piedeleu. 2019. Picturing Resources in Concurrency. Ph.D. Dissertation. University of Oxford."},{"key":"e_1_3_3_53_1","volume-title":"A Linear Logic Model of State","author":"Reddy Uday S.","year":"1993","unstructured":"Uday S. Reddy. 1993. A Linear Logic Model of State. Technical Report. Dept. of Computer Science, UIUC, Urbana, IL."},{"key":"e_1_3_3_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-3851-3_9"},{"key":"e_1_3_3_55_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2011.13"},{"key":"e_1_3_3_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/2629496"},{"key":"e_1_3_3_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_9"},{"key":"e_1_3_3_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500600"},{"key":"e_1_3_3_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/1122971.1122992"},{"key":"e_1_3_3_60_1","doi-asserted-by":"crossref","first-page":"256","DOI":"10.1007\/978-3-540-74407-8_18","volume-title":"Proceedings of the CONCUR 2007 \u2013 Concurrency Theory","author":"Vafeiadis Viktor","year":"2007","unstructured":"Viktor Vafeiadis and Matthew Parkinson. 2007. A marriage of rely\/guarantee and separation logic. In Proceedings of the CONCUR 2007 \u2013 Concurrency Theory. Lu\u00eds Caires and Vasco T. Vasconcelos (Eds.), Springer, Berlin,256\u2013271."}],"container-title":["Journal of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3643668","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3643668","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T00:05:33Z","timestamp":1750291533000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3643668"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,4,12]]},"references-count":59,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2024,4,30]]}},"alternative-id":["10.1145\/3643668"],"URL":"https:\/\/doi.org\/10.1145\/3643668","relation":{},"ISSN":["0004-5411","1557-735X"],"issn-type":[{"value":"0004-5411","type":"print"},{"value":"1557-735X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,4,12]]},"assertion":[{"value":"2022-12-02","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-01-09","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-04-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}