Sound Static Deadlock Analysis for C/Pthreads (Extended Version)

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.