我如何证明哲学家哲学家是否患有死亡或饥饿的可能性？从哪儿开始？

Question

我有一个家庭作业任务来证明哲学家哲学家问题上的特定变体是否遭受了死锁或饥饿。我怀疑这种情况根本没有受到任何影响，但我发现这种棘手的证明，我真的不知道从哪里开始。是否有针对这类问题的一般策略？

Answer 1

您可以阅读关于DAG（定向非循环图）的Wait-for graphs（更多详细信息here）并用于检测死锁。

欢呼声

Answer 2

首先，我会非常惊讶地听到有一个通用的策略来解决这个问题，这个问题不是那么抽象以至于毫无用处。

现在，显示的变化是安全得多，容易得多比证明它：你的任务是证明的变化是安全的？如果是这样，你可以减少零件的数量（将哲学家的数量减少到两个或三个），并尝试应用一个或多个方法formal verification。

实际上，形式验证非常罕见，我可以用一个例子来说明最好：我曾与在核设施中使用过软件的人们进行过交流（并没有详细介绍），当我问他们是否他们使用形式验证，我得到了“很好，是的，我们应该[正在使用它] ...”