哲学家就餐问题的饥饿可能性

Question

我需要检查解决餐厅哲学家问题的算法是否保证满足以下所有条件：

• 没有死锁的可能性。
• 没有饥饿的可能性。

我正在使用信号量来解决筷子的问题。

这是我的代码（算法）：

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]);
}

我确定这里没有死锁的可能性，但是可能会有饥饿问题吗？如果有，我该如何解决？

- Eng.Fouad

---

顺便说一句，我从这个网站上获取了这个算法：http://www.math-cs.gordon.edu/courses/cs322/projects/p2/dp/ - Eng.Fouad

我不认为它会引起任何问题，但要证明这一点很困难，但是还有其他已被证明的解决方案，例如Dijkstra的解决方案，它使用资源层次结构，是安全的，并且之前已经被证明过。 - Saeed Amiri

你正在使用公平信号量，对吗？否则，答案显然是肯定的。 - Per

Answer 1

定义。如果哲学家没有等待不可用的信号量，则称其为使能状态。一次执行是指由使能的哲学家所采取的无限步骤序列。如果每个在使能状态下无限次出现的哲学家都采取了无限步骤，那么该执行是强公正的。当在每个强公正的执行中，每个哲学家都会无限次进餐时，则一个哲学家进餐的解决方案是无饥饿的。

定理。对于任何没有死锁和循环并且非进餐哲学家不持有信号量的解决方案，都是无饥饿的。

证明。为了获得矛盾，假设存在一种强公正的执行，其中某个哲学家（称之为Phil）只有有限次进餐。我们将展示这个执行实际上已经死锁。

由于pickup_chopsticks 和 drop_chopsticks没有循环，因此Phil只采取了有限次的步骤。最后一步是semaphore_wait，例如在筷子i上。因为执行是强公正的，所以从某个有限时间开始，筷子i必然一直不可用。令Quentin是筷子i的最后一个持有者。如果Quentin采取了无限次的步骤，那么他会semaphore_signal筷子i，所以Quentin也只采取了有限次的步骤。轮到Quentin在等待筷子j，在相同的论证中，筷子j将一直不可用直到时间结束，并被（例如）Robert占用。通过遵循有限数量的哲学家之间的semaphore_wait链，我们必然到达一个死锁的循环。

证毕

- Per

---

不错。我必须思考一下你的说法，“筷子i从某个有限时间开始必然是持续不可用的”，但它是正确的：将那个时间称为t，那么要么筷子i从t开始持续不可用（这满足你的说法），要么它从t开始有有限次数的可用性（在这种情况下，我们可以选择一些t' > t来替换t并使你的说法成立），或者它从t开始有无限次数的可用性（这是不可能的，因为它会违反“执行是强公平”的组合和“Phil停止进餐”）。 - j_random_hacker

Answer 2

虽然我已经很多年没有使用过这个工具，但是有一个工具可以用来验证您的算法。你需要在Promela中编写你的算法。

http://spinroot.com/spin/whatispin.html

http://en.wikipedia.org/wiki/Promela

- Adrian Cornish