Sound Static Deadlock Analysis for C/Pthreads (Extended Version)
Daniel Kroening, Daniel Poetzl, Peter Schrammel, Bj\"orn Wachter

TL;DR
This paper introduces a sound and precise static deadlock analysis method for C/pthreads programs, capable of analyzing real-world code efficiently and proving deadlock-freedom in large software systems.
Contribution
It presents a novel context- and thread-sensitive abstract interpretation framework combined with a lightweight dependency analysis for deadlock detection in C/pthreads.
Findings
Proved deadlock-freedom for 262 Debian programs totaling 2.6 million lines of code.
Analysis completed in less than 11 hours for large real-world codebases.
Method is sound for programs with defined C standard behavior.
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 precise enough to prove deadlock-freedom for a large number of 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 262 programs from the Debian GNU/Linux distribution with in total 2.6 MLOC in less than 11 hours.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsSoftware System Performance and Reliability · Parallel Computing and Optimization Techniques · Software Testing and Debugging Techniques
