LOCKSMITH
Top Cited Papers
- 11 June 2006
- conference paper
- conference paper
- Published by Association for Computing Machinery (ACM)
- Vol. 41 (6), 320-331
- https://doi.org/10.1145/1133981.1134019
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 alarm.Keywords
This publication has 37 references indexed in Scilit:
- Dynamic inference of polymorphic lock typesScience of Computer Programming, 2005
- Optimized run-time race detection and atomicity checking using partial discovered typesPublished by Association for Computing Machinery (ACM) ,2005
- Banshee: A Scalable Constraint-Based Analysis ToolkitLecture Notes in Computer Science, 2005
- Type Inference for Parameterized Race-Free JavaLecture Notes in Computer Science, 2004
- Toward a Grainless Semantics for Shared-Variable ConcurrencyLecture Notes in Computer Science, 2004
- Type Inference Against RacesLecture Notes in Computer Science, 2004
- Ownership types for safe programmingPublished by Association for Computing Machinery (ACM) ,2002
- A region inference algorithmACM Transactions on Programming Languages and Systems, 1998
- Typed closure conversionPublished by Association for Computing Machinery (ACM) ,1996
- Type inference with polymorphic recursionACM Transactions on Programming Languages and Systems, 1993