Data Race Detection in the Linux Kernel with CPALockator

Authors

  • Pavel Andrianov Ivannikov Institute for System Programming of the RAS
  • Vadim Mutilin Ivannikov Institute for System Programming of the RAS

DOI:

https://doi.org/10.14279/tuj.eceasst.79.1115

Abstract

Most of the state-of-the-art verification tools do not scale well on complicated software. Our goal was to develop a tool, which becomes a golden mean between precise and slow software model checkers and fast and imprecise static analyzers.
It allows verifying industrial software more efficiently.
Our method is based on the Thread-Modular approach elaborating the idea of abstraction from precise thread interaction and considering every thread separately, but in a special environment, which models thread effects on each other.
The approach was implemented in the CPAchecker framework and was evaluated on benchmarks based on Linux device drivers for data race detection. It demonstrated that predicate abstraction allows keeping a false alarms rate at a reasonable level of 52\%. Moreover, it did not miss known real bugs found by analysis of commits in the Linux kernel repository thus confirming the soundness of the approach.

Downloads

Published

2021-05-10

How to Cite

[1]
P. Andrianov and V. Mutilin, “Data Race Detection in the Linux Kernel with CPALockator”, eceasst, vol. 79, May 2021.