Fast and Precise Symbolic Analysis of Concurrency Bugs in Device Drivers
File(s)paper.pdf (526.34 KB)
Accepted version
Author(s)
Deligiannis, P
Donaldson, AF
Rakamaric, Z
Type
Conference Paper
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.
Date Issued
2015-11-13
Date Acceptance
2015-07-18
Citation
30th IEEE/ACM International Conference on Automated Software Engineering, 2015, pp.166-177
ISBN
9781509000258
Publisher
IEEE
Start Page
166
End Page
177
Journal / Book Title
30th IEEE/ACM International Conference on Automated Software Engineering
Copyright Statement
© 2015 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works.
Source
30th IEEE/ACM International Conference on Automated Software Engineering
Publication Status
Published
Start Date
2015-11-09
Finish Date
2015-11-13
Coverage Spatial
Lincoln, NE, USA