The paper presents a configurable method for static data race detection. The method is based on a lightweight approach that implements Lockset algorithm with a simplified memory model. The paper contributes two heavyweight extensions which allow to adjust required precision of the analysis by choosing the balance between spent resources and a number of false alarms. The extensions are (1) counterexample guided refinement based on predicate abstraction and (2) thread analysis. The approach was implemented in the CPALockator tool and was applied to Linux kernel modules. Real races found by the tool have been approved and fixed by Linux kernel developers.
Andrianov, P., Mutilin, V., & Khoroshilov, A. (2018). Predicate abstraction based configurable method for data race detection in Linux Kernel. In Communications in Computer and Information Science (Vol. 779, pp. 11–23). Springer Verlag. https://doi.org/10.1007/978-3-319-71734-0_2