Обнаружение дефекта взаимной блокировки с помощью статического анализа
https://doi.org/10.15514/ISPRAS-2020-32(5)-2
Аннотация
В статье описывается расширение статического анализа программ на основе резюме для поиска ошибок взаимных блокировок потоков. Анализ на основе резюме является популярным подходом для поиска ошибок в программах благодаря высокой производительности и масштабируемости. При этом реализация детекторов поиска взаимных блокировок в таком анализе является нетривиальной, так как в процессе внутрипроцедурного анализа функций отсутствует информация об удерживаемых блокировках выше по стеку вызовов. Для моделирования семантики многопоточных программ используется граф блокировок, который строится во время основного анализа. Граф блокировок является модификацией графа вызовов с добавлением информации об удерживаемых блокировках. После построения графа блокировок запускается детектор обнаружения взаимных блокировок. Как построение графа блокировок, так и алгоритм обнаружения взаимных блокировок, не требуют существенного процессорного времени. На выполненных замерах общее время анализа увеличилось на 4%. По результатам анализа 8 проектов с открытым исходном кодом на языках C/C++/Java общим размером более 14 млн. строк кода предложенный алгоритм показал высокий уровень истинных срабатываний. Описываемые алгоритмы были реализованы в инструменте Svace.
Об авторах
Сергей Андреевич ПОЛЯКОВ
Институт системного программирования им. В.П. Иванникова РАН
Россия
Сотрудник отдела компиляторных технологий
Россия
Сотрудник отдела компиляторных технологий
Алексей Евгеньевич БОРОДИН
Институт системного программирования им. В.П. Иванникова РАН
Россия
Кандидат физико-математических наук, научный сотрудник
Россия
Кандидат физико-математических наук, научный сотрудник
Список литературы
1. А.П. Меркулов, С.А. Поляков, А.А. Белеванцев. Анализ программ на языке Java в инструменте Svace. Труды ИСП РАН, том 29, вып. 3, 2017 г., стр. 57-74 / A.P. Merkulov, S.A. Polyakov, A.A. Belevantsev. Supporting Java programming in the Svace static analyzer. Trudy ISP RAN/Proc.ISP RAS, vol.29, issue 3, 2017, pp. 57-74 (in Russian). DOI: 10.15514/ISPRAS-2017-29(3)-5.
2. W.R. Bush, J D. Pincus, and D.J. Sielaff. A static analyzer for finding dynamic programming errors. Software: Practice and Experience, vol. 30, no. 7, 2000, pp. 775-802.
3. Y. Xie, A. Chou, and D. Engler. Archer: using symbolic, path-sensitive analysis to detect memory access errors. In Proc. of the 9th European software engineering conference held jointly with 11th ACM SIGSOFT international symposium on Foundations of software engineering, 2003, pp. 327-336.
4. I. Dillig, T. Dillig, and A. Aiken. Static error detection using semantic inconsistency inference. In Proc. of the 28th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2007, pp. 435-445.
5. D. Babic and A.J. Hu. Calysto: scalable and precise extended static checking. In Proc. of the 30th international conference on Software engineering, 2008, pp. 211-220.
6. В.К. Кошелев, И.А. Дудина, В.Н. Игнатьев, А.И. Борзилов. Чувствительный к путям поиск дефектов в программах на языке C# на примере разыменования нулевого указателя. Труды ИСП РАН, том 27, вып. 5, 2015 г., стр. 59-86 / V. Koshelev, I. Dudina, V. Ignatyev, A. Borzilov. Path-Sensitive Bug Detection Analysis of C# Program Illustrated by Null Pointer Dereference. Trudy ISP RAN/Proc. ISP RAS, vol. 27, issue 5, 2015, pp.59-86 (in Russian). DOI: 10.15514/ISPRAS-2015-27(5)-5.
7. McPeak, C.-H. Gros, and M. K. Ramanathan. Scalable and incremental software bug detection. In Proc. of the 2013 9th Joint Meeting on Foundations of Software Engineering, 2013, pp. 554-564.
8. R. Agarwal and S. D. Stoller. Run-time detection of potential deadlocks for programs with locks, semaphores, and condition variables. In Proc. of the 2006 Workshop on Parallel and Distributed Systems: Testing and Debugging, 2006, pp. 51-60.
9. K. Havelund. Using runtime analysis to guide model checking of java programs. Lecture Notes in Computer Science, vol. 1885, 2000, pp. 245-264.
10. S. Savage, M. Burrows, G. Nelson, P. Sobalvarro, and T. Anderson. Eraser: a dynamic data race detector for multithreaded programs. ACM Transactions on Computer Systems (TOCS), vol. 15, no. 4, 1997, pp. 391-411.
11. T. Elmas, S. Qadeer, and S. Tasiran. Goldilocks: a race and transaction-aware java runtime. ACM SIGPLAN Notices, vol. 42, no. 6, 2007, pp. 245-255.
12. C. Boyapati and M. Rinard. A parameterized type system for race-free java programs. In Proc. of the 16th ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, 2001, pp. 56-69.
13. M. Naik, C.-S. Park, K. Sen, and D. Gay. Effective static deadlock detection. In Proc. of the IEEE 31st International Conference on Software Engineering, pp. 386-396.
14. M. Naik, A. Aiken, and J. Whaley. Effective static race detection for java. In Proc. of the 27th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2006, pp. 308-319, 2006.
15. S. D. Stoller. Model-checking multi-threaded distributed java programs. Lecture Notes in Computer Science, vol. 1885, 2000, pp. 224-244.
16. T.A. Henzinger, R. Jhala, and R. Majumdar. Race checking by context inference. In Proc. of the ACM SIGPLAN 2004 conference on Programming Language Design and Implementation, 2004, pp. 1-13.
Рецензия
Для цитирования:
ПОЛЯКОВ С.А., БОРОДИН А.Е. Обнаружение дефекта взаимной блокировки с помощью статического анализа. Труды Института системного программирования РАН. 2020;32(5):21-34. https://doi.org/10.15514/ISPRAS-2020-32(5)-2
For citation:
POLYAKOV S.A., BORODIN A.E. Deadlock Detection using Static Analysis. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2020;32(5):21-34. (In Russ.) https://doi.org/10.15514/ISPRAS-2020-32(5)-2
Послать статью по эл. почте 