Document Open Access Logo

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

Authors Tomáš Dacík , Tomáš Vojnar

PDF

File

Thumbnail PDF
PDF
LIPIcs.ECOOP.2025.37.pdf
  • Filesize: 1.23 MB
  • 19 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Software and its engineering → Automated static analysis
Keywords
  • concurrency
  • data race detection
  • static analysis

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

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.

Cite As Get BibTex

Tomáš Dacík and Tomáš Vojnar. RacerF: Lightweight Static Data Race Detection for C Code (Experience Paper). In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 37:1-37:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.ECOOP.2025.37

Author Details

Tomáš Dacík
  • Faculty of Information Technology, Brno University of Technology, Czech Republic
Tomáš Vojnar
  • Faculty of Informatics, Masaryk University, Brno, Czech Republic
  • Faculty of Information Technology, Brno University of Technology, Czech Republic

Funding

The research was supported by the Czech Science Foundation project 23-06506S and the FIT BUT internal project FIT-S-23-8151. Tomáš Dacík was also supported by the Brno PhD Talent Scholarship of the Brno City Municipality. The research involved discussions with Julien Signoles from the Frama-C team at CEA that were supported by the project VASSAL: "Verification and Analysis for Safety and Security of Applications in Life" funded by the European Union under Horizon Europe WIDERA Coordination and Support Action/Grant Agreement No. 101160022.

Acknowledgements

We appreciate discussions on the subject with Julien Signoles from the Frama-C team at CEA, France and with Adam Rogalewicz from FIT BUT, Czechia.

Supplementary Materials

