Sound Static Deadlock Analysis for C/Pthreads

Abstract

We present a static deadlock analysis 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.

Paper

Sound Static Deadlock Analysis for C/Pthreads
D. Kroening, D. Poetzl, P. Schrammel, and B. Wachter
ASE '16
Extended version on arXiv

Tool

Our tool is maintained in a branch of the CBMC git repository. To get the tool, clone the repository and checkout the deadlock-analysis branch as follows:

git clone https://github.com/diffblue/cbmc.git git checkout deadlock-analysis

Then follow the instructions in the COMPILING file.

The tool is run as follows

Compile the source code using the goto-cc tool
Analyze it using goto-instrument myfile.o --show-deadlocks

Experiments

There is a package for replicating the experiments reported in the paper. The package contains all the benchmarks and a script that downloads, builds and runs the tool on them.