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 RC20 model, its release-acquire (RA) fragment, the strong and weak variants of RA (SRA and WRA), as well as the Relaxed fragment of RC20. 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.

翻译：近年来，多种内存模型被提出以捕捉C/C++中微妙的并发语义。与内存模型M相关的最基本问题之一是一致性检查：给定一个执行X，X是否与M一致？该问题位于众多应用的核心，包括规范测试与石蕊测试、无状态模型检查以及动态分析。因此，这一问题已被广泛研究，其在SC和TSO等传统模型下的复杂度已得到充分理解。然而，对于C/C++的众多模型变体，由于并发原语的复杂性，该问题变得更具挑战性，相关认知仍较为有限。本文研究了C11内存模型主流变体的一致性检查问题，特别关注RC20模型、其释放-获取（RA）片段、RA的强变体与弱变体（SRA与WRA），以及RC20的松弛片段。受测试与模型检查应用的启发，我们重点研究读自一致性检查。输入是指定事件集合、程序顺序及读自关系的执行X，任务是在给定内存模型下，判定是否存在一种写操作上的修改顺序使得X保持一致。我们为这一问题绘制了丰富的复杂度景观：结果包括（i）针对某些变体的近线性时间算法——优于先前结果，（ii）细粒度最优性结果，以及（iii）针对其他变体的匹配上下界（NP困难性）。据我们所知，这是首次对C11内存模型一致性检查的复杂度进行刻画。我们已在TruSt模型检查器和C11Tester测试工具中实现了所提算法。标准基准测试实验表明，我们的新算法显著提升了一致性检查的性能。