一句话：首次为含内联汇编（Intel x86，含非临时存储与存储栅栏）的 C/C++ 提出内存模型，并证明既有编译器优化与映射仍正确。
C/C++ 程序常使用内联汇编访问底层功能，但其对一致性的影响尚无形式化研究。本文考察内联汇编如何影响 C/C++ 程序的一致性语义，提出首个支持 Intel x86 内联汇编的 C++ 内存模型，涵盖非临时存储（non-temporal stores）和存储栅栏（store fences）。作者认为，此前已被证明正确的编译器优化与编译器映射在扩展模型下仍应保持正确，并将该要求作为设计约束；论文证明所提模型满足这一要求。结果给出内联汇编的正式语义基础，并为验证编译器在含内联汇编时的正确性提供依据。
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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{Vilhena0VR24,
title = {Extending the C/C++ Memory Model with Inline Assembly},
author = {Paulo Emílio de Vilhena and Ori Lahav and Viktor Vafeiadis and Azalea Raad},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {OOPSLA2},
year = {2024},
doi = {10.1145/3689749}
}