@article{10.1145/3689749,
author = {de Vilhena, Paulo Em\'{\i}lio and Lahav, Ori and Vafeiadis, Viktor and Raad, Azalea},
title = {Extending the C/C++ Memory Model with Inline Assembly},
year = {2024},
issue_date = {October 2024},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {8},
number = {OOPSLA2},
url = {https://doi.org/10.1145/3689749},
doi = {10.1145/3689749},
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.},
journal = {Proc. ACM Program. Lang.},
month = oct,
articleno = {309},
numpages = {27},
keywords = {Concurrency, Semantics of Programming Languages, Weak Memory Models}
}