An empirical evaluation of three methods for deadlock analysis of Ada tasking programs

ABSTRACT

Static analysis of Ada tasking programs has been hindered by the well known state explosion problem that arises in the verification of concurrent systems. Many different techniques have been proposed to combat this state explosion. All proposed methods excel on certain kinds of systems, but there is little empirical data comparing the performance of the methods. In this paper, we select one representative from each of three very different approaches to the state explosion problem: partial-orders (representing state-space reductions), symbolic model checking (representing OBDD-based approaches), and inequality necessary conditions (representing integer programming-based approaches). We apply the methods to several scalable concurrency examples from the literature and to one real Ada tasking program. The results of these experiments are presented and their significance is discussed.

REFERENCES

• 1: George S. Avrunin , Ugo A. Buy , James C. Corbett , Laura K. Dillon , Jack C. Wileden, Automated Analysis of Concurrent Systems with the Constrained Expression Toolset, IEEE Transactions on Software Engineering, v.17 n.11, p.1204-1222, November 1991 [doi>10.1109/32.106975]
• 2: Randal E. Bryant, Symbolic Boolean manipulation with ordered binary-decision diagrams, ACM Computing Surveys (CSUR), v.24 n.3, p.293-318, Sept. 1992 [doi>10.1145/136035.136043]
• 3: J. Burch, E. Clarke, K. McMillan, D. Dill, and L. Hwang. Symbolic model checking: 102o states and beyond. In Proceeain gs of the Fifth Annual IEEE Symposium on Logic in Computer Science, pages 428- 439, 1990.
• 4: Edmund M. Clarke , Orna Grumberg , David E. Long, Model checking and abstraction, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.343-354, January 19-22, 1992, Albuquerque, New Mexico, United States [doi>10.1145/143165.143235]
• 5: James C. Corbett, Verifying General Safety and Liveness Propterties with Integer Programming, Proceedings of the Fourth International Workshop on Computer Aided Verification, p.357-369, June 29-July 01, 1992
• 6: J. Corbett , G. Avrunin, A practical technique for bounding the time between events in concurrent real-time systems, Proceedings of the 1993 ACM SIGSOFT international symposium on Software testing and analysis, p.110-116, June 28-30, 1993, Cambridge, Massachusetts, United States
• 7: S. Duri , U. Buy , R. Devarapalli , S. M. Shatz, Using state space reduction methods for deadlock analysis in Ada tasking, Proceedings of the 1993 ACM SIGSOFT international symposium on Software testing and analysis, p.51-60, June 28-30, 1993, Cambridge, Massachusetts, United States
• 8: Patrice Godefroid , Didier Pirottin, Refining Dependencies Improves Partial-Order Verification Methods (Extended Abstract), Proceedings of the 5th International Conference on Computer Aided Verification, p.438-449, June 28-July 01, 1993
• 9: D. Helmbold and D. Luckham. Debugging Ada tasking programs. IEEE Software, 2(2):47-57, March 1985.
• 10: C. A. R. Hoare, Communicating sequential processes, Prentice-Hall, Inc., Upper Saddle River, NJ, 1985
• 11: Gerard J. Holzmann, Design and validation of computer protocols, Prentice-Hall, Inc., Upper Saddle River, NJ, 1990
• 12: G. M. Karam , R. J. A. Buhr, Starvation and Critical Race Analyzers for Ada, IEEE Transactions on Software Engineering, v.16 n.8, p.829-843, August 1990 [doi>10.1109/32.57622]
• 13: Douglas L. Long , Lori A. Clarke, Task interaction graphs for concurrency analysis, Proceedings of the 11th international conference on Software engineering, p.44-52, May 1989, Pittsburgh, Pennsylvania, United States [doi>10.1145/74587.74592]
• 14: S. P. Masficola and B. G. Ryder. Static infinite wait anomaly detection in polynomial time. In Proceedings of the 1990 International Conference on Parallel Processing, volume II, pages 78-87, 1990.
• 15: Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
• 16: Tadao Murata , Sol M. Shatz , Boris Shenker, Detection of Ada Static Deadlocks Using Petri Net Invariants, IEEE Transactions on Software Engineering, v.15 n.3, p.314-326, March 1989 [doi>10.1109/32.21759]
• 17: Leon Osterweil , Lori A. Clarke, A Proposed Testing and Analysis Research Initiative, IEEE Software, v.9 n.5, p.89-96, September 1992 [doi>10.1109/52.156901]
• 18: T. Ostrancl and E. Weyuker, editors. Proceedings of the 1993 International Symposium on Software Testing andAnalysis (ISSTA),New York,June 1993. ACM Press.
• 19: R. N. Taylor. Complexity of analyzing the synchronization structure of concurrent programs. Acta Informatica, 19:57-84, 1983.
• 20: W. Tichy, N. Habermann, and L. Prechelt. Summary of the Dagstuhl workshop on future directions in software engineering. ACM Sigsoft, Jan. 1993.
• 21: S. Tu, S. M. Shatz, and T. Murata. Theory and application of Petri net reduction for Aria-tasking deadlock analysis. Technical Report 91-15, EECS Department, University of illinois, Chicago, 1991.
• 22: Antti Valmari, A Stubborn Attack On State Explosion, Proceedings of the 2nd International Workshop on Computer Aided Verification, p.156-165, June 18-21, 1990
• 23: Wei Jen Yeh , Michal Young, Compositional reachability analysis using process algebra, Proceedings of the symposium on Testing, analysis, and verification, p.49-59, October 08-10, 1991, Victoria, British Columbia, Canada [doi>10.1145/120807.120812]
• 24: M. Young , R. Taylor , K. Forester , D. Brodbeck, Integrated concurrency analysis in a software development enviornment, ACM SIGSOFT Software Engineering Notes, v.14 n.8, p.200-209, Dec. 1989

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING

Additional Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Reliability
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications

          Nouns: Ada
      D.3.4 Processors
          Subjects: Translator writing systems and compiler generators

General Terms:
Algorithms, Design, Experimentation, Languages, Reliability, Verification