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

сигнала от сигнальной переменной без памяти. Благодаря этому все
ожидающие процессы продолжают свою работу.
SPIN поддерживает верификацию следующего набора общих
свойств, называемых в SPIN базовыми:
• из класса свойств безопасности:
◦ проверка сохранения локальных инвариантов, описанных с по-
мощью оператора assert;
◦ проверка на наличие некорректных конечных состояний, т.е. об-
наружение взаимных блокировок процессов;
• из класса свойств живости:
◦ проверка отсутствия бесконечных циклов, не содержащих опера-
торов, помеченных меткой progress;
◦ проверка отсутствия циклов с бесконечно частым выполением
операторов с меткой accept.
Таким образом, обнаружение взаимных блокировок в модели мно-
гопоточной программы в SPIN происходит вследствие проверки моде-
ли на наличие некорректных конечных состояний.
Пример выявления взаимной блокировки в модели многопо-
точной программы. Для демонстрации возможностей по выявлению
взаимных блокировок в моделях многопоточных программ рассмо-
трим следующий пример. Пусть логика использования средств син-
хронизации в программе, выполняемой в двух потоках, построена та-
ким образом, что возможна взаимная блокировка потоков на этапе
их выполнения (табл. 2). Предположим, что оба потока хотят полу-
чить эксклюзивный доступ к двум разделяемым ресурсам А и В . Для
синхронизации доступа к данным ресурсам используются операции
захвата исключающих семафоров, каждый из которых соответствует
одному ресурсу.
Таблица 2
Очередность выполнения потоков, приводящая к взаимной блокировке
Шаг Поток 1 Поток 2
0 Хочет получить доступ к ресурсам
A и B, начинает с A
Хочет получить доступ к ресурсам
A и B, начинает с B
1 Получает доступ к ресурсу A
2 Получает доступ к ресурсу B
3 Ожидает освобождения ресурса A
4 Ожидает освобождения ресурса B
5 Взаимная блокировкa
Для моделирования описанной многопоточной программы на язы-
ке Promela необходимо создать два процесса, каждый из которых пы-
тается осуществить захват двух исключающих семафоров. Порядок
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2012 91