Atomicity Violation Detection for Interrupt-Driven Programs via Incrementally Exploring Concurrent Paths
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.