Является ли эта модель алгоритма Петерсона неверной?

Вы правы, алгоритм Петерсона должен быть свободен от голодания, и это действительно так.

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

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

Временные решения.

Есть в основном два обходных пути для этой проблемы:

• во-первых, просто спросить, что если какой-то процесс пытается войти в критическую секцию, то какой-то процесс в конце концов войдет в нее:

  ltl p2 { [] ((P[0]@req || P[1]@req) -> <> (P[0]@cs || P[1]@cs) }
  

  Это гарантирует прогресс в системе в целом, но не гарантирует, что ни один из P[0] и P[1] не подвергнется зависанию.

• #P11#

  ltl p3 { ([]<> (_last == 0)) -> [] (P[0]@req -> <> (P[0]@cs)) }
  

  #P12# <цитата> #P13# #P14# #P15#

Подходящее решение.

Я бы предложил изменить вашу модель, чтобы 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] могли выполняться бесконечно часто, потому что в противном случае будет найден еще один ложный контрпример.

Является ли эта модель алгоритма Петерсона неверной?

Итак, чтобы ответить на ваш вопрос более прямо, ваша модель не является функционально неправильной, но для надлежащей проверки отсутствия голодания необходимо внести некоторые незначительные изменения.