Data Race Detection in the Linux Kernel with CPALockator

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.