Lecture

Context-sensitive Correlation Analysis for Detecting Races

Speaker:	Polyvios Pratikakis
Date:	Monday, 17 March 2008
Time:	14:30-16:00
Location:	"Mediterranean Studies" Seminar Room, FORTH. Heraklion, Crete
Host:	Prof. C. Stephanidis

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 lambda-corr 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.

Bio:

Polyvios Pratikakis is a Ph.D. candidate at the Department of Computer Science at the Unieversity of Maryland. 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. 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.