RacerF: Lightweight Static Data Race Detection for C Code
(Experience Paper)

D 2025

RacerF: Lightweight Static Data Race Detection for C Code (Experience Paper)

DACÍK, Tomáš a Tomáš VOJNAR

Základní údaje

Originální název

RacerF: Lightweight Static Data Race Detection for C Code (Experience Paper)

Autoři

DACÍK, Tomáš a Tomáš VOJNAR

Vydání

Schloss Dagstuhl, Proc. of 39th European Conference on Object-Oriented Programming – ECOOP'25, od s. 1-19, 19 s. 2025

Nakladatel

Leibniz International Proceedings in Informatics (LIPIcs)

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Německo

Utajení

není předmětem státního či obchodního tajemství

Forma vydání

elektronická verze "online"

Odkazy

Associated technical report, Publisher's webpage, The RacerF tool

Organizační jednotka

Fakulta informatiky

ISSN

DOI

https://doi.org/10.4230/LIPIcs.ECOOP.2025.37

EID Scopus

2-s2.0-105009693533

Klíčová slova anglicky

program analysis;static analysis;concurrent programs;data races;

Štítky

core_A, firank_A

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 14. 8. 2025 17:53, prof. Ing. Tomáš Vojnar, Ph.D.

Anotace

V originále

We present RacerF, a novel static analyser for thread-modular data race detection. The approach behind RacerF exploits static analysis of sequential program behaviour whose results are generalised for multi-threaded programs using a combination of lightweight under- and over-approximating methods. The tool is implemented as a plugin of the Frama-C platform and can leverage several analysis backends, most notably the Frama-C’s abstract interpreter EVA. Although our methods are mostly heuristic without providing formal guarantees, our experimental evaluation shows that even for intricate programs, RacerF can provide very precise results competitive with more heavyweight approaches while being faster than them.

Návaznosti

GA23-06506S, projekt VaV

Název: Pokročilá analýza a verifikace pro pokročilý software

Investor: Grantová agentura ČR, Pokročilá analýza a verifikace pro pokročilý software

Citovat

DACÍK, Tomáš a Tomáš VOJNAR. RacerF: Lightweight Static Data Race Detection for C Code (Experience Paper). Online. In Proc. of 39th European Conference on Object-Oriented Programming – ECOOP'25. Schloss Dagstuhl: Leibniz International Proceedings in Informatics (LIPIcs), 2025, s. 1-19. ISSN 1868-8969. Dostupné z: https://doi.org/10.4230/LIPIcs.ECOOP.2025.37.

@inproceedings{2512082,
   author = {Dacík, Tomáš and Vojnar, Tomáš},
   address = {Schloss Dagstuhl},
   booktitle = {Proc. of 39th European Conference on Object-Oriented Programming – ECOOP'25},
   doi = {https://doi.org/10.4230/LIPIcs.ECOOP.2025.37},
   keywords = {program analysis;static analysis;concurrent programs;data races;},
   howpublished = {elektronická verze "online"},
   language = {eng},
   location = {Schloss Dagstuhl},
   pages = {1-19},
   publisher = {Leibniz International Proceedings in Informatics (LIPIcs)},
   title = {RacerF: Lightweight Static Data Race Detection for C Code (Experience Paper)},
   url = {https://doi.org/10.48550/arXiv.2502.04905},
   year = {2025}
}

TY  - CONF
ID  - 2512082
AU  - Dacík, Tomáš - Vojnar, Tomáš
PY  - 2025
TI  - RacerF: Lightweight Static Data Race Detection for C Code (Experience Paper)
PB  - Leibniz International Proceedings in Informatics (LIPIcs)
CY  - Schloss Dagstuhl
KW  - program analysis;static analysis;concurrent programs;data races;
UR  - https://doi.org/10.48550/arXiv.2502.04905
N2  - We present RacerF, a novel static analyser for thread-modular data race detection. The approach behind RacerF exploits static analysis of sequential program behaviour whose results are generalised for multi-threaded programs using a combination of lightweight under- and over-approximating methods. The tool is implemented as a plugin of the Frama-C platform and can leverage several analysis backends, most notably the Frama-C’s abstract interpreter EVA. Although our methods are mostly heuristic without providing formal guarantees, our experimental evaluation shows that even for intricate programs, RacerF can provide very precise results competitive with more heavyweight approaches while being faster than them.
ER  -

DACÍK, Tomáš a Tomáš VOJNAR. RacerF: Lightweight Static Data Race Detection for C Code (Experience Paper). Online. In \textit{Proc. of 39th European Conference on Object-Oriented Programming – ECOOP'25}. Schloss Dagstuhl: Leibniz International Proceedings in Informatics (LIPIcs), 2025, s.~1-19. ISSN~1868-8969. Dostupné z: https://doi.org/10.4230/LIPIcs.ECOOP.2025.37.

Přehled o publikaci