Static Data Race Detection for Interrupt-Driven Embedded Software

Interrupt mechanisms are widely used to process multiple concurrent tasks in the software without OS abstraction layer in various cyber physical systems (CPSs), such as space flight control systems. Data races caused by interrupt preemption frequently occur in those systems, leading to unexpected results or even severe system failures. In recent Chinese space projects, many software defects related to data races have been reported. How to detect interrupt based data races is an important issue in the quality assurance for aerospace software. In this paper, we propose a tool named Race Checker that can statically detect data races for interrupt-driven software. Given the source code or binary code of interrupt-driven software, the tool aggressively infers information such as interrupts priority states, interrupt enable states and memory accesses at each program point using our extended interprocedural data flow analysis. With the information above, it identifies the suspicious program points that may lead to data races. Race Checker is explicitly designed to find data race bugs in real-life aerospace software. Up to now, the tool has been applied in aerospace software V&V and found several severe data race bugs that may lead to system failures.