Data Race Detection for Interrupt-Driven Programs via Bounded Model Checking

In Cyber-Physical Systems with interrupt mechanism, interrupts may cause unexpected interleaving executions and even wrong execution results. A kind of frequently occurred errors are caused by data race. We present an approach under the framework of bounded model checking (BMC) to detect data race for interrupt driven programs. The key idea is to automatically serialize a concurrent interrupt driven program as a non-deterministic sequential program, whose possible execution set includes all the possible executions of the interrupt driven program. Moreover, our approach checks data race in the sequential program and collects all the path condition of the data race location. On this basis, we leverage bounded model checking to convert all the path conditions into SMT formulae. Furthermore, our analysis uses a decision procedure to determine whether the formula is satisfiable, from which the analysis eliminates false alarms which can't occur in real concurrent executions. A prototype based on CBMC is implemented and preliminary experimental results are encouraging.