13

如果它保证满足以下所有条件，我需要检查我解决餐饮哲学家问题的算法：

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

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

这是我的代码（算法）：

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

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

4

2 回答 2

17

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

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

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

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

量子点

于 2011-11-25T23:03:09.687 回答
5

我已经很多年没有使用它了，但是有一个工具可以用来验证你的算法。您将不得不在 Promela 中编写算法。

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

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

于 2011-11-25T21:43:37.433 回答