Sound Dynamic Deadlock Prediction in Linear Time
Sound Dynamic Deadlock Prediction in Linear Time
复制标题
DOI：
10.1145/3591291
复制
发表时间：
2023-04
影响因子：
--
通讯作者：
Umang Mathur;Andreas Pavlogiannis;Hunkar Can Tuncc;Mahesh Viswanathan
中科院分区：
文献类型：
--
作者：
Umang Mathur;Andreas Pavlogiannis;Hunkar Can Tuncc;Mahesh Viswanathan
僵局是最臭名昭著的并发错误之一，重大研究重点是有效地检测它们。动态预测分析通过观察并发执行，以及有关可以见证并发错误的替代交织的原因。这样的技术提供了可扩展性和声音错误报告，并已成为一种有效的并发错误检测方法，例如数据竞赛。然而，有效的动态僵局预测已证明是一项具有挑战性的任务，因为没有僵局预测因子目前符合健全，高精度和效率的要求。在本文中，我们首先正式确定这种权衡是不可避免的，它表明（a）声音和完整的僵局预测通常是棘手的，而且（b）即使是确定潜在僵局的存在似乎更简单的任务，这通常是作为实际可预测的僵局的不合适的证人，是棘手的。这项工作的主要贡献是一类新的可预测的僵局，称为同步（Hronization） - 保证僵局。在非正式的情况下，这些是可以通过在保留相互冲突的关键部分的相对顺序的同时重新排序所观察到的执行来预测的僵局。我们根据此概念提出了两种用于声音死锁预测的算法。我们的第一种算法SPDOFFLINE检测到所有同步保护的僵局，并且跑步时间是每个抽象僵局模式线性的，这是在这项工作中引入的一种新颖概念。我们的第二种算法SPDONLINE预测了所有同步保留的僵局，这些僵局涉及以严格的在线方式进行两个线程，在整个线性时间内运行，并且更适合运行时监视设置。我们实施了同时的算法，并评估了他们在大型标准基准数据集上执行离线和在线僵局的能力。我们的结果表明，我们对同步保存僵局的新概念非常有效，因为（i）它可以表征绝大多数僵局，并且（ii）可以使用在线，声音，完整且高效的算法检测到它。
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.