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