Effective random testing of concurrent programs

ABSTRACT

Multithreaded concurrent programs often exhibit wrong behaviors due to unintended interferences among the concurrent threads. Such errors are often hard to find because they typically manifest under very specific thread schedules. Traditional testing, which pays no attention to thread schedules and non-deterministically exercises a few arbitrary schedules, often misses such bugs. Traditional model checking techniques, which try to systematically explore all thread schedules, give very high confidence in the correctness of the system, but, unfortunately, they suffer from the state explosion problem. Recently, dynamic partial order techniques have been proposed to alleviate the problem. However, such techniques fail for large programs because the state space remains large in spite of reduction. An inexpensive and a simple alternative approach is to perform random testing by choosing thread schedules at random. We show that such a naive approach often explores some states with very high probability compared to the others. We propose a random partial order sampling algorithm (or RAPOS) that partly removes this non-uniformity in sampling the state space. We empirically compare the proposed algorithm with the simple random testing algorithm and show that the former outperforms the latter

REFERENCES

• 1: David L Bird , Carlos Urias Munoz, Automatic generation of random self-checking test cases, IBM Systems Journal, v.22 n.3, p.229-245, 1983
• 2: D. Bruening. Systematic testing of multithreaded Java programs. Master's thesis, MIT, 1999.
• 3: 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.
• 4: Koen Claessen , John Hughes, QuickCheck: a lightweight tool for random testing of Haskell programs, Proceedings of the fifth ACM SIGPLAN international conference on Functional programming, p.268-279, September 2000
• 5: Christoph Csallner , Yannis Smaragdakis, JCrasher: an automatic robustness tester for Java, Software—Practice & Experience, v.34 n.11, p.1025-1050, September 2004 [doi>10.1002/spe.602]
• 6: Marcelo d'Amorim , Carlos Pacheco , Tao Xie , Darko Marinov , Michael D. Ernst, An Empirical Comparison of Automated Generation and Classification Techniques for Object-Oriented Unit Testing, Proceedings of the 21st IEEE/ACM International Conference on Automated Software Engineering, p.59-68, September 18-22, 2006 [doi>10.1109/ASE.2006.13]
• 7: 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]
• 8: 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]
• 9: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 10: O. Edelstein, E. Farchi, Y. Nir, G. Ratsaby,, and S. Ur. Multithreaded Java program test generation. IBM Systems Journal, 41(1):111--125, 2002.
• 11: Cormac Flanagan , Patrice Godefroid, Dynamic partial-order reduction for model checking software, Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.110-121, January 12-14, 2005, Long Beach, California, USA
• 12: Justin E. Forrester , Barton P. Miller, An empirical study of the robustness of Windows NT applications using random testing, Proceedings of the 4th conference on USENIX Windows Systems Symposium, p.6-6, August 03-04, 2000, Seattle, Washington
• 13: Patrice Godefroid , J. van Leeuwen , J. Hartmanis , G. Goos , Pierre Wolper, Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem, Springer-Verlag New York, Inc., Secaucus, NJ, 1996
• 14: 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]
• 15: 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.
• 16: 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.
• 17: 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]
• 18: Yong Lei , James H. Andrews, Minimization of Randomized Unit Test Cases, Proceedings of the 16th IEEE International Symposium on Software Reliability Engineering, p.267-276, November 08-11, 2005 [doi>10.1109/ISSRE.2005.28]
• 19: Rupak Majumdar , Koushik Sen, Hybrid Concolic Testing, Proceedings of the 29th international conference on Software Engineering, p.416-426, May 20-26, 2007 [doi>10.1109/ICSE.2007.41]
• 20: Antoni W. Mazurkiewicz, Trace Theory, Proceedings of an Advanced Course on Petri Nets: Central Models and Their Properties, Advances in Petri Nets 1986-Part II, p.279-324, September 08-19, 1986
• 21: 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
• 22: A. Jefferson Offutt , J. Huffman Hayes, A semantic model of program faults, Proceedings of the 1996 ACM SIGSOFT international symposium on Software testing and analysis, p.195-200, January 08-10, 1996, San Diego, California, United States
• 23: C. Pacheco and M. D. Ernst. Eclat: Automatic generation and classification of test inputs. In ECOOP 05: European Conference Object-Oriented Programming, LNCS 3586, pages 504--527, 2005.
• 24: Carlos Pacheco , Shuvendu K. Lahiri , Michael D. Ernst , Thomas Ball, Feedback-Directed Random Test Generation, Proceedings of the 29th international conference on Software Engineering, p.75-84, May 20-26, 2007 [doi>10.1109/ICSE.2007.37]
• 25: Doron Peled, All from One, One for All: on Model Checking Using Representatives, Proceedings of the 5th International Conference on Computer Aided Verification, p.409-423, June 28-July 01, 1993
• 26: 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.
• 27: K. Sen, M. Viswanathan, and G. Agha. Statistical model checking of black-box probabilistic systems. In 16th International Conference on Computer Aided Verification (CAV'04), volume 3114 of LNCS, pages 202--215, 2004.
• 28: 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]
• 29: S. D. Stoller. Testing concurrent Java programs using randomized scheduling. In Workshop on Runtime Verification (RV'02), volume 70 of ENTCS, 2002.
• 30: Raja Vallée-Rai , Phong Co , Etienne Gagnon , Laurie Hendren , Patrick Lam , Vijay Sundaresan, Soot - a Java bytecode optimization framework, Proceedings of the 1999 conference of the Centre for Advanced Studies on Collaborative research, p.13, November 08-11, 1999, Mississauga, Ontario, Canada
• 31: Antti Valmari, Stubborn sets for reduced state space generation, Proceedings of the 10th International Conference on Applications and Theory of Petri Nets: Advances in Petri Nets 1990, p.491-515, June 01, 1989
• 32: 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
• 33: Håkan L. S. Younes , Reid G. Simmons, Probabilistic Verification of Discrete Event Systems Using Acceptance Sampling, Proceedings of the 14th International Conference on Computer Aided Verification, p.223-235, July 27-31, 2002

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.5 Testing and Debugging
          Subjects: Testing tools (e.g., data generators, coverage testing)

General Terms:
Reliability, Verification

Keywords:
concurrent programs, random testing