Стр. 1 - Г.П. Можаров, И.В. Парфилов - Подход к поиску взаимных блокировок в многопоточном программном обеспечении с помощью верификатора SPIN
Упрощенная HTML-версия
УДК 004.05
Г. П. М о ж а р о в, И. В. П а р ф и л о в
ПОДХОД К ПОИСКУ ВЗАИМНЫХ БЛОКИРОВОК
В МНОГОПОТОЧНОМ ПРОГРАММНОМ
ОБЕСПЕЧЕНИИ С ПОМОЩЬЮ ВЕРИФИКАТОРА
SPIN
Рассмотрена задача поиска потенциальных взаимных блокировок
в многопоточном программном обеспечении. Предложен подход к
выявлению потенциальных взаимных блокировок в многопоточных
программных комплексах на основе метода Model Checking. Опи-
сано, каким образом основные примитивы синхронизации могут
быть представлены на входном языке верификатора SPIN. При-
веден пример моделирования и выявления взаимной блокировки в
многопоточной программе.
E-mail:
Ключевые слова
:
взаимная блокировка, синхронизация потоков, проверка
модели.
В настоящее время в связи с развитием многоядерных микропро-
цессорных технологий возрастает актуальность параллельного про-
граммирования. При разработке сложных многопоточных программ-
ных средств важно учитывать ряд возможных проблем, которые в
дальнейшем могут привести к их нестабильной работе. Одним из
признаков нестабильной работы многопоточной программы является
возникновение взаимной блокировки потоков в процессе их выпол-
нения. Взаимные блокировки происходят в результате некорректного
использования средств синхронизации потоков, когда имеется группа
потоков, каждый из которых пытается получить эксклюзивный доступ
к некоторым ресурсам и претендует на ресурсы, принадлежащие дру-
гому потоку. В итоге все они оказываются в состоянии бесконечного
ожидания доступа к ресурсу.
Основной проблемой выявления ошибок в использовании средств
синхронизации стандартными методами (в результате динамическо-
го анализа [1, 2]) является сильная зависимость возникновения си-
туаций взаимных блокировок от динамики выполнения программы в
конкретной программно-аппаратной среде. Это свойство не позволя-
ет создать эффективные алгоритмы выявления взаимных блокировок
на этапе тестирования программного обеспечения (ПО). Практиче-
ски об устранении взаимных блокировок необходимо заботиться на
этапе детализированного проектирования системы. Для решения про-
блемы возникновения взаимных блокировок на этапе детализирован-
ного проектирования целесообразно использовать технологии вери-
фикации, основанные на методе Model Checking [3, 4]. Верификация
программных систем с помощью метода Model Checking состоит из
86
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2012
