ABSTRACT
Data races are among the most reliable indicators of programming errors in concurrent software. For at least two decades, Lamport's happens-before (HB) relation has served as the standard test for detecting races--other techniques, such as lockset-based approaches, fail to be sound, as they may falsely warn of races. This work introduces a new relation, causally-precedes (CP), which generalizes happens-before to observe more races without sacrificing soundness. Intuitively, CP tries to capture the concept of happens-before ordered events that must occur in the observed order for the program to observe the same values. What distinguishes CP from past predictive race detection approaches (which also generalize an observed execution to detect races in other plausible executions) is that CP-based race detection is both sound and of polynomial complexity. We demonstrate that the unique aspects of CP result in practical benefit. Applying CP to real-world programs, we successfully analyze server-level applications (e.g., Apache FtpServer) and show that traces longer than in past predictive race analyses can be analyzed in mere seconds to a few minutes. For these programs, CP race detection uncovers races that are hard to detect by repeated execution and HB race detection: a single run of CP race detection produces several races not discovered by 10 separate rounds of happens-before race detection.
Supplemental Material
- M. Abadi, C. Flanagan, and S. N. Freund. Types for safe locking: Static race detection for Java. Transactions on Programming Languages and Systems (TOPLAS), 28(2):207--255, 2006. Google ScholarDigital Library
- R. Agarwal, A. Sasturkar, L. Wang, and S. D. Stoller. Optimized runtime race detection and atomicity checking using partial discovered types. In International Conference on Automated Software Engineering (ASE), 2005. Google ScholarDigital Library
- A. Aiken and D. Gay. Barrier inference. In Symposium on Principles of Programming Languages (POPL), 1998. Google ScholarDigital Library
- D. F. Bacon, R. E. Strom, and A. Tarafdar. Guava: a dialect of Java without data races. In Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2000. Google ScholarDigital Library
- U. Banerjee, B. Bliss, Z. Ma, and P. Petersen. A theory of data race detection. In Workshop on Parallel and Distributed Systems: Testing, Analysis, and Debugging (PADTAD), 2006. Google ScholarDigital Library
- E. Bodden and K. Havelund. Racer: effective race detection using AspectJ. In International Symposium on Software Testing and Analysis (ISSTA), 2008. Google ScholarDigital Library
- M. D. Bond, K. E. Coons, and K. S. McKinley. PACER: proportional detection of data races. In Conference on Programming Language Design and Implementation (PLDI), 2010. Google ScholarDigital Library
- C. Boyapati, R. Lee, and M. Rinard. A type system for preventing data races and deadlocks in Java programs. In Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2002. Google ScholarDigital Library
- F. Chen and G. Roşu. Predicting concurrency errors at runtime using sliced causality. Technical Report UIUCDCS-R-2006--2965, Department of Computer Science, University of Illinois at Urbana-Champaign, 2006.Google Scholar
- F. Chen and G. Roşu. Parametric and Sliced Causality. In Computer Aided Verification (CAV), 2007. Google ScholarDigital Library
- F. Chen, T. F. Serbanuta, and G. Rosu. Effective predictive runtime analysis using sliced causality and atomicity. Technical Report UIUCDCS-R-2007--2905, University of Illinois at Urbana-Champaign, Department of Computer Science, October 2007.Google Scholar
- F. Chen, T. F. Serbanuta, and G. Rosu. jPredictor: a predictive runtime analysis tool for Java. In International Conference on Software Engineering (ICSE), 2008. Google ScholarDigital Library
- J.-D. Choi, K. Lee, A. Loginov, R. O'Callahan, V. Sarkar, and M. Sridhara. Efficient and precise datarace detection for multithreaded object-oriented programs. In Conference on Programming Language Design and Implementation (PLDI), 2002. Google ScholarDigital Library
- M. Christiaens and K. D. Bosschere. TRaDe: Data Race Detection for Java. In International Conference on Computational Science, 2001. Google ScholarDigital Library
- A. Dinning and E. Schonberg. Detecting access anomalies in programs with critical sections. SIGPLAN Notices, 26(12):85--96, 1991. Google ScholarDigital Library
- M. B. Dwyer and L. A. Clarke. Data flow analysis for verifying properties of concurrent programs. In International Symposium on Foundations of Software Engineering (FSE), 1994. Google ScholarDigital Library
- T. Elmas, S. Qadeer, and S. Tasiran. Goldilocks: a race and transaction-aware Java runtime. In Conference on Programming Language Design and Implementation (PLDI), 2007. Google ScholarDigital Library
- M. Emmi, S. Qadeer, and Z. Rakamarić. Delay-bounded scheduling. In Symposium on Principles of Programming Languages (POPL), 2011. Google ScholarDigital Library
- D. R. Engler and K. Ashcraft. RacerX: Effective, static detection of race conditions and deadlocks. In ACM Symposium on Operating Systems Principles (SOSP), 2003. Google ScholarDigital Library
- A. Farzan, P. Madhusudan, and F. Sorrentino. Meta-analysis for atomicity violations under nested locking. In Computer Aided Verification (CAV), 2009. Google ScholarDigital Library
- C. Flanagan and S. N. Freund. FastTrack: efficient and precise dynamic race detection. In Conference on Programming Language Design and Implementation (PLDI), 2009. Google ScholarDigital Library
- C. Flanagan and S. N. Freund. The roadrunner dynamic analysis framework for concurrent programs. In PASTE, pages 1--8, 2010. Google ScholarDigital Library
- C. Flanagan, S. N. Freund, and J. Yi. Velodrome: A sound and complete dynamic atomicity checker for multithreaded programs. In Conference on Programming Language Design and Implementation (PLDI), 2008. Google ScholarDigital Library
- D. Grossman. Type-safe multithreading in Cyclone. In Workshop on Types in Language Design and Implementation (TLDI), 2003. Google ScholarDigital Library
- J. J. Harrow. Runtime checking of multithreaded applications with visual threads. In International SPIN Workshop on Model Checking of Software, 2000. Google ScholarDigital Library
- D. P. Helmbold, C. E. McDowell, and J. zhong Wang. Detecting data races by analyzing sequential traces. In HICCS-24, Hawaii Intl. Conference on System Sciences (HICCS-24), 1990.Google Scholar
- V. Kahlon, F. Ivancić, and A. Gupta. Reasoning about threads communicating via locks. In Computer Aided Verification (CAV), 2005. Google ScholarDigital Library
- V. Kahlon and C. Wang. Universal causality graphs: A precise happens-before model for detecting bugs in concurrent programs. In Computer Aided Verification (CAV), 2010. Google ScholarDigital Library
- S. K. Lahiri, S. Qadeer, and Z. Rakamarić. Static and precise detection of concurrency errors in systems code using smt solvers. In Computer Aided Verification (CAV), 2009. Google ScholarDigital Library
- L. Lamport. Time, clocks, and the ordering of events in a distributed system. Communications of the ACM, 21:558--565, July 1978. Google ScholarDigital Library
- J. Manson, W. Pugh, and S. V. Adve. The Java memory model. In Conference on Programming Language Design and Implementation (PLDI), 2005. Google ScholarDigital Library
- J. M. Mellor-Crummey. On-the-fly detection of data races for programs with nested fork-join parallelism. In Supercomputing, 1991. Google ScholarDigital Library
- M. Musuvathi, S. Qadeer, T. Ball, G. Basler, P. A. Nainar, and I. Neamtiu. Finding and reproducing heisenbugs in concurrent programs. In Operating Systems Design and Implementation (OSDI), 2008. Google ScholarDigital Library
- M. Naik, A. Aiken, and J. Whaley. Effective static race detection for Java. In Conference on Programming Language Design and Implementation (PLDI), 2006. Google ScholarDigital Library
- H. Nishiyama. Detecting data races using dynamic escape analysis based on read barrier. In Virtual Machine Research and Technology Symposium (VM), 2004. Google ScholarDigital Library
- R. O'Callahan and J.-D. Choi. Hybrid dynamic data race detection. In Symposium on Principles and Practice of Parallel Programming (PPoPP), 2003. Google ScholarDigital Library
- E. Pozniansky and A. Schuster. Efficient on-the-fly data race detection in multihreaded C+ programs. In Symposium on Principles and Practice of Parallel Programming (PPoPP), 2003. Google ScholarDigital Library
- E. Pozniansky and A. Schuster. Multirace: efficient on-the-fly data race detection in multithreaded C+ programs. Concurrency and Computation: Practice and Experience, 19(3):327--340, 2007. Google ScholarCross Ref
- P. Pratikakis, J. S. Foster, and M. Hicks. Context-sensitive correlation analysis for detecting races. In Conference on Programming Language Design and Implementation (PLDI), 2006. Google ScholarDigital Library
- M. Said, C. Wang, Z. Yang, and K. Sakallah. Generating data race witnesses by an smt-based analysis. In NASA Formal Methods Symposium, pages 313--327. Springer, 2011. Google ScholarDigital Library
- A. Sasturkar, R. Agarwal, L. Wang, and S. D. Stoller. Automated type-based analysis of data races and atomicity. In Symposium on Principles and Practice of Parallel Programming (PPoPP), 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 ACM Symposium on Operating Systems Principles (SOSP), 1997. Google ScholarDigital Library
- E. Schonberg. On-the-fly detection of access anomalies. In Conference on Programming Language Design and Implementation (PLDI), 1989. Google ScholarDigital Library
- K. Sen. Race directed random testing of concurrent programs. In Conference on Programming Language Design and Implementation (PLDI), 2008. Google ScholarDigital Library
- K. Sen and G. Agha. Detecting errors in multithreaded programs by generalized predictive analysis of executions. In IIFIP International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS), 2005. Google ScholarDigital Library
- K. Sen, G. Rosu, and G. Agha. Online efficient predictive safety analysis of multithreaded programs. International Journal on Software Technology and Tools Transfer (STTT), 8(3):248--260, 2006. Google ScholarDigital Library
- T. F. Serbanuta, F. Chen, and G. Roşu. Maximal causal models for multithreaded systems. Technical Report UIUCDCS-R-2008--3017, University of Illinois at Urbana-Champaign, Department of Computer Science, December 2008.Google Scholar
- N. Sinha and C. Wang. On interference abstractions. In Symposium on Principles of Programming Languages (POPL), 2011. Google ScholarDigital Library
- F. Sorrentino, A. Farzan, and P. Madhusudan. PENELOPE: weaving threads to expose atomicity violations. In International Symposium on Foundations of Software Engineering (FSE), 2010. Google ScholarDigital Library
- N. Sterling. Warlock: A static data race analysis tool. In USENIX Winter Technical Conference, 1993.Google Scholar
- The Apache Software Foundation. Apache FtpServer. Available at http://mina.apache.org/ftpserver/, 2009.Google Scholar
- The Apache Software Foundation. Apache JMeter. Available at http://jakarta.apache.org/jmeter/, 2009.Google Scholar
- The World Wide Web Consortium. Jigsaw Web Server. Available from http://www.w3.org/Jigsaw/, 2009.Google Scholar
- C. von Praun and T. Gross. Static conflict analysis for multi-threaded object-oriented programs. In Conference on Programming Language Design and Implementation (PLDI), 2003. Google ScholarDigital Library
- C. von Praun and T. R. Gross. Object race detection. In Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2001. Google ScholarDigital Library
- J. W. Voung, R. Jhala, and S. Lerner. Relay: static race detection on millions of lines of code. In International Symposium on Foundations of Software Engineering (FSE), 2007. Google ScholarDigital Library
- C. Wang, S. Kundu, M. Ganai, and A. Gupta. Symbolic predictive analysis for concurrent programs. In World Congress on Formal Methods (FM), 2009. Google ScholarDigital Library
- C. Wang, R. Limaye, M. Ganai, and A. Gupta. Trace-based symbolic analysis for atomicity violations. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2010. Google ScholarDigital Library
- L. Wang and S. D. Stoller. Accurate and efficient runtime detection of atomicity errors in concurrent programs. In Symposium on Principles and Practice of Parallel Programming (PPoPP), 2006. Google ScholarDigital Library
- J. Whaley. Context-Sensitive Pointer Analysis using Binary Decision Diagrams. PhD thesis, Stanford University, Mar. 2007. Google ScholarDigital Library
- Y. Yu. RaceTrack: Efficient detection of data race conditions via adaptive tracking. In ACM Symposium on Operating Systems Principles (SOSP), 2005. Google ScholarDigital Library
Index Terms
- Sound predictive race detection in polynomial time
Recommendations
Fast, sound, and effectively complete dynamic race prediction
Writing concurrent programs is highly error-prone due to the nondeterminism in interprocess communication. The most reliable indicators of errors in concurrency are data races, which are accesses to a shared resource that can be executed concurrently. We ...
What happens-after the first race? enhancing the predictive power of happens-before based dynamic race detection
Dynamic race detection is the problem of determining if an observed program execution reveals the presence of a data race in a program. The classical approach to solving this problem is to detect if there is a pair of conflicting memory accesses that are ...
Sound predictive race detection in polynomial time
POPL '12Data races are among the most reliable indicators of programming errors in concurrent software. For at least two decades, Lamport's happens-before (HB) relation has served as the standard test for detecting races--other techniques, such as lockset-based ...
Comments