{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T22:17:27Z","timestamp":1770243447951,"version":"3.49.0"},"reference-count":32,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2024,10,8]],"date-time":"2024-10-08T00:00:00Z","timestamp":1728345600000},"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":[[2024,10,8]]},"abstract":"<jats:p>\n                    Programs written in C\/C++ often include\n                    <jats:italic toggle=\"yes\">inline assembly<\/jats:italic>\n                    : a snippet of architecture-specific assembly code used to access low-level functionalities that are impossible or expensive to simulate in the source language. Although inline assembly is widely used, its semantics has not yet been formally studied.\n                  <\/jats:p>\n                  <jats:p>\n                    In this paper, we overcome this deficiency by investigating the effect of inline assembly on the\n                    <jats:italic toggle=\"yes\">consistency<\/jats:italic>\n                    semantics of C\/C++ programs. We propose the first memory model of the C++ Programming Language with support for inline assembly for Intel\u2019s x86 including\n                    <jats:italic toggle=\"yes\">non-temporal stores<\/jats:italic>\n                    and\n                    <jats:italic toggle=\"yes\">store fences<\/jats:italic>\n                    . We argue that previous provably correct compiler optimizations and correct compiler mappings should remain correct under such an extended model and we prove that this requirement is met by our proposed model.\n                  <\/jats:p>","DOI":"10.1145\/3689749","type":"journal-article","created":{"date-parts":[[2024,10,8]],"date-time":"2024-10-08T03:23:04Z","timestamp":1728357784000},"page":"1081-1107","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Extending the C\/C++ Memory Model with Inline Assembly"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7379-310X","authenticated-orcid":false,"given":"Paulo Em\u00edlio","family":"de Vilhena","sequence":"first","affiliation":[{"name":"Imperial College London, London, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4305-6998","authenticated-orcid":false,"given":"Ori","family":"Lahav","sequence":"additional","affiliation":[{"name":"Tel Aviv University, Tel Aviv, Israel"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8436-0334","authenticated-orcid":false,"given":"Viktor","family":"Vafeiadis","sequence":"additional","affiliation":[{"name":"MPI-SWS, Kaiserslautern, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2319-3242","authenticated-orcid":false,"given":"Azalea","family":"Raad","sequence":"additional","affiliation":[{"name":"Imperial College London, London, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,10,8]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","unstructured":"Jade Alglave Richard Grisenthwaite Artem Khyzha Luc Maranget and Nikos Nikoleris. 2024. Puss In Boots: on formalizing Arm\u2019s Virtual Memory System Architecture. IEEE Micro (July 2024) 1\u20139. https:\/\/doi.org\/10.1109\/MM.2024.3422668 10.1109\/MM.2024.3422668","DOI":"10.1109\/MM.2024.3422668"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2627752"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","unstructured":"Mark Batty Kayvan Memarian Scott Owens Susmit Sarkar and Peter Sewell. 2012. Clarifying and Compiling C\/C++ Concurrency: From C++11 to POWER (Principles of Programming Languagaes (POPL)). 509\u2014-520. https:\/\/doi.org\/10.1145\/2103656.2103717 10.1145\/2103656.2103717","DOI":"10.1145\/2103656.2103717"},{"key":"e_1_3_1_5_1","first-page":"55","volume-title":"Principles of Programming Languages (POPL)","author":"Batty Mark","year":"2011","unstructured":"Mark Batty, Scott Owens, Susmit Sarkar, Peter Sewell, and Tjark Weber. 2011. Mathematizing C++ concurrency. In Principles of Programming Languages (POPL). ACM Press, 55\u201366. https:\/\/www.cl.cam.ac.uk\/~pes20\/cpp\/popl085ap-sewell.pdf"},{"key":"e_1_3_1_6_1","unstructured":"Clang Project. 2007. Clang: a C language family frontend for LLVM. https:\/\/clang.llvm.org\/"},{"key":"e_1_3_1_7_1","unstructured":"Cppreference Community. 2019. Cppreference - Memory Order. https:\/\/en.cppreference.com\/w\/cpp\/atomic\/memory_order"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","unstructured":"Paulo Em\u00edlio de Vilhena Ori Lahav Viktor Vafeiadis and Azalea Raad. 2024. Extending the C\/C++ Memory Model with Inline Assembly \u2013 Technical Appendix. https:\/\/doi.org\/10.5281\/zenodo.13625916 10.5281\/zenodo.13625916","DOI":"10.5281\/zenodo.13625916"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/321420.321422"},{"key":"e_1_3_1_10_1","doi-asserted-by":"crossref","unstructured":"Michael J. Flynn. 1972. Some Computer Organizations and Their Effectiveness. IEEE Trans. Computers C-21 (Nov. 1972). https:\/\/ieeexplore.ieee.org\/document\/5009071","DOI":"10.1109\/TC.1972.5009071"},{"key":"e_1_3_1_11_1","unstructured":"GNU Project. 1987. GNU Compiler Collection. https:\/\/gcc.gnu.org\/git\/gcc.git"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591267"},{"key":"e_1_3_1_13_1","unstructured":"Intel. 2024. Intel 64 and IA-32 Architectures Software Developer\u2019s Manual (Combined Volumes). https:\/\/software.intel.com\/content\/www\/us\/en\/develop\/download\/intel-64-and-ia-32-architectures-sdm-combined-volumes-1-2a-2b-2c-2d-3a-3b-3c-3d-and-4.html Order Number: 325462-083US."},{"key":"e_1_3_1_14_1","unstructured":"ISO. 2011. ISO International Standard ISO\/IEC 14882:2011(E) \u2013 Programming Language C++. International Organization for Standardization (ISO). https:\/\/www.iso.org\/standard\/50372.html"},{"key":"e_1_3_1_15_1","doi-asserted-by":"crossref","unstructured":"Jeehoon Kang Chung-Kil Hur Ori Lahav Viktor Vafeiadis and Derek Dreyer. 2017. A promising semantics for relaxed- memory concurrency. In Principles of Programming Languages (POPL). 175\u2013189. https:\/\/www.cs.tau.ac.il\/~orilahav\/papers\/popl17.pdf","DOI":"10.1145\/3009837.3009850"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571212"},{"key":"e_1_3_1_17_1","doi-asserted-by":"crossref","unstructured":"Ori Lahav Viktor Vafeiadis Jeehoon Kang Chung-Kil Hur and Derek Dreyer. 2017. Repairing sequential consistency in C\/C++11. In Programming Language Design and Implementation (PLDI). ACM Press 618\u2013632. https:\/\/plv.mpi-sws.org\/scfix\/paper.pdf","DOI":"10.1145\/3062341.3062352"},{"key":"e_1_3_1_18_1","unstructured":"Xavier Leroy. 2021. The CompCert C verified compiler. http:\/\/compcert.org\/man."},{"key":"e_1_3_1_19_1","unstructured":"Linux Kernel Community. 2007. Linux Kernel-Based Virtual Machine. https:\/\/git.kernel.org\/pub\/scm\/virt\/kvm\/kvm.git"},{"key":"e_1_3_1_20_1","unstructured":"Linux Kernel Mailing List. 1999. spin_unlock optimization(i386). https:\/\/lists.archive.carbon60.com\/linux\/kernel\/105412"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434285"},{"key":"e_1_3_1_22_1","unstructured":"Microsoft Learn. 2021. Advantages of Inline Assembly. https:\/\/learn.microsoft.com\/en-us\/cpp\/assembler\/inline\/advantages-of-inline-assembly"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","unstructured":"Anton Podkopaev Ori Lahav and Viktor Vafeiadis. 2019. Bridging the Gap between Programming Languages and Hardware Weak Memory Models. In Principles of Programming Languages (POPL) Vol. 3. ACM Press 69:1\u201369:31. https:\/\/doi.org\/10.1145\/3290382 10.1145\/3290382","DOI":"10.1145\/3290382"},{"key":"e_1_3_1_25_1","unstructured":"Jeff Preshing. 2012. Memory Ordering at Compile Time. https:\/\/preshing.com\/20120625\/memory-ordering-at-compile-time"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","unstructured":"Christopher Pulte Shaked Flur Will Deacon Jon French Susmit Sarkar and Peter Sewell. 2017. Simplifying ARM Concurrency: Multicopy-Atomic Axiomatic and Operational Models for ARMv8 Vol. 2. ACM Press 19:1\u201319:29. https:\/\/doi.org\/10.1145\/3158107 10.1145\/3158107","DOI":"10.1145\/3158107"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498683"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","unstructured":"Michael Sammler Simon Spies Youngju Song Emanuele D\u2019Osualdo Robbert Krebbers Deepak Garg and Derek Dreyer. 2023. DimSum: A Decentralized Approach to Multi-Language Semantics and Verification Vol. 7. 27:1\u201327:31. https:\/\/doi.org\/10.1145\/3571220 10.1145\/3571220","DOI":"10.1145\/3571220"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","unstructured":"Susmit Sarkar Kayvan Memarian Scott Owens Mark Batty Peter Sewell Luc Maranget Jade Alglave and Derek Williams. 2012. Synchronising C\/C++ and POWER (Programming Language Design and Implementation (PLDI)). 311\u2014-322. https:\/\/doi.org\/10.1145\/2254064.2254102 10.1145\/2254064.2254102","DOI":"10.1145\/2254064.2254102"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1785414.1785443"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","unstructured":"Ben Simner Alasdair Armstrong Jean Pichon-Pharabod Christopher Pulte Richard Grisenthwaite and Peter Sewell. 2022. Relaxed Virtual Memory in Armv8-A. In European Symposium on Programming (ESOP) (Lecture Notes in Computer Science Vol. 13240). Springer 143\u2013173. https:\/\/doi.org\/10.1007\/978-3-030-99336-8_6 10.1007\/978-3-030-99336-8_6","DOI":"10.1007\/978-3-030-99336-8_6"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","unstructured":"Pradeep S. Sindhu Jean-Marc Frailong and Michel Cekleov. 1992. Formal Specification of Memory Models. Springer 25\u201341. https:\/\/doi.org\/10.1007\/978-1-4615-3604-8_2 10.1007\/978-1-4615-3604-8_2","DOI":"10.1007\/978-1-4615-3604-8_2"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","unstructured":"Viktor Vafeiadis Thibault Balabonski Soham Chakraborty Robin Morisset and Francesco Zappa Nardelli. 2015. Common Compiler Optimisations are Invalid in the C11 Memory Model and What We Can Do About It. In Principles of Programming Languages (POPL). ACM Press 209\u2013220. https:\/\/dl.acm.org\/doi\/10.1145\/2676726.2676995 10.1145\/2676726.2676995","DOI":"10.1145\/2676726.2676995"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3689749","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3689749","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T09:10:46Z","timestamp":1770196246000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3689749"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,8]]},"references-count":32,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2024,10,8]]}},"alternative-id":["10.1145\/3689749"],"URL":"https:\/\/doi.org\/10.1145\/3689749","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,10,8]]},"assertion":[{"value":"2024-04-05","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-08-18","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-10-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}