Вы правы, алгоритм Петерсона должен быть свободен от голодания, и, действительно, это так.
Голодание происходит, когда процесс запрашивает некотороересурсы но им постоянно отказано .Таким образом, лучшей кодировкой формулы progress будет:
ltl p1 { [] (P[0]@req -> <> (P[0]@cs) }
, где req - метка, размещенная следующим образом:
do
:: true ->
req: want[me] = true
turn = you
!want[you] || turn == me
cs: want[me] = false
od
К сожалению, предыдущая формула по-прежнему считается false.
Причина этого заключается в том, что планировщик процесса системы, в которой вы проверяете модель , не являетсявообще говоря, справедливо .Фактически он допускает выполнение, в котором процесс с _pid, равным 0, навсегда не выбран для выполнения.
Модуль проверки моделей spin дает вам контрпример, который попадает именно в этоситуация:
~$ spin -t -g -l -p t.pml
ltl ltl_0: [] (<> ((P[0]@cs)))
starting claim 1
using statement merging
Never claim moves to line 3 [(!((P[0]._p==cs)))]
2: proc 1 (P:1) t.pml:10 (state 1) [want[me] = 1]
want[0] = 0
want[1] = 1
<<<<<START OF CYCLE>>>>>
Never claim moves to line 8 [(!((P[0]._p==cs)))]
4: proc 1 (P:1) t.pml:11 (state 2) [turn = you]
6: proc 1 (P:1) t.pml:12 (state 3) [((!(want[you])||(turn==me)))]
8: proc 1 (P:1) t.pml:13 (state 4) [want[me] = 0]
want[0] = 0
want[1] = 0
10: proc 1 (P:1) t.pml:10 (state 1) [want[me] = 1]
want[0] = 0
want[1] = 1
spin: trail ends after 10 steps
#processes: 2
want[0] = 0
want[1] = 1
turn = 0
cs = 0
10: proc 1 (P:1) t.pml:11 (state 2)
10: proc 0 (P:1) t.pml:9 (state 5)
10: proc - (ltl_0:1) _spin_nvr.tmp:7 (state 10)
2 processes created
Обходные пути.
Существует в основном два обходных пути для этой проблемы:
theсначала нужно просто спросить, что если какой-то процесс пытается войти в критическую секцию , то какой-то процесс в конечном итоге входит в него:
ltl p2 { [] ((P[0]@req || P[1]@req) -> <> (P[0]@cs || P[1]@cs) }
Это гарантирует, что есть прогресс в системе в целом, но это не гарантирует, что ни один из P[0] и P[1] специально не повлечет за собой голодание .
второе - ввести условие справедливости , которое требует сосредоточить проверку модели только на тех выполнениях, в которых процесс планируется выполнять бесконечно часто:
ltl p3 { ([]<> (_last == 0)) -> [] (P[0]@req -> <> (P[0]@cs)) }
, где _last - это предопределенная внутренняя переменнаяописывается в документах следующим образом:
ОПИСАНИЕ _last - это предопределенная глобальная переменная только для чтения типа pid, которая содержитномер экземпляра процесса, который выполнил последний шаг в текущей последовательности выполнения.Начальное значение _last равно нулю.
Переменная _last может использоваться только внутри никогда не утверждений.Ошибочно присваивать значение этой переменной в любом контексте.
К сожалению, этот подход не так хорош при проверке отсутствия голодания в вашей модели.Это связано с тем, что требование [] <> _last == 0 будет не только удалять любое выполнение, в котором P[0] не планируется бесконечно часто для выполнения из-за несправедливости планировщика, но также и в тех ситуациях, в которых P[0] не планируется из-за реальной проблемы голод .
Подходящее решение.
Я бы предложил изменить вашу модель так, чтобы P[0] выполнял Ожидание занято вместо блокировка при ожидании собственного хода .Это делает использование _last менее проблематичным при попытке доказать отсутствие голодания .Окончательная модель будет выглядеть следующим образом:
bool flag[2], turn
active [2] proctype P() {
pid i = _pid;
pid j = 1 - i;
do
:: true ->
req: flag[i] = true
turn = j;
do
:: (flag[j] && (turn == j)) -> skip
:: else -> break;
od;
cs: skip;
flag[i] = false;
od
}
ltl p1 { (
([]<> (_last == 0)) &&
([]<> (_last == 1))
) ->
([] (P[0]@req -> <> (P[0]@cs)))
}
И свойство действительно проверяется, не выбрасывая потенциально интересную трассировку выполнения:
~$ spin -a t.pml
ltl p1: (! (([] (<> ((_last==0)))) && ([] (<> ((_last==1)))))) || ([] ((! ((P[0]@req))) || (<> ((P[0]@cs)))))
~$ gcc pan.c
~$ ./a.out -a
(Spin Version 6.4.8 -- 2 March 2018)
Full statespace search for:
never claim + (p1)
assertion violations + (if within scope of claim)
acceptance cycles + (fairness disabled)
invalid end states - (disabled by never claim)
State-vector 40 byte, depth reached 97, errors: 0
269 states, stored (415 visited)
670 states, matched
1085 transitions (= visited+matched)
0 atomic steps
hash conflicts: 0 (resolved)
Stats on memory usage (in Megabytes):
0.017 equivalent memory usage for states (stored*(State-vector + overhead))
0.287 actual memory usage for states
128.000 memory used for hash table (-w24)
0.534 memory used for DFS stack (-m10000)
128.730 total actual memory usage
unreached in proctype P
t.pml:18, state 16, "-end-"
(1 of 16 states)
unreached in claim p1
_spin_nvr.tmp:23, state 33, "-end-"
(1 of 33 states)
pan: elapsed time 0 seconds
Обратите внимание, что нам требуются и P[0], и P[1] разрешено выполнять бесконечно часто, потому что в противном случае был бы найден другой ложный контрпример.
Является ли эта модель алгоритма Петерсона неправильной?
ИтакЧтобы ответить на ваш вопрос более прямо, ваша модель не является функционально неправильной, но для надлежащей проверки отсутствия голода необходимо внести некоторые незначительные изменения.