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 NP-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 NP-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.

翻译：弱内存模型是跨硬件、编程语言和分布式系统的并发操作的标准形式化规范。一个基本的计算问题是一致性测试：并发程序的观测执行是否与底层系统的规范一致？该问题已在顺序一致性（SC）和弱内存领域得到广泛研究，并已被证明当输入的部分参数（如线程数/内存位置数）无界时是NP完全的。这种无界性留下了自然问题：测试是否存在高效的参数化算法？本文的主要贡献在于，针对多种主流弱内存模型，揭示了一致性测试的深层困难性结果：即使在有界设置中（候选执行包含有界数量的线程、内存位置和值），该问题仍保持NP完全性。这种困难性延伸至C11的多种Release-Acquire变体、其Relaxed片段的主流变体、主流因果一致性模型以及POWER架构。据我们所知，这是首个完全揭示弱内存测试困难性并证明该问题在标准输入参数下不存在参数化的结果。同时，这些模型与SC、x86-TSO、PSO及Relaxed在计算上产生了分离——对于后者（SC已知，其余本文证明），有界一致性测试可在多项式时间内完成。