kirancodes.me
To Proof Maintenance & Beyond!
ASE 2015

Fast and Precise Symbolic Analysis of Concurrency Bugs in Device Drivers (T)

Pantazis Deligiannis, Alastair F. Donaldson, Zvonimir Rakamaric

DOI 10.1109/ase.2015.30dblp

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

BibTeX
@inproceedings{Deligiannis-al:ASE15,
  author    = {Pantazis Deligiannis and
               Alastair F. Donaldson and
               Zvonimir Rakamaric},
  title     = {Fast and Precise Symbolic Analysis of Concurrency Bugs in Device Drivers {(T)}},
  booktitle = {ASE},
  pages     = {166--177},
  publisher = {{IEEE} Computer Society},
  year      = {2015},
}

Related papers