Publication Details
Static Deadlock Detection in Low-Level C Code
Marcin Vladimír, Ing.
Svobodová Lucie, Bc.
Vojnar Tomáš, prof. Ing., Ph.D. (DITS)
static analysis, abstract interpretation, function summaries, modular analysis,
concurrent code, deadlock, Infer
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.
@inproceedings{BUT187815,
author="Dominik {Harmim} and Vladimír {Marcin} and Lucie {Svobodová} and Tomáš {Vojnar}",
title="Static Deadlock Detection in Low-Level C Code",
booktitle="International Conference on Computer Aided Systems Theory (EUROCAST'22)",
year="2023",
series="Lecture Notes in Computer Science",
volume="13789",
pages="267--276",
publisher="Springer Nature Switzerland AG",
address="Cham",
doi="10.1007/978-3-031-25312-6\{_}31",
isbn="978-3-031-25311-9",
url="https://link.springer.com/chapter/10.1007/978-3-031-25312-6_31"
}