Abstract:

Data race is a common problem in multithreaded programs. Due to the state explosion of thread interleaving, it is difficult to accurately detect bugs triggered by data races. Moreover, it is hard to replay and triage such bugs because of the facts that thread scheduling is difficult to control and the number of interleaving is astronomically large. A data race detection and witness generation method for multithreaded programs is proposed. A semantic model is designed to encode the execution path and the condition of data races as firstorder logic formula. The satisfiability of the formula, solvable by constraint solvers, indicates the existence of data races under multiple thread interleavings without requiring repeated executions. The solutions produced by an SMT solver serve as witnesses to localize and verify data races. In the experiments, we compare existing tools threadsanitizer and helgrind with ours to detect the data races for 10 multithreaded programs. It is shown that our method can detect 287.5% and 264.7% more bugs respectively without false alarm, while the false alarm positive rate of threadsanitizer and helgrind are 10.5% and 9.8%.

Key words: multithreaded program testing;data race;constraint solving;witness generation