Detail publikačního výsledku

Static Deadlock Detection in Low-Level C Code

HARMIM, D.; MARCIN, V.; SVOBODOVÁ, L.; VOJNAR, T.

Originální název

Static Deadlock Detection in Low-Level C Code

Anglický název

Static Deadlock Detection in Low-Level C Code

Druh

Stať ve sborníku v databázi WoS či Scopus

Originální abstrakt

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.

Anglický abstrakt

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.

Klíčová slova

static analysis, abstract interpretation, function summaries, modular analysis, concurrent code, deadlock, Infer

Klíčová slova v angličtině

static analysis, abstract interpretation, function summaries, modular analysis, concurrent code, deadlock, Infer

Autoři

HARMIM, D.; MARCIN, V.; SVOBODOVÁ, L.; VOJNAR, T.

Rok RIV

2024

Vydáno

10.02.2023

Nakladatel

Springer Nature Switzerland AG

Místo

Cham

ISBN

978-3-031-25311-9

Kniha

International Conference on Computer Aided Systems Theory (EUROCAST'22)

Edice

Lecture Notes in Computer Science

Svazek

13789

Strany od

267

Strany do

276

Strany počet

10

URL

https://link.springer.com/chapter/10.1007/978-3-031-25312-6_31

BibTex

@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"
}