Математическая модель взаимных блокировок. Корректное использование исключающих семафоров
Опубликовано: 01.01.2013
Авторы: Свирин И.С., Силин П.А., Сюзев В.В., Зарецкая Е.А.
Опубликовано в выпуске: #11(11)/2012
DOI: 10.18698/2308-6033-2012-11-483
Раздел: Информационные технологии | Рубрика: Компьютерные системы и сети
Одной из основных проблем разработки многопоточного программного обеспечения является взаимная блокировка потоков, которую чрезвычайно трудно выявить. Введена математическая модель взаимных блокировок.
Литература
[1] Savage S., Burrows M., Nelson G., Sobalvarro P. and Anderson T. Eraser: A dynamic data race detector for multi-threaded programs // Proceedings of the 16th ACM Symposium on Operating Systems Principles. – 1997. – P. 27–37
[2] Bensalem S. and Havelund K. Dynamic deadlock analysis of multi-threaded programs // Shmuel Ur, Eyal Bin, and Yaron Wolfsthal, editors, Haifa Verification Conference. – 2005. – Vol. 3875. – P. 208
[3] Detlefs D.L., Rustan K., Leino M., Nelson G. and Saxe J.B. Extended static checking. Technical Report 159, Compaq Systems Research Center, Palo Alto, California, USA, 1998
[4] Engler D. and Ashcraft K. RacerX: Effective, static detection of race conditions and deadlocks // Proc. of the 19th ACM Symposium on Operating Systems Principles. – 2003. – P. 237–252
[5] Havelund K. and Pressburger T. Model Checking Java programs using Java PathFinder // International J. on Software Tools for Technology Transfer, 2(4): 366–381, April 2000. Special issue of STTT containing selected submissions to the 4th SPIN workshop, Paris, France, 1998
[6] Artho C. and Biere A. Applying static analysis to large-scale, multi-threaded Java programs // D. Grant, editor, 13th Australien Software Engineering Conference, pages 68–75. IEEE Computer Society, August 2001
[7] Кларк Э., Грамберг О., Пелед Д. Верификация моделей программ: Model Checking. – М.: МНЦМО, 2002
[8] Карпов Ю. MODEL CHECKING. Bерификация параллельных и распределенных программных систем. – СПб.: БХВ-Петербург, 2010
[9] Holzmann G. Design and validation of computer protocols // Prentice Hall, 1991
[10] Lamport L. Specifying systems: The TLA+ language and tools for Hardware and Software Engineers // Addison-Wesley, 2002