Lightweight Static Analysis for Data Race Detection in Operating System Kernels

The paper presents an approach to lightweight static data race detection, called CPALockator. It takes into account the specifics of operating system kernels, such as complex parallelism and kernel specifics synchronization mechanisms. The method is based on the Lockset one, but it implements two he...

Full description

Bibliographic Details
Main Authors: P. S. Andrianov, V. S. Mutilin, A. V. Khoroshilov
Format: Article
Language:English
Published: Ivannikov Institute for System Programming of the Russian Academy of Sciences 2018-10-01
Series:Труды Института системного программирования РАН
Subjects:
Online Access:https://ispranproceedings.elpub.ru/jour/article/view/677
Description
Summary:The paper presents an approach to lightweight static data race detection, called CPALockator. It takes into account the specifics of operating system kernels, such as complex parallelism and kernel specifics synchronization mechanisms. The method is based on the Lockset one, but it implements two heuristics that are aimed to reduce amount of false alarms: a memory model and a model of parallelism. The main target of our research and evaluation is operating system kernels but the approach can be applied to the other programs as well.
ISSN:2079-8156
2220-6426