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.

翻译：C/C++程序常包含内联汇编：即一段特定架构的汇编代码片段，用于访问在源语言中无法实现或模拟成本过高的底层功能。尽管内联汇编被广泛使用，但其语义尚未得到形式化研究。本文通过探究内联汇编对C/C++程序一致性语义的影响来弥补这一不足。我们首次提出了支持Intel x86架构内联汇编（包括非临时存储和存储屏障）的C++编程语言内存模型。我们认为先前可证明正确的编译器优化及正确的编译器映射在此扩展模型下应保持正确性，并证明我们提出的模型满足这一要求。