Proceedings of ISP RAS


Adjustable method with predicate abstraction for detection of race conditions in operating systems

P.S. Andrianov (ISP RAS, Moscow, Russia)
V.S. Mutilin (ISP RAS, Moscow, Russia)
A.V. Khoroshilov (ISP RAS, Moscow, Russia, MSU, Moscow, Russia, MIPT, Dolgoprudny, Russia, HSE, Moscow, Russia)

Abstract

The paper presents a configurable method of static data race detection that is trying to keep a balance between resource consumption and a number of false alarms. The method is based on well known Lockset approach. It uses simplified memory model to be fast enough. At the same time it includes advanced techniques aimed to achieve acceptable false alarms rate. The key techniques are thread analysis and predicate abstraction based refinement. The method was implemented in CPALockator tool built on top of CPAchecker framework. The tool was evaluated on Linux kernel modules and it has detected several actual data races, which were approved by developers and were fixed in upstream Linux kernel.

Keywords

static analysis, race condition, kernel of operating system

Edition

Proceedings of the Institute for System Programming, vol. 28, issue 6, 2016, pp. 65-86.

ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).

DOI: 10.15514/ISPRAS-2016-28(6)-5

Full text of the paper in pdf (in Russian) Back to the contents of the volume