一句话：提出强化多执行内存模型 Weakestmo2，并实现性能接近逐执行模型工具的模型检测器 WMC。
多执行内存模型（如 Promising 和 Weakestmo）通过同时考虑多个候选执行来解释并发程序的某些结果，因而支持编译到硬件模型和多种编译器优化，但也使推理和模型检测更困难。作者发现这类模型会允许无法逐执行生成的弱行为，从而阻碍有效模型检测。为此，论文提出 Weakestmo2：约束 Weakestmo 的多执行特性，同时保留 DRF 定理、编译到硬件模型的正确性以及局部程序变换正确性。该强化排除了异常弱行为，并用 load buffering race freedom 与 certification locality 两个新性质刻画。作者还实现了模型检测器 WMC，其性能接近最好的逐执行模型工具。
Multi-execution memory models, such as Promising and Weakestmo, are an advanced class of weak memory consistency models that justify certain outcomes of a concurrent program by considering multiple candidate executions collectively. While this key characteristic allows them to support effective compilation to hardware models and a wide range of compiler optimizations, it makes reasoning about them substantially more difficult. In particular, we observe that Promising and Weakestmo inhibit effective model checking because they allow some suprisingly weak behaviors that cannot be generated by examining one execution at a time. We therefore introduce Weakestmo2, a strengthening of Weakestmo by constraining its multi-execution nature, while preserving the important properties of Weakestmo: DRF theorems, compilation to hardware models, and correctness of local program transformations. Our strengthening rules out a class of surprisingly weak program behaviors, which we attempt to characterize with the help of two novel properties: load buffering race freedom and certification locality. In addition, we develop WMC, a model checker for Weakestmo2 with performance close to that of the best tools for per-execution models.
@article{paperbot1470,
title = {Model checking for a multi-execution memory model},
author = {Evgenii Moiseenko and Michalis Kokologiannakis and Viktor Vafeiadis},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {OOPSLA2},
year = {2022},
doi = {10.1145/3563315}
}