一句话：提出按序弱内存并发模型，通过 source/IR 分离支持非原子访问与单线程优化，并在 Coq 中验证到 Armv8 的映射。
论文为 C/C++ 等语言设计“按序”共享内存并发模型，使指令按程序顺序执行，以便推理与验证。作者证明按序模型仍能支持非原子访问，并验证单线程代码中的编译器优化（含无关 load 引入）。核心方法是区分源模型（catch-fire 语义）与中间表示模型（竞态读取未定义值），并形式证明源到 IR 映射的可靠性。对于 relaxed atomic 访问，按序模型必须禁止 load-store 重排序，但性能影响有限。源与 IR 语义基于 promising semantics，源到 IR 及 IR 到 Armv8 的正确性证明在 Coq 中机器化。
We investigate the problem of developing an "in-order" shared-memory concurrency model for languages like C and C++, which executes instructions following their program order, and is thus more amenable to reasoning and verification compared to recent complex proposals with out-of-order execution. We demonstrate that it is possible to fully support non-atomic accesses in an in-order model in a way that validates all compiler optimizations that are performed in single-threaded code (including irrelevant load introduction). The key to doing so is to utilize the distinction between a source model (with catch-fire semantics) and an intermediate representation (IR) model (with undefined value for racy reads) and formally establish the soundness of mapping from source to IR. As for relaxed atomic accesses, an in-order model must forbid load-store reordering. We discuss the rather limited performance impact of this fact and present a pragmatic approach to this problem, which, in the long term, requires a new kind of hardware store instructions for implementing relaxed stores. The source and IR semantics proposed in this paper are based on recent versions of the promising semantics, and the correctness proofs of the mappings from the source to the IR and from the IR to Armv8 are mechanized in Coq. This work is the first to formally relate an in-order source model and an out-of-order IR model with the goal of having an in-order source semantics without any performance overhead for non-atomics.
@article{paperbot1953,
title = {Putting Weak Memory in Order via a Promising Intermediate Representation},
author = {Sung-Hwan Lee and Minki Cho and Roy Margalit and Chung-Kil Hur and Ori Lahav},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {PLDI},
year = {2023},
doi = {10.1145/3591297}
}