用餐哲学家挨饿的可能性

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

• 不存在僵局的可能性。
• 没有挨饿的可能。

我正在使用信号 http://en.wikipedia.org/wiki/Semaphore_%28programming%29放在筷子上即可解决问题。

这是我的代码（算法）：

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

我确信这里不存在死锁的可能性，但是这里有可能出现饥饿问题吗？如果是，我该如何解决？

定义。哲学家是enabled前提是他没有在等待不可用的信号量。一个执行是有能力的哲学家所采取的无限步骤序列。执行是非常公平假设每个哲学家都可以无限地执行无限多个步骤。哲学家就餐的解决方案是免饥饿iff，在每一次强烈公平的执行中，每个哲学家都无限频繁地进餐。

Theorem.每个无循环、无死锁的就餐哲学家解决方案（其中非就餐哲学家不持有信号量）都是无饥饿的。

Proof.为了获得矛盾，假设存在一个非常公平的执行，其中某个哲学家（称他为菲尔）只有限次地进餐。我们证明这个执行实际上是僵局的。

Since pickup_chopsticks and drop_chopsticks由于没有循环，Phil 只执行有限的步骤。最后一步是semaphore_wait，说筷子i。因为执行是非常公平的，所以筷子 i 必然从某个有限时间开始持续不可用。让昆汀成为筷子i的最后一个持有者。如果昆汀走了无限多步，那么他会semaphore_signal筷子 i，所以昆汀也采取有限的步数。反过来，昆汀正在等待一根筷子 j，根据同样的论点，它一直无法使用，直到时间结束，并且由（比如说）罗伯特持有。通过遵循链semaphore_wait在有限的哲学家中，我们必然会遇到一个循环，这是一个僵局。

QED