{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,30]],"date-time":"2026-04-30T19:53:21Z","timestamp":1777578801724,"version":"3.51.4"},"reference-count":35,"publisher":"Association for Computing Machinery (ACM)","issue":"3","funder":[{"DOI":"10.13039\/501100000038","name":"NSERC","doi-asserted-by":"crossref","award":["RGPIN-2019-05213"],"award-info":[{"award-number":["RGPIN-2019-05213"]}],"id":[{"id":"10.13039\/501100000038","id-type":"DOI","asserted-by":"crossref"}]},{"name":"EPSRC UK","award":["EP\/X015076\/1"],"award-info":[{"award-number":["EP\/X015076\/1"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2025,9,30]]},"abstract":"<jats:p>\n            A memory consistency model specifies the allowed behaviors of shared memory concurrent programs. At the language level, these models are known to have a non-trivial impact on the safety of program optimizations. This limits the ability to rearrange\/refactor code without introducing new behaviors. Existing programming language memory models try to address this by permitting more (\n            <jats:italic>relaxed\/weak<\/jats:italic>\n            ) concurrent behaviors, but are still unable to allow all the desired optimizations. A core problem is that\n            <jats:italic>weaker<\/jats:italic>\n            consistency models may also render optimizations unsafe, a conclusion that goes against the intuition of them allowing more behaviors. This exposes an open problem of the\n            <jats:italic>compositional interaction<\/jats:italic>\n            between memory consistency semantics and optimizations; which parts of the semantics correspond to allowing\/disallowing which set of optimizations is unclear. In this work, we establish a formal foundation suitable enough to understand this compositional nature. We decompose optimizations into a finite set of elementary\n            <jats:italic>effects<\/jats:italic>\n            , over which aspects of safety can be assessed. We use this decomposition to identify a desirable compositional property (\n            <jats:italic>complete<\/jats:italic>\n            ) that would guarantee the safety of optimizations from one memory model to another. We showcase its practicality by proving such a property between Sequential Consistency (SC) and\n            <jats:italic>SC<\/jats:italic>\n            <jats:sub>\n              <jats:italic>RR<\/jats:italic>\n            <\/jats:sub>\n            , the latter allowing independent read-read reordering over\n            <jats:italic>SC<\/jats:italic>\n            . Our work potentially paves way to a new design methodology of programming-language memory models, one that places emphasis on the optimizations desired to be performed.\n          <\/jats:p>","DOI":"10.1145\/3721143","type":"journal-article","created":{"date-parts":[[2025,3,5]],"date-time":"2025-03-05T10:11:03Z","timestamp":1741169463000},"page":"1-42","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Memory Consistency and Program Transformations"],"prefix":"10.1145","volume":"37","author":[{"ORCID":"https:\/\/orcid.org\/0009-0005-2587-0605","authenticated-orcid":false,"given":"Akshay","family":"Gopalakrishnan","sequence":"first","affiliation":[{"name":"Computer Science, McGill University, Montreal, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0663-7347","authenticated-orcid":false,"given":"Clark","family":"Verbrugge","sequence":"additional","affiliation":[{"name":"Computer Science, McGill University, Montreal, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7053-4364","authenticated-orcid":false,"given":"Mark","family":"Batty","sequence":"additional","affiliation":[{"name":"Computer Science, University of Kent, Canterbury, United Kingdom of Great Britain and Northern Ireland"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,6,14]]},"reference":[{"key":"e_1_3_4_2_2","doi-asserted-by":"publisher","DOI":"10.1145\/1787234.1787255"},{"key":"e_1_3_4_3_2","doi-asserted-by":"publisher","DOI":"10.1109\/2.546611"},{"key":"e_1_3_4_4_2","doi-asserted-by":"publisher","DOI":"10.5555\/6448"},{"key":"e_1_3_4_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/2627752"},{"key":"e_1_3_4_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/1925844.1926442"},{"key":"e_1_3_4_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_12"},{"key":"e_1_3_4_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926394"},{"key":"e_1_3_4_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/2618128.2618134"},{"key":"e_1_3_4_10_2","doi-asserted-by":"publisher","DOI":"10.5555\/2001252.2001255"},{"key":"e_1_3_4_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/2854038.2854051"},{"key":"e_1_3_4_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/3290383"},{"key":"e_1_3_4_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/1281700.1281703"},{"key":"e_1_3_4_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_36"},{"key":"e_1_3_4_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-95953-1_14"},{"key":"e_1_3_4_16_2","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009850"},{"key":"e_1_3_4_17_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-48989-6_29"},{"key":"e_1_3_4_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062352"},{"key":"e_1_3_4_19_2","doi-asserted-by":"publisher","DOI":"10.1109\/12.599898"},{"key":"e_1_3_4_20_2","unstructured":"Sung-Hwan Lee. 2023. A Miscompilation Bug in Loop Invariant Code Motion Pass (LLVM). Retrieved April 2024 from https:\/\/github.com\/llvm\/llvm-project\/issues\/64188"},{"key":"e_1_3_4_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040336"},{"key":"e_1_3_4_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993522"},{"key":"e_1_3_4_23_2","doi-asserted-by":"publisher","DOI":"10.1134\/S0361768821060050"},{"key":"e_1_3_4_24_2","volume-title":"Advanced Compiler Design and Implementation","author":"Muchnick Steven","year":"1997","unstructured":"Steven Muchnick. 1997. Advanced Compiler Design and Implementation. Morgan Kaufmann."},{"key":"e_1_3_4_25_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_27"},{"key":"e_1_3_4_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-44914-8_22"},{"key":"e_1_3_4_27_2","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837616"},{"key":"e_1_3_4_28_2","doi-asserted-by":"publisher","unstructured":"Jean Yves Alexis Pichon-Pharabod. 2018. A no-thin-air memory model for programming languages. phdthesis. Apollo - University of Cambridge Repository. DOI:10.17863\/CAM.21597","DOI":"10.17863\/CAM.21597"},{"key":"e_1_3_4_29_2","doi-asserted-by":"publisher","DOI":"10.1145\/3290382"},{"key":"e_1_3_4_30_2","doi-asserted-by":"publisher","DOI":"10.1145\/304065.304106"},{"key":"e_1_3_4_31_2","doi-asserted-by":"publisher","DOI":"10.1002\/1096-9128(200005)12:6<445::AID-CPE484>3.0.CO;2-A"},{"key":"e_1_3_4_32_2","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993520"},{"key":"e_1_3_4_33_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70592-5_3"},{"key":"e_1_3_4_34_2","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676995"},{"key":"e_1_3_4_35_2","doi-asserted-by":"publisher","DOI":"10.1145\/1993316.1993534"},{"key":"e_1_3_4_36_2","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385973"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3721143","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,15]],"date-time":"2025-06-15T07:17:38Z","timestamp":1749971858000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3721143"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,14]]},"references-count":35,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2025,9,30]]}},"alternative-id":["10.1145\/3721143"],"URL":"https:\/\/doi.org\/10.1145\/3721143","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,6,14]]},"assertion":[{"value":"2024-06-03","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-02-25","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-06-14","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}