Стр. 17 - Ил.С. Свирин, П.А. Силин, В.В. Сюзев - Математическая модель многопоточной программы и правила безопасного многопоточного программирования

Выводы. Представлены правила корректного использования
средств синхронизации. Система правил построена таким образом,
что применяющий их разработчик избегает появления в ПО кон-
струкций, которые приводят к невыполнению достаточного условия
отсутствия потенциальных ситуаций взаимной блокировки.
Достаточные условия сформулированы на основе математической
модели взаимных блокировок, разработанной авторами. В рамках мо-
дели доказано, что из достаточного условия следует отсутствие потен-
циальных ситуаций взаимной блокировки в системе.
Различные группы правил предназначены для разработчиков раз-
личного уровня. Императивные правила адресованы разработчикам
начального уровня. Рекомендательные правила — опытным разработ-
чикам. Показано, на какие аспекты средств синхронизации следует
обратить особое внимание.
СПИСОК ЛИТЕРАТУРЫ
1. L a m p o r t L. Specifying systems: The TLA+ language and tools for hardware and
software engineers // Addison-Wesley, 2002.
2. 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. – 208 p.
3. D e t l e f s D. L., R u s t a n K., L e i n o M., N e l s o n G. and S a x e J. B.
Extended static checking. Technical Report 159, Compaq Systems Research Center,
Palo Alto, California, USA, 1998.
4. Д а л У., Д е й к с т р а Э., Х о о р К. Структурное программирование.
Structured programming. – М.: Мир, 1975.
5. E n g l e r D. and A s h c r a f t 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.
6. A r t h o C. and B i e r e 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. Верификация параллельных и распреде-
ленных программных систем. – СПб.: БХВ-Петербург, 2010.
9. H a v e l u n d K. and P r e s s b u r g e r 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.
10. H o l z m a n n G. Design and validation of computer protocols. – Prentice Hall,
1991.
11. S a v a g e S., B u r r o w s M., N e l s o n G., S o b a l v a r r o P. and A n d e r -
s o n 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.
Статья поступила в редакцию 15.12.2011
ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. “Приборостроение”. 2012 111