Static Deadlock Detection in Low-Level C Code

TL;DR

This paper introduces L2D2, a scalable deadlock detection tool for low-level C code that analyzes functions independently and efficiently detects potential deadlocks through lock dependency cycles.

Contribution

The paper presents L2D2, a novel deadlock analyser capable of handling unstructured low-level C code by analyzing functions once without call context, improving scalability and effectiveness.

Findings

L2D2 effectively detects deadlocks in large C and C++ codebases.

L2D2 operates efficiently as a plugin within the Facebook/Meta Infer framework.

Experimental results demonstrate L2D2's scalability and accuracy.

Abstract

We present a novel scalable deadlock analyser L2D2 capable of handling C code with low-level unstructured lock manipulation. L2D2 runs along the call tree of a program, starting from its leaves, and analyses each function just once, without any knowledge of the call context. L2D2 builds function summaries recording information about locks that are assumed or known to be locked or unlocked at the entry, inside, and at the exit of functions, together with lock dependencies, and reports warnings about possible deadlocks when cycles in the lock dependencies are detected. We implemented L2D2 as a plugin of the Facebook/Meta Infer framework and report results of experiments on a large body of C as well as C++ code illustrating the effectiveness and efficiency of L2D2.