Atomicity Violation Detection for Interrupt-Driven Aerospace Embedded Software

The dependability of embedded software is vital to the success of the aerospace mission. Aerospace embedded software extensively uses interrupt-driven concurrency mechanisms. However, uncertain interleaving execution of interrupts may cause concurrency bugs, which could result in serious safety problems. Researches had showed that atomicity violation was the most prominent interrupt concurrency bug. Current atomicity violation detection methods for interrupt-driven embedded software cannot achieve both high precision and high scalability, and their effectiveness on real embedded software has not been evaluated. To significantly improve the ability of techniques in bug detection, we design an empirical study on 82 atomicity violations in aerospace embedded software and gain their manifestation characteristics of atomic region range, the number of interrupt nesting levels, shared data access interleaving pattern, access patterns and access granularities. On this basis, we present intAtom-S, a precise and efficient static detection technique for atomicity violations. Firstly, to realize accurate analysis of shared data, intAtom-S constructs a fine-grained memory model parameterized by numerical invariants, and introduces rule-based method to eliminate flag variable accesses. Moreover, it can handle array elements as well as shared I/O addresses. Then, a lightweight data flow analysis technique is used to find all access interleavings that match the patterns as potential bug candidates. Finally, intAtom-S adopts a consecutive access pair feasibility analysis and access interleaving feasibility analysis to prune the infeasible paths. intAtom-S gradually eliminates false positives, and obtains the final atomicity violations. Experiments on a benchmark and 8 real-world aerospace embedded software show that intAtom-S reduces the false positive rate by 72% and improves the detection speed by 3 times, compared with the state-of-the-art methods. Furthermore, it can finish analyzing the real-world aerospace embedded software very fast with an average false positive rate of 8.9%, while finding 23 bugs that had been confirmed by developers.