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

Мне нужно проверить мой алгоритм решения проблемы обеденного философа, если он гарантирует, что все из следующего удовлетворены или нет:

Отсутствие возможности блокировки.
Отсутствие возможности голодания.

Я использую 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]);
}

Я уверен, что здесь нет возможности зайти в тупик, но есть ли здесь проблема голодания? Если да, то как я могу его решить?

Ответ 1

Определение. Философ включен, если он не ждет недоступного семафора. Выполнение - это бесконечная последовательность шагов, предпринятых активированными философами. Исполнение строго справедливо, если каждый философ бесконечно часто принимает бесконечно много шагов. Решение столовых философов не содержит голода, если в каждом строго честном исполнении каждый философ умирает бесконечно часто.

Теорема. Каждое безрецептурное решение для столовых философов, в котором не обеденные философы не имеют семафоров, не содержит голода.

Доказательство. Предположим, что для получения противоречия существует строго справедливое исполнение, в котором какой-то философ, называя его Филом, обедает только финитно. Мы показываем, что это выполнение фактически зашло в тупик.

Так как pickup_chopsticks и drop_chopsticks не имеют циклов, Фил выполняет только конечное число шагов. Последний шаг - semaphore_wait, скажем, на палочке i. Поскольку выполнение является справедливым, палочка я обязательно непрерывно недоступна с некоторого конечного времени вперед. Пусть Квентин станет последним обладателем палочки для еды. Если Квентин выполнил бесконечно много шагов, тогда он будет semaphore_signal chopstick i, поэтому Квентин также выполняет конечные шаги. Квинтин, в свою очередь, ждет палочки j, которая, по тем же аргументам, постоянно недоступна до конца и удерживается (скажем) Робертом. Следуя цепочке semaphore_wait среди конечного числа философов, мы обязательно приходим к циклу, который является тупиком.

КЭД

Ответ 2

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

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

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