jPredictor: a predictive runtime analysis tool for java

ABSTRACT

jPredictor is a tool for detecting concurrency errors in Java programs. The Java program is instrumented to emit property-relevant events at runtime and then executed. The resulting execution trace is collected and analyzed by Predictor, which extracts a causality relation sliced using static analysis and refined with lock-atomicity information. The resulting abstract model, a hybrid of a partial order and atomic blocks, is then exhaustively analyzed against the property and errors with counter-examples are reported to the user. Thus, jPredictor can "predict" errors that did not happen in the observed execution, but which could have happened under a different thread scheduling. The analysis technique employed in jPredictor is fully automatic, generic (works for any trace property), sound (produces no false alarms) but it is incomplete may miss errors). Two common types of errors are investigated in this paper: dataraces and atomicity violations. Experiments show that jPredictor is precise (in its predictions), effective and efficient. After the code producing them was executed only once, jPredictor found all the errors reported by other tools. It also found errors missed by other tools, including static race detectors, as well as unknown errors in popular systems like Tomcat and the Apache FTP server.

REFERENCES

• 1: Hiralal Agrawal , Joseph R. Horgan, Dynamic program slicing, Proceedings of the ACM SIGPLAN 1990 conference on Programming language design and implementation, p.246-256, June 1990, White Plains, New York, United States
• 2: Apache Commons project. http://commons.apache.org/.
• 3: Apache FTP server project. incubator.apache.org/ftpserver/.
• 4: Graham Brightwell , Peter Winkler, Counting linear extensions is #P-complete, Proceedings of the twenty-third annual ACM symposium on Theory of computing, p.175-181, May 05-08, 1991, New Orleans, Louisiana, United States [doi>10.1145/103418.103441]
• 5: F. Chen and G. Rosu. Predicting concurrency errors at runtime using sliced causality. Technical Report UIUCDCS-R-2005-2660, Department of CS at UIUC, 2005.
• 6: Feng Chen , Grigore Roşu, Mop: an efficient and generic runtime verification framework, Proceedings of the 22nd annual ACM SIGPLAN conference on Object oriented programming systems and applications, October 21-25, 2007, Montreal, Quebec, Canada
• 7: F. Chen and G. Rosu. Parametric and Sliced Causality. In Computer Aided Verification (CAV'07), 2007.
• 8: F. Chen and G. Rosu. Parametric and termination-sensitive control dependence - extended abstract. In Static Analysis Symposium (SAS'06), 2006.
• 9: O. Edelstein, E. Farchi, Y. Nir, G. Ratsaby, and S. Ur. Multithreaded java program test generation. IBM Systems Journal, 41(1):111--125, 2002.
• 10: Eitan Farchi , Yarden Nir , Shmuel Ur, Concurrent Bug Patterns and How to Test Them, Proceedings of the 17th International Symposium on Parallel and Distributed Processing, p.286.2, April 22-26, 2003
• 11: A. Farzan and M. Parthasarathy. Causal atomicity. In Computer Aided Verification (CAV'06), 2006.
• 12: 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
• 13: John Hatcliff , James C. Corbett , Matthew B. Dwyer , Stefan Sokolowski , Hongjun Zheng, A Formal Study of Slicing for Multi-threaded Programs with JVM Concurrency Primitives, Proceedings of the 6th International Symposium on Static Analysis, p.1-18, September 22-24, 1999
• 14: Susan Horwitz , Thomas Reps, The use of program dependence graphs in software engineering, Proceedings of the 14th international conference on Software engineering, p.392-411, May 11-15, 1992, Melbourne, Australia [doi>10.1145/143062.143156]
• 15: Java. http://java.sun.com.
• 16: jPredictor. http://fsl.cs.uiuc.edu/jPredictor/.
• 17: Leslie Lamport, Time, clocks, and the ordering of events in a distributed system, Communications of the ACM, v.21 n.7, p.558-565, July 1978 [doi>10.1145/359545.359563]
• 18: 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
• 19: 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
• 20: 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]
• 21: A. Sen and V. K. Garg. Detecting temporal logic predicates in distributed programs using computation slicing. In International Conference on Principles of Distributed Systems (OPODIS'03), 2003.
• 22: Koushik Sen , Grigore Rosu , Gul Agha, Runtime safety analysis of multithreaded programs, Proceedings of the 9th European software engineering conference held jointly with 11th ACM SIGSOFT international symposium on Foundations of software engineering, September 01-05, 2003, Helsinki, Finland
• 23: K. Sen, G. Rosu, and G. Agha. Detecting errors in multithreaded programs by generalized predictive analysis of executions. In Formal Methods for Open Object-Based Distributed Systems (FMOODS'05), 2005.
• 24: Soot website. http://www.sable.mcgill.ca/soot/.
• 25: Apache group. Tomcat. http://jakarta.apache.org/tomcat/.
• 26: Mandana Vaziri , Frank Tip , Julian Dolby, Associating synchronization constraints with data in an object-oriented language, Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.334-345, January 11-13, 2006, Charleston, South Carolina, USA
• 27: 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
• 28: 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, Verification

Keywords:
predictive runtime analysis, runtime verification, sliced causality