IMDEA Software

Iniciativa IMDEA

Inicio > Eventos > Charlas Invitadas > 2008 > Sound, precise and efficient static race detection for multi-threaded programs
Esta página aún no ha sido traducida. A continuación se muestra la página en inglés.

Polyvios Pratikakis

lunes 13 de octubre de 2008

2:00pm Amphitheatre H-1002

Polyvios Pratikakis, Post-doctoral Researcher, Verimag

Sound, precise and efficient static race detection for multi-threaded programs


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.