Parallel test generation and execution with Korat

ABSTRACT

We present novel algorithms for parallel testing of code that takes structurally complex test inputs. The algorithms build on the Korat algorithm for constraint-based generation of structurally complex test inputs. Given an imperative predicate that specifies the desired structural constraints and a finitization that bounds the desired input size, Korat performs a systematic search to generate all test inputs (within the bounds) that satisfy the constraints. We present how to generate test inputs with a parallel search in Korat and how to execute test inputs in parallel, both off-line (when the inputs are saved on disk) and on-line (when execution immediately follows generation).

The inputs that Korat generates enable bounded-exhaustive testing that checks the code under test exhaustively for all inputs within the given bounds. We also describe a novel methodology for reducing the number of equivalent inputs that Korat can generate. Our development of parallel Korat and the methodology for reducing equivalent inputs are motivated by testing an application developed at Google. The experimental results on running parallel Korat across up to 1024 machines on the Google's infrastructure show that parallel test generation and execution can achieve significant speedup, up to 543.55 times.

REFERENCES

• 1: Fadi A. Aloul , Arathi Ramani , Igor L. Markov , Karem A. Sakallah, Solving difficult SAT instances in the presence of symmetry, Proceedings of the 39th conference on Design automation, June 10-14, 2002, New Orleans, Louisiana, USA [doi>10.1145/513918.514102]
• 2: J. Barnat, L. Brim, and J. Chaloupka. Parallel breadth-first search ltl model-checking. In Proc. of the 18th IEEE International Conference on Automated Software Engineering, 2003.
• 3: Boris Beizer, Software Testing Techniques, John Wiley & Sons, Inc., New York, NY, 1990
• 4: Chandrasekhar Boyapati , Sarfraz Khurshid , Darko Marinov, Korat: automated testing based on Java predicates, Proceedings of the 2002 ACM SIGSOFT international symposium on Software testing and analysis, July 22-24, 2002, Roma, Italy
• 5: L. A. Clarke, A System to Generate Test Data and Symbolically Execute Programs, IEEE Transactions on Software Engineering, v.2 n.3, p.215-222, May 1976 [doi>10.1109/TSE.1976.233817]
• 6: J. Crawford, M. Ginsberg, E. Luks, and A. Roy. Symmetry-breaking predicates for search problems. In Proc. Fifth International Conference on Principles of Knowledge Representation and Reasoning, 1996.
• 7: Jeffrey Dean , Sanjay Ghemawat, MapReduce: simplified data processing on large clusters, Proceedings of the 6th conference on Symposium on Opearting Systems Design & Implementation, p.10-10, December 06-08, 2004, San Francisco, CA
• 8: 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]
• 9: Sanjay Ghemawat , Howard Gobioff , Shun-Tak Leung, The Google file system, Proceedings of the nineteenth ACM symposium on Operating systems principles, October 19-22, 2003, Bolton Landing, NY, USA
• 10: Arnaud Gotlieb , Bernard Botella , Michel Rueher, Automatic test data generation using constraint solving techniques, Proceedings of the 1998 ACM SIGSOFT international symposium on Software testing and analysis, p.53-62, March 02-04, 1998, Clearwater Beach, Florida, United States
• 11: Ananth Grama , Vipin Kumar, State of the Art in Parallel Search Techniques for Discrete Optimization Problems, IEEE Transactions on Knowledge and Data Engineering, v.11 n.1, p.28-35, January 1999 [doi>10.1109/69.755612]
• 12: 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]
• 13: J. C. Huang, An Approach to Program Testing, ACM Computing Surveys (CSUR), v.7 n.3, p.113-128, Sept. 1975 [doi>10.1145/356651.356652]
• 14: Radu Iosif, Exploiting Heap Symmetries in Explicit-State Model Checking of Software, Proceedings of the 16th IEEE international conference on Automated software engineering, p.254, November 26-29, 2001
• 15: Daniel Jackson, Software Abstractions: Logic, Language, and Analysis, The MIT Press, 2006
• 16: V. K. Janakiram , D. P. Agrawal , R. Mehrotra, A Randomized Parallel Backtracking Algorithm, IEEE Transactions on Computers, v.37 n.12, p.1665-1676, December 1988 [doi>10.1109/12.9745]
• 17: Michael D. Jones , Jacob Sorber, Parallel search for LTL violations, International Journal on Software Tools for Technology Transfer (STTT), v.7 n.1, p.31-42, February 2005 [doi>10.1007/s10009-003-0115-8]
• 18: Richard M. Karp , Yanjun Zhang, Randomized parallel algorithms for backtrack search and branch-and-bound computation, Journal of the ACM (JACM), v.40 n.3, p.765-789, July 1993 [doi>10.1145/174130.174145]
• 19: Sarfraz Khurshid , Daniel Jackson, Generating structurally complex tests from declarative constraints, Massachusetts Institute of Technology, 2004
• 20: S. Khurshid and D. Marinov. Checking Java implementation of a naming architecture using TestEra. In S. D. Stoller and W. Visser, editors, Electronic Notes in Theoretical Computer Science (ENTCS), volume 55. Elsevier Science Publishers, 2001.
• 21: Sarfraz Khurshid , Darko Marinov, TestEra: Specification-Based Testing of Java Programs Using SAT, Automated Software Engineering, v.11 n.4, p.403-434, October 2004 [doi>10.1023/B:AUSE.0000038938.10589.b9]
• 22: S. Khurshid, D. Marinov, I. Shlyakhter, and D. Jackson. A case for efficient solution enumeration. In Proc. of the Sixth International Conference on Theory and Applications of Satisfiability Testing (SAT 2003), Santa Margherita Ligure, Italy, May 2003.
• 23: James C. King, Symbolic execution and program testing, Communications of the ACM, v.19 n.7, p.385-394, July 1976 [doi>10.1145/360248.360252]
• 24: Bogdan Korel, Automated test data generation for programs with procedures, Proceedings of the 1996 ACM SIGSOFT international symposium on Software testing and analysis, p.209-215, January 08-10, 1996, San Diego, California, United States
• 25: R. Kumar and E. G. Mercer. Load balancing parallel explicit state model checking. Electr. Notes Theor. Comput. Sci., 128(3):19--34, 2005.
• 26: Flavio Lerda , Riccardo Sisto, Distributed-Memory Model Checking with SPIN, Proceedings of the 5th and 6th International SPIN Workshops on Theoretical and Practical Aspects of SPIN Model Checking, p.22-39, September 21-24, 1999
• 27: Flavio Lerda , Willem Visser, Addressing dynamic issues of program model checking, Proceedings of the 8th international SPIN workshop on Model checking of software, p.80-102, May 2001, Toronto, Ontario, Canada
• 28: Barbara Liskov , John Guttag, Program Development in Java: Abstraction, Specification, and Object-Oriented Design, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 2000
• 29: Darko Marinov , Martin C. Rinard, Automatic testing of software with structurally complex inputs, Massachusetts Institute of Technology, Cambridge, MA, 2005
• 30: D. Marinov, A. Andoni, D. Daniliuc, S. Khurshid, and M. Rinard. An evaluation of exhaustive testing for data structures. Technical Report MIT-LCS-TR-921, MIT Computer Science and Artificial Intelligence Lab, Cambridge, MA, Sept. 2003.
• 31: B. D. McKay. Practical graph isomorphism. Congressus Numerantium, 1(30):45--87, 1981. http://cs.anu.edu.au/~bdm/nauty/.
• 32: W. M. McKeeman. Differential testing for software. Digital Technical Journal, 10(1), 1998.
• 33: Aleksandar Milicevic , Sasa Misailovic , Darko Marinov , Sarfraz Khurshid, Korat: A Tool for Generating Structurally Complex Test Inputs, Proceedings of the 29th international conference on Software Engineering, p.771-774, May 20-26, 2007 [doi>10.1109/ICSE.2007.48]
• 34: S. Misailovic, A. Milicevic, S. Khurshid, and D. Marinov. Generating test inputs for fault-tree analyzers using imperative predicates. In the Workshop on Advances and Innovations in Systems Testing (STEP 2007), Memphis, TN, May 2007.
• 35: Robert Palmer , Ganesh Gopalakrishnan, A Distributed Partial Order Reduction Algorithm, Proceedings of the 22nd IFIP WG 6.1 International Conference Houston on Formal Techniques for Networked and Distributed Systems, p.370, November 11-14, 2002
• 36: C. V. Ramamoorthy , S. -B. F. Ho , W. T. Chen, On the Automated Generation of Program Test Data, IEEE Transactions on Software Engineering, v.2 n.4, p.293-300, July 1976 [doi>10.1109/TSE.1976.233835]
• 37: N. J. A. Sloane, S. Plouffe, J. M. Borwein, and R. M. Corless. The encyclopedia of integer sequences. SIAM Review, 38(2), 1996. http://www.research.att.com/~njas/sequences/Seis.html.
• 38: Ulrich Stern , David L. Dill, Parallelizing the Murphi Verifier, Proceedings of the 9th International Conference on Computer Aided Verification, p.256-278, June 22-25, 1997
• 39: Ulrich Stern , David L. Dill, Parallelizing the Murϕ Verifier, Formal Methods in System Design, v.18 n.2, p.117-129, March 1, 2001 [doi>10.1023/A:1008771324652]
• 40: K. Stobie. Advanced modeling, model based test generation, and Abstract state machine Language (AsmL). Seattle Area Software Quality Assurance Group, http://www.sasqag.org/pastmeetings/asml.ppt, Jan. 2003.
• 41: Kevin Sullivan , Jinlin Yang , David Coppit , Sarfraz Khurshid , Daniel Jackson, Software assurance by bounded exhaustive testing, Proceedings of the 2004 ACM SIGSOFT international symposium on Software testing and analysis, July 11-14, 2004, Boston, Massachusetts, USA
• 42: R. Tarjan. Depth-first search and linear graph algorithms. SIAM Journal on Computing, 1(2):146--160, 1972.
• 43: Margus Veanes , Colin Campbell , Wolfram Schulte , Nikolai Tillmann, Online testing with model programs, Proceedings of the 10th European software engineering conference held jointly with 13th ACM SIGSOFT international symposium on Foundations of software engineering, September 05-09, 2005, Lisbon, Portugal
• 44: 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
• 45: E. J. Weyuker , T. J. Ostrand, Theories of Program Testing and the Application of Revealing Subdomains, IEEE Transactions on Software Engineering, v.6 n.3, p.236-246, May 1980 [doi>10.1109/TSE.1980.234485]
• 46: Tao Xie , Darko Marinov , David Notkin, Rostra: A Framework for Detecting Redundant Object-Oriented Unit Tests, Proceedings of the 19th IEEE international conference on Automated software engineering, p.196-205, September 20-24, 2004 [doi>10.1109/ASE.2004.61]

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)

Additional Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
      D.1.3 Concurrent Programming
          Subjects: Parallel programming

General Terms:
Algorithms, Performance, Reliability

Keywords:
Korat, bounded-exhaustive testing, parallel testing, test data generation