一句话：提出混合测试框架 DD4AV，解耦输入空间与调度空间的探索，高效检测中断驱动程序的原子性违反。
中断驱动程序广泛部署于航空航天、嵌入式等安全关键领域，其行为受外部输入与中断服务例程（ISR）非确定性抢占的共同影响，极易产生原子性违反等严重并发缺陷。现有动态检测方法存在明显不足：一类仅探索调度空间而忽略输入变化，覆盖不充分；另一类虽尝试联合探索输入与调度空间，但因混合约束求解困难而遭遇性能瓶颈。为此，本文提出 DD4AV，一个混合（concolic）测试框架，其核心创新在于将经由编译式符号执行探索的输入空间与经由系统化测试探索的调度空间解耦；同时引入前缀引导的惰性测试生成策略，仅在动态执行过程中发现新程序路径时才触发约束求解与调度生成。在真实基准上的评估表明，DD4AV 在准确率与效率上均显著优于当前最先进的检测器。
Interrupt-driven programs are widely deployed in safety-critical domains such as aerospace and embedded systems. However, their behavior is determined by external inputs and the non-deterministic preemption of Interrupt Service Routines (ISRs), which can easily lead to severe concurrency bugs like atomicity violations. Existing dynamic detection methods have clear shortcomings: some explore only the scheduling space and neglect input variation, resulting in insufficient coverage, while others attempt to jointly explore both input and scheduling spaces but encounter performance bottlenecks due to the challenges of solving mixed constraints. To address this, this paper presents DD4AV as a concolic testing framework, whose core innovation lies in decoupling the input space explored via compiled symbolic execution from the scheduling space explored via systematic testing. Furthermore, a prefix-guided lazy test generation strategy is introduced so as to trigger constraint solving and schedule generation only when new program paths are discovered during dynamic execution. Evaluation on real-world benchmarks shows that DD4AV significantly outperforms state-of-the-art detectors in both accuracy and efficiency.
@inproceedings{paperbot12023,
title = {Atomicity Violation Detection for Interrupt-Driven Programs via Incrementally Exploring Concurrent Paths},
author = {Yuanzhe Liu and Bin Yu and Ruixue Li and Cheng Wen and Xu Lu and Chu Chen and Cong Tian},
booktitle = {ICSE},
year = {2026},
doi = {10.1145/3786582.3786834}
}