References

  1. Patrick Baudin, François Bobot, David Bühler, Loïc Correnson, Florent Kirchner, Nikolai Kosmatov, André Maroneze, Valentin Perrelle, Virgile Prevosto, Julien Signoles, and Nicky Williams. The Dogged Pursuit of Bug-Free C Programs: The Frama-C Software Analysis Platform. Commun. ACM, 64(8):56-68, 2021. URL: https://doi.org/10.1145/3470569.
  2. Dirk Beyer, Stefan Löwe, and Philipp Wendler. Reliable Benchmarking: Requirements and Solutions. International Journal on Software Tools for Technology Transfer, 21(1):1-29, 2019. URL: https://doi.org/10.1007/s10009-017-0469-y.
  3. Dirk Beyer and Jan Strejček. Improvements in Software Verification and Witness Validation: SV-COMP 2025. In Proc. of TACAS'25, LNCS, 2025. Google Scholar
  4. Sam Blackshear, Nikos Gorogiannis, Peter W. O'Hearn, and Ilya Sergey. RacerD: Compositional static race detection. Proc. of ACM Program. Lang., 2(OOPSLA), 2018. URL: https://doi.org/10.1145/3276514.
  5. Allan Blanchard, Loïc Correnson, Tristan Le Gall, Jan Rochel, and Julien Signoles. Alias, Efficient May-alias and Points-to Analysis. URL: https://www.frama-c.com/fc-plugins/alias.html.
  6. Sandrine Blazy, David Bühler, and Boris Yakobowski. Structuring Abstract Interpreters Through State and Value Abstractions. In Proc. of VMCAI, pages 112-130, 2017. URL: https://doi.org/10.1007/978-3-319-52234-0_7.
  7. François Bourdoncle. Efficient Chaotic Iteration Strategies with Widenings. In Formal Methods in Programming and Their Applications, 1993. Google Scholar
  8. David Bühler, Pascal Cuoq, and Boris Yakobowski. The Eva Plug-in (For Frama-C 30.0). Available from URL: https://frama-c.com/download/frama-c-eva-manual.pdf.
  9. Sylvain Conchon, Jean-Christophe Filliâtre, and Julien Signoles. Designing a Generic Graph Library using ML Functors. In Symposium on Trends in Functional Programming, 2007. Google Scholar
  10. Pascal Cuoq, Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, and Boris Yakobowski. Frama-C: A Software Analysis Perspective. In Proc. of SEFM, pages 233-247, 2012. URL: https://doi.org/10.1007/978-3-642-33826-7_16.
  11. Tomáš Dacík and Tomáš Vojnar. TDacik/Deadlock_and_Racer. Software, (visited on 2025-06-18). URL: https://github.com/TDacik/Deadlock_and_Racer
    Software Heritage Logo archived version
    full metadata available at: https://doi.org/10.4230/artifacts.23614
  12. Daniel Dietsch, Matthias Heizmann, Dominik Klumpp, Mehdi Naouar, Andreas Podelski, and Claus Schätzle. Verification of Concurrent Programs Using Petri Net Unfoldings. In Proc. of VMCAI, pages 174-195, 2021. URL: https://doi.org/10.1007/978-3-030-67067-2_9.
  13. Orit Edelstein, Eitan Farchi, Evgeny Goldin, Yarden Nir, Gil Ratsaby, and Shmuel Ur. Framework for Testing Multi-threaded Java Programs. Concurrency and Computation: Practice and Experience, 15(3-5), 2003. URL: https://doi.org/10.1002/cpe.654.
  14. Tayfun Elmas, Shaz Qadeer, and Serdar Tasiran. Goldilocks: A Race and Transaction-aware Java Runtime. In Proc. of PLDI'07. ACM, 2007. URL: https://doi.org/10.1145/1273442.1250762.
  15. Dawson Engler and Ken Ashcraft. RacerX: Effective, Static Detection of Race Conditions and Deadlocks. SIGOPS Oper. Syst. Rev., 37(5):237-252, 2003. URL: https://doi.org/10.1145/1165389.945468.
  16. Hongyu Fan, Zhihang Sun, and Fei He. Satisfiability Modulo Ordering Consistency Theory for SC, TSO, and PSO Memory Models. ACM Trans. Program. Lang. Syst., 45(1), 2023. URL: https://doi.org/10.1145/3579835.
  17. J. Fiedor, V. Hrubá, B. Křena, Z. Letko, S. Ur, and T. Vojnar. Advances in Noise-Based Testing of Concurrent Software. Software Testing Verification and Reliability, 25(3):272-309, 2015. URL: https://doi.org/10.1002/stvr.1546.
  18. Jan Fiedor and Tomas Vojnar. Noise-based Testing and Analysis of Multi-Threaded C/C++ Programs on the Binary Level. 2012 10th Workshop on Parallel and Distributed Systems: Testing, Analysis, and Debugging, PADTAD 2012 - Proceedings, 2012. URL: https://doi.org/10.1145/2338967.233681.
  19. C. Flanagan and S. Freund. FastTrack: Efficient and Precise Dynamic Race Detection. In Proc. of PLDI'09. ACM, 2009. URL: https://doi.org/10.1145/1543135.1542490.
  20. Natalia Gavrilenko, Hernán Ponce-de León, Florian Furbach, Keijo Heljanko, and Roland Meyer. BMC for Weak Memory Models: Relation Analysis for Compact SMT Encodings. In Proc. of CAV, pages 355-365, 2019. URL: https://doi.org/10.1007/978-3-030-25540-4_19.
  21. Fei He, Zhihang Sun, and Hongyu Fan. Deagle: An SMT-based Verifier for Multi-threaded Programs (Competition Contribution). In Proc. of TACAS'22, pages 424-428, 2022. URL: https://doi.org/10.1007/978-3-030-99527-0_25.
  22. M. Heizmann, M. Bentele, D. Dietsch, X. Jiang, D. Klumpp, F. Schüssele, and A. Podelski. Ultimate Automizer and the Abstraction of Bitwise Operations (Competition Contribution). In Proc. of TACAS'24, LNCS 14572, pages 418-423, 2024. URL: https://doi.org/10.1007/978-3-031-57256-2_31.
  23. Dominik Klumpp, Daniel Dietsch, Matthias Heizmann, Frank Schüssele, Marcel Ebbinghaus, Azadeh Farzan, and Andreas Podelski. Ultimate GemCutter and the Axes of Generalization. In Proc. TACAS'22, pages 479-483, 2022. URL: https://doi.org/10.1007/978-3-030-99527-0_35.
  24. Daniel Kästner, Antoine Miné, Laurent Mauborgne, X. Rival, Jérôme Feret, Patrick Cousot, Stephan Wilhelm, and Christian Ferdiand. Taking Static Analysis to the Next Level: Proving the Absence of Run-Time Errors and Data Races with Astrée. In In ERTS’16, 2016. Google Scholar
  25. A. Lal and T. Reps. Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis. In Proc. of CAV'08, pages 37-51, 2008. URL: https://doi.org/10.1007/978-3-540-70545-1_7.
  26. B. Liu, P. Liu, Y. Li, C.-C. Tsai, D. Da Silva, and J. Huang. When Threads Meet Events: Efficient and Precise Static Race Detection with Origins. In Proc. of PLDI'21. ACM, 2021. URL: https://doi.org/10.1145/3453483.345407.
  27. Antoine Miné. Relational Thread-Modular Static Value Analysis by Abstract Interpretation. In Proc. of VMCAI, pages 39-58, 2014. URL: https://doi.org/10.1007/978-3-642-54013-4_3.
  28. T. Nguyen, B. Fischer, S. Torre, and G. Parlato. Lazy sequentialization for the safety verification of unbounded concurrent programs. In Proc. of ATVA'16, volume 9938 of LNCS, 2016. URL: https://doi.org/10.1007/978-3-319-46520-3_12.
  29. S. Saan, J. Erhard, M. Schwarz, S. Bozhilov, K. Holter, S. Tilscher, V. Vojdani, and H. Seidl. Goblint: Abstract Interpretation for Memory Safety and Termination (Competition Contribution). In Proc. of TACAS'24, LNCS 14572, pages 381-386, 2024. URL: https://doi.org/10.1007/978-3-031-57256-2_25.
  30. Stefan Savage, Michael Burrows, Greg Nelson, Patrick Sobalvarro, and Thomas Anderson. Eraser: A Dynamic Data Race Detector for Multithreaded Programs. ACM Transactions on Computer Systems (TOCS), 15(4):391-411, 1997. URL: https://doi.org/10.1145/265924.265927.
  31. Bjarne Steensgaard. Points-to Analysis in Almost Linear Time. In Proc. of POPL'96, pages 32-41, 1996. URL: https://doi.org/10.1145/237721.237727.
  32. Vesal Vojdani, Kalmer Apinis, Vootele Rõtov, Helmut Seidl, Varmo Vene, and Ralf Vogler. Static Race Detection for Device Drivers: the Goblint Approach. In Proc. of ASE, pages 391-402, 2016. URL: https://doi.org/10.1145/2970276.2970337.
  33. J. Wu, Y. Tang, H. Hu, H. Cui, and J. Yang. Sound and Precise Analysis of Parallel Programs through Schedule Specialization. In Proc. of PLDI'12. ACM, 2012. URL: https://doi.org/10.1145/2345156.2254090.
  34. Boris Yakobowski and Richard Bonichon. The Mthread plugin. Available from URL: https://frama-c.com/download/frama-c-mthread-manual.pdf.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact