Deadlock Detection using Static Analysis
https://doi.org/10.15514/ISPRAS-2020-32(5)-2
Abstract
The paper describes an extension to summary based static program analysis to find deadlock errors. Summary based analysis is a popular approach aimed at the detection of bugs in programs due to its high performance and scalability. At the same time, the implementation of deadlock detectors in such an analysis is nontrivial, because there is no information about the locks held higher in the call stack during the process of function intraprocedural analysis. A lock graph, which is built during the main analysis, is used to model the semantics of multithreaded programs. Lock graph is a modification of call graph which contains additional information about held locks. After the lock graph is built, the deadlock detector is launched. Both the construction of the lock graph and the deadlock detection algorithm do not require significant processor time. On the performed measurements, the total analysis time increased by 4%. Based on the results of the analysis of 8 open source projects in C/C++/Java with a total size of more than 14 million lines of code, the proposed algorithm showed a high level of true positives. The described algorithms were implemented in the Svace tool.
About the Authors
Sergey Andreevich POLYAKOV
Ivannikov Institute for System Programming of the Russian Academy of Sciences
Russian Federation
Researcher
Russian Federation
Researcher
Alexey Evgenevich BORODIN
Ivannikov Institute for System Programming of the Russian Academy of Sciences
Russian Federation
PhD, researcher
Russian Federation
PhD, researcher
References
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.
Review
For citations:
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
Email this article 