SOUND, PRECISE AND EFFICIENT STATIC RACE DETECTION FOR MULTI-THREADED PROGRAMS
SOUND, PRECISE AND EFFICIENT STATIC RACE DETECTION FOR MULTI-THREADED PROGRAMS
Files
Publication or External Link
Date
2008-08-21
Authors
Pratikakis, Polyvios
Advisor
Hicks, Michael
Foster, Jeffrey
Foster, Jeffrey
Citation
DRUM DOI
Abstract
Multithreaded programming is increasingly relevant due to the growing
prevalence of multi-core processors. Unfortunately, the
non-determinism in parallel processing makes it easy to make mistakes
but difficult to detect them, so that writing concurrent programs is
considered very difficult. A data race, which happens when two
threads access the same memory location without synchronization is a
common concurrency error, with potentially disastrous consequences.
This dissertation presents Locksmith, a tool for automatically
finding data races in multi-threaded C programs by analyzing their
source code. Locksmith uses a collection of static analysis
techniques to reason about program properties, including a novel
effect system to compute memory locations that are shared between
threads, a system for inferring ``guarded-by'' correlations between
locks and memory locations, and a novel analysis of data structures
using existential types. We present the main analyses in detail and
give formal proofs to support their soundness. We discuss the
implementation of each analysis in Locksmith, present the problems
that arose when extending it to the full C programming language, and
discuss some alternative solutions. We provide extensive measurements
for the precision and performance of each analysis and compare
alternative techniques to find the best combination.