Conditional must not aliasing for static race detection

11 years 10 months ago
Conditional must not aliasing for static race detection
Race detection algorithms for multi-threaded programs using the common lock-based synchronization idiom must correlate locks with the memory locations they guard. The heart of a proof of race freedom is showing that if two locks are distinct, then the memory locations they guard are also distinct. This is an example of a general property we call conditional must not aliasing: Under the assumption that two objects are not aliased, prove that two other objects are not aliased. This paper introduces and gives an algorithm for conditional must not alias analysis and discusses experimental results for sound race detection of Java programs. Categories and Subject Descriptors D.2.4 [Software Engineering]: Software/Program Verification -- Reliability General Terms Experimentation, Reliability, Verification Keywords static race detection, Java, synchronization, concurrency, multi-threading
Mayur Naik, Alex Aiken
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2007
Where POPL
Authors Mayur Naik, Alex Aiken
Comments (0)