Sound and efficient concurrency bug prediction

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 SeqChec 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, SeqChec explicitly analyzes branch events and includes a set of efficient algorithms. We show that SeqChec is sound; and it is also complete on traces of two threads.

We have implemented SeqChec 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, SeqChec detected 333 races in 30 minutes; while others detected from 130 to 285 races in 6 to 12 hours. SeqChec detected 20 deadlocks in 6 seconds. This is only one less than Dirk; but Dirk spent more than one hour. SeqChec also detected 30 atomicity violations in 20 minutes. The evaluation shows SeqChec can significantly outperform existing concurrency bug detectors.