Sound static deadlock analysis for C/Pthreads

ABSTRACT

We present a static deadlock analysis approach for C/pthreads. The design of our method has been guided by the requirement to analyse real-world code. Our approach is sound (i.e., misses no deadlocks) for programs that have defined behaviour according to the C standard and the pthreads specification, and is precise enough to prove deadlock-freedom for a large number of such programs. The method consists of a pipeline of several analyses that build on a new context- and thread-sensitive abstract interpretation framework. We further present a lightweight dependency analysis to identify statements relevant to deadlock analysis and thus speed up the overall analysis. In our experimental evaluation, we succeeded to prove deadlock-freedom for 292 programs from the Debian GNU/Linux distribution with in total 2.3 MLOC in 4 hours.

References

1. R. Agarwal, S. Bensalem, E. Farchi, K. Havelund, Y. Nir-Buchbinder, S. D. Stoller, S. Ur, and L. Wang. Detection of deadlock potentials in multithreaded programs. IBM Journal of Research and Development, 54(5):3, 2010.
2. R. Agarwal and S. D. Stoller. Run-time detection of potential deadlocks for programs with locks, semaphores, and condition variables. In Workshop on Parallel and Distributed Systems: Testing, Analysis, pages 51–60. ACM, 2006.
3. E. Albert, A. Flores-Montoya, and S. Genaim. Analysis of may-happen-in-parallel in concurrent objects. In FMOODS/FORTE, volume 7273 of LNCS, pages 35–51. Springer, 2012.
4. C. Artho and A. Biere. Applying static analysis to large-scale, multi-threaded Java programs. In Australian Software Engineering Conference, pages 68–75. IEEE, 2001.
5. S. Bensalem, M. Bozga, T. Nguyen, and J. Sifakis. D-Finder: A tool for compositional deadlock detection and verification. In CAV, volume 5643 of LNCS, pages 614–619. Springer, 2009.
6. S. Bensalem, A. Griesmayer, A. Legay, T. Nguyen, and D. Peled. Efficient deadlock detection for concurrent systems. In Formal Methods and Models for Codesign, pages 119–129. IEEE, 2011.
7. M. G. Burke, P. R. Carini, J.-D. Choi, and M. Hind. Flow-insensitive interprocedural alias analysis in the presence of pointers. In LCPC, volume 892 of LNCS, pages 234–250. Springer, 1995.
8. Y. Cai and W. K. Chan. Magiclock: Scalable detection ofpotential deadlocks in large-scale multithreaded programs. IEEE Trans. Software Eng., 40(3):266–281, 2014.
9. Z. Chen, X. Li, J. Chen, H. Zhong, and F. Qin. SyncChecker: detecting synchronization errors between MPI applications and libraries. In International Parallel and Distributed Processing Symposium, pages 342–353. IEEE, 2012.
10. E. M. Clarke, D. Kroening, and F. Lerda. A tool for checking ANSI-C programs. In TACAS, volume 2988 of LNCS, pages 168–176. Springer, 2004.
11. L. C. Cordeiro and B. Fischer. Verifying multi-threaded software using SMT-based context-bounded model checking. In ICSE, pages 331–340. ACM, 2011.
12. P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In POPL, pages 238–252. ACM, 1977.
13. D. R. Engler and K. Ashcraft. RacerX: effective, static detection of race conditions and deadlocks. In Symposium on Operating Systems Principles, pages 237–252. ACM, 2003.
14. M. Eslamimehr and J. Palsberg. Sherlock: scalable deadlock detection for concurrent programs. In Foundations of Software Engineering, pages 353–365. ACM, 2014.
15. R. Feldt and A. Magazinius. Validity threats in empirical software engineering research – an initial survey. In Software Engineering & Knowledge Engineering (SEKE), pages 374–379. Knowledge Systems Institute Graduate School, 2010.
16. A. Flores-Montoya, E. Albert, and S. Genaim. May-happen-in-parallel based deadlock analysis for concurrent objects. In FMOODS/FORTE, volume 7892 of LNCS, pages 273–288. Springer, 2013.
17. V. Forejt, D. Kroening, G. Narayanaswamy, and S. Sharma. Precise predictive analysis for discovering communication deadlocks in MPI programs. In Formal Methods, volume 8442 of LNCS, pages 263–278. Springer, 2014.
18. K. Havelund. Using runtime analysis to guide model checking of Java programs. In SPIN, volume 1885 of LNCS, pages 245–264. Springer, 2000.
19. T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Lazy abstraction. In POPL. ACM, 2002.
20. International Organization for Standardization. C standard, 2011. ISO/IEC 9899:2011.
21. O. Inverso, T. L. Nguyen, B. Fischer, S. La Torre, and G. Parlato. Lazy-CSeq: A context-bounded model checking tool for multi-threaded C-programs. In ASE, pages 807–812. IEEE, 2015.
22. P. Joshi, M. Naik, K. Sen, and D. Gay. An effective dynamic analysis for detecting generalized deadlocks. In Foundations of Software Engineering, pages 327–336. ACM, 2010.
23. P. Joshi, C. Park, K. Sen, and M. Naik. A randomized dynamic program analysis technique for detecting real deadlocks. In PLDI, pages 110–120. ACM, 2009.
24. V. Kahlon, Y. Yang, S. Sankaranarayanan, and A. Gupta. Fast and accurate static data-race detection for concurrent programs. In CAV, pages 226–239. Springer, 2007.
25. J. Krinke. Static slicing of threaded programs. In PASTE, pages 35–42. ACM, 1998.
26. J. Krinke. Context-sensitive slicing of concurrent programs. In ESEC/FSE, pages 178–187. ACM, 2003.
27. D. Kroening, D. Poetzl, P. Schrammel, and B. Wachter. Sound static deadlock analysis for C/Pthreads (extended version). CoRR, abs/1607.06927, 2016.
28. D. Kroening and M. Tautschnig. Automating software analysis at large scale. In MEMICS, volume 8934 of LNCS, pages 30–39. Springer, 2014.
29. J. K. Lee, J. Palsberg, R. Majumdar, and H. Hong. Efficient may happen in parallel analysis for async-finish parallelism. In SAS, volume 7460 of LNCS, pages 5–23. Springer, 2012.
30. Z. D. Luo, R. Das, and Y. Qi. Multicore SDK: A practical and efficient deadlock detector for real-world applications. In International Conference on Software Testing, Verification and Validation, pages 309–318. IEEE, 2011.
31. S. P. Masticola and B. G. Ryder. Non-concurrency analysis. In PPoPP, pages 129–138. ACM, 1993.
32. M. Naik, C. Park, K. Sen, and D. Gay. Effective static deadlock detection. In International Conference on Software Engineering, pages 386–396. IEEE, 2009.
33. M. G. Nanda and S. Ramesh. Slicing concurrent programs. In ISSTA, pages 180–190. ACM, 2000.
34. G. Naumovich and G. S. Avrunin. A conservative data flow algorithm for detecting all pairs of statement that may happen in parallel. In FSE, pages 24–34. ACM, 1998.
35. M. C. Rinard. Analysis of multithreaded programs. In SAS, volume 2126 of LNCS, pages 1–19. Springer, 2001.
36. S. F. Siegel, M. Zheng, Z. Luo, T. K. Zirkel, A. V. Marianiello, J. G. Edenhofner, M. B. Dwyer, and M. S. Rogers. CIVL: The concurrency intermediate verification language. In SC, pages 61:1–61:12. ACM, 2015.
37. F. Sorrentino. PickLock: A deadlock prediction approach under nested locking. In SPIN, volume 9232 of LNCS, pages 179–199. Springer, 2015.
38. The Open Group and IEEE. The open group base specifications issue 7, 2013. IEEE Std 1003.1-2008/Cor 1-2013.
39. E. Tomasco, O. Inverso, B. Fischer, S. La Torre, and G. Parlato. Verifying concurrent programs by memory unwinding. In TACAS, LNCS, pages 551–565. Springer, 2015.
40. C. von Praun. Detecting Synchronization Defects in Multi-Threaded Object-Oriented Programs. PhD thesis, 2004.
41. M. Weiser. Program slicing. In ICSE, pages 439–449. IEEE, 1981.
42. A. Williams, W. Thies, and M. D. Ernst. Static deadlock detection for Java libraries. In European Conference on Object-Oriented Programming, volume 3586 of LNCS, pages 602–629. Springer, 2005.
43. M. Zheng, M. S. Rogers, Z. Luo, M. B. Dwyer, and S. F. Siegel. CIVL: formal verification of parallel programs. In ASE, pages 830–835. IEEE, 2015.

Index Terms

• Theory of computation

  • Semantics and reasoning

    • Program reasoning

      • Program analysis