RacerF: Lightweight Static Data Race Detection for C Code

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.