{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,20]],"date-time":"2026-01-20T11:37:13Z","timestamp":1768909033145,"version":"3.49.0"},"reference-count":61,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2020,11,13]],"date-time":"2020-11-13T00:00:00Z","timestamp":1605225600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"National Science Foundation","award":["CCR-1617175"],"award-info":[{"award-number":["CCR-1617175"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2020,11,13]]},"abstract":"<jats:p>Relaxed memory models must simultaneously achieve efficient implementability and thread-compositional reasoning. Is that why they have become so complicated? We argue that the answer is no: It is possible to achieve these goals by combining an idea from the 60s (preconditions) with an idea from the 80s (pomsets), at least for X64 and ARMv8. We show that the resulting model (1) supports compositional reasoning for temporal safety properties, (2) supports all expected sequential compiler optimizations, (3) satisfies the DRF-SC criterion, and (4) compiles to X64 and ARMv8 microprocessors without requiring extra fences on relaxed accesses.<\/jats:p>","DOI":"10.1145\/3428262","type":"journal-article","created":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T23:36:06Z","timestamp":1606260966000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":22,"title":["Pomsets with preconditions: a simple model of relaxed memory"],"prefix":"10.1145","volume":"4","author":[{"given":"Radha","family":"Jagadeesan","sequence":"first","affiliation":[{"name":"DePaul University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alan","family":"Jeffrey","sequence":"additional","affiliation":[{"name":"Mozilla Research, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"James","family":"Riely","sequence":"additional","affiliation":[{"name":"DePaul University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2020,11,13]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/151646.151649"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/325164.325100"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/71.242161"},{"key":"e_1_2_2_5_1","unstructured":"Jade Alglave. 2019. This commit adds the Armv8 memory model for mixed-size accesses. https:\/\/github.com\/herd\/herdtools7\/ commit\/95785c747750be4a3b64adfab9d5f5ee0ead8240.  Jade Alglave. 2019. This commit adds the Armv8 memory model for mixed-size accesses. https:\/\/github.com\/herd\/herdtools7\/ commit\/95785c747750be4a3b64adfab9d5f5ee0ead8240."},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2627752"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1098\/rsta.2015.0406"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837637"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_12"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926394"},{"key":"e_1_2_2_12_1","unstructured":"Hans-J. Boehm. 2007. Memory Model Rationales. http:\/\/www.open-std.org\/jtc1\/sc22\/wg21\/docs\/papers\/2007\/n2176.  Hans-J. Boehm. 2007. Memory Model Rationales. http:\/\/www.open-std.org\/jtc1\/sc22\/wg21\/docs\/papers\/2007\/n2176."},{"key":"e_1_2_2_13_1","unstructured":"Hans-J. Boehm. 2018. Out-of-thin-air revisited again. http:\/\/www.open-std.org\/jtc1\/sc22\/wg21\/docs\/papers\/2018\/p1217r0.  Hans-J. Boehm. 2018. Out-of-thin-air revisited again. http:\/\/www.open-std.org\/jtc1\/sc22\/wg21\/docs\/papers\/2018\/p1217r0."},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2618128.2618134"},{"key":"e_1_2_2_15_1","unstructured":"Stephen Brookes. 2016. A denotational semantics for weak memory concurrency. http:\/\/www.cs.bham.ac.uk\/~pbl\/mgs2016\/ brookesslides.pdf. Midlands Graduate School in the Foundations of Computing Science.  Stephen Brookes. 2016. A denotational semantics for weak memory concurrency. http:\/\/www.cs.bham.ac.uk\/~pbl\/mgs2016\/ brookesslides.pdf. Midlands Graduate School in the Foundations of Computing Science."},{"key":"e_1_2_2_16_1","first-page":"39","article-title":"Weak memory models using event structures. In Vingt-septi\u00e8mes Journ\u00e9es Francophones des Langages Applicatifs (JFLA 2016 ). HAL-Inria, Saint-Malo","author":"Castellan Simon","year":"2016","unstructured":"Simon Castellan . 2016 . Weak memory models using event structures. In Vingt-septi\u00e8mes Journ\u00e9es Francophones des Langages Applicatifs (JFLA 2016 ). HAL-Inria, Saint-Malo , France , 39 - 53 . https:\/\/hal.inria.fr\/hal-01333582 Simon Castellan. 2016. Weak memory models using event structures. In Vingt-septi\u00e8mes Journ\u00e9es Francophones des Langages Applicatifs (JFLA 2016 ). HAL-Inria, Saint-Malo, France, 39-53. https:\/\/hal.inria.fr\/hal-01333582","journal-title":"France"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71316-6_23"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/3049832.3049844"},{"key":"e_1_2_2_19_1","unstructured":"Soham Chakraborty and Viktor Vafeiadis. 2018. Private correspondence.  Soham Chakraborty and Viktor Vafeiadis. 2018. Private correspondence."},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290383"},{"key":"e_1_2_2_21_1","unstructured":"Will Deacon. 2017. Formal memory model for Armv8.0 application level. https:\/\/github.com\/herd\/herdtools7\/commit\/ daa126680b6ecba97ba47b3e05bbaa51a89f27b7.  Will Deacon. 2017. Formal memory model for Armv8.0 application level. https:\/\/github.com\/herd\/herdtools7\/commit\/ daa126680b6ecba97ba47b3e05bbaa51a89f27b7."},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429110"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2019.00047"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192421"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293883.3295708"},{"key":"e_1_2_2_26_1","unstructured":"ECMA International. 2019. ECMAScript 2019 Language Specification. https:\/\/www.ecma-international. org\/ecma-262\/10.0\/.  ECMA International. 2019. ECMAScript 2019 Language Specification. https:\/\/www.ecma-international. org\/ecma-262\/10.0\/."},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837615"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009839"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(88)90124-7"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11957-6_17"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2934536"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-15(1:33)2019"},{"key":"e_1_2_2_34_1","first-page":"175","volume-title":"Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017","author":"Kang Jeehoon","year":"2017","unstructured":"Jeehoon Kang , Chung-Kil Hur , Ori Lahav , Viktor Vafeiadis , and Derek Dreyer . 2017 . A promising semantics for relaxedmemory concurrency . In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017 , Paris, France , January 18-20, 2017, Giuseppe Castagna and Andrew D. Gordon (Eds.). ACM, 175 - 189 . http:\/\/dl.acm.org\/citation.cfm?id= 3009850 Jeehoon Kang, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis, and Derek Dreyer. 2017. A promising semantics for relaxedmemory concurrency. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, Giuseppe Castagna and Andrew D. Gordon (Eds.). ACM, 175-189. http:\/\/dl.acm.org\/citation.cfm?id= 3009850"},{"key":"e_1_2_2_35_1","unstructured":"Jeehoon Kang Chung-Kil Hur Ori Lahav Viktor Vafeiadis and Derek Dreyer. 2018. Private correspondence.  Jeehoon Kang Chung-Kil Hur Ori Lahav Viktor Vafeiadis and Derek Dreyer. 2018. Private correspondence."},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-15(2:10)2019"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-48989-6_29"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062352"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1979.1675439"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01786227"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.5555\/648065.747612"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2518191"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/1047659.1040336"},{"key":"e_1_2_2_44_1","unstructured":"Paul E. McKenney Alan Jerfey Ali Sezgin and Tony Tye. 2016. 0422R0: Out-of-thin-air execution is vacuous. http:\/\/www.open-std.org\/jtc1\/sc22\/wg21\/docs\/papers\/2016\/p0422r0.  Paul E. McKenney Alan Jerfey Ali Sezgin and Tony Tye. 2016. 0422R0: Out-of-thin-air execution is vacuous. http:\/\/www.open-std.org\/jtc1\/sc22\/wg21\/docs\/papers\/2016\/p0422r0."},{"key":"e_1_2_2_45_1","volume-title":"Communicating and Mobile Systems: The-calculus","author":"Milner Robin","unstructured":"Robin Milner . 1999. Communicating and Mobile Systems: The-calculus . Cambridge University Press , New York, NY, USA . Robin Milner. 1999. Communicating and Mobile Systems: The-calculus. Cambridge University Press, New York, NY, USA."},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1981.230844"},{"key":"e_1_2_2_47_1","volume-title":"Reconciling Event Structures with Modern Multiprocessors. CoRR abs\/","author":"Moiseenko Evgenii","year":"1911","unstructured":"Evgenii Moiseenko , Anton Podkopaev , Ori Lahav , Orestis Melkonian , and Viktor Vafeiadis . 2019. Reconciling Event Structures with Modern Multiprocessors. CoRR abs\/ 1911 .06567 ( 2019 ), 34 pages. arXiv: 1911.06567 http:\/\/arxiv.org\/abs\/ 1911.06567 To appear in ECOOP 2020. Evgenii Moiseenko, Anton Podkopaev, Ori Lahav, Orestis Melkonian, and Viktor Vafeiadis. 2019. Reconciling Event Structures with Modern Multiprocessors. CoRR abs\/ 1911.06567 ( 2019 ), 34 pages. arXiv: 1911.06567 http:\/\/arxiv.org\/abs\/ 1911.06567 To appear in ECOOP 2020."},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-44914-8_22"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837616"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1090\/dimacs\/029\/07"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-82453-1_5"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290382"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/304065.304106"},{"key":"e_1_2_2_55_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_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158107"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314624"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/1229428.1229469"},{"key":"e_1_2_2_60_1","unstructured":"Jaroslav Sev\u010d\u00edk. 2011. Private correspondence.  Jaroslav Sev\u010d\u00edk. 2011. Private correspondence."},{"key":"e_1_2_2_61_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-16042-6_21"},{"key":"e_1_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_13"},{"key":"e_1_2_2_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676995"},{"key":"e_1_2_2_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385973"},{"key":"e_1_2_2_65_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\/3428262","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3428262","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:02:57Z","timestamp":1750197777000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3428262"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,11,13]]},"references-count":61,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2020,11,13]]}},"alternative-id":["10.1145\/3428262"],"URL":"https:\/\/doi.org\/10.1145\/3428262","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,11,13]]},"assertion":[{"value":"2020-11-13","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}