Locksmith: Context-Sensitive Correlation Analysis for Race Detection
Locksmith: Context-Sensitive Correlation Analysis for Race Detection
Loading...
Files
Publication or External Link
Date
2006-06
Authors
Pratikakis, Polyvios
Foster, Jeffrey S.
Hicks, Michael
Advisor
Citation
DRUM DOI
Abstract
One common technique for preventing data races in multi-threaded
programs is to ensure that all accesses to shared locations are
consistently protected by a lock. We present a tool called Locksmith
for detecting data races in C programs by looking for violations of
this pattern. We call the relationship between locks and the
locations they protect consistent correlation, and the core of our
technique is a novel constraint-based analysis that infers
consistent correlation context-sensitively, using the results to check
that locations are properly guarded by locks. We present the core of
our algorithm for a simple formal language which we have
proven sound, and discuss how we scale it up to an algorithm that
aims to be sound for all of C.
We develop several techniques to improve the precision and
performance of the analysis, including a sharing analysis for
inferring thread locality; existential quantification for modeling
locks in data structures; and heuristics for modeling unsafe
features of C such as type casts. When applied to several
benchmarks, including multi-threaded servers and Linux device
drivers, Locksmith found several races while producing a modest
number of false alarms.