Conditional Must Not Aliasing for Static Race Detection

---

Mayur Naik and Alex Aiken

---

Race detection algorithms for multi-threaded programs using the common lock-based synchronization idiom must correlate lock values 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 values are not aliased, prove that two other values are not aliased. This paper introduces and gives an algorithm for conditional must not alias analysis and discusses experimental results with an implementation for sound race detection for Java programs.

---

In Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'07), Nice, France, January 2007 (to appear).

---

[PDF paper] [PS paper] [PPT slides]

---