改进的哲学家进餐问题无饥饿解的Petri网模型

An Improved Petri Net Model of a Starvation-free Solution to the Dining Philosophers Problem

哲学家进餐问题是计算机科学中反映同步与并发的经典示例,活性与无饥饿是求解此问题的基本要求。基于两个许可卡轮转的策略,已经给出了一个无饥饿解的Petri网模型。此模型中可能出现两种情况:一个哲学家正在进餐时,另一张许可卡也轮转到他手中,但此卡只能在进餐后传下去;当两个相邻的哲学家都持有许可卡,并都希望进餐时,被竞争的那根筷子不能确定分配给谁。针对这两种情况,对原模型作了修改,提高了系统的效率。

The dining philosophers problem is a classical example of synchronization and concurrency in computer science. Its solution should guarantee the system is live and starvation-free. A Petri net-based starvation-free solution was described, and the policy, in which two dining-cards were cycled, was utilized in this model. Two cases that could lower the system efficiency occurred possibly in the above model： 1） while a philosopher was eating, another card was also transmitted to him, but this card could not be released until he finished dining; 2） when the two adjacent philosophers held one dining-card respectively and wanted to eat, it was not decided which one would possess that shared chopstick. Two corresponding policies are proposed to improve the above Petri net model, and can enhance the system efficiency.