基于常微分方程的死锁检测实验分析

Experiments on Detecting Program Deadlock with Ordinary Differential Equation Model

用静态分析方法对并发程序进行死锁检测通常比较困难,其原因是会遇到状态空间爆炸问题.文中针对作者曾提出的一种可有效避免状态爆炸问题的死锁检测方法,进行进一步实验验证.该方法的基本框架是首先将表示并发系统的离散Petri网模型连续化,得到一种新的连续Petri网模型;在此基础上,建立系统的常微分方程模型;通过分析常微分方程组的解来检测系统中是否存在死锁.与传统方法不同点在于:该方法不需要遍历状态空间,而是分析一组常微分方程组的解.为了减少在求解常微分方程模型过程中的计算机系统的开销,作者还釆取了一系列优化策略.哲学家进餐问题被用来说明死锁检测的方法.大量的实验结果说明作者所提出的方法有着较强的静态分析能力.作为副产品,这种分析方法还可以用来判定系统的有界性.

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.