Подход к поиску взаимных блокировок в многопоточном программном обеспечении с помощью верификатора SPIN
Опубликовано: 01.01.2013
Авторы: Можаров Г.П., Парфилов И.В.
Опубликовано в выпуске: #11(11)/2012
DOI: 10.18698/2308-6033-2012-11-481
Раздел: Информационные технологии | Рубрика: Компьютерные системы и сети
Рассмотрена задача поиска потенциальных взаимных блокировок в многопоточном программном обеспечении. Предложен подход к выявлению потенциальных взаимных блокировок в многопоточных программных комплексах на основе метода Model Checking. Описано, каким образом основные примитивы синхронизации могут быть представлены на входном языке верификатора SPIN. Приведен пример моделирования и выявления взаимной блокировки в многопоточной программе.
Литература
[1] Bensalem S. and Havelund 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] Harrow 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] Holzmann G. Spin model checker: primer and reference manual. – NJ: Addison-Wesley Professional, 2003
[6] Эхтер Ш., Робертс Д. Многоядерное программирование. – СПб.: Питер, 2010
[7] Peled D. Combining partial order reductions with on-the-fly Model Checking // J. of Formal Methods in Systems Design, 8. 1996. – P. 39–64