ABSTRACT
Atomicity 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 multithreaded programming languages provide no built-in support to ensure atomicity; instead they rely on the fact that programmers would use locks properly in order to guarantee that atomic code blocks are indeed atomic. However, improper use of locks can sometimes fail to ensure atomicity. Therefore, we need tools that can check atomicity properties of lock-based code automatically.
We propose a randomized dynamic analysis technique to detect a special, but important, class of atomicity violations that are often found in real-world programs. Specifically, our technique modifies the existing Java thread scheduler behavior to create atomicity violations with high probability. Our approach has several advantages over existing dynamic analysis tools. First, we can create a real atomicity violation and see if an exception can be thrown. Second, we can replay an atomicity violating execution by simply using the same seed for random number generation---we do not need to record the execution. Third, we give no false warnings unlike existing dynamic atomicity checking techniques. We have implemented the technique in a prototype tool for Java and have experimented on a number of large multi-threaded Java programs and libraries. We report a number of previously known and unknown bugs and atomicity violations 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
- 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
- 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
- A. Farzan and P. Madhusudan. Causal atomicity. In Computer Aided Verification (CAV'06), volume 4144 of Lecture Notes in Computer Science, pages 315--328. Springer, 2006. Google ScholarDigital Library
- C. Flanagan. Verifying commit-atomicity using model-checking. In 11th International SPIN Workshop, pages 252--266, 2004.Google ScholarCross Ref
- 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, S. N. Freund, and J. Yi. Velodrome: a sound and complete dynamic atomicity checker for multithreaded programs. In PLDI '08: Proceedings of the 2008 ACM SIGPLAN conference on Programming language design and implementation, pages 293--303. ACM, 2008. Google ScholarDigital Library
- C. Flanagan and S. Qadeer. A type and effect system for atomicity. In Proc. of the ACM SIGPLAN Conference on Programming language design and implementation (PLDI'03), pages 338--349, 2003. Google ScholarDigital Library
- S. N. Freund and S. Qadeer. Checking concise specifications for multithreaded software. Journal of Object Technology, 3(6):81--101, 2004.Google ScholarCross Ref
- 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
- J. Hatcliff, Robby, and M. B. Dwyer. Verifying atomicity specifications for concurrent object-oriented software using model-checking. In Proc. of the International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'04), pages 175--190, 2004.Google ScholarCross Ref
- 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
- R. J. Lipton. Reduction: A method of proving properties of parallel programs. Communications of the ACM, 18(12):717--721, 1975. 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, 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 racesallusing replay analysis. In ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation (PLDI), pages 22--31, 2007. 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
- 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
- K. Sen. Effective random testing of concurrent programs. In 22nd IEEE/ACM International Conference on Automated Software Engineering (ASE'07), 2007. Google ScholarDigital Library
- K. Sen. Race directed random testing of concurrent programs. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'08), 2008. To appear. 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
- 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
- R. Vallee-Rai, L. Hendren, V. Sundaresan, P. Lam, E. Gagnon, and P. Co. Soot - a Java optimization framework. In CASCON 1999, pages 125--135, 1999.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
- L. Wang and S. D. Stoller. Run-time analysis for atomicity. In 3rd Workshop on Run-time Verification (RV'03), volume 89 of ENTCS, 2003.Google ScholarCross Ref
- L. Wang and S. D. Stoller. Accurate and efficient runtime detection of atomicity errors in concurrent programs. In Proc. ACM SIGPLAN 2006 Symposium on Principles and Practice of Parallel Programming (PPoPP), pages 137--146. ACM Press, Mar. 2006. Google ScholarDigital Library
Index Terms
- Randomized active atomicity violation detection in 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 ...
Race directed random testing of concurrent programs
PLDI '08Bugs 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 ...
Synthesizing tests for detecting atomicity violations
ESEC/FSE 2015: Proceedings of the 2015 10th Joint Meeting on Foundations of Software EngineeringUsing thread-safe libraries can help programmers avoid the complexities of multithreading. However, designing libraries that guarantee thread-safety can be challenging. Detecting and eliminating atomicity violations when methods in the libraries are ...
Comments