Sound and efficient concurrency bug prediction
Sound and efficient concurrency bug prediction
复制标题
DOI：
10.1145/3468264.3468549
复制
发表时间：
2021-08
期刊：
影响因子：
--
通讯作者：
Yan Cai;Hao Yun;Jinqiu Wang;L. Qiao;J. Palsberg
中科院分区：
文献类型：
--
作者：
Yan Cai;Hao Yun;Jinqiu Wang;L. Qiao;J. Palsberg
并发错误很难检测到。最近，几种动态技术实现了声音分析。 M2甚至是两个线程的完整。它旨在决定是否可以连续发生两个事件。但是，实际并发错误可能涉及更多事件和线程。当两个或多个事件的顺序不连续发生时，可能会发生一些。我们提出了一种新技术Seqcheck，以精心确定是否可以按指定顺序发生一系列事件。有序序列代表一个潜在的并发错误。并且可以轻松地将已知形式的并发错误形式编码到事件序列中，在这些事件序列中，每个序列都代表可能发生错误的方式。为了实现这一目标，Seqcheck明确分析了分支事件，并包括一组有效的算法。我们证明了Seqcheck是合理的。并且它在两个线程的轨迹上也完成。我们已经实施了Seqcheck来检测三种类型的并发错误，并在51个Java基准测试中对其进行了评估，并产生了多达数十亿个事件。与M2和其他三个最近的Sound Race探测器相比，Seqcheck在约30分钟内检测到333场比赛；而其他人则在〜6至〜12小时内从130到285场比赛中发现。 Seqcheck在约6秒内检测到20个僵局。这只比Dirk少。但是德克花了一个多小时。 Seqcheck在约20分钟内还检测到30种原子性违规。评估表明，Seqcheck可以显着胜过现有的并发错误检测器。
Concurrency bugs are extremely difficult to detect. Recently, several dynamic techniques achieve sound analysis. M2 is even complete for two threads. It is designed to decide whether two events can occur consecutively. However, real-world concurrency bugs can involve more events and threads. Some can occur when the order of two or more events can be exchanged even if they occur not consecutively. We propose a new technique SeqCheck to soundly decide whether a sequence of events can occur in a specified order. The ordered sequence represents a potential concurrency bug. And several known forms of concurrency bugs can be easily encoded into event sequences where each represents a way that the bug can occur. To achieve it, SeqCheck explicitly analyzes branch events and includes a set of efficient algorithms. We show that SeqCheck is sound; and it is also complete on traces of two threads. We have implemented SeqCheck to detect three types of concurrency bugs and evaluated it on 51 Java benchmarks producing up to billions of events. Compared with M2 and other three recent sound race detectors, SeqCheck detected 333 races in ~30 minutes; while others detected from 130 to 285 races in ~6 to ~12 hours. SeqCheck detected 20 deadlocks in ~6 seconds. This is only one less than Dirk; but Dirk spent more than one hour. SeqCheck also detected 30 atomicity violations in ~20 minutes. The evaluation shows SeqCheck can significantly outperform existing concurrency bug detectors.