Static Deadlock Detection in Low-Level C Code

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F23%3APU150742" target="_blank" >RIV/00216305:26230/23:PU150742 - isvavai.cz</a>

Výsledek na webu

<a href="https://link.springer.com/chapter/10.1007/978-3-031-25312-6_31" target="_blank" >https://link.springer.com/chapter/10.1007/978-3-031-25312-6_31</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-031-25312-6_31" target="_blank" >10.1007/978-3-031-25312-6_31</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Static Deadlock Detection in Low-Level C Code

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Static Deadlock Detection in Low-Level C Code

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

<a href="/cs/project/GA20-07487S" target="_blank" >GA20-07487S: Škálovatelné techniky pro analýzu komplexních vlastností počítačových systémů</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2023

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

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

ISBN

978-3-031-25311-9

ISSN

—

e-ISSN

—

Počet stran výsledku

10

Strana od-do

267-276

Název nakladatele

Springer Nature Switzerland AG

Místo vydání

Cham

Místo konání akce

Las Palmas de Gran Canaria, Canary Islands

Datum konání akce

20. 2. 2022

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—