paperbot · PL 论文追踪

全部论文 待读 收藏

P2 How Hard Is Weak-Memory Testing?

弱内存测试有多难?
POPL 8(POPL)2024匹配度 3/10 · 论文研究弱内存模型下一致性测试的计算复杂度,属于并发/内存模型与形式化验证的理论工作,与用户画像中 LLM/Agent 驱动的静态分析、浮点程序分析、贝叶斯程序分析等核心方向无直接关联。虽涉及 PL 形式化,但缺乏 AI/LLM 交叉与工程落地,仅可作为并发分析的理论背景存档。引用 9 inbox
Soham Chakraborty, Shankara Narayanan Krishna, Umang Mathur, Andreas Pavlogiannis
crossref: 2026-09-10

AI 速览

一句话:证明多种弱内存模型下一致性测试在参数有界时仍 NP 完全,并与 SC、x86-TSO、PSO、Relaxed 形成计算分离。

弱内存模型是并发系统的标准形式规范,一致性测试判断程序的可观测执行是否符合底层规范。已有研究在 SC 与弱内存下证明:当输入某方面(如线程数或内存位置数)无界时问题为 NP 完全,但是否存在高效参数化算法一直未决。本文给出深层硬度结果:即使候选执行中线程数、内存位置数和取值均有界,一致性测试仍 NP 完全。该硬度覆盖 C11 的多个 Release-Acquire 变体、其 Relaxed 片段的流行变体、常见 Causal Consistency 模型及 POWER 架构。这是首个充分揭示弱内存测试硬度、并证明其在标准输入参数下无可参数化算法的结果;同时给出这些模型与 SC、x86-TSO、PSO、Relaxed 的计算分离,后者的有界一致性测试可在多项式时间内判定。

问题
弱内存模型下一致性测试的计算复杂度,尤其是当线程数、内存位置数和取值均有界时是否存在高效算法。
方法
本文对多个弱内存模型的有界一致性测试进行复杂性分析,证明其 NP 完全性,并与若干强/弱内存模型进行比较。
评估
通过覆盖 C11 Release-Acquire/Relaxed、Causal Consistency 与 POWER 的硬度结果,以及与 SC、x86-TSO、PSO、Relaxed 的多项式时间上界形成计算分离。
原文摘要(Abstract)

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.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@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}
}