{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:08:26Z","timestamp":1776305306748,"version":"3.50.1"},"reference-count":35,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T00:00:00Z","timestamp":1744156800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000266","name":"EPSRC","doi-asserted-by":"crossref","award":["EP\/X015076\/1, EP\/X021173\/1, and EP\/V000470\/1"],"award-info":[{"award-number":["EP\/X015076\/1, EP\/X021173\/1, and EP\/V000470\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,4,9]]},"abstract":"<jats:p>We present the first thin-air free memory model that admits compiler optimisations that aggressively leverage knowledge from alias analysis, an assumption of freedom from undefined behaviour, and from the extrinsic choices of real implementations such as over-alignment. Our model has tooling support with state-of-the-art performance, executing a battery of tests orders of magnitude quicker than other executable thin-air free semantics. The model integrates with the C\/C++ memory model through an exportable semantic dependency relation, it allows standard compilation mappings for atomics, and it matches all tests in the recently published desiderata for C\/C++ from the ISO.<\/jats:p>","DOI":"10.1145\/3721089","type":"journal-article","created":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T13:48:26Z","timestamp":1744206506000},"page":"1858-1882","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Symbolic MRD: Dynamic Memory, Undefined Behaviour, and Extrinsic Choice"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0009-0001-1738-3576","authenticated-orcid":false,"given":"Jay","family":"Richards","sequence":"first","affiliation":[{"name":"University of Kent, Canterbury, United Kingdom"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7404-2367","authenticated-orcid":false,"given":"Daniel","family":"Wright","sequence":"additional","affiliation":[{"name":"University of Surrey, Guildford, United Kingdom"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9365-9717","authenticated-orcid":false,"given":"Simon","family":"Cooksey","sequence":"additional","affiliation":[{"name":"Nvidia, Canterbury, United Kingdom"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7053-4364","authenticated-orcid":false,"given":"Mark","family":"Batty","sequence":"additional","affiliation":[{"name":"University of Kent, Canterbury, United Kingdom"}]}],"member":"320","published-online":{"date-parts":[[2025,4,9]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72019-3_1"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3458926"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594347"},{"key":"e_1_2_2_4_1","unstructured":"Mark Batty Simon Cooksey Scott Owens Anouk Paradis Marco Paviotti and Daniel Wright. 2014. P1780R2: Modular Relaxed Dependencies\u2013 A new approach to the Out-Of-Thin-Air Problem. https:\/\/graymalk.in\/iso-papers\/p1780\/p1780r2.html"},{"key":"e_1_2_2_5_1","unstructured":"Mark Batty Kayvan Memarian Kyndylan Nienhuis Jean Pichon and Peter Sewell. 2014. N4136: C Concurrency Challenges Draft. https:\/\/www.open-std.org\/jtc1\/sc22\/wg21\/docs\/papers\/2014\/n4136.pdf"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_12"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926394"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290383"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454082"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-54997-8_31"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66706-5_15"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_2_13_1","volume-title":"Standard for Programming Language C++","author":"International Organization for Standardization. 2023. Working Draft","year":"2023","unstructured":"International Organization for Standardization. 2023. Working Draft, Standard for Programming Language C++. International Organization for Standardization. https:\/\/www.open-std.org\/jtc1\/sc22\/wg21\/docs\/papers\/2023\/n4950.pdf"},{"key":"e_1_2_2_14_1","unstructured":"Matt Godbolt. 2012. Compiler explorer. https:\/\/godbolt.org"},{"key":"e_1_2_2_15_1","unstructured":"Richard Grisenthwaite. 2023. Views on Relaxed Atomics in C++ from Arm\u2019s technical leadership team. https:\/\/community.arm.com\/arm-community-blogs\/b\/architectures-and-processors-blog\/posts\/arm-technical-view-on-relaxed-atomics"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2934536"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498716"},{"key":"e_1_2_2_18_1","volume-title":"McKenney Alan Jeffrey and Ali Sezgin","author":"Paul","year":"2014","unstructured":"Paul E. McKenney Alan Jeffrey and Ali Sezgin. 2014. N4323: Out-of-Thin-Air Execution is Vacuous. https:\/\/www.open-std.org\/jtc1\/sc22\/wg21\/docs\/papers\/2014\/n4323.html"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009850"},{"key":"e_1_2_2_20_1","unstructured":"Ori Lahav. [n. d.]. A case against semantic dependencies. https:\/\/www.cs.tau.ac.il\/~orilahav\/papers\/sdep-fowm24.pdf"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062352"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_22"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386010"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3297858.3304043"},{"key":"e_1_2_2_25_1","unstructured":"Paul E. McKenney Alan Jeffrey Ali Sezgin and Tony Tye. 2016. Out-of-Thin-Air Execution is Vacuous. http:\/\/www.open-std.org\/jtc1\/sc22\/wg21\/docs\/papers\/2016\/p0422r0.html"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290380"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2983997"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-44914-8_22"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837616"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290382"},{"key":"e_1_2_2_31_1","unstructured":"William Pugh. 2004. Java Causality Test Cases. https:\/\/www.cs.umd.edu\/~pugh\/java\/memoryModel\/CausalityTestCases.html Accessed: 2018-11-17"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993520"},{"key":"e_1_2_2_33_1","volume-title":"Program transformations in weak memory models. Ph. D. Dissertation","author":"\u0160ev\u010d\u00edk Jaroslav","year":"1842","unstructured":"Jaroslav \u0160ev\u010d\u00edk. 2009. Program transformations in weak memory models. Ph. D. Dissertation. University of Edinburgh, UK. https:\/\/hdl.handle.net\/1842\/3132"},{"key":"e_1_2_2_34_1","unstructured":"Alan Stern Paul E. McKenney Michael Wong and Maged Michael. 2024. P3064R2: How to Avoid OOTA Without Really Trying. https:\/\/www.open-std.org\/jtc1\/sc22\/wg21\/docs\/papers\/2024\/p3064r2.pdf"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009838"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3721089","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3721089","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T17:10:08Z","timestamp":1760029808000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3721089"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,4,9]]},"references-count":35,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2025,4,9]]}},"alternative-id":["10.1145\/3721089"],"URL":"https:\/\/doi.org\/10.1145\/3721089","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,4,9]]},"assertion":[{"value":"2024-10-16","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-02-18","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-04-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}