kirancodes.me
To Proof Maintenance & Beyond!
ASE 2016

Sound static deadlock analysis for C/Pthreads

Daniel Kroening, Daniel Poetzl, Peter Schrammel, Björn Wachter

Full textDOI 10.1145/2970276.2970309dblp

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.

BibTeX
@inproceedings{Kroening-al:ASE16,
  author    = {Daniel Kroening and
               Daniel Poetzl and
               Peter Schrammel and
               Bj{\"{o}}rn Wachter},
  title     = {Sound static deadlock analysis for {C/Pthreads}},
  booktitle = {ASE},
  pages     = {379--390},
  publisher = {{ACM}},
  year      = {2016},
}

Related papers