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

захвата исключающих семафоров в данных процессах различен. Да-
лее приведен исходный код модели на языке Promela:
byte semA=1;
byte semB=1;
active proctype P( )
{
printf("MSC: Noncritical section P");
atomic
{
semA>0;
semA- -
}
atomic
{
semB>0;
semB–
}
printf("MSC: Critical section P");
semB++;
semA++;
}
active proctype Q()
{
printf("MSC: Noncritical section Q ");
atomic
{
semB>0;
semB- -
}
atomic
{
semA>0;
semA- -
}
printf("MSC: Critical section Q");
semA++;
semB++;
}
После проведения анализа составленной модели с помощью ве-
рификатора SPIN был получен отчет, содержащий информацию об
ошибке в модели (рис. 1).
92 ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2012