{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:08:27Z","timestamp":1776305307417,"version":"3.50.1"},"reference-count":45,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T00:00:00Z","timestamp":1641945600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCR-1617175"],"award-info":[{"award-number":["CCR-1617175"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/V000470\/1, EP\/R032971\/1"],"award-info":[{"award-number":["EP\/V000470\/1, EP\/R032971\/1"]}],"id":[{"id":"10.13039\/501100000266","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":[[2022,1,16]]},"abstract":"<jats:p>Program logics and semantics tell a pleasant story about sequential composition: when executing (S1;S2), we first execute S1 then S2. To improve performance, however, processors execute instructions out of order, and compilers reorder programs even more dramatically. By design, single-threaded systems cannot observe these reorderings; however, multiple-threaded systems can, making the story considerably less pleasant. A formal attempt to understand the resulting mess is known as a \u201crelaxed memory model.\u201d Prior models either fail to address sequential composition directly, or overly restrict processors and compilers, or permit nonsense thin-air behaviors which are unobservable in practice.<\/jats:p>\n          <jats:p>To support sequential composition while targeting modern hardware, we enrich the standard event-based approach with preconditions and families of predicate transformers. When calculating the meaning of (S1; S2), the predicate transformer applied to the precondition of an event e from S2 is chosen based on the set of events in S1 upon which e depends. We apply this approach to two existing memory models.<\/jats:p>","DOI":"10.1145\/3498716","type":"journal-article","created":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T17:03:12Z","timestamp":1642006992000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":17,"title":["The leaky semicolon: compositional semantic dependencies for relaxed-memory concurrency"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6342-0318","authenticated-orcid":false,"given":"Alan","family":"Jeffrey","sequence":"first","affiliation":[{"name":"Roblox, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8731-1463","authenticated-orcid":false,"given":"James","family":"Riely","sequence":"additional","affiliation":[{"name":"DePaul University, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7053-4364","authenticated-orcid":false,"given":"Mark","family":"Batty","sequence":"additional","affiliation":[{"name":"University of Kent, UK"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9365-9717","authenticated-orcid":false,"given":"Simon","family":"Cooksey","sequence":"additional","affiliation":[{"name":"University of Kent, UK"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6301-152X","authenticated-orcid":false,"given":"Ilya","family":"Kaysin","sequence":"additional","affiliation":[{"name":"JetBrains Research, Russia \/ University of Cambridge, UK"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9448-6587","authenticated-orcid":false,"given":"Anton","family":"Podkopaev","sequence":"additional","affiliation":[{"name":"HSE University, Russia"}]}],"member":"320","published-online":{"date-parts":[[2022,1,12]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3458926"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2627752"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_12"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926394"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2618128.2618134"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0056"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290383"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454082"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-54997-8_31"},{"key":"e_1_2_2_10_1","unstructured":"Russ Cox. 2016. Go\u2019s Memory Model. http:\/\/nil.csail.mit.edu\/6.824\/2016\/notes\/gomem.pdf  Russ Cox. 2016. Go\u2019s Memory Model. http:\/\/nil.csail.mit.edu\/6.824\/2016\/notes\/gomem.pdf"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192421"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/232627.232649"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(88)90124-7"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428262"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11957-6_17"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2934536"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009850"},{"key":"e_1_2_2_21_1","volume-title":"A denotational account of C11-style memory. CoRR, abs\/1804.04214","author":"Kavanagh Ryan","year":"2018","unstructured":"Ryan Kavanagh and Stephen Brookes . 2018. A denotational account of C11-style memory. CoRR, abs\/1804.04214 ( 2018 ), 13 pages. arxiv:1804.04214. arxiv:1804.04214 Ryan Kavanagh and Stephen Brookes. 2018. A denotational account of C11-style memory. CoRR, abs\/1804.04214 (2018), 13 pages. arxiv:1804.04214. arxiv:1804.04214"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062352"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1979.1675439"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276495"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062343"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386010"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314611"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3462206"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1047659.1040336"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.SNAPL.2015.177"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1992.185532"},{"key":"e_1_2_2_32_1","unstructured":"Paul E. McKenney Alan Jeffrey Ali Sezgin and Tony Tye. 2016. Out-of-Thin-Air Execution is vacuous. http:\/\/wg21.link\/p0422  Paul E. McKenney Alan Jeffrey Ali Sezgin and Tony Tye. 2016. Out-of-Thin-Air Execution is vacuous. http:\/\/wg21.link\/p0422"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(77)90053-6"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.035"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-44914-8_22"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837616"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(77)90044-5"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-15648-8_22"},{"key":"e_1_2_2_39_1","unstructured":"William Pugh. 2004. Causality Test Cases. https:\/\/perma.cc\/PJT9-XS8Z  William Pugh. 2004. Causality Test Cases. https:\/\/perma.cc\/PJT9-XS8Z"},{"key":"e_1_2_2_40_1","volume-title":"Program Transformations in Weak Memory Models. Laboratory for Foundations of Computer Science","author":"Sev\u010d\u00edk Jaroslav","unstructured":"Jaroslav Sev\u010d\u00edk . 2008. Program Transformations in Weak Memory Models. Laboratory for Foundations of Computer Science , University of Edinburgh. Jaroslav Sev\u010d\u00edk. 2008. Program Transformations in Weak Memory Models. Laboratory for Foundations of Computer Science, University of Edinburgh."},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70592-5_3"},{"key":"e_1_2_2_42_1","unstructured":"Joel Spolsky. 2002. The Law of Leaky Abstractions. https:\/\/www.joelonsoftware.com\/2002\/11\/11\/the-law-of-leaky-abstractions\/  Joel Spolsky. 2002. The Law of Leaky Abstractions. https:\/\/www.joelonsoftware.com\/2002\/11\/11\/the-law-of-leaky-abstractions\/"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509532"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385973"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360559"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498716","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3498716","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3498716","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:30:28Z","timestamp":1750188628000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498716"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,1,12]]},"references-count":45,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2022,1,16]]}},"alternative-id":["10.1145\/3498716"],"URL":"https:\/\/doi.org\/10.1145\/3498716","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,1,12]]},"assertion":[{"value":"2022-01-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}