Extending the C/C++ Memory Model with Inline Assembly
Paulo Emílio de Vilhena, Ori Lahav, Viktor Vafeiadis, Azalea Raad
TL;DR
This work extends the RC11 memory model for C/C++ with formal support for inline x86 assembly, incorporating non-temporal stores and memory fences via a new extension $RC11^{Ex86}$. The authors define a rigorous hybrid memory model that preserves RC11 semantics for pure RC11 code and Ex86 semantics for pure inline-assembly code, while enabling safe mixing across threads and memory locations. They develop a precise operational framework, including mixed execution graphs, to prove compilation correctness and the soundness of optimizations in the presence of inline assembly, and they address architecture-specific behaviors such as multi-copy atomicity and IRIW-like patterns. The result is a principled, theory-backed model that supports realistic inline-assembly usage while ensuring compiler mappings and optimizations remain correct, providing practical guidance for developers and compiler writers working with hybrid C/C++ and x86 code.
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.