Skip to main content

Predicate abstraction based configurable method for data race detection in Linux Kernel

4Citations
Citations of this article
1Readers
Mendeley users who have this article in their library.
Get full text

Abstract

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.

Cite

CITATION STYLE

APA

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

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free