Fast and Precise Symbolic Analysis of Concurrency Bugs in Device Drivers

Abstract

Concurrency errors, such as data races, make device drivers notoriously hard to develop and debug without automated tool support. We present WHOOP, a new fully automatic approach that statically analyzes drivers for data races. WHOOP is empowered by symbolic pairwise lockset analysis, a novel analysis that can soundly detect all potential races in a driver. Our analysis avoids reasoning about thread interleavings and thus can scale well. Exploiting the race-freedom guarantees provided by WHOOP, we achieve a sound partial-order reduction that can significantly accelerate CORRAL, an industrial-strength bug-finder for concurrent programs. Using the combination of WHOOP and CORRAL, we analyzed 16 drivers from the Linux 4.0 kernel, showing that we can achieve 1.5–20× speedups over standalone CORRAL.