Fast and Precise Symbolic Analysis of Concurrency Bugs in Device Drivers

Pantazis Deligiannis, Alastair F. Donaldson, Zvonimir Rakamaric. 30th IEEE/ACM International Conference on Automated Software Engineering (ASE 2015), Lincoln, NE, USA.
[pdf] [bib]

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 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–20x speedups over standalone Corral.

Bibtex:

@inproceedings{ase2015-ddr,
  author = {Pantazis Deligiannis and Alastair F. Donaldson and Zvonimir Rakamari\'c},
  title = {Fast and Precise Symbolic Analysis of Concurrency Bugs in Device Drivers},
  booktitle = {Proceedings of the 30th IEEE/ACM International Conference on Automated
    Software Engineering (ASE)},
  publisher = {IEEE},
  year = {2015},
  pages = {166--177},
}