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

broadcastCounter=condvarReaders;
do :: (broadcastCounter >0) -> condvar ! a;
broadcastCounter–;
:: (broadcastCounter<= 0) ->break ;
od;
}
printf("MSC: B(): Широковещательная посылка \n");
}
Основой для реализации сигнальной переменной без памяти на
языке Promela служит такое средство взаимодействия процессов, как
канал сообщений. Каналы сообщений используются для моделирова-
ния передачи данных от одного процесса к другому. Они объявляются
локально или глобально при помощи служебного слова chan:
chan server = [16] of { short }
Здесь объявлен канал server с буфером 16, т.е. этот канал может
хранить до 16 сообщений типа short, т.е. в канале может находиться
не более 16 непрочитанных сообщений.
Для работы с каналами существуют операторы посылки и получе-
ния сообщений. Оператор “!” посылает сообщение со значением пе-
ременной expr в канал server, добавляя это значение к концу очереди
в канале:
server ! expr
По умолчанию оператор выполняется, если канал назначения не пере-
полнен, в противном случае он блокируется. Каналы передают сооб-
щения в порядке FIFO: первым вошел — первым вышел.
Оператор приема сообщения “?” принимает сообщение из начала
буфера канала и сохраняет его в переменной msg:
server ? msg
Выполнение приема сообщения возможно только в случае, если канал
не пуст.
В представленной реализации сигнальной переменной без памя-
ти создается три процесса. Процесс W выполняет операцию ожида-
ния сигнала, процесс E выполняет операцию посылки сигнала для
сигнальной переменной без памяти, процесс B выполняет операцию
широковещательной посылки сигнала для сигнальной переменной без
памяти. Операция ожидания сигнала реализована как операция чтения
сообщения из канала. При отсутствии сообщений в канале процесс пе-
реходит в состояние ожидания сообщения. Операции посылки сигна-
ла и широковещания реализованы как операции отправки сообщения
в канал. В случае широковещания число сообщений, посылаемых в
канал, равно числу процессов, находящихся в состоянии ожидания
90 ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2012