Multi-threaded 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.
We present 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.
Polyvios Pratikakis is a CNRS postdoctoral researcher at Verimag, Grenoble. He graduated from the Department of Electrical and Computer Engineering of the National Technical University of Athens in 2002. He received a Master's degree in Computer Science from the University of Maryland in 2004, and a Ph.D. in Computer Science in 2008. His research interests span programming languages, type systems, static analysis, concurrent software and mechanized proofs. He received the University of Maryland Dean's Fellowship award for student research in 2006.