Petri Net Based Deadlock Prevention Policy Of A Class Of Concurrent Programs

As the development of computer technology, multicore computer system is becoming very common and brings much more need for concurrent programming. Petri net is a important formal model in computer science and can efficiently model and analyse concurrent program.At present, one of the hot issues about concurrent program is the deadlock control problem. Deadlock in concurrent program is a state of some processes being blocked for waiting for the events will never be generated. Deadlock will cause the program crash and increase system costs, especially in real-time system, the deadlock will cause serious consequences. To solve deadlocks of the system and ensure the normal operation of concurrent programs, deadlock control has become an important research contents.This paper first studied the concurrent programs with synchronization signals, defined a Petri net subnets S3PS (system of simple sequential process with signals) net to model and analysis the program. A necessary and sufficient condition of liveness of the S^PS net which is its strict minimal siphons being non-empty was proved, while liveness is a sufficient condition for deadlock-free, Petri nets satisfying liveness will not generate deadlock. On this basis, a deadlock prevention polocy was designed, which was achieved by adding control arc to make every strict minimal siphon being non-empty in every operation state of the S3PS net and to ensure the controled net formed by adding control arc satisfying liveness and deadlock-free.This paper further extended the research, introduced the shared resource allocation system in concurrent programs with synchronization signals, defined S3PRS (system of simple sequential process with resources and signals) net. Because the non-signal subnet of S3PRS net belongs to S4PR net, the siphon computing method of S4PR net was used to compute non-signal siphons, on this basis, a minimal siphon computing method of siphons containing signals was proposed, so that the minimal Siphon set of S3PRS net was fined. Then the paper proved a necessary and sufficient condition of liveness of the S3PS net which is its strict minimal siphon being non-empty, and designed a deadlock prevention polocy by iteratively adding control place to make the strict minimal siphons being non-empty, ensured the final controlled net formed by adding control place satisfying liveness and the system becoming deadlock-free.