Extending the C/C++ Memory Model with Inline Assembly
Article No.: 309, Pages 1081 - 1107
Abstract
Programs written in C/C++ often include inline assembly: 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. In this paper, we overcome this deficiency by investigating the effect of inline assembly on the consistency semantics of C/C++ programs. We propose the first memory model of the C++ Programming Language with support for inline assembly for Intel's x86 including non-temporal stores and store fences. 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.
References
[1]
Jade Alglave, Richard Grisenthwaite, Artem Khyzha, Luc Maranget, and Nikos Nikoleris. 2024. Puss In Boots: on formalizing Arm’s Virtual Memory System Architecture. IEEE Micro, July, 1–9. https://doi.org/10.1109/MM.2024.3422668
[2]
Jade Alglave, Luc Maranget, and Michael Tautschnig. 2014. Herding Cats - Modelling, simulation, testing, and data-mining for weak memory. ACM Transactions on Programming Languages and Systems, 36, 2 (2014), https://doi.org/10.1145/2627752
[3]
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 Languages (POPL). 509––520. https://doi.org/10.1145/2103656.2103717
[4]
Mark Batty, Scott Owens, Susmit Sarkar, Peter Sewell, and Tjark Weber. 2011. Mathematizing C++ concurrency. In Principles of Programming Languages (POPL). ACM Press, 55–66. https://www.cl.cam.ac.uk/~pes20/cpp/popl085ap-sewell.pdf
[5]
Clang Project. 2007. Clang: a C language family frontend for LLVM. https://clang.llvm.org/
[6]
Cppreference Community. 2019. Cppreference - Memory Order. https://en.cppreference.com/w/cpp/atomic/memory_order
[7]
Robert W. Floyd. 1967. Nondeterministic Algorithms. Journal of the ACM, 14, 4 (1967), Oct., 636–644. https://doi.org/10.1145/321420.321422
[8]
Michael J. Flynn. 1972. Some Computer Organizations and Their Effectiveness. IEEE Trans. Computers, C-21 (1972), Nov., https://ieeexplore.ieee.org/document/5009071
[9]
GNU Project. 1987. GNU Compiler Collection. https://gcc.gnu.org/git/gcc.git
[10]
Andrés Goens, Soham Chakraborty, Susmit Sarkar, Sukarn Agarwal, Nicolai Oswald, and Vijay Nagarajan. 2023. Compound Memory Models. 7, ACM Press, 153:1–153:24. https://doi.org/10.1145/3591267
[11]
Intel. 2024. Intel 64 and IA-32 Architectures Software Developer’s 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
[12]
ISO. 2011. ISO International Standard ISO/IEC 14882:2011(E) – Programming Language C++. International Organization for Standardization (ISO). https://www.iso.org/standard/50372.html
[13]
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–189. https://www.cs.tau.ac.il/~orilahav/papers/popl17.pdf
[14]
Michalis Kokologiannakis, Ori Lahav, and Viktor Vafeiadis. 2023. Kater: Automating Weak Memory Model Metatheory and Consistency Checking. In Principles of Programming Languages (POPL). 7, https://doi.org/10.1145/3571212
[15]
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–632. https://plv.mpi-sws.org/scfix/paper.pdf
[16]
Xavier Leroy. 2021. The CompCert C verified compiler. http://compcert.org/man
[17]
Linux Kernel Community. 2007. Linux Kernel-Based Virtual Machine. https://git.kernel.org/pub/scm/virt/kvm/kvm.git
[18]
Linux Kernel Mailing List. 1999. spin_unlock optimization(i386). https://lists.archive.carbon60.com/linux/kernel/105412
[19]
Roy Margalit and Ori Lahav. 2021. Verifying Observational Robustness Against a C11-Style Memory Model. Proceedings of the ACM on Programming Languages, 5, POPL (2021), Jan., https://doi.org/10.1145/3434285
[20]
Microsoft Learn. 2021. Advantages of Inline Assembly. https://learn.microsoft.com/en-us/cpp/assembler/inline/advantages-of-inline-assembly
[21]
Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. 2002. Isabelle/HOL — A Proof Assistant for Higher-Order Logic (Lecture Notes in Computer Science, Vol. 2283). Springer. https://doi.org/10.1007/3-540-45949-9
[22]
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). 3, ACM Press, 69:1–69:31. https://doi.org/10.1145/3290382
[23]
Jeff Preshing. 2012. Memory Ordering at Compile Time. https://preshing.com/20120625/memory-ordering-at-compile-time
[24]
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. 2, ACM Press, 19:1–19:29. https://doi.org/10.1145/3158107
[25]
Azalea Raad, Luc Maranget, and Viktor Vafeiadis. 2022. Extending Intel-X86 Consistency and Persistency: Formalising the Semantics of Intel-X86 Memory Types and Non-Temporal Stores. Proceedings of the ACM on Programming Languages, 6, POPL (2022), Jan., 22:1–22:31. https://doi.org/10.1145/3498683
[26]
Michael Sammler, Simon Spies, Youngju Song, Emanuele D’Osualdo, Robbert Krebbers, Deepak Garg, and Derek Dreyer. 2023. DimSum: A Decentralized Approach to Multi-Language Semantics and Verification. 7, 27:1–27:31. https://doi.org/10.1145/3571220
[27]
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––322. https://doi.org/10.1145/2254064.2254102
[28]
Peter Sewell, Susmit Sarkar, Scott Owens, Francesco Zappa Nardelli, and Magnus O. Myreen. 2010. X86-TSO: A Rigorous and Usable Programmer’s Model for X86 Multiprocessors. Commun. ACM, 53, 7 (2010), July, 89––97. https://doi.org/10.1145/1785414.1785443
[29]
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–173. https://doi.org/10.1007/978-3-030-99336-8_6
[30]
Pradeep S. Sindhu, Jean-Marc Frailong, and Michel Cekleov. 1992. Formal Specification of Memory Models. Springer, 25–41. https://doi.org/10.1007/978-1-4615-3604-8_2
[31]
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–220. https://dl.acm.org/doi/10.1145/2676726.2676995
Index Terms
- Extending the C/C++ Memory Model with Inline Assembly
Recommendations
A study of inline assembly in solidity smart contracts
The Solidity programming language is the most widely used language for smart contract development. Improving smart contracts’ correctness, security, and performance has been the driving force for research in vulnerability detection, program analysis, and ...
An Analysis of x86-64 Inline Assembly in C Programs
VEE '18C codebases frequently embed nonportable and unstandardized elements such as inline assembly code. Such elements are not well understood, which poses a problem to tool developers who aspire to support C code. This paper investigates the use of x86-64 ...
An Analysis of x86-64 Inline Assembly in C Programs
VEE '18: Proceedings of the 14th ACM SIGPLAN/SIGOPS International Conference on Virtual Execution EnvironmentsC codebases frequently embed nonportable and unstandardized elements such as inline assembly code. Such elements are not well understood, which poses a problem to tool developers who aspire to support C code. This paper investigates the use of x86-64 ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
October 2024
2691 pages
Copyright © 2024 Owner/Author.
This work is licensed under a Creative Commons Attribution International 4.0 License.
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 08 October 2024
Published in PACMPL Volume 8, Issue OOPSLA2
Check for updates
Author Tags
Qualifiers
- Research-article
Funding Sources
- UKRI Future Leaders Fellowship
- Engineering & Physical Sciences Research Council
- VeTSS
- European Research Council
- Israel Science Foundation
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 156Total Downloads
- Downloads (Last 12 months)156
- Downloads (Last 6 weeks)57
Reflects downloads up to 21 Dec 2024
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in