一句话：提出 sync-preserving 死锁概念，并给出线性时间、可靠且高精度的动态死锁预测算法。
动态预测分析通过观察并发执行并重排交错来发现死锁，但现有方法难以同时满足可靠、高精度与高效。本文首先证明该权衡不可避免：可靠且完备的死锁预测一般计算难解，甚至判断潜在死锁是否存在也难解。为突破此限制，作者提出保同步（sync-preserving）死锁类：保持冲突临界区相对顺序的重排所能预测的死锁。基于此给出两个可靠算法：SPDOffline 对每个抽象死锁模式线性时间检测所有保同步死锁；SPDOnline 以严格在线方式线性时间预测涉及两线程的保同步死锁。标准基准评估表明，该概念能刻画绝大多数死锁，并可在线、可靠、完备且高效地检测。
Deadlocks are one of the most notorious concurrency bugs, and significant research has focused on detecting them efficiently. Dynamic predictive analyses work by observing concurrent executions, and reason about alternative interleavings that can witness concurrency bugs. Such techniques offer scalability and sound bug reports, and have emerged as an effective approach for concurrency bug detection, such as data races. Effective dynamic deadlock prediction, however, has proven a challenging task, as no deadlock predictor currently meets the requirements of soundness, high-precision, and efficiency. In this paper, we first formally establish that this tradeoff is unavoidable, by showing that (a) sound and complete deadlock prediction is intractable, in general, and (b) even the seemingly simpler task of determining the presence of potential deadlocks, which often serve as unsound witnesses for actual predictable deadlocks, is intractable. The main contribution of this work is a new class of predictable deadlocks, called sync(hronization)-preserving deadlocks. Informally, these are deadlocks that can be predicted by reordering the observed execution while preserving the relative order of conflicting critical sections. We present two algorithms for sound deadlock prediction based on this notion. Our first algorithm SPDOffline detects all sync-preserving deadlocks, with running time that is linear per abstract deadlock pattern, a novel notion also introduced in this work. Our second algorithm SPDOnline predicts all sync-preserving deadlocks that involve two threads in a strictly online fashion, runs in overall linear time, and is better suited for a runtime monitoring setting. We implemented both our algorithms and evaluated their ability to perform offline and online deadlock-prediction on a large dataset of standard benchmarks. Our results indicate that our new notion of sync-preserving deadlocks is highly effective, as (i) it can characterize the vast majority of deadlocks and (ii) it can be detected using an online, sound, complete and highly efficient algorithm.
@article{paperbot1948,
title = {Sound Dynamic Deadlock Prediction in Linear Time},
author = {Hünkar Can Tunç and Umang Mathur and Andreas Pavlogiannis and Mahesh Viswanathan},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {PLDI},
year = {2023},
doi = {10.1145/3591291}
}