Rchecker: A CBMC-based Data Race Detector for Interrupt-driven Programs

Interrupt-driven programs are widely used in aerospace, medical equipment, and other embedded systems that require extreme safety and stability. However, uncertain interrupt interleaving executions may cause serious data race problems. Static analysis is an important technology to detect data race problems. Existing methods are either too conservative to have low accuracy, or bring lots of false alarms, there still need a more effective solution. The program verification tool CBMC has an excellent performance in the analysis and verification of C multi-threaded modeling, but it doesn't support interrupt-driven programs. In this paper, we proposed a method based on CBMC to detect data race in interrupt-driven programs. Our method achieved accurate analysis of interrupt-driven programs by performing analysis toward interrupt preemption and synchronization semantics, and further validation of the program can be supported. Experiments results on related benchmarks demonstrate our approach's usability and effectiveness.