一句话：提出再执行式内存模型 XMM，以近似每执行的语义统一解释宽松并发，并实例化为 XC20。
为编程语言定义能同时满足程序员、编译器与体系结构冲突需求的并发模型是长期难题。传统按单次执行推理的公理化模型被认为不足；多执行模型虽有突破，却结构复杂、难适配按单执行书写的语言规范，也不利于自动化推理。本文提出再执行式内存模型 XMM：它仍推理单次执行，但通过再执行原则关联多次执行，使内存一致性公理与乱序再执行机制正交，因而可作为由给定公理化内存模型参数化的语义框架。作者将 XMM 实例化为 RC20 的模型 XC20，证明其提供 DRF 保证、支持标准硬件映射与编译器优化（首个支持线程顺序化优化的同类模型），并实现可靠的模型检测器 XMC 在并发基准上评估。
Defining a formal model for concurrency in programming languages that addresses conflicting requirements from programmers, compilers, and architectures has been a long-standing research question. It is widely believed that traditional axiomatic per-execution models that reason about individual executions do not suffice to address these conflicting requirements. Consequently, several multi-execution models were proposed that reason about multiple executions together. Although multi-execution models were major breakthroughs in satisfying several desired properties, these models are complicated, challenging to adapt to existing language specifications given in per-execution style, and they are typically not friendly to automated reasoning tools. In response, we propose a re-execution-based memory model (XMM). Debunking the beliefs around per-execution and multi-execution models, XMM is (almost) a per-execution model. XMM reasons about individual executions, but unlike traditional per-execution models, it relates executions by a re-execution principle. As such, the memory consistency axioms and the out-of-order re-execution mechanics are orthogonal in XMM, allowing to use it as a semantic framework parameterized by a given axiomatic memory model. We instantiated the XMM framework for the RC20 language model, and proved that the resulting model XC20 provides DRF guarantees and allows standard hardware mappings and compiler optimizations. Note-worthy, XC20 is the first model of its kind that also supports thread sequentialization optimization. Moreover, XC20 is also amenable to automated reasoning. To demonstrate this, we developed a sound model checker XMC and evaluated it on several concurrency benchmarks.
@article{paperbot3233,
title = {Relaxed Memory Concurrency Re-executed},
author = {Evgenii Moiseenko and Matteo Meluzzi and Innokentii Meleshchenko and Ivan Kabashnyi and Anton Podkopaev and Soham Chakraborty},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {POPL},
year = {2025},
doi = {10.1145/3704908}
}