Стр. 4 - Г.П. Можаров, И.В. Парфилов - Подход к поиску взаимных блокировок в многопоточном программном обеспечении с помощью верификатора SPIN

что данный блок при верификации принимается за одно состояние си-
стемы, что позволяет уменьшить число глобальных состояний модели.
Операция увеличения счетчика сигнальной переменной с памятью
реализована командой semA++.
Реализация исключающих семафоров на языке Promela эквивалент-
на реализации семафоров для случая, когда начальное значение счет-
чика равно единице. В данном случае операция уменьшения счетчика
сигнальной переменной с памятью будет эквивалентна операции за-
хвата исключающего семафора, а операция увеличения счетчика сиг-
нальной переменной с памятью будет эквивалентна операции освобо-
ждения.
Сигнальные переменные без памяти можно реализовать на языке
Promela следующим образом:
chan condvar = [256] of { bit };
bit a =1;
byte condvarReaders = 0;
byte broadcastCounter=0;
active proctype W()
{
printf("MSC: P(): Ожидания сигнала \n ");
/* Операция ожидания сигнала */
condvarReaders++;
atomic
{
condvar ? a;
condvarReaders–;
}
printf("MSC: P(): Сигнал получен \n");
}
active proctype E( )
{
/* Посылка сигнала */
if :: (condvarReaders > 0) -> condvar ! a;
:: (condvarReaders <= 0) -> ;
fi;
printf("MSC: Q(): Посылка сигнала \n");
}
active proctype B( )
{
/* Широковещательная посылка сигнала */
atomic
{
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2012 89