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 heuristics that are aimed to reduce amount of false alarms: a memory model and a model of parallelism. We consider locks as synchronization primitives. The main target of our research and evaluation is operating system kernels but the approach may be applied to the other programs as well. The method is based on idea of Configurable Program Analysis (CPA) and was implemented in CPAchecker tool. The implementation of the method was done in two stages. Firstly, the set of shared data is determined for every program location, then the analysis of synchronization primitives is performed. On the second stage, information about all potential accesses to shared variables and acquired synchronization primitives is also collected. After analysis the report with results is created. The tool was applied to the kernel of Real-Time operating system. It has about 200 000 lines of source code. CPALocator found 20 new race conditions, which are confirmed by developers. Also, the tool was launched on the Linux device drivers using the LDV framework for preparing tasks for CPALockator. The future investigations will be related to development more precise thread model and integration with more precise heavyweight methods of static analysis.