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]	Wang Chenze, Shen Xuehao, Huang Zhenli, Wang Zhengxia. Interactive Visualization Framework for Panoramic Super-Resolution Images Based on Localization Data[J]. Journal of Computer Research and Development, 2024, 61(7): 1741-1753. DOI: 10.7544/issn1000-1239.202330643
[2]	Fan Wei, Liu Yong. Social Network Information Diffusion Prediction Based on Spatial-Temporal Transformer[J]. Journal of Computer Research and Development, 2022, 59(8): 1757-1769. DOI: 10.7544/issn1000-1239.20220064
[3]	Zhou Weilin, Yang Yuan, Xu Mingwei. Network Function Virtualization Technology Research[J]. Journal of Computer Research and Development, 2018, 55(4): 675-688. DOI: 10.7544/issn1000-1239.2018.20170937
[4]	Yang Shuaifeng, Zhao Ruizhen. Image Super-Resolution Reconstruction Based on Low-Rank Matrix and Dictionary Learning[J]. Journal of Computer Research and Development, 2016, 53(4): 884-891. DOI: 10.7544/issn1000-1239.2016.20140726
[5]	Dou Nuo, Zhao Ruizhen, Cen Yigang, Hu Shaohai, Zhang Yongdong. Noisy Image Super-Resolution Reconstruction Based on Sparse Representation[J]. Journal of Computer Research and Development, 2015, 52(4): 943-951. DOI: 10.7544/issn1000-1239.2015.20140047
[6]	Yang Xin, Zhou Dake, Fei Shumin. A Self-Adapting Bilateral Total Variation Technology for Image Super-Resolution Reconstruction[J]. Journal of Computer Research and Development, 2012, 49(12): 2696-2701.
[7]	Wang Kai, Hou Zifeng. A Relaxed Co-Scheduling Method of Virtual CPUs on Xen Virtual Machines[J]. Journal of Computer Research and Development, 2012, 49(1): 118-127.
[8]	Wang Dan, Feng Dengguo, and Xu Zhen. An Approach to Data Sealing Based on Trusted Virtualization Platform[J]. Journal of Computer Research and Development, 2009, 46(8): 1325-1333.
[9]	Xiao Chuangbai, Yu Jing, Xue Yi. A Novel Fast Algorithm for MAP Super-Resolution Image Reconstruction[J]. Journal of Computer Research and Development, 2009, 46(5): 872-880.
[10]	Huang Hua, Fan Xin, Qi Chun, and Zhu Shihua. Face Image Super-Resolution Reconstruction Based on Recognition and Projection onto Convex Sets[J]. Journal of Computer Research and Development, 2005, 42(10): 1718-1725.