Как я могу смоделировать этот код в promela/SP?

Следующий алгоритм пытается обеспечить взаимное исключение между двумя процессами P1 и P2, каждый из которых выполняет приведенный ниже код. Можно считать, что изначально sema = 0.

while true do{
atomic{if sema = 0
then sema:= 1
else
 go to line 2}
critical section;
sema:= 0;
  }

Как я могу смоделировать этот код в promela/SPIN?

Спасибо.


promela spin
person oralo    schedule 24.02.2014    source источник

Ответы (1)


arrow_upward
0
arrow_downward

Это должно быть довольно просто:

active proctype P() {
  bit sema = 0;

  do
    :: atomic {
         sema == 0 -> sema = 1
       }

       // critical section

       sema = 0
  od
}

Возможно, вам не нужен цикл do, если в вашем коде он нужен только для некоторого активного ожидания. Атомарный блок является исполняемым, только если sema установлен в 0, и тогда он выполняется сразу. Spin имеет встроенную семантику пассивного ожидания.

person dsteinhoefel    schedule 24.02.2014