paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Optimal prediction of synchronization-preserving races

同步保持型竞态的最优预测
POPL 5(POPL)2021匹配度 3/10 · 论文研究并发程序中的同步保持型竞态预测,属于程序分析与形式化方法,但与用户重点关注的 LLM/Agent 与静态分析交叉、浮点程序分析、贝叶斯程序分析均无直接关系,也不涉及 AI/LLM。引用 35 inbox
Umang Mathur, Andreas Pavlogiannis, Mahesh Viswanathan
crossref: 2026-09-10

AI 速览

一句话:提出同步保持型竞态,并给出可靠完备、时空近最优的预测算法,证明其恰为竞态预测可处理边界。

并发程序中的数据竞争难以检测,动态竞态预测旨在判断一条无竞态观察轨迹 σ 能否重排为隐藏竞态的见证轨迹。本文提出同步保持竞态:要求见证轨迹中锁获取/释放等同步操作的相对顺序与 σ 一致,严格包含经典 happens-before 竞态。作者给出可靠且完备的预测算法:在线程数等参数适中时以 Õ(N) 时间和空间运行(N 为轨迹长度),并证明 Ω(N/log^2 N) 空间下界,表明算法基本最优。进一步,仅反转一对同步操作的竞态预测已是 NP-complete,按线程数参数化时为 W[1]-hard,说明同步保持恰是可处理边界;实验显示算法快速且能发现现有方法漏掉的竞态。

问题
如何从观察到的无竞态轨迹中预测隐藏的数据竞争,并刻画该问题的可处理与不可处理边界。
方法
定义同步保持竞态,设计可靠且完备的预测算法,并分析其时间空间复杂度、空间下界以及单次同步反转变体的计算复杂性。
评估
理论上给出复杂度上界、Ω(N/log^2 N) 空间下界以及 NP-complete/W[1]-hard 结果;实验上验证算法的实际速度与发现现有方法常漏竞态的能力。
原文摘要(Abstract)

Concurrent programs are notoriously hard to write correctly, as scheduling nondeterminism introduces subtle errors that are both hard to detect and to reproduce. The most common concurrency errors are (data) races, which occur when memory-conflicting actions are executed concurrently. Consequently, considerable effort has been made towards developing efficient techniques for race detection. The most common approach is dynamic race prediction: given an observed, race-free trace σ of a concurrent program, the task is to decide whether events of σ can be correctly reordered to a trace σ * that witnesses a race hidden in σ. In this work we introduce the notion of sync(hronization)-preserving races. A sync-preserving race occurs in σ when there is a witness σ * in which synchronization operations (e.g., acquisition and release of locks) appear in the same order as in σ. This is a broad definition that strictly subsumes the famous notion of happens-before races. Our main results are as follows. First, we develop a sound and complete algorithm for predicting sync-preserving races. For moderate values of parameters like the number of threads, the algorithm runs in Õ( N ) time and space, where N is the length of the trace σ. Second, we show that the problem has a Ω( N /log 2 N ) space lower bound, and thus our algorithm is essentially time and space optimal. Third, we show that predicting races with even just a single reversal of two sync operations is NP-complete and even W1-hard when parameterized by the number of threads. Thus, sync-preservation characterizes exactly the tractability boundary of race prediction, and our algorithm is nearly optimal for the tractable side. Our experiments show that our algorithm is fast in practice, while sync-preservation characterizes races often missed by state-of-the-art methods.

链接与引用

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

BibTeX
@article{paperbot1159,
  title = {Optimal prediction of synchronization-preserving races},
  author = {Umang Mathur and Andreas Pavlogiannis and Mahesh Viswanathan},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {5},
  number = {POPL},
  year = {2021},
  doi = {10.1145/3434317}
}