一句话:证明多种弱内存模型下一致性测试在参数有界时仍 NP 完全,并与 SC、x86-TSO、PSO、Relaxed 形成计算分离。
弱内存模型是并发系统的标准形式规范,一致性测试判断程序的可观测执行是否符合底层规范。已有研究在 SC 与弱内存下证明:当输入某方面(如线程数或内存位置数)无界时问题为 NP 完全,但是否存在高效参数化算法一直未决。本文给出深层硬度结果:即使候选执行中线程数、内存位置数和取值均有界,一致性测试仍 NP 完全。该硬度覆盖 C11 的多个 Release-Acquire 变体、其 Relaxed 片段的流行变体、常见 Causal Consistency 模型及 POWER 架构。这是首个充分揭示弱内存测试硬度、并证明其在标准输入参数下无可参数化算法的结果;同时给出这些模型与 SC、x86-TSO、PSO、Relaxed 的计算分离,后者的有界一致性测试可在多项式时间内判定。
Weak-memory models are standard formal specifications of concurrency across hardware, programming languages, and distributed systems. A fundamental computational problem is consistency testing : is the observed execution of a concurrent program in alignment with the specification of the underlying system? The problem has been studied extensively across Sequential Consistency (SC) and weak memory, and proven to be N P -complete when some aspect of the input (e.g., number of threads/memory locations) is unbounded. This unboundedness has left a natural question open: are there efficient parameterized algorithms for testing? The main contribution of this paper is a deep hardness result for consistency testing under many popular weak-memory models: the problem remains N P -complete even in its bounded setting, where candidate executions contain a bounded number of threads, memory locations, and values. This hardness spreads across several Release-Acquire variants of C11, a popular variant of its Relaxed fragment, popular Causal Consistency models, and the POWER architecture. To our knowledge, this is the first result that fully exposes the hardness of weak-memory testing and proves that the problem admits no parameterization under standard input parameters. It also yields a computational separation of these models from SC, x86-TSO, PSO, and Relaxed, for which bounded consistency testing is either known (for SC), or shown here (for the rest), to be in polynomial time.
@article{paperbot2603,
title = {How Hard Is Weak-Memory Testing?},
author = {Soham Chakraborty and Shankara Narayanan Krishna and Umang Mathur and Andreas Pavlogiannis},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {POPL},
year = {2024},
doi = {10.1145/3632908}
}