Experiments on detecting program deadlock with ordinary differential equation model

Detection of deadlock of concurrent programs by static analysis is in general difficult because of state-space explosion. This paper gives the feasibility test of a deadlock detection method avoiding explosion of state space entirely, which method was proposed by author, by conducting more experiments. The frame of this method is as following: Firstly a Petri net, which represents a concurrent system, is continued to a new continuous Petri net. Then based on this continuous Petri net model, a concurrent system can be modeled by a family of ordinary differential equations. Finally the system deadlocks can be checked by analyzing the solution of this family of ordinary differential equations. Thus instead of exploring reachable states as in traditional methods, the solution of a family of ordinary differential equations is analyzed. Some strategies are developed in order to optimize the method. Dining philosopher problem has been employed to illustrate the method. More experiments have been conducted, and the experimental data shows that the method has strong ability in static analysis. As a byproduct, the method can also been used to check the boundedness of a system.