Atomicity Violation Detection for Interrupt-Driven Aerospace Embedded Software

Yu Tingting; Li Chao; Wang Boxiang; Chen Rui; Jiang Yunsong

doi:10.7544/issn1000-1239.202220908

Journal of Computer Research and Development > 2023 > 60(2): 294-310. > DOI: 10.7544/issn1000-1239.202220908 CSTR: 32373.14.issn1000-1239.202220908

Yu Tingting, Li Chao, Wang Boxiang, Chen Rui, Jiang Yunsong. Atomicity Violation Detection for Interrupt-Driven Aerospace Embedded Software[J]. Journal of Computer Research and Development, 2023, 60(2): 294-310. DOI: 10.7544/issn1000-1239.202220908

Citation:

PDF (2240 KB)

Atomicity Violation Detection for Interrupt-Driven Aerospace Embedded Software

Yu Tingting^{1, 2,},
Li Chao^{1, 2},
Wang Boxiang¹,
Chen Rui^{1, 2, ,},
Jiang Yunsong^{1, 2}

1.
Beijing Sunwise Information Technology Ltd., Beijing 100190
2.
Beijing Institute of Control Engineering, Beijing 100190

Funds: This work was supported by the National Natural Science Foundation of China (61802017, 62192730).

More Information

Received Date: October 25, 2022
Revised Date: December 28, 2022
Available Online: February 10, 2023

Graphical Abstract

Abstract

Abstract

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.
- aerospace embedded software,
- interrupt,
- concurrency bugs,
- bug characteristics,
- atomicity violation,
- static analysis

FullText(HTML)

References (33)

References

