Evaluating deadlock detection methods for concurrent software
- 1 March 1996
- journal article
- Published by Institute of Electrical and Electronics Engineers (IEEE) in IEEE Transactions on Software Engineering
- Vol. 22 (3) , 161-180
- https://doi.org/10.1109/32.489078
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 searching 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.Keywords
This publication has 32 references indexed in Scilit:
- Using integer programming to verify general safety and liveness propertiesFormal Methods in System Design, 1995
- Data flow analysis for verifying properties of concurrent programsACM SIGSOFT Software Engineering Notes, 1994
- Model checking and abstractionACM Transactions on Programming Languages and Systems, 1994
- An empirical evaluation of three methods for deadlock analysis of Ada tasking programsPublished by Association for Computing Machinery (ACM) ,1994
- A practical technique for bounding the time between events in concurrent real-time systemsPublished by Association for Computing Machinery (ACM) ,1993
- Using state space reduction methods for deadlock analysis in Ada taskingPublished by Association for Computing Machinery (ACM) ,1993
- The concurrency workbenchACM Transactions on Programming Languages and Systems, 1993
- Computer Aided VerificationPublished by Springer Nature ,1993
- Concurrent algorithms for real-time memory managementIEEE Software, 1988
- The program dependence graph and its use in optimizationACM Transactions on Programming Languages and Systems, 1987