餐饮哲学家饥饿的可能性

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

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

Answer 1

定义.如果他没有等待不可用的信号量,则启用哲学家.的执行是由启用哲学家所采取的步骤的无限序列.如果每个被无限启用的哲学家经常采取无限多步,那么执行是非常公平的.餐饮哲学家的解决方案是没有饥饿的,如果在每次强烈公平的执行中,每个哲学家都会无限地用餐.

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

证明.假设为了获得矛盾,存在一种强烈公平的执行,其中一些哲学家称他为菲尔,只是经常有限地用餐.我们证明这个执行事实上已经陷入僵局.

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

QED

Answer 2

多年来我没有使用过这个,但是有一个工具可以用来验证你的算法.您必须在Promela中为您编写算法.

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

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