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一致？该问题位于众多应用的核心，包括规范测试与litmus测试、无状态模型检查以及动态分析。因此，它已被广泛研究，其复杂性对于SC和TSO等传统模型已得到充分理解。然而，对于C/C++的众多模型变体，由于并发原语的复杂性，该问题的求解变得颇具挑战，且相关认知相对有限。本文针对C11内存模型的常见变体——特别是RC20模型、其释放-获取（RA）片段、RA的强变体和弱变体（SRA与WRA）以及RC20的松散片段——研究一致性检查问题。受测试与模型检查应用的驱动，我们聚焦于读取一致性检查。输入为指定事件集、程序顺序及读取关系对的执行轨迹X，任务是判断是否存在一个关于X中写操作的修改顺序，使得X在特定内存模型下保持一致。我们为该问题刻画了一个丰富的复杂度景观图；主要成果包括：(i) 针对某些变体提出近线性时间算法，显著优于先前结果；(ii) 细粒度最优性结论；(iii) 针对其他变体给出匹配的上界与下界（NP难性）。据我们所知，这是首项刻画C11内存模型一致性检查复杂性的工作。我们已在TruSt模型检查器和C11Tester测试工具中实现所提算法。在标准基准测试上的实验表明，新算法能显著提升一致性检查的效率。