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.