Верифицирующий алгоритм для математической модели взаимных блокировок
Автор: Парфилов Иван Васильевич, Свирин Илья Сергеевич, Силин Павел Александрович, Шумилов Юрий Юрьевич
Журнал: Спецтехника и связь @st-s
Статья в выпуске: 6, 2011 года.
Бесплатный доступ
Одной из основных проблем многопоточного программного обеспечения являются взаимные блокировки. Проявление взаимных блокировок зависит от относительной динамики выполнения потоков, которая опирается на слабо прогнозируемые факторы, поэтому данный вид ошибок практически невозможно выявить на этапе тестирования. Взаимная блокировка приводит к невозможности дальнейшего выполнения одного или нескольких потоков многопоточного программного обеспечения, что является прямой угрозой безопасности обрабатываемой информации. В данной статье представлена математическая модель взаимных блокировок. На основе данной модели разработан алгоритм выявления взаимных блокировок в многопоточном программном обеспечении.
Многопоточное по, взаимные блокировки, верификация
Короткий адрес: https://sciup.org/14967070
IDR: 14967070
Список литературы Верифицирующий алгоритм для математической модели взаимных блокировок
- C. Artho and A. Biere. Applying Static Analysis to Large-Scale, Multi-threaded Java Programs. In D. Grant, editor, 13th Australien Software Engineering Conference./IEEE Computer Society, August 2001. -РР. 68 -75.
- S. Bensalem and K. Havelund. Dynamic Deadlock Analysis of Multi-threaded Programs./In Shmuel Ur, Eyal Bin, and Yaron Wolfsthal, editors./Haifa Verification Conference, Springer, 2005. -V. 3875 of LNCS. -PP. 208 -223.
- D.L. Detlefs, K. Rustan M. Leino, G. Nelson, and J. B. Saxe. Extended Static Checking. Technical Report 159./Compaq Systems Research Center, Palo Alto, California, USA, 1998.
- D. Engler and K. Ashcraft. RacerX: Effective, Static Detection of Race Conditions and Deadlocks./In Proceedings of the 19th ACM Symposium on Operating Systems Principles, Oct. 2003. -PP. 237 -252.
- K. Havelund and T. Pressburger. Model Checking Java Programs using Java./PathFinder. International Journal 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.
- G. Holzmann. Design and Validation of Computer Protocols. Prentice Hall, 1991.
- L. Lamport. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, 2002.
- S. Savage, M. Burrows, G. Nelson, P. Sobalvarro, and T. Anderson. Eraser: A Dynamic Data Race Detector for Multi-threaded Programs. In Proceedings of the 16th ACM Symposium on Operating Systems Principles, Oct. 1997. -PP. 27 -37.
- Дал У., Дейкстра Э., Хоор К. Структурное программирование = Structured Programming. -1-е изд. -М.: Мир, 1975.
- Э. Кларк, О. Грамберг, Д. Пелед. Верификация моделей программ: Model Checking. -М.: МНЦМО, 2002.
- Ю. Карпов. Model Checking: верификация параллельных и распределенных программных систем. -СПб.: БХВ-Петербург, 2010.
- Р. Седжвик. Фундаментальные алгоритмы на С++. Алгоритмы на графах./Пер. с англ. -СПб: ООО «ДиаСофтЮП», 2002.
