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, doi:10.1109/ASE.2015.30, 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)},
publisher = {IEEE Computer Society},
pages = {166--177},
doi = {10.1109/ASE.2015.30},
year = {2015}
}
Acknowledgements
We thank Akash Lal for his input and for helping us with Corral issues, and Montgomery Carter for modeling Linux locks. Thanks to Jeroen Ketema, Tyler Sorensen, Anton Burtsev, and Charlie Jacobsen for discussions and feedback in various stages of this work. This work is part of the project “Automatic Synthesis of High-Assurance Device Drivers” and was generously funded by a gift from Intel Corporation; it was also supported in part by NSF CCF 1346756.