Randomized active atomicity violation detection in concurrent programs

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.

REFERENCES

• 1: Sarita V. Adve , Mark D. Hill , Barton P. Miller , Robert H. B. Netzer, Detecting data races on weak memory systems, Proceedings of the 18th annual international symposium on Computer architecture, p.234-243, May 27-30, 1991, Toronto, Ontario, Canada
• 2: Rahul Agarwal , Amit Sasturkar , Liqiang Wang , Scott D. Stoller, Optimized run-time race detection and atomicity checking using partial discovered types, Proceedings of the 20th IEEE/ACM international Conference on Automated software engineering, November 07-11, 2005, Long Beach, CA, USA [doi>10.1145/1101908.1101944]
• 3: Alexander Aiken , David Gay, Barrier inference, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.342-354, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268974]
• 4: David F. Bacon , Robert E. Strom , Ashis Tarafdar, Guava: a dialect of Java without data races, Proceedings of the 15th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.382-400, October 2000, Minneapolis, Minnesota, United States
• 5: Chandrasekhar Boyapati , Martin Rinard, A parameterized type system for race-free Java programs, Proceedings of the 16th ACM SIGPLAN conference on Object oriented programming, systems, languages, and applications, p.56-69, October 14-18, 2001, Tampa Bay, FL, USA
• 6: D. Bruening. Systematic testing of multithreaded Java programs. Master's thesis, MIT, 1999.
• 7: Sebastian Burckhardt , Rajeev Alur , Milo M. K. Martin, CheckFence: checking consistency of concurrent data types on relaxed memory models, Proceedings of the 2007 ACM SIGPLAN conference on Programming language design and implementation, June 10-13, 2007, San Diego, California, USA
• 8: 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.
• 9: Jong-Deok Choi , Keunwoo Lee , Alexey Loginov , Robert O'Callahan , Vivek Sarkar , Manu Sridharan, Efficient and precise datarace detection for multithreaded object-oriented programs, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 10: Jong-Deok Choi , Barton P. Miller , Robert H. B. Netzer, Techniques for debugging parallel programs with flowback analysis, ACM Transactions on Programming Languages and Systems (TOPLAS), v.13 n.4, p.491-530, Oct. 1991 [doi>10.1145/115372.115324]
• 11: Anne Dinning , Edith Schonberg, Detecting access anomalies in programs with critical sections, Proceedings of the 1991 ACM/ONR workshop on Parallel and distributed debugging, p.85-96, May 20-21, 1991, Santa Cruz, California, United States
• 12: Matthew B. Dwyer , Sebastian Elbaum , Suzette Person , Rahul Purandare, Parallel Randomized State-Space Search, Proceedings of the 29th international conference on Software Engineering, p.3-12, May 20-26, 2007 [doi>10.1109/ICSE.2007.62]
• 13: Matthew B. Dwyer , John Hatcliff , Robby , Venkatesh Prasad Ranganath, Exploiting Object Escape and Locking Information in Partial-Order Reductions for Concurrent Object-Oriented Programs, Formal Methods in System Design, v.25 n.2-3, p.199-240, September-November 2004 [doi>10.1023/B:FORM.0000040028.49845.67]
• 14: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 15: O. Edelstein, E. Farchi, Y. Nir, G. Ratsaby, and S. Ur. Multithreaded Java program test generation. IBM Systems Journal, 41(1):111--125, 2002.
• 16: Dawson Engler , Ken Ashcraft, RacerX: effective, static detection of race conditions and deadlocks, Proceedings of the nineteenth ACM symposium on Operating systems principles, October 19-22, 2003, Bolton Landing, NY, USA
• 17: 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.
• 18: C. Flanagan. Verifying commit-atomicity using model-checking. In 11th International SPIN Workshop, pages 252--266, 2004.
• 19: Cormac Flanagan , Stephen N. Freund, Type-based race detection for Java, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.219-232, June 18-21, 2000, Vancouver, British Columbia, Canada
• 20: Cormac Flanagan , Stephen N. Freund, Detecting race conditions in large programs, Proceedings of the 2001 ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, p.90-96, June 2001, Snowbird, Utah, United States [doi>10.1145/379605.379687]
• 21: Cormac Flanagan , Stephen N Freund, Atomizer: a dynamic atomicity checker for multithreaded programs, Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.256-267, January 14-16, 2004, Venice, Italy
• 22: Cormac Flanagan , Stephen N. Freund , Jaeheon Yi, Velodrome: a sound and complete dynamic atomicity checker for multithreaded programs, Proceedings of the 2008 ACM SIGPLAN conference on Programming language design and implementation, June 07-13, 2008, Tucson, AZ, USA
• 23: Cormac Flanagan , Shaz Qadeer, A type and effect system for atomicity, Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, June 09-11, 2003, San Diego, California, USA
• 24: S. N. Freund and S. Qadeer. Checking concise specifications for multithreaded software. Journal of Object Technology, 3(6):81--101, 2004.
• 25: David Gay , Philip Levis , Robert von Behren , Matt Welsh , Eric Brewer , David Culler, The nesC language: A holistic approach to networked embedded systems, Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, June 09-11, 2003, San Diego, California, USA
• 26: Patrice Godefroid, Model checking for programming languages using VeriSoft, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.174-186, January 15-17, 1997, Paris, France [doi>10.1145/263699.263717]
• 27: 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.
• 28: 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.
• 29: 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.
• 30: Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar, Race checking by context inference, ACM SIGPLAN Notices, v.39 n.6, May 2004
• 31: Gerard J. Holzmann, The Model Checker SPIN, IEEE Transactions on Software Engineering, v.23 n.5, p.279-295, May 1997 [doi>10.1109/32.588521]
• 32: Richard J. Lipton, Reduction: a method of proving properties of parallel programs, Communications of the ACM, v.18 n.12, p.717-721, Dec. 1975 [doi>10.1145/361227.361234]
• 33: Madanlal Musuvathi , Shaz Qadeer, Iterative context bounding for systematic testing of multithreaded programs, Proceedings of the 2007 ACM SIGPLAN conference on Programming language design and implementation, June 10-13, 2007, San Diego, California, USA
• 34: Mayur Naik , Alex Aiken , John Whaley, Effective static race detection for Java, Proceedings of the 2006 ACM SIGPLAN conference on Programming language design and implementation, June 11-14, 2006, Ottawa, Ontario, Canada
• 35: Satish Narayanasamy , Zhenghao Wang , Jordan Tigani , Andrew Edwards , Brad Calder, Automatically classifying benign and harmful data racesallusing replay analysis, Proceedings of the 2007 ACM SIGPLAN conference on Programming language design and implementation, June 10-13, 2007, San Diego, California, USA
• 36: Polyvios Pratikakis , Jeffrey S. Foster , Michael Hicks, LOCKSMITH: context-sensitive correlation analysis for race detection, Proceedings of the 2006 ACM SIGPLAN conference on Programming language design and implementation, June 11-14, 2006, Ottawa, Ontario, Canada
• 37: Shaz Qadeer , Dinghao Wu, KISS: keep it simple and sequential, Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation, June 09-11, 2004, Washington DC, USA
• 38: Stefan Savage , Michael Burrows , Greg Nelson , Patrick Sobalvarro , Thomas Anderson, Eraser: a dynamic data race detector for multithreaded programs, ACM Transactions on Computer Systems (TOCS), v.15 n.4, p.391-411, Nov. 1997 [doi>10.1145/265924.265927]
• 39: Koushik Sen, Effective random testing of concurrent programs, Proceedings of the twenty-second IEEE/ACM international conference on Automated software engineering, November 05-09, 2007, Atlanta, Georgia, USA [doi>10.1145/1321631.1321679]
• 40: Koushik Sen, Race directed random testing of concurrent programs, Proceedings of the 2008 ACM SIGPLAN conference on Programming language design and implementation, June 07-13, 2008, Tucson, AZ, USA
• 41: 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.
• 42: Stephen F. Siegel , Anastasia Mironova , George S. Avrunin , Lori A. Clarke, Using model checking with symbolic execution to verify parallel numerical programs, Proceedings of the 2006 international symposium on Software testing and analysis, July 17-20, 2006, Portland, Maine, USA [doi>10.1145/1146238.1146256]
• 43: N. Sterling. Warlock: A static data race analysis tool. In USENIX Winter Technical Conference, pages 97--106, 1993.
• 44: S. D. Stoller. Testing concurrent Java programs using randomized scheduling. In Workshop on Runtime Verification (RV'02), volume 70 of ENTCS, 2002.
• 45: 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.
• 46: Willem Visser , Klaus Havelund , Guillaume Brat , SeungJoon Park, Model Checking Programs, Proceedings of the 15th IEEE international conference on Automated software engineering, p.3, September 11-15, 2000
• 47: Christoph von Praun , Thomas R. Gross, Object race detection, Proceedings of the 16th ACM SIGPLAN conference on Object oriented programming, systems, languages, and applications, p.70-82, October 14-18, 2001, Tampa Bay, FL, USA
• 48: 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.
• 49: Liqiang Wang , Scott D. Stoller, Accurate and efficient runtime detection of atomicity errors in concurrent programs, Proceedings of the eleventh ACM SIGPLAN symposium on Principles and practice of parallel programming, March 29-31, 2006, New York, New York, USA [doi>10.1145/1122971.1122993]

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.5 Testing and Debugging

General Terms:
Algorithms, Languages, Verification

Keywords:
atomicity violation detection, concurrency, dynamic analysis, random testing