RacerF: Lightweight Static Data Race Detection for C Code

TL;DR

RacerF is a lightweight static analysis tool for detecting data races in C programs, combining static sequential analysis with multi-threaded generalization, achieving a good balance of precision and speed.

Contribution

The paper introduces RacerF, a novel static analysis approach for data race detection that is lightweight, flexible, and integrates with existing tools like Frama-C.

Findings

RacerF provides precise data race detection results.

It operates faster than traditional heavy-weight methods.

It is effective on complex multi-threaded C programs.

Abstract

We present a novel static analysis for thread-modular data race detection. Our approach 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. We have implemented this approach in a new tool called RacerF as a plugin of the Frama-C platform. RacerF 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 heavy-weight approaches while being faster than them.