ABSTRACT
Despite the numerous static and dynamic program analysis techniques in the literature, data races remain one of the most common bugs in modern concurrent software. Further, the techniques that do exist either have limited detection capability or are unsound, meaning that they report false positives. We present a sound race detection technique that achieves a provably higher detection capability than existing sound techniques. A key insight of our technique is the inclusion of abstracted control flow information into the execution model, which increases the space of the causal model permitted by classical happens-before or causally-precedes based detectors. By encoding the control flow and a minimal set of feasibility constraints as a group of first-order logic formulae, we formulate race detection as a constraint solving problem. Moreover, we formally prove that our formulation achieves the maximal possible detection capability for any sound dynamic race detector with respect to the same input trace under the sequential consistency memory model. We demonstrate via extensive experimentation that our technique detects more races than the other state-of-the-art sound race detection techniques, and that it is scalable to executions of real world concurrent applications with tens of millions of critical events. These experiments also revealed several previously unknown races in real systems (e.g., Eclipse) that have been confirmed or fixed by the developers. Our tool is also adopted by Eclipse developers.
- https://bugs.eclipse.org/bugs/show_bug.cgi?id=419383.Google Scholar
- https://bugs.eclipse.org/bugs/show_bug.cgi?id=419543.Google Scholar
- http://www.eclipse.org/virgo/.Google Scholar
- A. Aiken and D. Gay. Barrier inference. In POPL, 1998. Google ScholarDigital Library
- S. M. Blackburn, R. Garner, C. Hoffmann, A. M. Khang, K. S. McKinley, R. Bentzur, A. Diwan, D. Feinberg, D. Frampton, S. Z. Guyer, M. Hirzel, A. Hosking, M. Jump, H. Lee, J. E. B. Moss, A. Phansalkar, D. Stefanović, T. VanDrunen, D. von Dincklage, and B. Wiedermann. The dacapo benchmarks: Java benchmarking development and analysis. In OOPSLA, 2006. Google ScholarDigital Library
- R. L. Bocchino, Jr., V. S. Adve, D. Dig, S. V. Adve, S. Heumann, R. Komuravelli, J. Overbey, P. Simmons, H. Sung, and M. Vakilian. A type and effect system for deterministic parallel Java. In OOPSLA, 2009. Google ScholarDigital Library
- M. D. Bond, K. E. Coons, and K. S. McKinley. PACER: Proportional detection of data races. In PLDI, 2010. Google ScholarDigital Library
- C. Boyapati and M. Rinard. A parameterized type system for race-free java programs. In OOPSLA, 2001. Google ScholarDigital Library
- F. Chen and G. Roşu. Parametric and sliced causality. In CAV, 2007. Google ScholarDigital Library
- F. Chen, T. F. Serbanuta, and G. Rosu. jPredictor: a predictive runtime analysis tool for Java. In ICSE, 2008. Google ScholarDigital Library
- L. De Moura and N. Bjørner. Z3: an efficient SMT solver. In TACAS, 2008. Google ScholarDigital Library
- B. Dutertre and L. D. Moura. The Yices SMT solver. Technical report, 2006.Google Scholar
- L. Effinger-Dean, B. Lucia, L. Ceze, D. Grossman, and H.-J. Boehm. IFRit: Interference-free regions for dynamic data-race detection. In OOPSLA, 2012. Google ScholarDigital Library
- T. Elmas, S. Qadeer, and S. Tasiran. Goldilocks: a race and transaction-aware Java runtime. In PLDI, 2007. Google ScholarDigital Library
- D. Engler and K. Ashcraft. RacerX: Effective, static detection of race conditions and deadlocks. In SOSP, 2003. Google ScholarDigital Library
- J. Erickson, M. Musuvathi, S. Burckhardt, and K. Olynyk. Effective data-race detection for the kernel. In OSDI, 2010. Google ScholarDigital Library
- E. Farchi, Y. Nir, and S. Ur. Concurrent bug patterns and how to test them. IPDPS, 2003. Google ScholarDigital Library
- A. Farzan, P. Madhusudan, N. Razavi, and F. Sorrentino. Predicting null-pointer dereferences in concurrent programs. In FSE, 2012. Google ScholarDigital Library
- C. Flanagan and S. N. Freund. FastTrack: Efficient and precise dynamic race detection. In PLDI, 2009. Google ScholarDigital Library
- M. P. Herlihy and J. M. Wing. Linearizability: a correctness condition for concurrent objects. TOPLAS, 1990. Google ScholarDigital Library
- J. Huang and C. Zhang. PECAN: Persuasive prediction of concurrency access anomalies. In ISSTA, 2011. Google ScholarDigital Library
- L. Lamport. Time, clocks, and the ordering of events in a distributed system. CACM, 1978. Google ScholarDigital Library
- J. Manson, W. Pugh, and S. V. Adve. The Java memory model. In POPL, 2005. Google ScholarDigital Library
- D. Marino, M. Musuvathi, and S. Narayanasamy. LiteRace: Effective sampling for lightweight data-race detection. In PLDI, 2009. Google ScholarDigital Library
- A. Mazurkiewicz. Trace theory. In Advances in Petri nets, 1987.Google Scholar
- M. Musuvathi, S. Qadeer, T. Ball, G. Basler, P. A. Nainar, and I. Neamtiu. Finding and reproducing heisenbugs in concurrent programs. In OSDI, 2008. Google ScholarDigital Library
- M. Naik, A. Aiken, and J. Whaley. Effective static race detection for Java. In PLDI, 2006. Google ScholarDigital Library
- R. O'Callahan and J.-D. Choi. Hybrid dynamic data race detection. In PPoPP, 2003. Google ScholarDigital Library
- P. Pratikakis, J. S. Foster, and M. Hicks. LOCKSMITH: Context-sensitive correlation analysis for race detection. In PLDI, 2006. Google ScholarDigital Library
- M. Said, C. Wang, Z. Yang, and K. Sakallah. Generating data race witnesses by an smt-based analysis. In NFM, 2011. Google ScholarDigital Library
- S. Savage, M. Burrows, G. Nelson, P. Sobalvarro, and T. Anderson. Eraser: a dynamic data race detector for multi-threaded programs. TOCS, 1997. Google ScholarDigital Library
- K. Sen. Race directed random testing of concurrent programs. In PLDI, 2008. Google ScholarDigital Library
- T. F. Serbanuta, F. Chen, and G. Rosu. Maximal causal models for sequentially consistent systems. In RV, 2012.Google Scholar
- O. Shacham, M. Sagiv, and A. Schuster. Scaling model checking of dataraces using dynamic information. In PPoPP, 2005. Google ScholarDigital Library
- Y. Smaragdakis, J. Evans, C. Sadowski, J. Yi, and C. Flanagan. Sound predictive race detection in polynomial time. In POPL, 2012. Google ScholarDigital Library
- F. Sorrentino, A. Farzan, and P. Madhusudan. PENELOPE: Weaving threads to expose atomicity violations. In FSE, 2010. Google ScholarDigital Library
- N. Sterling. Warlock: a static data race analysis tool. In USENIX Winter Technical Conference, 1993.Google Scholar
- W. Visser, C. S. Păsăreanu, and S. Khurshid. Test input generation with Java pathfinder. In ISSTA, 2004. Google ScholarDigital Library
- J. W. Voung, R. Jhala, and S. Lerner. RELAY: Static race detection on millions of lines of code. ESEC-FSE, 2007. Google ScholarDigital Library
Index Terms
- Maximal sound predictive race detection with control flow abstraction
Recommendations
Maximal sound predictive race detection with control flow abstraction
PLDI '14Despite the numerous static and dynamic program analysis techniques in the literature, data races remain one of the most common bugs in modern concurrent software. Further, the techniques that do exist either have limited detection capability or are ...
Precise and maximal race detection from incomplete traces
OOPSLA '16We present RDIT, a novel dynamic technique to detect data races in multithreaded programs with incomplete trace information, i.e., in the presence of missing events. RDIT is both precise and maximal: it does not report any false alarms and it detects a ...
Sound predictive race detection in polynomial time
POPL '12: Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languagesData 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