一句话：提出首个无 thin-air 的 C/C++ 内存模型，支持别名分析驱动的编译器优化、未定义行为假设和外在选择，并提供高性能可执行工具。
本文针对 C/C++ 弱内存模型中 thin-air 读与编译器优化难以共存的问题，提出首个无 thin-air 的内存模型 Symbolic MRD。该模型统一处理动态内存、未定义行为以及实现层面的外在选择（如过度对齐），通过可导出的语义依赖关系与 C/C++ 内存模型集成，并支持原子操作的标准编译映射。作者给出了可执行语义与工具支持，其性能达到先进水平，运行一批测试的速度比其他可执行无 thin-air 语义快数个数量级。该模型还通过了 ISO C/C++ 内存模型最新需求清单中的全部测试，表明其与现有规范兼容。
We present the first thin-air free memory model that admits compiler optimisations that aggressively leverage knowledge from alias analysis, an assumption of freedom from undefined behaviour, and from the extrinsic choices of real implementations such as over-alignment. Our model has tooling support with state-of-the-art performance, executing a battery of tests orders of magnitude quicker than other executable thin-air free semantics. The model integrates with the C/C++ memory model through an exportable semantic dependency relation, it allows standard compilation mappings for atomics, and it matches all tests in the recently published desiderata for C/C++ from the ISO.
@article{paperbot3188,
title = {Symbolic MRD: Dynamic Memory, Undefined Behaviour, and Extrinsic Choice},
author = {Jay Richards and Daniel Wright and Simon Cooksey and Mark Batty},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA1},
year = {2025},
doi = {10.1145/3721089}
}