Математическая модель многопоточной программы и правила безопасного многопоточного программирования
Авторы: Свирин И.С., Силин П.А., Сюзев В.В.
Опубликовано в выпуске: #11(11)/2012
DOI: 10.18698/2308-6033-2012-11-482
Раздел: Информационные технологии | Рубрика: Компьютерные системы и сети
Одной из основных проблем разработки многопоточного программного обеспечения являются взаимные блокировки потоков. Взаимные блокировки потоков чрезвычайно трудно выявить, поскольку их возникновение напрямую связано с относительной динамикой выполнения потоков в программном обеспечении, которая зависит от множества трудно учитываемых факторов. Представлена система правил разработки многопоточной структуры программного обеспечения, направленная на уменьшение числа вносимых на этапе разработки ситуаций взаимной блокировки. Преимущество данной системы перед эмпирически выведенными аналогами заключается в том, что она выведена в процессе разработки математической модели взаимных блокировок.
Литература
[1] Lamport L. Specifying systems: The TLA+ language and tools for hardware and software engineers // Addison-Wesley, 2002
[2] 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. – 208 p.
[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] Дал У., Дейкстра Э., Хоор К. Структурное программирование. Structured programming. – М.: Мир, 1975. 5. Engler D. and Ashcraft K. RacerX: Effective, Static Detection of Race Conditions and Deadlocks // In Proc. of the 19th ACM Symposium on Operating Systems Principles. – 2003. – P. 237–252
[5] 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
[6] Кларк Э., Грамберг О., Пелед Д. Верификация моделей программ: Model checking. – М.: МНЦМО, 2002
[7] Карпов Ю. MODEL CHECKING. Верификация параллельных и распределенных программных систем. – СПб.: БХВ-Петербург, 2010
[8] 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
[9] Holzmann G. Design and validation of computer protocols. – Prentice Hall, 1991
[10] 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, pp 27–37, Oct. 1997