一句话：为 C11 风格内存模型（RC20、RA、SRA/WRA、Relaxed）的 reads-from 一致性检查给出最优算法与复杂度下界。
本文研究 C/C++ 内存模型的一致性检查：给定执行 X（含事件、程序序和 reads-from 关系），判定是否存在写事件的修改序使 X 满足内存模型。作者针对 C11 的 RC20、RA、SRA/WRA 及 RC20 Relaxed 片段，聚焦 reads-from 一致性检查。论文给出丰富的复杂度图景：部分变体有近线性时间算法，优于先前结果；并给出细粒度最优性结果；对其他变体证明 NP 难下界并与上界匹配。算法实现在 TruSt 模型检查器和 C11Tester 测试工具中，标准基准实验显示一致性检查常获显著加速。这是首个刻画 C11 内存模型一致性检查复杂度的工作。
Over the years, several memory models have been proposed to capture the subtle concurrency semantics of C/C++. One of the most fundamental problems associated with a memory model M is consistency checking: given an execution X , is X consistent with M ? This problem lies at the heart of numerous applications, including specification testing and litmus tests, stateless model checking, and dynamic analyses. As such, it has been explored extensively and its complexity is well-understood for traditional models like SC and TSO. However, less is known for the numerous model variants of C/C++, for which the problem becomes challenging due to the intricacies of their concurrency primitives. In this work we study the problem of consistency checking for popular variants of the C11 memory model, in particular, the RC 20 model, its release-acquire ( RA ) fragment, the strong and weak variants of RA ( SRA and WRA ), as well as the Relaxed fragment of RC 20. Motivated by applications in testing and model checking, we focus on reads-from consistency checking. The input is an execution X specifying a set of events, their program order and their reads-from relation, and the task is to decide the existence of a modification order on the writes of X that makes X consistent in a memory model. We draw a rich complexity landscape for this problem; our results include (i) nearly-linear-time algorithms for certain variants, which improve over prior results, (ii) fine-grained optimality results, as well as (iii) matching upper and lower bounds (NP-hardness) for other variants. To our knowledge, this is the first work to characterize the complexity of consistency checking for C11 memory models. We have implemented our algorithms inside the TruSt model checker and the C11Tester testing tool. Experiments on standard benchmarks show that our new algorithms improve consistency checking, often by a significant margin.
@article{paperbot1983,
title = {Optimal Reads-From Consistency Checking for C11-Style Memory Models},
author = {Hünkar Can Tunç and Parosh Aziz Abdulla and Soham Chakraborty and Shankaranarayanan Krishna and Umang Mathur and Andreas Pavlogiannis},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {PLDI},
year = {2023},
doi = {10.1145/3591251}
}