Ordinary Differential Equation-Based Deadlock Detection

Deadlock detection for concurrent systems via static analysis is in general difficult because of state-space explosion; indeed it is PSPACE compete. This paper presents a new method to detect the deadlocks. A concurrent system consisting of several processes that communicate using a resource sharing mechanism is represented by a set of ordinary differential equations of a restricted type. The equations describe the system state changes, and their solutions, also called state measures, indicate the extent to which the state can be reached in execution. Based on the solutions, the resource deadlock can be detected. By taking into account the computation errors of numerical solution for the differential equations, the detection can be performed via a MATLAB solver, as shown in the experiments. The complexity of the proposed method is polynomial.