Стр. 3 - Г.П. Можаров, И.В. Парфилов - Подход к поиску взаимных блокировок в многопоточном программном обеспечении с помощью верификатора SPIN
Упрощенная HTML-версия
Таблица 1
Примитивы синхронизации и операции над ними
Примитив синхронизации
Операции над примитивом
Исключающий семафор (мьютекс)
Захват
Освобождение
Сигнальная переменная без памяти
Ожидание сигнала
Посылка сигнала
Широковещательная посылка сигнала
Сигнальная переменная с памятью
Уменьшение счетчика
Увеличение счетчика
{
semA>0;
semA- -
}
/* Уменьшение счетчика сигнальной переменной */
atomic
{
semA>0;
semA- -
}
printf("MSC: Защищенный сигнальной переменной
блок P
\
n");
/* Увеличение счетчика сигнальной переменной */
semA++;
semA++;
}
В данном примере значение счетчика сигнальной переменной с
памятью хранится в глобальной переменной semA. Операция умень-
шения счетчика реализована с помощью блока
atomic
{
semA>0;
semA- -
}
Реализация данной операции потребовала использования ключе-
вого слова atomic, позволяющего объединять команды в неделимые
блоки. При верификации данный блок может быть выполнен, если вы-
полнено условие semA > 0, в противном случае процесс, содержащий
этот блок перейдет в состояние ожидания. Следует также отметить,
88
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2012
