This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Evaluating Deadlock Detection Methods for Concurrent Software
March 1996 (vol. 22 no. 3)
pp. 161-180

Abstract—Static analysis of concurrent programs has been hindered by the well known state explosion problem. Although many different techniques have been proposed to combat this state explosion, there is little empirical data comparing the performance of the methods. This information is essential for assessing the practical value of a technique and for choosing the best method for a particular problem. In this paper, we carry out an evaluation of three techniques for combating the state explosion problem in deadlock detection: reachability search with a partial order state space reduction, symbolic model checking, and inequality necessary conditions. We justify the method used for the comparison, and carefully analyze several sources of potential bias. The results of our evaluation provide valuable data on the kinds of programs to which each technique might best be applied. Furthermore, we believe that the methodological issues we discuss are of general significance in comparison of analysis techniques.

[1] G.S. Avrunin, U.A. Buy, J.C. Corbett, L.K. Dillon, and J.C. Wileden, "Automated Analysis of Concurrent Systems with the Constrained Expression Toolset," IEEE Trans. Software Eng. vol. 17, no. 11, pp. 1204-1222, Nov. 1991.
[2] G.S. Avrunin, J.C. Corbett, L.K. Dillon, and J.C. Wileden, Automated Derivation of Time Bounds in Uniprocessor Concurrent Systems IEEE Trans. Software Eng., vol. 20, no. 9, 1994.
[3] R.E. Bryant, "Symbolic Boolean Manipulation with Ordered Binary-Decision Diagrams," ACM Computing Surveys, vol., 24 no. 3, pp. 293-318, 1992.
[4] J. Burch, E. Clarke, K. McMillan, D. Dill, and L. Hwang, "Symbolic Model Checking: 1020States and Beyond," Proc. IEEE Symp. Logic in Computer Science, pp. 428-439, 1990.
[5] S.C. Cheung and J. Kramer, "Enhancing Compositional Reachability Analysis Using Context Constraints," Proc. First ACM SIGSOFT Symp. Foundations of Software Engineering, pp. 115-125, Dec. 1993.
[6] E.M. Clarke, O. Grumberg, and D.E. Long, "Model Checking and Abstraction," ACM Trans. Programming Language Systems, vol. 16, no. 5, pp. 1,512-1,542, Sept. 1994.
[7] R. Cleaveland, J. Parrow, and B. Steffen, "The Concurrency Workbench: A Semantics-Based Tool for the Verification of Concurrent Systems," ACM Trans. Programming Languages and Systems, Jan. 1993, pp. 36-72.
[8] J.C. Corbett, "Verifying General Safety and Liveness Properties with Integer Programming," Computer Aided Verification, Fourth Int'l Workshop Proc., vol. 663, Lecture Notes in Computer Science,Montreal, Canada: Springer-Verlag, v. Bochmann and Probst, eds. [42], pp. 357-369, 1992.
[9] J.C. Corbett, "An SEDL Translator," Tech. Report ICS-TR-93-03, Information and Computer Science Dept., Univ. of Hawaii at Ma noa, 1993.
[10] J.C. Corbett, "An Empirical Evaluation of Three Methods for Deadlock Analysis of Ada Tasking Programs," Software Eng. Notes, pp. 204-215, Proc. Int'l Symp. Software Testing and Analysis, Aug. 1994
[11] J.C. Corbett and G.S. Avrunin, "A Practical Method for Bounding the Time Between Events in Concurrent Real-Time Systems," Proc. Int'l Symp. Software Testing and Analysis (ISSTA), Ostrand and Weyuker [37], New York: ACM Press, pp. 110-116, June 1993.
[12] J.C. Corbett and G.S. Avrunin, "Using Integer Programming to Verify General Safety and Liveness Properties," Formal Methods in System Design, vol. 6, pp. 97-123, Jan. 1995.
[13] C. Courcoubetis ed., Proc. Fifth Int'l Conf. Computer Aided Verification,Elounda, Greece, 1993.
[14] S. Duri, U. Buy, R. Devarapalli, and S.M. Shatz, "Using State Space Reduction Methods for Deadlock Analysis in Ada Tasking," Proc. Int'l Symp. Software Testing and Analysis (ISSTA), Ostrand and Weyuker, eds., [37], pp. 51-60,New York: ACM Press, June 1993.
[15] M.B. Dwyer, "Data Flow Analysis for Verifying Correctness Properties of Concurrent Programs," PhD thesis, Univ. of Massachusetts at Amherst, 1995.
[16] M.B. Dwyer and L.A. Clarke, "Data Flow Analysis for Verifying Properties of Concurrent Programs," Software Eng. Notes, vol. 19, no. 5, pp. 62-75, Proc. ACM SIGSOFT Symp. Foundations of Software Eng., Dec. 1994.
[17] J. Ferrante,K.J. Ottenstein,, and J.D. Warren,“The program dependence graph and its use in optimization,” ACM Trans. Programming Languages and Systems, vol. 9, no. 3, pp. 319-349, June 1987.
[18] R. Ford, "Concurrent Algorithms for Real-Time Memory Management," IEEE Software, pp. 10-23, Sept. 1988.
[19] P. Godefroid, "Partial Order Methods for the Verification of Concurrent Systems: An Approach to the State Explosion Problem," PhD thesis, Univ. de Liege, 1994.
[20] P. Godefroid and D. Pirottin, “Refining Dependencies Improves Partial-Order Verification Methods,” Proc. Fifth Int'l Conf. Computer Aided Verification, pp. 438-449, June 1993.
[21] P. Godefroid and P. Wolper, "Using Partial Orders for the Efficient Verification of Deadlock Freedom and Safety Properties," Proc. Third Workshop Computer Aided Verification, pp. 417-428, July 1991.
[22] S. Graf and C. Loiseaux, "A Tool for Symbolic Program Verification and Abstraction," Proc. Computer Aided Verification, pp. 71-84, 1993.
[23] D. Helmbold and D. Luckham, "Debugging Ada Tasking Programs," IEEE Software, vol. 2, no. 2, pp. 47-57, Mar. 1985.
[24] C.A.R. Hoare, Communicating Sequential Processes, Prentice Hall, Englewood Cliffs, N.J., 1985.
[25] G.J. Holzmann, Design and Validation of Computer Protocols, Prentice Hall, 1991.
[26] A.J. Hu and D.L. Dill, "Efficient Verification with BDDs Using Implicitly Conjoined Invariants," Courcoubetis, ed., [13], Proc. Fifth Int'l Conf. Computer Aided Verification, pp. 3-14,Elounda, Greece, 1993.
[27] A.J. Hu, D.L. Dill, A.J. Drexler, and C.H. Yang, "Higher-Level Specification and Verification With BDDs," v. Bochmann and Probst [42], pp. 84-96, Computer Aided Verification, Proc. Fourth Int'l Workshop vol. 663 Lecture Notes in Computer Science,,Montreal, Canada, Springer-Verlag, 1992.
[28] G.M. Karam and R.J. Buhr, "Starvation and Critical Race Analyzers For Ada," IEEE Trans. Software Eng., vol. 16, no. 8, pp. 829-843, 1990.
[29] D.L. Long and L.A. Clarke, "Task Interaction Graphs for Concurrency Analysis," Proc. 11th Int'l Conf. Software Eng., pp. 44-52, May 1989.
[30] S.P. Masticola and B.G. Ryder, "Static Infinite Wait Anomaly Detection in Polynomial Time," Proc. Int'l Conf. Parallel Processing, vol. 2, pp. 78-87, 1990.
[31] C.E. McDowell, "A Practical Algorithm for Static Analysis of Parallel Programs," J. Parallel and Distributed Processing, vol. 6, no. 3, pp. 515-536, June 1989.
[32] K.L. McMillan, Symbolic Model Checking. Kluwer Academic, 1993.
[33] R. Milner, A Calculus of Communicating Systems. Berlin: Springer Verlag, vol. 92, 1980.
[34] T. Murata, B. Shenker, and S.M. Shatz, "Detection of Ada Static Deadlocks Using Petri Net Invariants," IEEE Trans. Software Eng., vol. 15, no. 3, pp. 314-326, Mar. 1989.
[35] L. Osterweil and L. Clarke, "A Proposed Testing and Analysis Research Initiative," IEEE Software, pp. 89-96, Sept. 1992.
[36] Proc. 1994 Int'l Symp. Software Testing and Analysis (ISSTA), T. Ostrand, ed., ACM Press, Aug. 1994.
[37] Proc 1993 Int'l Symp. Software Testing and Analysis (ISSTA), T. Ostrand and E. Weyuker, eds., New York: ACM Press, June 1993.
[38] P.H. Starke, "Reachability Analysis of Petri Nets Using Symmetries," Systems Analysis, Modeling, and Simulation, vol. 8, pp. 293-303, 1991.
[39] L.J. Stockmeyer and A.R. Meyer, "Word Problems Requiring Exponential Time," Proc. Fifth ACM Symp. Theory of Computing, pp. 1-9, 1973.
[40] W. Tichy, N. Habermann, and L. Prechelt, "Summary of the Dagstuhl Workshop on Future Directions in Software Engineering, ACM Sigsoft, Jan. 1993.
[41] S. Tu, S.M. Shatz, and T. Murata, "Theory and Application of Petri Net Reduction for Ada-Tasking Deadlock Analysis," Tech. Report 91-15, EECS Dept., Univ. of Illi nois, Chicago, 1991.
[42] Computer Aided Verification, vol. 663, Fourth Int'l Workshop Proc., G.v. Bochmann and D.K. Probst, eds., Lecture Notes in Computer Science,Montreal: Springer-Verlag, 1992.
[43] A. Valmari, "A Stubborn Attack on State Explosion," Proc. Second Workshop Computer Aided Verification, vol. 531, Lecture Notes in Computer Science, pp. 156-165. Springer-Verlag, 1991.
[44] W.J. Yeh and M. Young, "Compositional Reachability Analysis Using Process Algebra," Proc. ACM SIGSOFT Symp. Testing, Analysis and Verification, pp. 49-59, Oct. 1991.
[45] W.J. Yeh and M. Young, "Compositional Analysis of Ada Programs Using Process Algebra," Tech. Report, Software Eng. Research Center, Dept. of Computer Science, Purdue Univ., July 1993.
[46] W.J. Yeh and M. Young, "Redesigning Tasking Structures of Ada Programs for Analysis: A Case Study," J. Software Testing, Verification, and Reliability, Dec. 1994.
[47] M. Young, R.N. Taylor, K. Forester, and D. Brodbeck, "Integrated Concurrency Analysis in a Software Development Environment," R.A. Kemmerer, ed., Proc. Third Symp. Software Testing, Analysis and Verification, ACM SIGSOFT, pp. 200-209, 1989. Appeared as Software Engineering Notes, vol. 14, no. 8.

Index Terms:
Concurrency analysis, empirical evaluation, state space reduction, symbolic model checking, inequality necessary conditions, Ada tasking.
Citation:
James C. Corbett, "Evaluating Deadlock Detection Methods for Concurrent Software," IEEE Transactions on Software Engineering, vol. 22, no. 3, pp. 161-180, March 1996, doi:10.1109/32.489078
Usage of this product signifies your acceptance of the Terms of Use.