Efficient data race detection for interrupt-driven programs via path feasibility analysis

Interrupt-driven programs are widely used in embedded systems with high security requirements. However, uncertain interleaving execution of tasks and interrupts may cause concurrency bugs, with data races being a significant factor in threatening security. Most of the previous research has focused on detecting data races in multi-threaded programs. And existing static analysis methods for interrupt-related data race detection often produce many false positives. This paper presents IntRace, an accurate and efficient static detection technique for interrupt data race. IntRace eliminates false data race by analyzing potential concurrency relationships and path reachability. It first identifies all race candidate pairs using access interleaving pattern matching. Then for each pair of operational accesses, IntRace analyzes potential concurrency relationships, including the special case of interrupt nesting, and uses this information to filter out access pairs that cannot concurrently access the same location. Finally, it checks the feasibility of events in the access pairs by constructing path constraints, which effectively eliminating infeasible paths in concurrent contexts. In addition, IntRace was evaluated on benchmark tests and 9 real embedded programs. The experimental results show that IntRace reduces the false positive rate by 73.2% compared to recent studies.