LOCKSMITH

摘要: One common technique for preventing data races in multi-threaded programs is to ensure that all accesses shared locations are consistently protected by a lock. We present tool called LOCKSMITH detecting C looking violations of this pattern. call the relationship between locks and they protect consistent correlation, core our novel constraint-based analysis infers correlation context-sensitively, using results check properly guarded locks. algorithm simple formal language λ> which we have proven sound, discuss how scale it up an aims be sound C. develop several techniques improve precision performance analysis, including sharing inferring thread locality; existential quantification modeling structures; heuristics unsafe features such as type casts. When applied benchmarks, servers Linux device drivers, found while producing modest number false alarm.