{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T09:11:08Z","timestamp":1770282668614,"version":"3.49.0"},"reference-count":47,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2025,1,7]],"date-time":"2025-01-07T00:00:00Z","timestamp":1736208000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,1,7]]},"abstract":"<jats:p>Defining a formal model for concurrency in programming languages that addresses conflicting requirements from programmers, compilers, and architectures has been a long-standing research question. It is widely believed that traditional axiomatic per-execution models that reason about individual executions do not suffice to address these conflicting requirements. Consequently, several multi-execution models were proposed that reason about multiple executions together. Although multi-execution models were major breakthroughs in satisfying several desired properties, these models are complicated, challenging to adapt to existing language specifications given in per-execution style, and they are typically not friendly to automated reasoning tools.<\/jats:p>\n                  <jats:p>In response, we propose a re-execution-based memory model (XMM). Debunking the beliefs around per-execution and multi-execution models, XMM is (almost) a per-execution model. XMM reasons about individual executions, but unlike traditional per-execution models, it relates executions by a re-execution principle. As such, the memory consistency axioms and the out-of-order re-execution mechanics are orthogonal in XMM, allowing to use it as a semantic framework parameterized by a given axiomatic memory model.<\/jats:p>\n                  <jats:p>We instantiated the XMM framework for the RC20 language model, and proved that the resulting model XC20 provides DRF guarantees and allows standard hardware mappings and compiler optimizations. Note-worthy, XC20 is the first model of its kind that also supports thread sequentialization optimization. Moreover, XC20 is also amenable to automated reasoning. To demonstrate this, we developed a sound model checker XMC and evaluated it on several concurrency benchmarks.<\/jats:p>","DOI":"10.1145\/3704908","type":"journal-article","created":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T05:48:42Z","timestamp":1736401722000},"page":"2149-2175","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Relaxed Memory Concurrency Re-executed"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2715-1143","authenticated-orcid":false,"given":"Evgenii","family":"Moiseenko","sequence":"first","affiliation":[{"name":"JetBrains Research, Belgrade, Serbia"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-4329-1025","authenticated-orcid":false,"given":"Matteo","family":"Meluzzi","sequence":"additional","affiliation":[{"name":"TU Delft, Delft, Netherlands"}]},{"ORCID":"https:\/\/orcid.org\/0009-0004-2539-7160","authenticated-orcid":false,"given":"Innokentii","family":"Meleshchenko","sequence":"additional","affiliation":[{"name":"JetBrains Research, Paphos, Cyprus"},{"name":"Neapolis University Pafos, Paphos, Cyprus"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-5044-4953","authenticated-orcid":false,"given":"Ivan","family":"Kabashnyi","sequence":"additional","affiliation":[{"name":"JetBrains Research, Bremen, Germany"},{"name":"Constructor University Bremen, Bremen, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9448-6587","authenticated-orcid":false,"given":"Anton","family":"Podkopaev","sequence":"additional","affiliation":[{"name":"JetBrains Research, Amsterdam, Netherlands"},{"name":"Constructor University Bremen, Bremen, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4454-2050","authenticated-orcid":false,"given":"Soham","family":"Chakraborty","sequence":"additional","affiliation":[{"name":"TU Delft, Delft, Netherlands"}]}],"member":"320","published-online":{"date-parts":[[2025,1,9]]},"reference":[{"key":"e_1_3_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_28"},{"key":"e_1_3_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-016-0275-0"},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/325164.325100"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74591-4_4"},{"key":"e_1_3_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429099"},{"key":"e_1_3_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837637"},{"key":"e_1_3_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_12"},{"key":"e_1_3_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926394"},{"key":"e_1_3_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375591"},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290383"},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_20"},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3575693.3575729"},{"key":"e_1_3_2_15_1","unstructured":"James Gosling Bill Joy and Guy Steele. 1996. The Java Language Specification. Addison Wesley (1996)."},{"key":"e_1_3_2_16_1","unstructured":"ISO\/IEC 14882. 2011. Programming Language C++. (2011)."},{"key":"e_1_3_2_17_1","unstructured":"ISO\/IEC 9899. 2011. Programming Language C. (2011)."},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428262"},{"key":"e_1_3_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2934536"},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498716"},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498716"},{"key":"e_1_3_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3093333.3009850"},{"key":"e_1_3_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498711"},{"key":"e_1_3_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373376.3378480"},{"key":"e_1_3_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-8_20"},{"key":"e_1_3_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485475"},{"key":"e_1_3_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062352"},{"key":"e_1_3_2_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1979.1675439"},{"key":"e_1_3_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386010"},{"key":"e_1_3_2_30_1","unstructured":"Litmus. [n. d.]. Causality Test Cases. http:\/\/www.cs.umd.edu\/~pugh\/java\/memoryModel\/unifiedProposal\/testcases.html. ([n. d.])."},{"key":"e_1_3_2_31_1","doi-asserted-by":"publisher","unstructured":"Weiyu Luo and Brian Demsky. 2021. C11Tester: a race detector for C\/C++ atomics. In ASPLOS 2021. 630\u2013646. https:\/\/doi.org\/10.1145\/3445814.3446711 10.1145\/3445814.3446711","DOI":"10.1145\/3445814.3446711"},{"key":"e_1_3_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040336"},{"key":"e_1_3_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040336"},{"key":"e_1_3_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434285"},{"key":"e_1_3_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563315"},{"key":"e_1_3_2_36_1","doi-asserted-by":"publisher","unstructured":"Evgenii Moiseenko Matteo Meluzzi Innokentii Meleshchenko Ivan Kabashnyi Anton Podkopaev and Soham Chakraborty. 2025a. Relaxed memory concurrency re-executed (artifact). (2025). Available at https:\/\/doi.org\/10.5281\/zenodo.13912067 10.5281\/zenodo.13912067.","DOI":"10.5281\/zenodo.13912067"},{"key":"e_1_3_2_37_1","doi-asserted-by":"crossref","unstructured":"Evgenii Moiseenko Matteo Meluzzi Innokentii Meleshchenko Ivan Kabashnyi Anton Podkopaev and Soham Chakraborty. 2025b. Relaxed memory concurrency re-executed (technical appendix). (2025). Available at https:\/\/eupp.github.io\/papers\/popl2025-xmm-apdx.pdf.","DOI":"10.1145\/3704908"},{"key":"e_1_3_2_38_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2020.5"},{"key":"e_1_3_2_39_1","doi-asserted-by":"publisher","unstructured":"Brian Norris and Brian Demsky. 2013. CDSChecker: Checking Concurrent Data Structures Written with C\/C++ Atomics. In OOPSLA\u201913. https:\/\/doi.org\/10.1145\/2509136.2509514 10.1145\/2509136.2509514","DOI":"10.1145\/2509136.2509514"},{"key":"e_1_3_2_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-44914-8_22"},{"key":"e_1_3_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676995"},{"key":"e_1_3_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290382"},{"key":"e_1_3_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/304065.304106"},{"key":"e_1_3_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314624"},{"key":"e_1_3_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254102"},{"key":"e_1_3_2_46_1","doi-asserted-by":"publisher","unstructured":"Susmit Sarkar Peter Sewell Jade Alglave Luc Maranget and Derek Williams. 2011. Understanding POWER Multiprocessors. In PLDI \u201811. 175\u2013186. https:\/\/doi.org\/10.1145\/1993498.1993520 10.1145\/1993498.1993520","DOI":"10.1145\/1993498.1993520"},{"key":"e_1_3_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591251"},{"key":"e_1_3_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676995"},{"key":"e_1_3_2_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70592-5_3"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704908","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3704908","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T10:17:15Z","timestamp":1770200235000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704908"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,7]]},"references-count":47,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2025,1,7]]}},"alternative-id":["10.1145\/3704908"],"URL":"https:\/\/doi.org\/10.1145\/3704908","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,1,7]]},"assertion":[{"value":"2024-07-11","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-11-07","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-01-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}