Interrupt-driven programs are widely deployed in safety-critical embedded systems to perform hardware and resource dependent data operation tasks. The frequent use of interrupts in these systems can cause race conditions to occur due to interactions between application tasks and interrupt handlers (or two interrupt handlers). Numerous program analysis and testing techniques have been proposed to detect races in multithreaded programs. Little work, however, has addressed race condition problems related to hardware interrupts. In this paper, we present SDRacer, an automated framework that can detect, validate and repair race conditions in interrupt-driven embedded software. It uses a combination of static analysis and symbolic execution to generate input data for exercising the potential races. It then employs virtual platforms to dynamically validate these races by forcing the interrupts to occur at the potential racing points. Finally, it provides repair candidates to eliminate the detected races. We evaluate SDRacer on nine real-world embedded programs written in C language. The results show that SDRacer can precisely detect and successfully fix race conditions.

翻译：中断驱动程序广泛应用于安全关键的嵌入式系统中，以执行与硬件及资源相关的数据处理任务。此类系统中频繁使用中断可能导致应用程序任务与中断处理程序（或两个中断处理程序）之间的交互引发竞态条件。已有大量程序分析与测试技术被提出用于检测多线程程序中的竞态，但针对硬件中断相关竞态条件问题的研究尚少。本文提出SDRacer，一个能够自动检测、验证并修复中断驱动嵌入式软件中竞态条件的自动化框架。该框架结合静态分析与符号执行来生成输入数据，以触发潜在的竞态，随后利用虚拟平台通过强制中断在潜在竞态点发生来动态验证这些竞态，最后提供修复候选方案以消除检测到的竞态。我们在九个用C语言编写的真实嵌入式程序上评估SDRacer，结果表明该框架能够精确检测并成功修复竞态条件。