Abstract
Bugs in multi-threaded programs often arise due to data races. Numerous static and dynamic program analysis techniques have been proposed to detect data races. We propose a novel randomized dynamic analysis technique that utilizes potential data race information obtained from an existing analysis tool to separate real races from false races without any need for manual inspection. Specifically, we use potential data race information obtained from an existing dynamic analysis technique to control a random scheduler of threads so that real race conditions get created with very high probability and those races get resolved randomly at runtime. Our approach has several advantages over existing dynamic analysis tools. First, we can create a real race condition and resolve the race randomly to see if an error can occur due to the race. Second, we can replay a race revealing execution efficiently by simply using the same seed for random number generation--we do not need to record the execution. Third, our approach has very low overhead compared to other precise dynamic race detection techniques because we only track all synchronization operations and a single pair of memory access statements that are reported to be in a potential race by an existing analysis. We have implemented the technique in a prototype tool for Java and have experimented on a number of large multi-threaded Java programs. We report a number of previously known and unknown bugs and real races in these Java programs.
- S. V. Adve, M. D. Hill, B. P. Miller, and R. H. B. Netzer. Detecting data races on weak memory systems. In 18th annual International Symposium on Computer architecture (ISCA), pages 234--243. ACM, 1991. Google ScholarDigital Library
- R. Agarwal, A. Sasturkar, L. Wang, and S. D. Stoller. Optimized run-time race detection and atomicity checking using partial discovered types. In 20th IEEE/ACM international Conference on Automated software engineering (ASE), pages 233--242. ACM, 2005. Google ScholarDigital Library
- R. Agarwal and S. D. Stoller. Type inference for parameterized race-free java. In Verification, Model Checking, and Abstract Interpretation, 5th International Conference (VMCAI), pages 149--160, 2004.Google Scholar
- A. Aiken and D. Gay. Barrier inference. In 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 342--354. ACM, 1998. Google ScholarDigital Library
- D. F. Bacon, R. E. Strom, and A. Tarafdar. Guava: a dialect of java without data races. In ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA'00), pages 382--400, 2000. Google ScholarDigital Library
- C. Boyapati and M. C. Rinard. A parameterized type system for race-free java programs. In ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA'01), pages 56--69, 2001. Google ScholarDigital Library
- D. Bruening. Systematic testing of multithreaded Java programs. Master's thesis, MIT, 1999.Google Scholar
- S. Burckhardt, R. Alur, and M. M. K. Martin. Checkfence: checking consistency of concurrent data types on relaxed memory models. In CM SIGPLAN 2007 Conference on Programming Language Design and Implementation (PLDI), pages 12--21, 2007. Google ScholarDigital Library
- R. H. Carver and Y. Lei. A general model for reachability testing of concurrent programs. In 6th International Conference on Formal Engineering Methods (ICFEM'04), volume 3308 of LNCS, pages 76--98, 2004.Google ScholarCross Ref
- J. D. Choi, K. Lee, A. Loginov, R. O'Callahan, V. Sarkar, and M. Sridharan. Efficient and precise datarace detection for multithreaded object-oriented programs. In Proc. of the ACM SIGPLAN Conference on Programming language design and implementation, pages 258--269, 2002. Google ScholarDigital Library
- J.-D. Choi, B. P. Miller, and R. H. B. Netzer. Techniques for debugging parallel programs with flowback analysis. ACM Trans. Program. Lang. Syst., 13(4):491--530, 1991. Google ScholarDigital Library
- J.-D. Choi and A. Zeller. Isolating failure-inducing thread schedules. In ISSTA '02: Proceedings of the 2002 ACM SIGSOFT international symposium on Software testing and analysis, pages 210--220. ACM, 2002. Google ScholarDigital Library
- M. Christiaens and K. D. Bosschere. Trade, a topological approach to on-the-fly race detection in java programs. In JavaTM Virtual Machine Research and Technology Symposium (JVM), pages 15--15. USENIX Association, 2001. Google ScholarDigital Library
- A. Dinning and E. Schonberg. Detecting access anomalies in programs with critical sections. In Proc. of the ACM/ONR Workshop on Parallel and Distributed Debugging, 1991. Google ScholarDigital Library
- M. B. Dwyer, S. Elbaum, S. Person, and R. Purandare. Parallel randomized state-space search. In 29th International Conference on Software Engineering (ICSE), pages 3--12. IEEE, 2007. Google ScholarDigital Library
- M. B. Dwyer, J. Hatcliff, Robby, and V. P. Ranganath. Exploiting object escape and locking information in partial-order reductions for concurrent object-oriented programs. Form. Methods Syst. Des., 25(2--3):199--240, 2004. Google ScholarDigital Library
- J. E. M. Clarke, O. Grumberg, and D. A. Peled. Model checking. MIT Press, 1999. Google ScholarDigital Library
- O. Edelstein, E. Farchi, Y. Nir, G. Ratsaby, , and S. Ur. Multithreaded Java program test generation. IBM Systems Journal, 41(1):111--125, 2002. Google ScholarDigital Library
- D. R. Engler and K. Ashcraft. Racerx: effective, static detection of race conditions and deadlocks. In 19th ACM Symposium on Operating Systems Principles (SOSP), pages 237--252, 2003. Google ScholarDigital Library
- C. Flanagan and S. N. Freund. Type-based race detection for java. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'00), pages 219--232, 2000. Google ScholarDigital Library
- C. Flanagan and S. N. Freund. Detecting race conditions in large programs. In Proc. of the Program Analysis for Software Tools and Engineering Conference, 2001. Google ScholarDigital Library
- C. Flanagan and S. N. Freund. Atomizer: a dynamic atomicity checker for multithreaded programs. In 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 256--267, 2004. Google ScholarDigital Library
- C. Flanagan and S. Qadeer. A type and effect system for atomicity. In ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation, pages 338--349, 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 ACM SIGPLAN Conference on Programming language design and implementation, pages 1--11, 2003. Google ScholarDigital Library
- P. Godefroid. Model checking for programming languages using verisoft. In 24th Symposium on Principles of Programming Languages, pages 174--186, 1997. Google ScholarDigital Library
- R. Grosu and S. A. Smolka. Monte carlo model checking. In 11th International Conference Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2005), volume 3440 of LNCS, pages 271--286, 2005. Google ScholarDigital Library
- K. Havelund and T. Pressburger. Model Checking Java Programs using Java PathFinder. Int. Journal on Software Tools for Technology Transfer, 2(4):366--381, 2000.Google ScholarCross Ref
- T. A. Henzinger, R. Jhala, and R. Majumdar. Race checking by context inference. SIGPLAN Not., 39(6):1--13, 2004. Google ScholarDigital Library
- G. Holzmann. The Spin model checker. IEEE Transactions on Software Engineering, 23(5):279--295, 1997. Google ScholarDigital Library
- J. Mellor-Crummey. On-the-fly detection of data races for programs with nested fork-join parallelism. In ACM/IEEE conference on Supercomputing, pages 24--33. ACM, 1991. Google ScholarDigital Library
- M. Musuvathi and S. Qadeer. Iterative context bounding for systematic testing of multithreaded programs. In ACM Symposium on Programming Language Design and Implementation (PLDI'07), 2007. Google ScholarDigital Library
- M. Naik and A. Aiken. Conditional must not aliasing for static race detection. In 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 327--338, 2007. Google ScholarDigital Library
- M. Naik, A. Aiken, and J. Whaley. Effective static race detection for java. In ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 308--319, 2006. Google ScholarDigital Library
- S. Narayanasamy, Z. Wang, J. Tigani, A. Edwards, and B. Calder. Automatically classifying benign and harmful data races using replay analysis. In ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation (PLDI), pages 22--31, 2007. Google ScholarDigital Library
- R. Netzer and B. Miller. Detecting data races in parallel program executions. In Advances in Languages and Compilers for Parallel Computing. MIT Press, 1990.Google Scholar
- H. Nishiyama. Detecting data races using dynamic escape analysis based on read barrier. In Virtual Machine Research and Technology Symposium, pages 127--138, 2004. Google ScholarDigital Library
- R. O'Callahan and J.-D. Choi. Hybrid dynamic data race detection. In ACM SIGPLAN symposium on Principles and practice of parallel programming, pages 167--178. ACM, 2003. Google ScholarDigital Library
- E. Pozniansky and A. Schuster. Efficient on-the-fly data race detection in multithreaded c++ programs. In Ninth ACM SIGPLAN symposium on Principles and practice of parallel programming (PPoPP), pages 179--190. ACM, 2003. Google ScholarDigital Library
- P. Pratikakis, J. S. Foster, and M. Hicks. LOCKSMITH: context-sensitive correlation analysis for race detection. In ACM SIGPLAN conference on Programming language design and implementation (PLDI), pages 320--331. ACM, 2006. Google ScholarDigital Library
- S. Qadeer and D. Wu. Kiss: keep it simple and sequential. In ACM SIGPLAN 2004 conference on Programming language design and implementation (PLDI), pages 14--24. ACM, 2004. Google ScholarDigital Library
- B. Richards and J. R. Larus. Protocol-based data-race detection. In Proc. of the SIGMETRICS symposium on Parallel and distributed tools, pages 40--47, 1998. Google ScholarDigital Library
- M. Ronsse and K. D. Bosschere. Recplay: a fully integrated practical record/replay system. ACM Trans. Comput. Syst., 17(2):133--152, 1999. Google ScholarDigital Library
- S. Savage, M. Burrows, G. Nelson, P. Sobalvarro, and T. E. Anderson. Eraser: A dynamic data race detector for multithreaded programs. ACM Trans. Comput. Syst., 15(4):391--411, 1997. Google ScholarDigital Library
- E. Schonberg. On-the-fly detection of access anomalies. In ACM SIGPLAN '89 Conference on Programming Language Design and Implementation (PLDI), volume 24, pages 285--297, 1989. Google ScholarDigital Library
- K. Sen. Effective random testing of concurrent programs. In 22nd IEEE/ACM nternational Conference on Automated Software Engineering (ASE'07), 2007. Google ScholarDigital Library
- K. Sen and G. Agha. A race-detection and flipping algorithm for automated testing of multi-threaded programs. In Haifa verification conference 2006 (HVC'06), Lecture Notes in Computer Science. Springer, 2006. Google ScholarDigital Library
- O. Shacham, M. Sagiv, and A. Schuster. Scaling model checking of dataraces using dynamic information. J. Parallel Distrib. Comput., 67(5):536--550, 2007. Google ScholarDigital Library
- S. F. Siegel, A. Mironova, G. S. Avrunin, and L. A. Clarke. Using model checking with symbolic execution to verify parallel numerical programs. In International symposium on Software testing and analysis (ISSTA), pages 157--168. ACM Press, 2006. Google ScholarDigital Library
- N. Sterling. Warlock: A static data race analysis tool. In USENIX Winter Technical Conference, pages 97--106, 1993.Google Scholar
- S. D. Stoller. Testing concurrent Java programs using randomized scheduling. In Workshop on Runtime Verification (RV'02), volume 70 of ENTCS, 2002.Google ScholarCross Ref
- M. Vaziri, F. Tip, and J. Dolby. Associating synchronization constraints with data in an object-oriented language. In 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 334--345, 2006. Google ScholarDigital Library
- W. Visser, K. Havelund, G. Brat, and S. Park. Model checking programs. In 15th International Conference on Automated Software Engineering (ASE). IEEE, 2000. Google ScholarDigital Library
- C. von Praun and T. R. Gross. Object race detection. In 16th ACM SIGPLAN conference on Object oriented programming, systems, languages, and applications (OOPSLA), pages 70--82. ACM, 2001. Google ScholarDigital Library
- Y. Yu, T. Rodeheffer, and W. Chen. Racetrack: efficient detection of data race conditions via adaptive tracking. SIGOPS Oper. Syst. Rev., 39(5):221--234, 2005. Google ScholarDigital Library
Index Terms
- Race directed random testing of concurrent programs
Recommendations
Race directed random testing of concurrent programs
PLDI '08: Proceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and ImplementationBugs in multi-threaded programs often arise due to data races. Numerous static and dynamic program analysis techniques have been proposed to detect data races. We propose a novel randomized dynamic analysis technique that utilizes potential data race ...
Randomized active atomicity violation detection in concurrent programs
SIGSOFT '08/FSE-16: Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of software engineeringAtomicity is an important specification that enables programmers to understand atomic blocks of code in a multi-threaded program as if they are sequential. This significantly simplifies the programmer's job to reason about correctness. Several modern ...
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