餐饮哲学家饥饿的可能性
如果它保证满足以下所有条件，我需要检查我解决餐饮哲学家问题的算法：
- 没有僵局的可能性。
- 没有饥饿的可能性。
我在筷子上使用信号量来解决问题。
这是我的代码（算法）：
while(true) { // He is Hungry pickup_chopsticks(i); // He is Eating... drop_chopsticks(i); // He is thinking } // ... void pickup_chopsticks(int i) { if(i % 2 == 0) /* Even number: Left, then right */ { semaphore_wait(chopstick[(i+1) % NUM_PHILOSOPHERS]); semaphore_wait(chopstick[i]); } else /* Odd number: Right, then left */ { semaphore_wait(chopstick[i]); semaphore_wait(chopstick[(i+1) % NUM_PHILOSOPHERS]); } } void drop_chopsticks(int i) { semaphore_signal(chopstick[i]); semaphore_signal(chopstick[(i+1) % NUM_PHILOSOPHERS]); } 我相信这里不存在死锁的可能，但这里有可能出现饥饿问题吗？ 如果是，我该如何解决？
定义 。 如果他不等待不可用的信号量，则启用哲学家。 执行是启用的哲学家采取的无限步骤。 如果每个被无限启用的哲学家经常采取无限多步，那么执行是非常公平的 。 餐饮哲学家的解决方案是没有饥饿的，如果在每一个强烈公平的执行中，每个哲学家都会经常无限地用餐。
定理。 每一个无循环无死锁的餐饮哲学家解决方案，其中非餐饮哲学家不拥有信号量是没有饥饿的。
certificate。 假设为了获得矛盾，存在一种强烈公平的执行，其中一些哲学家称他为菲尔，只是经常有限地用餐。 我们certificate这个执行事实上已经陷入僵局。
由于pickup_chopsticks和drop_chopsticks没有循环，因此Phil只需要有限的步骤。 最后一步是semaphore_wait ，比如筷子i。 因为执行非常公平，所以从一段有限的时间开始，筷子i必然是连续不可用的。 让昆汀成为筷子的最后持有者。 如果Quentin采取了无数的步骤，那么他就会使用semaphore_signal chopstick i，因此Quentin也采取了有限的步骤。 反过来，昆汀正在等待筷子j，根据相同的论点，筷子j一直无法使用，直到时间结束并由（比方说）罗伯特持有。 通过跟随有限多个哲学家中的semaphore_wait链，我们必然会到达一个循环，这是一个僵局。
QED
多年来我没有使用它，但有一个工具可以用来validation你的算法。 您必须在Promela中为您编写算法。