возможность голодания столовых философов

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 не имеют петель, Фил делает лишь конечное число шагов.Последний шаг - semaphore_wait, скажем, на палочке для еды i.Поскольку выполнение является строго справедливым, палочка i обязательно будет постоянно недоступна с некоторого конечного времени.Пусть Квентин будет последним держателем палочек для еды i.Если бы Квентин сделал бесконечно много шагов, то он бы semaphore_signal сделал палочку i, поэтому Квентин тоже сделал конечное число шагов.Квентин, в свою очередь, ждет палочки для еды j, которая по тому же аргументу постоянно недоступна до конца времени и удерживается (скажем) Робертом.Следуя цепочке semaphore_wait с среди конечного числа философов, мы обязательно придем к циклу, который зашёл в тупик.

QED

Answer 2

Я не использовал это много лет, но есть инструмент, который вы можете использовать для проверки вашего алгоритма.Вам придется написать свой алгоритм в Promela.

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

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