A randomized dynamic program analysis technique for detecting real deadlocks

ABSTRACT

We present a novel dynamic analysis technique that finds real deadlocks in multi-threaded programs. Our technique runs in two stages. In the first stage, we use an imprecise dynamic analysis technique to find potential deadlocks in a multi-threaded program by observing an execution of the program. In the second stage, we control a random thread scheduler to create the potential deadlocks with high probability. Unlike other dynamic analysis techniques, our approach has the advantage that it does not give any false warnings. We have implemented the technique in a prototype tool for Java, and have experimented on a number of large multi-threaded Java programs. We report a number of previously known and unknown real deadlocks that were found in these benchmarks.

REFERENCES

• 1: R. Agarwal, L. Wang, and S. D. Stoller. Detecting potential deadlocks with static analysis and runtime monitoring. In Parallel and Distributed Systems: Testing and Debugging 2005, 2005.
• 2: Cyrille Artho , Armin Biere, Applying Static Analysis to Large-Scale, Multi-Threaded Java Programs, Proceedings of the 13th Australian Conference on Software Engineering, p.68, August 27-28, 2001
• 3: Saddek Bensalem , Jean-Claude Fernandez , Klaus Havelund , Laurent Mounier, Confirmation of deadlock potentials detected by runtime analysis, Proceedings of the 2006 workshop on Parallel and distributed systems: testing and debugging, July 17-17, 2006, Portland, Maine, USA [doi>10.1145/1147403.1147412]
• 4: S. Bensalem and K. Havelund. Scalable dynamic deadlock analysis of multi-threaded programs. In Parallel and Distributed Systems: Testing and Debugging 2005 (PADTAD'05), 2005.
• 5: Chandrasekhar Boyapati , Robert Lee , Martin Rinard, Ownership types for safe programming: preventing data races and deadlocks, Proceedings of the 17th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, November 04-08, 2002, Seattle, Washington, USA
• 6: S. Chaki, E. Clarke, J. Ouaknine, N. Sharygina, and N. Sinha. Concurrent software verification with states, events, and deadlocks. Formal Aspects of Computing, 17(4):461--483, 2005.
• 7: Claudio DeMartini , Radu Iosif , Riccardo Sisto, A deadlock detection tool for concurrent Java programs, Software—Practice & Experience, v.29 n.7, p.577-603, June 1999 [doi>10.1002/(SICI)1097-024X(199906)29:7<577::AID-SPE246>3.0.CO;2-V]
• 8: O. Edelstein, E. Farchi, Y. Nir, G. Ratsaby, , and S. Ur. Multithreaded Java program test generation. IBM Systems Journal, 41(1):111--125, 2002.
• 9: 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
• 10: Cormac Flanagan , K. Rustan M. Leino , Mark Lillibridge , Greg Nelson , James B. Saxe , Raymie Stata, Extended static checking for Java, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 11: 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]
• 12: Jerry J. Harrow, Runtime Checking of Multithreaded Applications with Visual Threads, Proceedings of the 7th International SPIN Workshop on SPIN Model Checking and Software Verification, p.331-342, August 30-September 01, 2000
• 13: Klaus Havelund, Using Runtime Analysis to Guide Model Checking of Java Programs, Proceedings of the 7th International SPIN Workshop on SPIN Model Checking and Software Verification, p.245-264, August 30-September 01, 2000
• 14: 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.
• 15: 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]
• 16: P. Joshi, M. Naik, C.-S. Park, and K. Sen. An extensible active testing framework for concurrent programs. In 21st International Conference on Computer Aided Verification (CAV'09), Lecture Notes in Computer Science. Springer, 2009.
• 17: H. Jula, D. Tralamazza, C. Zamfir, and G. Candea. Deadlock immunity: Enabling systems to defend against deadlocks. In Proceedings of the 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI'08), 2008.
• 18: 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]
• 19: Stephen P. Masticola, Static detection of deadlocks in polynomial time, Rutgers University, New Brunswick, NJ, 1993
• 20: Ana Milanova , Atanas Rountev , Barbara G. Ryder, Parameterized object sensitivity for points-to analysis for Java, ACM Transactions on Software Engineering and Methodology (TOSEM), v.14 n.1, p.1-41, January 2005 [doi>10.1145/1044834.1044835]
• 21: Mayur Naik , Chang-Seo Park , Koushik Sen , David Gay, Effective static deadlock detection, Proceedings of the 2009 IEEE 31st International Conference on Software Engineering, p.386-396, May 16-24, 2009 [doi>10.1109/ICSE.2009.5070538]
• 22: Yarden Nir-Buchbinder , Rachel Tzoref , Shmuel Ur, Deadlocks: From Exhibiting to Healing, Runtime Verification: 8th International Workshop, RV 2008, Budapest, Hungary, March 30, 2008. Selected Papers, Springer-Verlag, Berlin, Heidelberg, 2008 [doi>10.1007/978-3-540-89247-2_7]
• 23: Chang-Seo Park , Koushik Sen, Randomized active atomicity violation detection in concurrent programs, Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of software engineering, November 09-14, 2008, Atlanta, Georgia [doi>10.1145/1453101.1453121]
• 24: Feng Qin , Joseph Tucek , Jagadeesan Sundaresan , Yuanyuan Zhou, Rx: treating bugs as allergies---a safe method to survive software failures, Proceedings of the twentieth ACM symposium on Operating systems principles, October 23-26, 2005, Brighton, United Kingdom
• 25: 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
• 26: S. D. Stoller. Testing concurrent Java programs using randomized scheduling. In Workshop on Runtime Verification (RV'02), volume 70 of ENTCS, 2002.
• 27: C. von Praun. Detecting Synchronization Defects in Multi-Threaded Object-Oriented Programs. PhD thesis, Swiss Federal Institute of Technology, Zurich, 2004.
• 28: 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
• 29: A. Williams, W. Thies, and M. Ernst. Static deadlock detection for Java libraries. In ECOOP 2005 -- 19th European Conference on Object--Oriented Programming (ECOOP'05), pages 602--629, 2005.
• 30: Bin Xin , William N. Sumner , Xiangyu Zhang, Efficient program execution indexing, Proceedings of the 2008 ACM SIGPLAN conference on Programming language design and implementation, June 07-13, 2008, Tucson, AZ, USA

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.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Model checking
      D.2.5 Testing and Debugging
          Subjects: Debugging aids; Monitors

General Terms:
Languages, Reliability, Verification

Keywords:
active testing, concurrency, deadlock detection, dynamic program analysis