{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T21:10:10Z","timestamp":1751663410161,"version":"3.41.0"},"reference-count":46,"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":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["851811"],"award-info":[{"award-number":["851811"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100003977","name":"Israel Science Foundation","doi-asserted-by":"publisher","award":["814\/22"],"award-info":[{"award-number":["814\/22"]}],"id":[{"id":"10.13039\/501100003977","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":[[2024,6,20]]},"abstract":"<jats:p>We revisit the fundamental problem of defining a compositional semantics for a concurrent programming language under sequentially consistent memory with the aim of equating the denotations of pieces of code if and only if these pieces induce the same behavior under all program contexts. While the denotational semantics presented by Brookes [Information and Computation 127, 2 (1996)] has been considered a definitive solution, we observe that Brookes\u2019s full abstraction result crucially relies on the availability of an impractical whole-memory atomic read-modify-write instruction. In contrast, we consider a language with standard primitives, which apply to a single variable. For that language, we propose an alternative denotational semantics based on traces that track program write actions together with the writes expected from the environment, and equipped with several closure operators to achieve necessary abstraction. We establish the adequacy of the semantics, and demonstrate full abstraction for the case that the analyzed code segment is loop-free. Furthermore, we show that by including a whole-memory atomic read in the language, one obtains full abstraction for programs with loops. To gain confidence, our results are fully mechanized in Coq.<\/jats:p>","DOI":"10.1145\/3656399","type":"journal-article","created":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T16:27:20Z","timestamp":1718900840000},"page":"543-566","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Compositional Semantics for Shared-Variable Concurrency"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9381-764X","authenticated-orcid":false,"given":"Mikhail","family":"Svyatlovskiy","sequence":"first","affiliation":[{"name":"Tel Aviv University, Tel Aviv, Israel"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0001-9806-017X","authenticated-orcid":false,"given":"Shai","family":"Mermelstein","sequence":"additional","affiliation":[{"name":"Tel Aviv University, Tel Aviv, Israel"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4305-6998","authenticated-orcid":false,"given":"Ori","family":"Lahav","sequence":"additional","affiliation":[{"name":"Tel Aviv University, Tel Aviv, Israel"}],"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.2168\/LMCS-6(4:2)2010"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2627752"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2967973.2968602"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CSL.2012.107"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0056"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11970-5_7"},{"key":"e_1_3_1_8_1","volume-title":"The Stanford Encyclopedia of Philosophy (Spring 2021 ed.)","author":"Cardone Felice","year":"2021","unstructured":"Felice Cardone. 2021. Games, Full Abstraction and Full Completeness. In The Stanford Encyclopedia of Philosophy (Spring 2021 ed.), Edward N. Zalta (Ed.). Metaphysics Research Lab, Stanford University. https:\/\/plato.stanford.edu\/archives\/spr2021\/entries\/games-abstraction\/"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2854038.2854051"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523718"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-49253-4_18"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/s001650200032"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_36"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-21037-2_1"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-57267-8_5"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-4886-6"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.46298\/LMCS-17(3:9)2021"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591195.3595274"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/3921"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428262"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28729-9_12"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-15(1:33)2019"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498716"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/69575.69577"},{"key":"e_1_3_1_25_1","volume-title":"Ph. D. Dissertation","author":"Kammar Ohad","year":"2014","unstructured":"Ohad Kammar. 2014. Algebraic theory of type-and-effect systems. Ph. D. Dissertation. University of Edinburgh, UK. https:\/\/hdl.handle.net\/1842\/8910"},{"key":"e_1_3_1_26_1","unstructured":"Ryan Kavanagh and Stephen Brookes. 2018. A denotational account of C11-style memory. CoRR abs\/1804.04214 (2018). arXiv:1804.04214 http:\/\/arxiv.org\/abs\/1804.04214"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-15(2:10)2019"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99336-8_10"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837643"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-48989-6_29"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1979.1675439"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","DOI":"10.1561\/2500000041"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103711"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2576235"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-10235-3"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2491967"},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_27"},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-44914-8_22"},{"key":"e_1_3_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49674-9_30"},{"key":"e_1_3_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01379149"},{"key":"e_1_3_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571246"},{"key":"e_1_3_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571232"},{"key":"e_1_3_1_44_1","doi-asserted-by":"publisher","unstructured":"Mikhail Svyatlovskiy Shai Mermelstein and Ori Lahav. 2024. Coq Mechanization for \"Compositional Semantics for Shared-Variable Concurrency\" (PLDI 2024). https:\/\/doi.org\/10.5281\/zenodo.10925596 10.5281\/zenodo.10925596","DOI":"10.5281\/zenodo.10925596"},{"key":"e_1_3_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926415"},{"key":"e_1_3_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-17906-2_31"},{"key":"e_1_3_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211617"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656399","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3656399","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:38:59Z","timestamp":1751661539000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656399"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,6,20]]},"references-count":46,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2024,6,20]]}},"alternative-id":["10.1145\/3656399"],"URL":"https:\/\/doi.org\/10.1145\/3656399","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"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"}}]}}