Стр. 2 - Ил.С. Свирин, П.А. Силин, В.В. Сюзев - Математическая модель многопоточной программы и правила безопасного многопоточного программирования

имеет большее число ложных срабатываний и не гарантирует нахожде-
ния всех потенциальных ситуаций блокировки.
Статический анализ использует исходные коды или объектные
файлы ПО для построения моделей, которые проверяются на наличие
блокировок [3–6]. Этот подход является достаточно эффективным, хо-
тя порождает большое число ложных срабатываний и плохо применим
к ПО со сложной объектной структурой.
Верификация моделей по методу Model Checking основана на по-
строении формальной модели ПО [7, 8] с последующей верификацией
данной модели с помощью специализированных средств [9, 10]. Этот
подход принципиально не дает ложных срабатываний и исключает
возможность пропуска блокировок, но чрезвычайно требователен к
вычислительным ресурсам.
Подход, представленный в настоящей статье, относится к верифи-
кации моделей. Его отличие заключается в наглядности построенной
формальной модели, достаточной для того, чтобы на ее основе могла
быть построена система правил корректного использования средств
синхронизации.
В рамках проблемы выявления потенциальных ситуаций взаимной
блокировки наибольший практический интерес представляет разра-
ботка на основе формальной модели взаимных блокировок системы
правил корректного использования средств синхронизации. Использо-
вание данной системы правил позволяло бы разработчикам ПО избе-
гать создания конструкций на основе средств синхронизации, приво-
дящих к появлению потенциальных ситуаций взаимной блокировки.
При попытке создания системы правил на основе существующих фор-
мальных моделей взаимных блокировок возникает следующая пробле-
ма. Формальные модели, включающие в себя алгоритмы выявления
потенциальных ситуаций взаимной блокировки, как правило, основа-
ны на использовании математического аппарата (топологии, теории
графов), в терминах которого затруднительно сформулировать набор
четких и наглядных правил, понятных конечному разработчику, не
знакомому с тонкостями данных моделей. Результаты, полученные на
основе верификации, вовсе не ориентированы на выявление причин
возникновения взаимных блокировок.
Для решения данной проблемы авторами была разработана мате-
матическая модель взаимных блокировок, сочетающая необходимый
уровень формализма и наглядность получаемых на основе этой мо-
дели результатов. Настоящая статья содержит краткое описание этой
модели, включая достаточные условия отсутствия потенциальных си-
туаций взаимных блокировок в наиболее общем случае и систему
правил корректного использования средств синхронизации на основе
этого достаточного условия.
96 ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2012