Mayur Naik
Alex Aiken
Skip Abstract Section
Abstract
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.
- S. Adve, M. Hill, B. Miller, and R. Netzer. Detecting data races on weak memory systems. In Proceedings of ISCA'91, pages 234--243, 1991.]] Google Scholar
Digital Library
- R. Agarwal, A. Sasturkar, Wang L, and S. Stoller. Optimized run-time race detection and atomicity checking using partial discovered types. In Proceedings of ASE'05, pages 233--242, 2005.]] Google ScholarDigital Library
- C. Boyapati, R. Lee, and M. Rinard. Ownership types for safe programming: Preventing data races and deadlocks. In Proceedings of OOPSLA'02, pages 211--230, 2002.]] Google ScholarDigital Library
- C. Boyapati and M. Rinard. A parameterized type system for race-free Java programs. In Proceedings of OOPSLA'01, pages 56--69, 2001.]] Google ScholarDigital Library
- J. Choi, K. Lee, A. Loginov, R. O'Callahan, V. Sarkar, and M. Sridharan. Efficient and precise datarace detection for multithreaded object-oriented programs. In Proceedings of PLDI'02, pages 258--269, 2002.]] Google ScholarDigital Library
- J. Choi, A. Loginov, and V. Sarkar. Static datarace analysis for multithreaded object-oriented programs. Technical Report RC22146, IBM Research, 2001.]]Google Scholar
- J. Choi, B. Miller, and R. Netzer. Techniques for debugging parallel programs with flowback analysis. ACM TOPLAS, 13(4):491--530, 1991.]] Google ScholarDigital Library
- M. Christiaens and K. Brosschere. TRaDe: A topological approach to on-the-fly race detection in Java programs. In Proceedings of JVM'01, pages 105--116, 2001.]] Google ScholarDigital Library
- P. Cousot and R. Cousot. Static determination of dynamic properties of generalized type unions. In Language Design for Reliable Software, pages 77--94, 1977.]] Google ScholarDigital Library
- M. Das, S. Lerner, and M. Seigle. ESP: Path-sensitive program verification in polynomial time. In Proceedings of PLDI'02, pages 57--68, 2002.]] Google ScholarDigital Library
- A. Dinning and E. Schonberg. An empirical comparison of monitoring algorithms for access anomaly detection. In Proceedings of PPoPP'90, pages 1--10, 1990.]] Google ScholarDigital Library
- A. Dinning and E. Schonberg. Detecting access anomalies in programs with critical sections. In Proceedings of PADD'91, pages 85--96, 1991.]] Google ScholarDigital Library
- D. Engler and K. Ashcraft. RacerX: Effective, static detection of race conditions and deadlocks. In Proceedings of SOSP'03, pages 237--252, 2003.]] Google ScholarDigital Library
- C. Flanagan. Verifying commit-atomicity using model-checking. In Proceedings of SPIN'04, pages 252--266, 2004.]]Google ScholarCross Ref
- C. Flanagan and M. Abadi. Types for safe locking. In Proceedings of ESOP'99, pages 91--108, 1999.]] Google ScholarDigital Library
- C. Flanagan and S. Freund. Type-based race detection for Java. In Proceedings of PLDI'00, pages 219--232, 2000.]] Google ScholarDigital Library
- C. Flanagan and S. Freund. Atomizer: a dynamic atomicity checker for multithreaded programs. In Proceedings of POPL'04, pages 256--267, 2004.]] Google ScholarDigital Library
- C. Flanagan, S. Freund, and M. Lifshin. Type inference for atomicity. In Proceedings of TLDI'05, pages 47--58, 2005.]] Google ScholarDigital Library
- C. Flanagan and S. Qadeer. A type and effect system for atomicity. In Proceedings of PLDI'03, pages 338--349, 2003.]] Google ScholarDigital Library
- C. Flanagan and S. Qadeer. Types for atomicity. In Proceedings of TLDI'03, pages 1--12, 2003.]] Google ScholarDigital Library
- S. Ghemawat, K. Randall, and D. Scales. Field analysis: Getting useful and low-cost interprocedural information. In Proceedings of PLDI'00, pages 334--344, 2000.]] Google ScholarDigital Library
- D. Grossman. Type-safe multithreading in Cyclone. In Proceedings of TLDI'03, pages 13--25, 2003.]] Google ScholarDigital Library
- J. Harrow. Runtime checking of multithreaded applications with visual threads. In Proceedings of SPIN'00, pages 331--342, 2000.]] Google ScholarDigital Library
- D. Heine and M. Lam. A practical flow-sensitive and context-sensitive C and C++ memory leak detector. In Proceedings of PLDI'03, pages 168--181, 2003.]] Google ScholarDigital Library
- T. Henzinger, R. Jhala, and R. Majumdar. Race checking by context inference. In Proceedings of PLDI'04, pages 1--13, 2004.]] Google ScholarDigital Library
- L. Lamport. Time, clocks, and the ordering of events in a distributed system. CACM, 21(7):558--565, 1978.]] Google ScholarDigital Library
- T. Lev-Ami, N. Immerman, T. Reps, S. Sagiv, S. Srivastava, and G. Yorsh. Simulating reachability using first-order logic with applications to verification of linked data structures. In Proceedings of CADE'05, pages 99--115, 2005.]] Google ScholarDigital Library
- O. Lhoták and L. Hendren. Context-sensitive points-to analysis: is it worth it? In Proceedings of CC'06, 2006.]] Google ScholarDigital Library
- R. Lipton. Reduction: A method of proving properties of parallel programs. CACM, 18(12):717--721, 1975.]] Google ScholarDigital Library
- S. McPeak and G. Necula. Data structure specifications via local equality axioms. In Proceedings of CAV'05, pages 476--490, 2005.]] Google ScholarDigital Library
- J. Mellor-Crummey. On-the-fly detection of data races for programs with nested fork-join parallelism. In Proceedings of SC'91, pages 24--35, 1991.]] Google ScholarDigital Library
- A. Milanova, A. Rountev, and B. Ryder. Parameterized object sensitivity for points-to and side-effect analyses for Java. In Proceedings of ISSTA'02, pages 1--11, 2002.]] Google ScholarDigital Library
- M. Naik, A. Aiken, and J. Whaley. Effective static race detection for Java. In Proceedings of PLDI'06, pages 308--319, 2006.]] Google ScholarDigital Library
- R. O'Callahan and J. Choi. Hybrid dynamic data race detection. In Proceedings of PPoPP'03, pages 167--178, 2003.]] Google ScholarDigital Library
- E. Pozniansky and A. Schuster. Efficient on-the-fly data race detection in multithreaded C++ programs. In Proceedings of PPoPP'03, pages 179--190, 2003.]] Google ScholarDigital Library
- P. Pratikakis, J. Foster, and M. Hicks. LOCKSMITH: Context-sensitive correlation analysis for race detection. In Proceedings of PLDI'06, pages 320--331, 2006.]] Google ScholarDigital Library
- S. Qadeer and D. Wu. KISS: Keep it simple and sequential. In Proceedings of PLDI'04, pages 14--24, 2004.]] Google ScholarDigital Library
- M. Ronsse and K. Bosschere. RecPlay: A fully integrated practical record/replay system. ACM TOCS, 17(2):133--152, 1999.]] Google ScholarDigital Library
- A. Sasturkar, R. Agarwal, L. Wang, and S. Stoller. Automated type-based analysis of data races and atomicity. In Proceedings of PPoPP'05, pages 83--94, 2005.]] Google ScholarDigital Library
- S. Savage, M. Burrows, G. Nelson, P. Sobalvarro, and T. Anderson. Eraser: A dynamic data race detector for multi-threaded programs. In Proceedings of SOSP'97, pages 27--37, 1997.]] Google ScholarDigital Library
- E. Schonberg. On-the-fly detection of access anomalies. In Proceedings of PLDI'89, pages 285--297, 1989.]] Google ScholarDigital Library
- N. Sterling. WARLOCK - a static data race analysis tool. In Proceedings of the Usenix Winter 1993 Technical Conference, pages 97--106, 1993.]]Google Scholar
- C. von Praun and T. Gross. Object race detection. In Proceedings of OOPSLA'01, pages 70--82, 2001.]] Google ScholarDigital Library
- C. von Praun and T. Gross. Static conflict analysis for multi-threaded object-oriented programs. In Proceedings of PLDI'03, pages 115--128, 2003.]] Google ScholarDigital Library
- L. Wang and S. Stoller. Static analysis of atomicity for programs with non-blocking synchronization. In Proceedings of PPoPP'05, pages 61--71, 2005.]] Google ScholarDigital Library
- L. Wang and S. Stoller. Runtime analysis of atomicity for multi-threaded programs. IEEE TSE, 32(2):93--110, 2006.]] Google ScholarDigital Library
- Y. Yu, T. Rodeheffer, and W. Chen. RaceTrack: Efficient detection of data race conditions via adaptive tracking. In Proceedings of SOSP'05, pages 221--234, 2005.]] Google ScholarDigital Library
Index Terms
- Conditional must not aliasing for static race detection
Recommendations
Effective static race detection for Java
PLDI '06: Proceedings of the 27th ACM SIGPLAN Conference on Programming Language Design and ImplementationWe present a novel technique for static race detection in Java programs, comprised of a series of stages that employ a combination of static analyses to successively reduce the pairs of memory accesses potentially involved in a race. We have implemented ...
Effective static race detection for Java
Proceedings of the 2006 PLDI ConferenceWe present a novel technique for static race detection in Java programs, comprised of a series of stages that employ a combination of static analyses to successively reduce the pairs of memory accesses potentially involved in a race. We have implemented ...
Conditional must not aliasing for static race detection
POPL '07: Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languagesRace 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 ...
Comments