Стр. 9 - Г.П. Можаров, И.В. Парфилов - Подход к поиску взаимных блокировок в многопоточном программном обеспечении с помощью верификатора SPIN
Упрощенная HTML-версия
Заключение.
Предложен подход к выявлению потенциальных вза-
имных блокировок в многопоточных программных комплексах на
основе метода Model Checking. Данный подход может применять-
ся архитекторами и разработчиками многопоточных программных
комплексов для повышения их качества благодаря представленным
реализациям базовых примитивов синхронизации на входном язы-
ке верификатора SPIN и примеру использования данного подхода. К
недостаткам подхода можно отнести его применимость только для
сравнительно небольших программных систем. Действительно, не-
смотря на то, что разработано множество приемов для сокращения
числа состояний в модели системы, таких как редукция частичных
порядков [7], большинство из них не оказывают должного эффекта в
данной постановке задачи, поскольку используют свойство независи-
мости событий, выполняемых параллельно. Два события считаются
независимыми, если при любом порядке их осуществления будет до-
стигнуто одно и то же глобальное состояние. В данной постановке
задачи события, выполняемые параллельно, не являются независи-
мыми, поскольку именно ошибочный порядок выполнения операций
доступа к средствам синхронизации и приводит к взаимной блоки-
ровке.
СПИСОК ЛИТЕРАТУРЫ
1. B e n s a l e m S. and H a v e l u n d K. Dynamic deadlock analysis of multi-
threaded programs // In Shmuel Ur, Eyal Bin, and Yaron Wolfsthal, editors, Haifa
Verification Conference. – 2005. – Vol. 3875. – P. 208–223.
2. H a r r o w J. Runtime checking of multithreaded applications with visual threads //
SPIN Model Checking and Software Verification. – 2000. – Vol. 1885. – P. 331–342.
3. К л а р к Э., Г р а м б е р г О., П е л е д О. Верификация моделей программ:
Model Checking. – М.: МНЦМО, 2002.
4. К а р п о в Ю. MODEL CHECKING. Верификация параллельных и распреде-
ленных программных систем. – СПб.: БХВ-Петербург, 2010.
5. H o l z m a n n G. Spin model checker: primer and reference manual. – NJ: Addison-
Wesley Professional, 2003.
6. Э х т е р Ш., Р о б е р т с Д. Многоядерное программирование. – СПб.: Питер,
2010.
7. P e l e d D. Combining partial order reductions with on-the-fly Model Checking //
J. of Formal Methods in Systems Design, 8. 1996. – P. 39–64.
Статья поступила в редакцию 15.12.2011
94
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2012
