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)


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.


static analysis, race condition, kernel of operating system


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