一句话：统一并推广预测性并发分析的健全性定义，提出三步证明模板，并证明六个已有分析（含首个弱内存分析）健全。
预测性并发分析以执行轨迹为输入，在不访问程序源码的情况下发现并发缺陷；其健全性要求不产生误报。此前工作对该性质有多种定义。本文统一、简化并推广针对可由连续事件序列表示的并发缺陷的健全性定义。该定义基于图结构，区分线程局部性质与整段执行性质，并适用于弱内存执行。作者给出三步证明套路，并用其证明六个已有预测性分析健全，其中包括首个针对弱内存预测性分析的健全性证明。
A predictive analysis takes an execution trace as input and discovers concurrency bugs without accessing the program source code. A sound predictive analysis reports no false positives, which sounds like a property that can be defined easily, but which has been defined in many different ways in previous work. In this paper, we unify, simplify, and generalize those soundness defInitions for analyses that discover concurrency bugs that can be represented as a consecutive sequence of events. Our soundness defInition is graph based, separates thread-local properties and whole-execution properties, and works well with weak memory executions. We also present a three-step proof recipe, and we use it to prove six existing analyses sound. This includes the first proof of soundness for a predictive analysis that works with weak memory.
@article{paperbot3203,
title = {Soundness of Predictive Concurrency Analyses},
author = {Shuyang Liu and Doug Lea and Jens Palsberg},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA1},
year = {2025},
doi = {10.1145/3720435}
}