一句话：提出静态检测中断驱动程序原子性违反的方法，通过中断点选择与延迟 ISR 触发缩减状态空间，工具 CPA4AV 更精确。
中断驱动程序广泛用于航空航天与嵌入式等安全关键领域，但 ISR 的不确定交错执行常导致并发缺陷：当一个或多个 ISR 抢占本应原子执行的指令序列时，就会产生原子性违反，且难以精确高效地检测。本文提出一种静态检测方法：首先构建程序模型，通过选择中断点确定可能受影响的 ISR；随后进行可达性计算，构建完整的抽象可达树，并采用延迟 ISR 触发策略缩减状态空间；同时识别不可串行化的交错模式，以实现原子性违反检测。该方法实现为可配置工具 CPA4AV。大量实验表明，CPA4AV 相较现有相关工具精确度显著更高，仅带来很小的时间开销，且能处理更复杂的情形。
Interrupt-driven programs have been widely used in safety-critical areas such as aerospace and embedded systems. However, uncertain interleaving execution of interrupt service routines (ISRs) usually causes concurrency bugs. Specifically, when one or more ISRs attempt to preempt a sequence of instructions which are expected to be atomic, a kind of concurrency bugs namely atomicity violation may occur, and it is challenging to find this kind of bugs precisely and efficiently. In this paper, we propose a static approach for detecting atomicity violations in interrupt-driven programs. First, the program model is constructed with interruption points being selected to determine the possibly influenced ISRs. After that, reachability computation is conducted to build up a whole abstract reachability tree, and a delayed ISR-triggering strategy is employed to reduce the state space. Meanwhile, unserializable interleaving patterns are recognized to achieve the goal of atomicity violation detection. The approach has been implemented as a configurable tool namely CPA4AV. Extensive experiments show that CPA4AV is much more precise than the relative tools available with little extra time overhead. In addition, more complex situations can be dealt with CPA4AV.
@inproceedings{YuTXYS0YZLD23,
title = {Detecting Atomicity Violations in Interrupt-Driven Programs via Interruption Points Selecting and Delayed ISR-Triggering},
author = {Bin Yu and Cong Tian and Hengrui Xing and Zuchao Yang and Jie Su and Xu Lu and Jiyu Yang and Liang Zhao and Xiaofeng Li and Zhenhua Duan},
booktitle = {FSE},
year = {2023},
doi = {10.1145/3611643.3616276}
}