[1]	Sung C, Kusano M, Wang C. Modular verification of interrupt-driven software[C]//Proc of the 32nd IEEE/ACM Int Conf on Automated Software Engineering (ASE). Piscataway, NJ: IEEE, 2017: 206−216
[2]	Regehr J. Random testing of interrupt-driven software[C] //Proc of the 5th ACM Int Conf on Embedded Software. New York: ACM , 2005: 290−298.
[3]	中国空间技术研究院软件产品保证中心. 中国空间技术研究院软件质量问题分析报告[R]. 2015 China Academy of Space Technology Software Product Assurance Center. Analysis Report on Software Quality Problems of China Academy of Space Technology[R]. 2015(in Chinese)
[4]	陈睿, 杨孟飞, 郭向英. 基于变量访问序模式的中断数据竞争检测方法[J]. 软件学报, 2016, 27(3): 547−561 Chen Rui, Yang Mengfei, Guo Xiangying. Interrupt data race detection based on shared variable access order pattern[J]. Journal of Software, 2016, 27(3): 547−561 (in Chinese)
[5]	Flanagan C, Freund S N, Yi J. Velodrome: A sound and complete dynamic atomicity checker for multithreaded programs[C] //Proc of the ACM SIGPLAN Conf on Programming Language Design and Implementation. New York: ACM, 2008: 293–303
[6]	Park S, Harrold M J, Vuduc R. Griffin: Grouping suspicious memory-access patterns to improve understanding of concurrency bugs[C]//Proc of the Int Symp on Software Testing and Analysis. New York: ACM, 2013: 134–144
[7]	Park S, Vuduc R, Harrold M J. unicorn: A unified approach for localizing non-deadlock concurrency bugs[C] //Proc of the Software Testing, Verification and Reliability. Hoboken: Wiley, 2015: 167–190
[8]	Razavi N, Farzan A, McIlraith S A. Generating effective tests for concurrent programs via AI automated planning techniques[J]. International Journal on Software Tools for Technology Transfer, 2014, 16(1): 49−65
[9]	Sorrentino F, Farzan A, Madhusudan P. PENELOPE: Weaving threads to expose atomicity violations[C] //Proc of the 18th ACM SIGSOFT Int Symp on Foundations of Software Engineering. New York: ACM, 2010: 37–46
[10]	Wang Chao, Limaye R, Ganai M, et al. Trace-based symbolic analysis for atomicity violations[C] //Proc of the Int Conf on Tools and Algorithms for the Construction and Analysis of Systems. Berlin: Springer, 2010: 328–342
[11]	Park S. Fault comprehension for concurrent programs[C] //Proc of the 35th Int Conf on Software Engineering (ICSE). Piscataway, NJ: IEEE, 2013: 1444–1446
[12]	Park S, Vuduc R W, Harrold M J. Falcon: Fault localization in concurrent programs[C] //Proc of the 32nd ACM/IEEE Int Conf on Software Engineering. Piscataway, NJ: IEEE, 2010: 245–254
[13]	Sadowski C, Freund S N, Flanagan C. SingleTrack: A dynamic determinism checker for multithreaded programs[C] //Proc of the European Symp on Programming. Berlin: Springer. 2009: 394–409
[14]	Wang Liqiang, Stoller S D. Accurate and efficient runtime detection of atomicity errors in concurrent programs[C] //Proc of the 11th ACM SIGPLAN Symp on Principles and Practice of Parallel Programming. New York: ACM, 2006: 137–146
[15]	Feng Haining, Yin Liangze, Lin Wenfeng, et al. Rchecker: A cbmc-based data race detector for interrupt-driven programs[C] //Proc of the IEEE 20th Int Conf on Software Quality, Reliability and Security Companion (QRS-C). Piscataway, NJ: IEEE, 2020: 465–471
[16]	Racebench website. 2019.https://github.com/chenruibuaa/racebench.
[17]	Li Chao, Chen Rui, Wang Boxiang, et al. Precise and efficient atomicity violation detection for interrupt-driven programs via staged path pruning[C] //Proc of the 31st ACM SIGSOFT Int Symp on Software Testing and Analysis, New York: ACM, 2022: 506–518.
[18]	Wang Boxiang, Chen Rui, Li Chao, et al. SpecChecker-ISA: A data sharing analyzer for interrupt-driven embedded software[C] //Proc of the 31st ACM SIGSOFT Int Symp on Software Testing and Analysis. New York: ACM, 2022: 801−804
[19]	Wang Yu, Wang Linzhang, Yu Tingting, et al. Automatic detection and validation of race conditions in interrupt-driven embedded software[C] //Proc of the 26th ACM SIGSOFT Int Symp on Software Testing and Analysis. New York: ACM, 2017: 113–124
[20]	Lu Shan, Tucek J, Qin Feng, et al. AVIO: Detecting atomicity violations via access interleaving invariants[C] //Proc of the Int Conf on Architectural Support for Programming Languages & Operating Systems. New York: ACM, 2006: 37–48
[21]	Codish M, Mulkers A, Bruynooghe M, et al. Improving abstract interpretations by combining domains[J]. ACM Transactions on Programming Languages and Systems, 1995, 17(1): 28−44
[22]	Vaziri M, Tip F, Dolby J. Associating synchronization constraints with data in an object-oriented language[J]. ACM Sigplan Notices, 2006, 41(1): 334−345
[23]	DG website. 2021.https://github.com/mchalupa/dg
[24]	Shi Qingkai, Xiao Xiao, Wu Rongxin, et al. Pinpoint: Fast and precise sparse value flow analysis for million lines of code[C] //Proc of the 39th ACM SIGPLAN Conf on Programming Language Design and Implementation. New York: ACM, 2018: 693–706
[25]	Snelting G, Robschink T, Krinke J. Efficient path conditions in dependence graphs for software safety analysis[C] //Proc of the ACM Transactions on Software Engineering and Methodology (TOSEM). New York: ACM, 2006: 410–457
[26]	Huang J. Scalable thread sharing analysis[C] //Proc of the 38th Int Conf on Software Engineering. Piscataway, NJ: IEEE, 2016: 1097–1108
[27]	Lu Shan, Park S, Zhou Yuanyuan. Finding atomicity-violation bugs through unserializable interleaving testing[C] //Proc of the IEEE Transactions on Software Engineering. Piscataway, NJ: IEEE, 2011: 844–860
[28]	Lucia B, Devietti J, Strauss K, et al. Atom-aid: Detecting and surviving atomicity violations[C] //Proc of the 2008 Int Symp on Computer Architecture. Piscataway, NJ: IEEE, 2008: 277–288
[29]	Chew L, Lie D. Kivati: Fast detection and prevention of atomicity violations[C] //Proc of the 5th European Conf on Computer Systems. New York: ACM, 2010: 307–320
[30]	Chopra N, Pai R, D’Souza D. Data races and static analysis for interrupt-driven kernels[C] //Proc of the European Symp on Programming. New York: Springer, 2019: 697–723
[31]	Yu Tingting, Srisa-an W, Rothermel G. 2012. SimTester: A controllable and observable testing framework for embedded systems[C] //Proc of the 8th ACM SIGPLAN/SIGOPS Conf on Virtual Execution Environments. New York: ACM, 2012: 51–62
[32]	Wu Xueguang, Wen Yanjun, Chen Liqian, et al. Data race detection for interrupt-driven programs via bounded model checking[C] //Proc of the IEEE Seventh Int Conf on Software Security and Reliability Companion. Piscataway, NJ: IEEE, 2013: 204–210
[33]	Wu Xueguang, Chen Liqian, Miné A, et al. Static analysis of run-time errors in interrupt-driven programs via sequentialization[J]. ACM Transactions on Embedded Computing Systems, 2016, 15（4）: 1−26

