Sound Static Deadlock Analysis for C/Pthreads (Extended Version)
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.
Keywords
Cite
@article{arxiv.1607.06927,
title = {Sound Static Deadlock Analysis for C/Pthreads (Extended Version)},
author = {Daniel Kroening and Daniel Poetzl and Peter Schrammel and Björn Wachter},
journal= {arXiv preprint arXiv:1607.06927},
year = {2016}
}