{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,2]],"date-time":"2026-10-02T07:52:23Z","timestamp":1790927543133,"version":"4.1.0"},"reference-count":35,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,1,2]],"date-time":"2019-01-02T00:00:00Z","timestamp":1546387200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100002261","name":"Russian Foundation for Basic Research","doi-asserted-by":"publisher","award":["18-01-00380"],"award-info":[{"award-number":["18-01-00380"]}],"id":[{"id":"10.13039\/501100002261","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001742","name":"Israel Science Foundation","doi-asserted-by":"publisher","award":["5166651"],"award-info":[{"award-number":["5166651"]}],"id":[{"id":"10.13039\/501100001742","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100011643","name":"Blavatnik Family Foundation","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100011643","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":[[2019,1,2]]},"abstract":"<jats:p>We develop a new intermediate weak memory model, IMM, as a way of modularizing the proofs of correctness of compilation from concurrent programming languages with weak memory consistency semantics to mainstream multi-core architectures, such as POWER and ARM. We use IMM to prove the correctness of compilation from the promising semantics of Kang et al. to POWER (thereby correcting and improving their result) and ARMv7, as well as to the recently revised ARMv8 model. Our results are mechanized in Coq, and to the best of our knowledge, these are the first machine-verified compilation correctness results for models that are weaker than x86-TSO.<\/jats:p>","DOI":"10.1145\/3290382","type":"journal-article","created":{"date-parts":[[2019,1,4]],"date-time":"2019-01-04T13:33:51Z","timestamp":1546608831000},"page":"1-31","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":58,"title":["Bridging the gap between programming languages and hardware weak memory models"],"prefix":"10.1145","volume":"3","author":[{"given":"Anton","family":"Podkopaev","sequence":"first","affiliation":[{"name":"St. Petersburg University, Russia \/ JetBrains Research, Russia \/ MPI-SWS, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ori","family":"Lahav","sequence":"additional","affiliation":[{"name":"Tel Aviv University, Israel"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Viktor","family":"Vafeiadis","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,1,2]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3173162.3177156"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2627752"},{"key":"e_1_2_2_3_1","volume-title":"The Problem of Programming Language Concurrency Semantics. In ESOP 2015 (LNCS)","volume":"9032","author":"Batty Mark","year":"2015","unstructured":"Mark Batty , Kayvan Memarian , Kyndylan Nienhuis , Jean Pichon-Pharabod , and Peter Sewell . 2015 . The Problem of Programming Language Concurrency Semantics. In ESOP 2015 (LNCS) , Vol. 9032 . Springer, Berlin, Heidelberg, 283\u2013307. Mark Batty, Kayvan Memarian, Kyndylan Nienhuis, Jean Pichon-Pharabod, and Peter Sewell. 2015. The Problem of Programming Language Concurrency Semantics. In ESOP 2015 (LNCS), Vol. 9032. Springer, Berlin, Heidelberg, 283\u2013307."},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103717"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926394"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2618128.2618134"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/CGO.2017.7863732"},{"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\/3192366.3192373"},{"key":"e_1_2_2_10_1","volume-title":"Retrieved","author":"Deacon Will","year":"2017","unstructured":"Will Deacon . 2017 . The ARMv8 Application Level Memory Model . Retrieved June 27, 2018 from https:\/\/github.com\/herd\/ herdtools7\/blob\/master\/herd\/libdir\/aarch64.cat Will Deacon. 2017. The ARMv8 Application Level Memory Model. Retrieved June 27, 2018 from https:\/\/github.com\/herd\/ herdtools7\/blob\/master\/herd\/libdir\/aarch64.cat"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192421"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158106"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837615"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009839"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2934536"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009850"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837643"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-48989-6_29"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062352"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_2_2_21_1","volume-title":"Counterexamples and Proof Loophole for the C\/C++ to POWER and ARMv7 Trailing-Sync Compiler Mappings. CoRR abs\/1611.01507","author":"Manerkar Yatin A.","year":"2016","unstructured":"Yatin A. Manerkar , Caroline Trippel , Daniel Lustig , Michael Pellauer , and Margaret Martonosi . 2016. Counterexamples and Proof Loophole for the C\/C++ to POWER and ARMv7 Trailing-Sync Compiler Mappings. CoRR abs\/1611.01507 ( 2016 ). http:\/\/arxiv.org\/abs\/1611.01507 Yatin A. Manerkar, Caroline Trippel, Daniel Lustig, Michael Pellauer, and Margaret Martonosi. 2016. Counterexamples and Proof Loophole for the C\/C++ to POWER and ARMv7 Trailing-Sync Compiler Mappings. CoRR abs\/1611.01507 (2016). http:\/\/arxiv.org\/abs\/1611.01507"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040336"},{"key":"e_1_2_2_23_1","volume-title":"Retrieved","author":"Mapping","year":"2016","unstructured":"Mapping 2016 . C\/C++11 mappings to processors . Retrieved June 27, 2018 from http:\/\/www.cl.cam.ac.uk\/~pes20\/cpp\/ cpp0xmappings.html Mapping 2016. C\/C++11 mappings to processors. Retrieved June 27, 2018 from http:\/\/www.cl.cam.ac.uk\/~pes20\/cpp\/ cpp0xmappings.html"},{"key":"e_1_2_2_24_1","unstructured":"Luc Maranget Susmit Sarkar and Peter Sewell. 2012. A Tutorial Introduction to the ARM and POWER Relaxed Memory Models. http:\/\/www.cl.cam.ac.uk\/~pes20\/ppc-supplemental\/test7.pdf .  Luc Maranget Susmit Sarkar and Peter Sewell. 2012. A Tutorial Introduction to the ARM and POWER Relaxed Memory Models. http:\/\/www.cl.cam.ac.uk\/~pes20\/ppc-supplemental\/test7.pdf ."},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_27"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837616"},{"key":"e_1_2_2_27_1","volume-title":"ECOOP 2017 (LIPIcs)","volume":"74","author":"Podkopaev Anton","year":"2017","unstructured":"Anton Podkopaev , Ori Lahav , and Viktor Vafeiadis . 2017 . Promising Compilation to ARMv8 POP . In ECOOP 2017 (LIPIcs) , Vol. 74 . Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 22:1\u201322:28. Anton Podkopaev, Ori Lahav, and Viktor Vafeiadis. 2017. Promising Compilation to ARMv8 POP. In ECOOP 2017 (LIPIcs), Vol. 74. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 22:1\u201322:28."},{"key":"e_1_2_2_28_1","unstructured":"Anton Podkopaev Ori Lahav and Viktor Vafeiadis. 2018. Coq proof scripts and supplementary material for this paper available at http:\/\/plv.mpi- sws.org\/imm\/ .  Anton Podkopaev Ori Lahav and Viktor Vafeiadis. 2018. Coq proof scripts and supplementary material for this paper available at http:\/\/plv.mpi- sws.org\/imm\/ ."},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158107"},{"key":"e_1_2_2_30_1","volume-title":"The RISC-V Instruction Set Manual. Volume I: Unprivileged ISA.","author":"RISC-V","year":"2018","unstructured":"RISC-V 2018. The RISC-V Instruction Set Manual. Volume I: Unprivileged ISA. Available at https:\/\/github.com\/riscv\/ riscv- isa- manual\/releases\/download\/draft- 20180731- e264b74\/riscv- spec.pdf {Online; accessed 23- August - 2018 }. RISC-V 2018. The RISC-V Instruction Set Manual. Volume I: Unprivileged ISA. Available at https:\/\/github.com\/riscv\/ riscv- isa- manual\/releases\/download\/draft- 20180731- e264b74\/riscv- spec.pdf {Online; accessed 23-August-2018}."},{"key":"e_1_2_2_31_1","volume-title":"Retrieved","author":"RISCV","year":"2018","unstructured":"RISCV in herd 2018 . RISCV: herd vs. operational models . Retrieved October 22, 2018 from http:\/\/diy.inria.fr\/cats7\/riscv\/ RISCV in herd 2018. RISCV: herd vs. operational models. Retrieved October 22, 2018 from http:\/\/diy.inria.fr\/cats7\/riscv\/"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676995"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2487241.2487248"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009838"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISCA.2018.00021"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290382","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3290382","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:58:04Z","timestamp":1750208284000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290382"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,2]]},"references-count":35,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2019,1,2]]}},"alternative-id":["10.1145\/3290382"],"URL":"https:\/\/doi.org\/10.1145\/3290382","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,1,2]]},"assertion":[{"value":"2019-01-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}