c - 用餐哲学家饥饿的可能性

Question

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

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

我正在使用 semaphore在筷子上解决问题。

这是我的代码(算法):

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

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

Answer 1

定义。哲学家启用当且仅当他没有在等待不可用的信号量。 执行 是由启用的哲学家采取的无限步骤序列。一次执行是非常公平当且仅当每个无限启用的哲学家经常采取无限多的步骤。哲学家就餐的解决方案是无饥饿当且仅当，在每个非常公平的执行中，每个哲学家都无限频繁地用餐。

定理。每个无循环无死锁的无用餐哲学家解决方案，其中非用餐哲学家不持有信号量是无饥饿的。

证明。为了得到一个矛盾，假设存在一个非常公平的执行，其中某个哲学家，称他为菲尔，只在有限的时间内用餐。我们证明这个执行实际上是死锁的。

由于 pickup_chopsticks 和 drop_chopsticks 没有循环，Phil 只需要有限的步数。最后一步是 semaphore_wait，在筷子 i 上说。因为执行是非常公平的，所以从某个有限的时间开始，筷子 i 必然连续不可用。让 Quentin 成为筷子 i 的最后一个持有者。如果 Quentin 采取了无限多步，那么他将 semaphore_signal 筷子 i，因此 Quentin 也采取了有限多步。反过来，昆汀正在等待一根筷子 j，根据同样的论证，这根筷子在时间结束之前一直不可用，并由(比如说)罗伯特持有。通过遵循有限多个哲学家之间的 semaphore_wait 链，我们必然会到达一个循环，这是一个死锁。

QED