Fast And Precise Symbolic Analysis Of Concurrency Bugs In Device Drivers

Concurrency errors, such as data races, make device drivers notoriously hard to develop and debug without automated tool support. We present WHOOP, a new automated 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 scales well. Exploiting the race-freedom guarantees provided by WHOOP, we achieve a sound partial-order reduction that significantly accelerates 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, achieving 1.5-20 x speedups over standalone CORRAL.