[1]	Lin Hanyue, Wu Jingya, Lu Wenyan, Zhong Langhui, Yan Guihai. Neptune: A Framework for Generic Network Processor Microarchitecture Modeling and Performance Simulation[J]. Journal of Computer Research and Development, 2025, 62(5): 1091-1107. DOI: 10.7544/issn1000-1239.202440084
[2]	Zhang Qianlong, Hou Rui, Yang Sibo, Zhao Boyan, Zhang Lixin. The Role of Architecture Simulators in the Process of CPU Design[J]. Journal of Computer Research and Development, 2019, 56(12): 2702-2719. DOI: 10.7544/issn1000-1239.2019.20190044
[3]	Liu He, Ji Yu, Han Jianhui, Zhang Youhui, Zheng Weimin. Training and Software Simulation for ReRAM-Based LSTM Neural Network Acceleration[J]. Journal of Computer Research and Development, 2019, 56(6): 1182-1191. DOI: 10.7544/issn1000-1239.2019.20190113
[4]	Yang Meifang, Che Yonggang, Gao Xiang. Heterogeneous Parallel Optimization of an Engine Combustion Simulation Application with the OpenMP 4.0 Standard[J]. Journal of Computer Research and Development, 2018, 55(2): 400-408. DOI: 10.7544/issn1000-1239.2018.20160872
[5]	Liu Yuchen, Wang Jia, Chen Yunji, Jiao Shuai. Survey on Computer System Simulator[J]. Journal of Computer Research and Development, 2015, 52(1): 3-15. DOI: 10.7544/issn1000-1239.2015.20140104
[6]	Lü Huiwei, Cheng Yuan, Bai Lu, Chen Mingyu, Fan Dongrui, Sun Ninghui. Parallel Simulation of Many-Core Processor and Many-Core Clusters[J]. Journal of Computer Research and Development, 2013, 50(5): 1110-1117.
[7]	Yu Lisheng, Zhang Yansong, Wang Shan, and Zhang Qian. Research on Simulative Column-Storage Model Policy Based on Row-Storage Model[J]. Journal of Computer Research and Development, 2010, 47(5): 878-885.
[8]	Liu Shiguang, Chai Jiawei, Wen Yuan. A New Method for Fast Simulation of 3D Clouds[J]. Journal of Computer Research and Development, 2009, 46(9): 1417-1423.
[9]	Mao Chengying, Lu Yansheng. Strategies of Regression Test Case Selection for Component-Based Software[J]. Journal of Computer Research and Development, 2006, 43(10): 1767-1774.
[10]	Wang Shihao, Wang Xinmin, Liu Mingye. Software Simulation for Hardware/Software Co-Verification[J]. Journal of Computer Research and Development, 2005, 42(3).