Towards a better collaboration of static and dynamic analyses for testing concurrent programs

ABSTRACT

Testing concurrent programs remains a difficult task due to the non-deterministic nature of concurrent executions. Many approaches have been proposed to combine static and dynamic analysis to reduce the complexity of uncovering potential concurrency bugs. However, the existing collaboration schemes only provide a limited mechanism for exchanging relevant information between the two analyses. For example, alias information only flows from the static analysis module to the dynamic analysis module at the beginning of the dynamic analysis. Therefore, we cannot fully exploit the advantages of each type of analysis. Motivated by this observation, in this paper we present a new testing technique which enables a tighter collaboration between static analysis and dynamic analysis. In this collaboration scheme, static analysis and dynamic analysis interact iteratively throughout the whole testing process. Static analysis uses coarse-grained analysis to guide the dynamic analysis to concentrate on the relevant search space, while dynamic analysis collects concrete runtime information during the guided exploration. The runtime information provided by the dynamic analysis helps the static analysis to refine its coarse-grained analysis and provides better guidance on dynamic analysis. Currently, our implementation consists of a static analysis module based on Soot and a dynamic analysis module based on JPF (Java PathFinder).

REFERENCES

• 1: Martin Abadi , Cormac Flanagan , Stephen N. Freund, Types for safe locking: Static race detection for Java, ACM Transactions on Programming Languages and Systems (TOPLAS), v.28 n.2, p.207-255, March 2006 [doi>10.1145/1119479.1119480]
• 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: Marina Biberstein , Eitan Farchi , Shmuel Ur, Choosing among Alternative Pasts, Proceedings of the 17th International Symposium on Parallel and Distributed Processing, p.289.1, April 22-26, 2003
• 4: M. Biberstein, E. Farchi, and S. Ur. Fidgeting to the point of no return. In Proc. 18th International Parallel and Distributed Processing Symposium, page 266b, 2004.
• 5: Guillaume Brat , Willem Visser, Combining Static Analysis and Model Checking for Software Analysis, Proceedings of the 16th IEEE international conference on Automated software engineering, p.262, November 26-29, 2001
• 6: Jun Chen , Steve MacDonald, Testing concurrent programs using value schedules, Proceedings of the twenty-second IEEE/ACM international conference on Automated software engineering, November 05-09, 2007, Atlanta, Georgia, USA [doi>10.1145/1321631.1321678]
• 7: J. Chen and S. MacDonald. Incremental testing of concurrent programs using value schedules. Submitted to 23rd IEEE/ACM International Conference on Automated Software Engineering, 2008.
• 8: S. Copty and S. Ur. Multi-threaded testing with AOP is easy, and it finds bugs!. In Proc. 11th International Euro-Par Conference, volume 3648 of Lecture Notes in Computer Science, pages 740--749. Springer-Verlag, 2005.
• 9: Bruno Dufour , Barbara G. Ryder , Gary Sevitsky, Blended analysis for performance understanding of framework-based applications, Proceedings of the 2007 international symposium on Software testing and analysis, July 09-12, 2007, London, United Kingdom [doi>10.1145/1273463.1273480]
• 10: 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
• 11: Yaniv Eytani , Klaus Havelund , Scott D. Stoller , Shmuel Ur, Towards a framework and a benchmark for testing tools for multi-threaded programs: Research Articles, Concurrency and Computation: Practice & Experience, v.19 n.3, p.267-279, March 2007 [doi>10.1002/cpe.v19:3]
• 12: 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]
• 13: S. MacDonald, J. Chen, and D. Novillo. Choosing among alternative futures. In Haifa Verification Conference, volume 3875 of Lecture Notes in Computer Science, pages 247--264. Springer-Verlag, 2005.
• 14: Mayur Naik , Alex Aiken, Conditional must not aliasing for static race detection, Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 17-19, 2007, Nice, France
• 15: 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
• 16: Robert O'Callahan , Jong-Deok Choi, Hybrid dynamic data race detection, Proceedings of the ninth ACM SIGPLAN symposium on Principles and practice of parallel programming, June 11-13, 2003, San Diego, California, USA
• 17: G. Ramalingam, Context-sensitive synchronization-sensitive analysis is undecidable, ACM Transactions on Programming Languages and Systems (TOPLAS), v.22 n.2, p.416-430, March 2000 [doi>10.1145/349214.349241]
• 18: Stefan Savage , Michael Burrows , Greg Nelson , Patrick Sobalvarro , Thomas Anderson, Eraser: a dynamic data race detector for multi-threaded programs, Proceedings of the sixteenth ACM symposium on Operating systems principles, p.27-37, October 05-08, 1997, Saint Malo, France
• 19: R. N. Taylor. Complexity of analyzing the synchronization structure of concurrent programs. Acta Informatica, 19(1):57--84, 1983.
• 20: 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
• 21: Willem Visser , Klaus Havelund , Guillaume Brat , Seungjoon Park , Flavio Lerda, Model Checking Programs, Automated Software Engineering, v.10 n.2, p.203-232, April 2003 [doi>10.1023/A:1022920129859]
• 22: Yuan Yu , Tom Rodeheffer , Wei Chen, RaceTrack: efficient detection of data race conditions via adaptive tracking, Proceedings of the twentieth ACM symposium on Operating systems principles, October 23-26, 2005, Brighton, United Kingdom

INDEX TERMS

Primary Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
      D.1.3 Concurrent Programming

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

General Terms:
Languages, Reliability, Verification