Mayur Naik
Alex Aiken
Skip Abstract Section
Abstract
We 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 our technique and applied it to a suite of multi-threaded Java programs. Our experiments show that it is precise, scalable, and useful, reporting tens to hundreds of serious and previously unknown concurrency bugs in large, widely-used programs with few false alarms.
- S. Adve, M. Hill, B. Miller, and R. Netzer. Detecting data races on weak memory systems. In Proceedings of the 18th Annual International Symposium on Computer Architecture (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 the 20th IEEE/ACM International Conference on Automated Software Engineering (ASE'05), pages 233--242, 2005.]] Google ScholarDigital Library
- R. Agarwal and S. Stoller. Type inference for parameterized race-free Java. In Proceedings of the 5th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'04), pages 149--160, 2004.]]Google ScholarCross Ref
- A. Aiken and D. Gay. Barrier inference. In Proceedings of the 25th ACMSIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'98), pages 342--354, 1998.]] Google ScholarDigital Library
- D. Bacon, R. Strom, and A. Tarafdar. Guava: A dialect of Java without data races. In Proceedings of the ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'00), pages 382--400, 2000.]] Google ScholarDigital Library
- M. Berndl, O. Lhoták, F. Qian, L. Hendren, and N. Umanee. Points-to analysis using BDDs. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'03), pages 103--114, 2003.]] Google ScholarDigital Library
- C. Boyapati, R. Lee, and M. Rinard. Ownership types for safe programming: Preventing data races and deadlocks. In Proceedings of the ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (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 the ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'01), pages 56--69, 2001.]] Google ScholarDigital Library
- R. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, 35(8):677--691, 1986.]] Google ScholarDigital Library
- G. Cheng, M. Feng, C. Leiserson, K. Randall, and A. Stark. Detecting data races in Cilk programs that use locks. In Proceedings of the 10th Annual ACM Symposium on Parallel Algorithms and Architectures (SPAA'98), pages 298--309, 1998.]] 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 the ACM SIGPLAN Conference on Programming Language Design and Implementation (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 Transactions on Programming Languages and Systems, 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 the 1st Java Virtual Machine Research and Technology Symposium (JVM'01), pages 105--116, 2001.]] Google ScholarDigital Library
- A. Dinning and E. Schonberg. An empirical comparison of monitoring algorithms for access anomaly detection. In Proceedings of the ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (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 the 1991 ACM/ONR Workshop on Parallel and Distributed Debugging (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 the 19th ACM Symposium on Operating Systems Principles (SOSP'03), pages 237--252, 2003.]] Google ScholarDigital Library
- C. Flanagan. Verifying commit-atomicity using modelchecking. In Proceedings of the 11th International SPIN Workshop on Model Checking Software (SPIN'04), pages 252--266, 2004.]]Google Scholar
- C. Flanagan and M. Abadi. Types for safe locking. In Proceedings of the 8th European Symposium on Programming (ESOP'99), pages 91--108, 1999.]] Google ScholarDigital Library
- C. Flanagan and S. Freund. Type-based race detection for Java. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'00), pages 219--232, 2000.]] Google ScholarDigital Library
- C. Flanagan and S. Freund. Detecting race conditions in large programs. In Proceedings of the ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering (PASTE'01), pages 90--96, 2001.]] Google ScholarDigital Library
- C. Flanagan and S. Freund. Atomizer: a dynamic atomicity checker for multithreaded programs. In Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'04), pages 256--267, 2004.]] Google ScholarDigital Library
- C. Flanagan and S. Freund. Type inference against races. In Proceedings of the 11th International Static Analysis Symposium (SAS'04), pages 116--132, 2004.]]Google ScholarCross Ref
- C. Flanagan, S. Freund, and M. Lifshin. Type inference for atomicity. In Proceedings of the ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI'05), pages 47--58, 2005.]] Google ScholarDigital Library
- C. Flanagan and S. Qadeer. A type and effect system for atomicity. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'03), pages 338--349, 2003.]] Google ScholarDigital Library
- C. Flanagan and S. Qadeer. Types for atomicity. In Proceedings of the ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI'03), pages 1--12, 2003.]] Google ScholarDigital Library
- D. Gay, P. Levis, R. von Behren, M. Welsh, E. Brewer, and D. Culler. The nesC language: A holistic approach to networked embedded systems. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'03), pages 1--11, 2003.]] Google ScholarDigital Library
- J. Harrow. Runtime checking of multithreaded applications with visual threads. In Proceedings of the 7th International SPIN Workshop on Model Checking Software (SPIN'00), pages 331--342, 2000.]] Google ScholarDigital Library
- T. Henzinger, R. Jhala, and R. Majumdar. Race checking by context inference. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'04), pages 1--13, 2004.]] Google ScholarDigital Library
- M. Lam, J. Whaley, B. Livshits, M. Martin, D. Avots, M. Carbin, and C. Unkel. Context-sensitive program analysis as database queries. In Proceedings of the 24th ACMSIGACTSIGMOD-SIGART Symposium on Principles of Database Systems (PODS'05), pages 1--12, 2005.]] Google ScholarDigital Library
- L. Lamport. Time, clocks, and the ordering of events in a distributed system. Communications of the ACM, 21(7):558--565, 1978.]] Google ScholarDigital Library
- O. Lhoták and L. Hendren. Jedd: a BDD-based relational extension of Java. In Proceedings of the ACMSIGPLAN Conference on Programming Language Design and Implementation (PLDI'04), pages 158--169, 2004.]] Google ScholarDigital Library
- R. Lipton. Reduction: A method of proving properties of parallel programs. Communications of the ACM, 18(12):717--721, 1975.]] Google ScholarDigital Library
- J. Manson, W. Pugh, and S. Adve. The Java memory model. In Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'05), pages 378--391, 2005.]] Google ScholarDigital Library
- J. Mellor-Crummey. On-the-fly detection of data races for programs with nested fork-join parallelism. In Proceedings of the 4th Annual Conference on Supercomputing (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 the International Symposium on Software Testing and Analysis (ISSTA'02), pages 1--11, 2002.]] Google ScholarDigital Library
- A. Milanova, A. Rountev, and B. Ryder. Parameterized object sensitivity for points-to analysis for Java. ACM Transactions on Software Engineering Methodology, 14(1):1--41, 2005.]] Google ScholarDigital Library
- H. Nishiyama. Detecting data races using dynamic escape analysis based on read barrier. In Proceedings of the 3rd Virtual Machine Research and Technology Symposium (VM'04), pages 127--138, 2004.]] Google ScholarDigital Library
- R. O'Callahan and J. Choi. Hybrid dynamic data race detection. In Proceedings of the ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (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 the ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP'03), pages 179--190, 2003.]] Google ScholarDigital Library
- P. Pratikakis, J. Foster, and M. Hicks. LOCKSMITH: Contextsensitive correlation analysis for race detection. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'06), 2006.]] Google ScholarDigital Library
- S. Qadeer and D.Wu. KISS: Keep it simple and sequential. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'04), pages 14--24, 2004.]] Google ScholarDigital Library
- M. Ronsse and K. Bosschere. RecPlay: A fully integrated practical record/replay system. ACM Transactions on Computer Systems, 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 the ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (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 multithreaded programs. In Proceedings of the 16th ACM Symposium on Operating System Principles (SOSP'97), pages 27--37, 1997.]] Google ScholarDigital Library
- E. Schonberg. On-the-fly detection of access anomalies. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (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
- R. Vallée-Rai, P. Co, E. Gagnon, L. Hendren, P. Lam, and V. Sundaresan. Soot - a Java optimization framework. In Proceedings of the 1999 Conference of the Centre for Advanced Studies on Collaborative Research (CASCON'99), pages 125--135, 1999.]]Google Scholar
- C. von Praun and T. Gross. Object race detection. In Proceedings of the ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'01), pages 70--82, 2001.]] Google ScholarDigital Library
- C. von Praun and T. Gross. Static conflict analysis for multithreaded object-oriented programs. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (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 the ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP'05), pages 61--71, 2005.]] Google ScholarDigital Library
- L. Wang and S. Stoller. Runtime analysis of atomicity for multi-threaded programs. IEEE Transactions on Software Engineering, 32(2):93--110, 2006.]] Google ScholarDigital Library
- J. Whaley and M. Lam. Cloning-based context-sensitive pointer alias analysis using binary decision diagrams. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'04), pages 131--144, 2004.]] Google ScholarDigital Library
- Y. Yu, T. Rodeheffer, and W. Chen. RaceTrack: Efficient detection of data race conditions via adaptive tracking. In Proceedings of the 20th ACM Symposium on Operating Systems Principles (SOSP'05), pages 221--234, 2005.]] Google ScholarDigital Library
- J. Zhu and S. Calman. Symbolic pointer analysis revisited. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'04), pages 145--157, 2004.]] Google ScholarDigital Library
Index Terms
- Effective static race detection for Java
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 ...
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 ...
Conditional must not aliasing for static race detection
Proceedings of the 2007 POPL ConferenceRace 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