Research On Petri Net-based Deadlock Control For Multi-threaded Software

The multi-core revolution of computer hardware has promoted the emergence of multi-thread parallel programming system.A major feature of multi-threaded software is the the concurrency between programs,which makes the multi-threaded software vulnerable to concurrency errors.One of the most typical errors is deadlock.Deadlocks are ubiquitous in multi-threaded software and difficult to be detected and handled,which greatly threaten the security and reliability of software systems.Therefore,it is rather necessary to study effective deadlock control methods in multi-threaded software to ensure that deadlocks never occur.At present,there are few model-based methods to control deadlocks in multi-threaded software.Furthermore,these methods suffer from problems with complex control structure.Thus,we study the problem of deadlock control in multi-threaded software based on discrete event system and Petri nets,to guarantee that the controlled system is not only live but also with low structural complexity.The main contributions of our work are summarized as follows:1)A class of Petri nets,namely Gadara net,is employed to strictly model multi-threaded software and the deadlock-freeness of a multi-threaded software corresponds to the liveness of its Gadara net model.Hence,a mixed integer programming method is proposed to compute emptiable siphons for ordinary Gadara net.Thus,the liveness of ordinary Gadara net can be verified.Compared with existing methods,the computational efficiency of the proposed method is higher.2)For a class of ordinary Gadara nets(any two operation places on a same subnet cannot be marked simultaneously),an optimal iterative deadlock prevention policy is proposed.At each iteration,all the emptiable siphons containing the smallest number of resource places can be computed.Then,bad markings that may empty a siphon can be computed based on these siphons and reachability analysis.On the basis of these bad markings,a monitor is designed to forbid as many bad markings as possible.Compared with other methods,the controlled net obtained by the proposed policy is live and with a simplercontrol structure.3)For arbitrary Gadara net,an optimal deadlock control strategy is proposed.The strategy is mainly on the basis of the following results: a method for designing monitors based on siphons;an algorithm for computing redundant monitors in a controlled Gadara net;and an algorithm for admissible constraint transformation.The experimental results show that the proposed strategy can eliminate all the deadlocks in a Gadara net and the number of monitors added by our method is smaller than existing method.In conclusion,this paper focuses on the problem of deadlock control in multi-threaded software.The proposed methods can guarantee the liveness and maximal behavioral permissiveness of multi-threaded software and simplify the control structure.The results in this paper can provide a new idea and new technique for the study of deadlock control of multi-threaded software.