Fast and Precise Symbolic Analysis of Concurrency Bugs in Device Drivers

2015_ASE_ddr screenshot

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.

Citation

Pantazis Deligiannis, Alastair F. Donaldson, Zvonimir Rakamaric
Fast and Precise Symbolic Analysis of Concurrency Bugs in Device Drivers
Proceedings of the 30th IEEE/ACM International Conference on Automated Software Engineering (ASE), 166--177, 2015.

BibTeX

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