Fast and Accurate Static Data Race Detection for Concurrent ProgramsVineet Kahlon , Yu Yang , Sriram Sankaranarayanan and Aarti Gupta |
|
We present new techniques for fast, accurate and scalable static race
detection in concurrent programs. Focusing our analysis on Linux device
drivers allowed us to identify the unique challenges posed by debugging
large-scale real-life code and also pinpointed drawbacks in existing
race warning generation methods. This motivated the development of new
techniques that helped us in improving both the scalability as well as
the accuracy of each of the three main steps in a race warning generation
system. The first and most crucial step in data race detection is automatic
shared variable discovery. Towards that end, we present a new, efficient
dataflow algorithm for shared variable detection which is more effective
than existing correlation-based techniques that failed to detect shared
variables responsible for data races in majority of the drivers in our
benchmark suite. Secondly, accuracy of race warning generation strongly
hinges on the accuracy of the alias analysis used to compute aliases for
lock pointers. We formulate a new scalable context sensitive alias
analysis that effectively combines a divide and conquer strategy with
function summarization and is demonstrably more efficient than existing
BDD-based techniques. Finally, we provide a new warning reduction
technique that leverages lock acquisition patterns to yield provably
better warning reduction than existing lockset based methods.
|
| ps pdf |
| Computer-aided Verification (CAV 2007), Volume 4590 of Lecture Notes in Computer Science, pp. 226-239, Springer-Verlag. |
| Copyright (C) Springer-Verlag. Copy has been made available online for personal use only. Do not redistribute without permission. |