微信服务号

微信订阅号

2025-4-16- 7
Home > Archive>Volume 27, Issue 3, 2016 >547-561. DOI:10.13328/j.cnki.jos.004980
PDF HTML XML Export Cite reminder
Interrupt Data Race Detection Based on Shared Variable Access Order Pattern
Author:
Affiliation:

Fund Project:

National Natural Science Foundation of China (91118007)

  • Article
    • | |
  • Metrics
    • |
  • Reference [30]
    • |
  • Related [20]
    • |
  • Cited by
    • | |
  • Comments
    Abstract:

    Interrupt data race is a category of critical bugs in interrupt-driven software such as aerospace embedded software.However, interrupt is much different from thread or task on concurrency semantics, synchronization and schedule, and its ad-hoc characteristics is hard to describe.Thus the state-of-art data race detection techniques are not suitable to interrupt-driven software.In this paper, the data race bug repository of aerospace embedded software is reviews systematically, and seven bug patterns for harmful interrupt data race are proposed.For the pattern single variable access order, an efficient abstract interpretation based detection method is developed to support inter-procedural and interrupt concurrency analysis.A tool named SpaceDRC is designed to verify our method.The evaluation results show that SpaceDRC only takes 145ms to detect 21400 lines of code to find the true bugs.Up to now, SpaceDRC has been applied in several aerospace missions, increasing the efficiency of interrupt data race inspection by 5 times and making a significant reduction in bug omission rate.

    Reference
    [1] Leveson NG, Turner C. An investigation of the Therac-25 accidents. IEEE Computer, 1993,16(7):18-41.[doi:10.1109/MC.1993. 274940]
    [2] US-Canada power system outage task force. Final Report on the August 14. 2003 Blackout in the United States and Canada:Causes and Recommendations, 2004. http://energy.gov/sites/prod/files/oeprod/DocumentsandMedia/BlackoutFinal-Web.pdf
    [3] Duan YH, Chen R. Heuristic static data race detection for interrupt-driven software. Computer Engineering and Design, 2013,34(1):140-145(in Chinese with English abstract).[doi:10.3969/j.issn.1000-7024.2013.01.027]
    [4] Chen R, Guo XY, Duan YH, Gu B, Yang MF. Static data race detection for interrupt-driven embedded software. In:Proc. of the Int'l Conf. on Secure Integration and Reliability Improvement. IEEE Reliability Society, 2011. 47-52.[doi:10.1109/SSIRI-C. 2011.18]
    [5] Pratikakis P, Foster J, Hicks M. LOCKSMITH:Context sensitive correlation analysis for race detection. In:Proc. of the ACM SIGPLAN 2006 Conf. on Programming Language Design and Implementation(PLDI). ACM Press, 2006. 320-331.[doi:10.1145/1133981.1134019]
    [6] Li KQ, Chen SM, Zheng WJ. A dynamic detective algorithm based on lockset to solve multithreaded data race. Wuhan University Journal of Natural Sciences, 2000,46(3):289-292(in Chinese with English abstract).[doi:10.3321/j.issn:1671-8836.2000.03.008]
    [7] Zhang LB, Zhang FX, Wu SG, Chen YY. A lockset-based dynamic data race detection approach. Chinese Journal of Computers, 2003,26(10):1217-1223(in Chinese with English abstract).[doi:10.3321/j.issn:0254-4164.2003.10.001]
    [8] Lamport L. Time, clocks, and the ordering of events in a distributed system. Communications of the ACM, 1978,21(7):558-565.[doi:10.1145/359545.359563]
    [9] Savage S, Burrows M, Nelson G, Sobalvarro P, Anderson TE. Eraser:A dynamic data race detector for multi-threaded programs. ACM Trans. on Computer Systems, 1997,15(4):391-411.[doi:10.1145/265924.265927].
    [10] Wu P, Chen YY, Zhang J. Static data-race detection for multithread programs. Journal of Computer Research and Development, 2006,43(2):329-335(in Chinese with English abstract). http://crad.ict.ac.cn/CN/Y2006/V43/I2/329
    [11] O'Callahan R, Choi J. Hybrid dynamic data race detection. In:Proc. of the ACM SIGPLAN Symp. on Principles and Practice of Parallel Programming(PPoPP 2003). 2003. 167-178.[doi:10.1145/966049.781528]
    [12] Regehr J, Cooprider N. Interrupt verification via thread verification. Electronic Notes Theoretical Computer Science, 2007,174:139-150.[doi:10.1016/j.entcs.2007.04.002]
    [13] Henzinger TA, Jhala R, Majumdar R, Sutre G. Software verification with Blast. In:Proc. of the 10th Int'l Workshop on Model Checking of Software(SPIN 2003). 2003. 235-239.[doi:10.1007/3-540-44829-2_17]
    [14] Mercer EG, Jones MD. Model checking machine code with the GNU debugger. In:Proc. of the SPIN Workshop on Model Checking of Software(SPIN 2005). 2005. 251-265.[doi:10.1007/11537328_20]
    [15] Palsberg J, Ma D. A typed interrupt calculus. In:Proc. of the 7th Int'l Symp. on Formal Techniques in Real-Time and Fault-Tolerant Systems(FTRTFT 2002). 2002. 291-310.[doi:10.1007/3-540-45739-9_18]
    [16] Cooprider N. Data-Flow analysis for interrupt-driven microcontroller software[Ph.D. Thesis]. University of Utah, 2008.
    [17] Kroening D, Liang LH, Melham T, Schrammel P, Tautschnig M. Effective verification of low-level software with nested interrupts. In:Proc. of the 2015 Design, Automation & Test in Europe Conf. & Exhibition. 2015. 229-234.
    [18] Han L, Zhang HH, Jiang Y, Song XY, Gu M, Sun JG. iDola:Bridge modeling to verification and implementation of interruptdriven systems. In:Proc. of the Theoretical Aspects of Software Engineering Conf.(TASE). 2014. 193-200.[doi:10.1109/TASE. 2014.33]
    [19] Zhou XY, Gu B, Zhao JH, Yang MF, Li XD. Model checking technique for interrupt-driven system. Ruan Jian Xue Bao/Journal of Software, 2015,26(9):2221-2230(in Chinese with English abstract). http://www.jos.org.cn/1000-9825/4713.htm[doi:10.13328/j. cnki.jos.004713]
    [20] Wu XG, Wen YJ, Chen LQ, Dong W, Wang J. Data race detection for interrupt-driven programs via bounded model checking. In:Proc. of the IEEE 7th Int'l Conf. on Software Security and Reliability-Companion(SERE-C). IEEE Computer Society, 2013. 204-210.[doi:10.1109/SERE-C.2013.33].
    [21] Huo W, Yu HT, Feng XB, Zhang ZQ. Static race detection of interrupt-driven programs. Journal of Computer Research and Development, 2011,48(12):2290-2299(in Chinese with English abstract). http://crad.ict.ac.cn/CN/Y2011/V48/I12/2290
    [22] Chen YJ, Shi JJ, Wang LZ, Li XD. Data race detection tool for interrupt-driven embedded system. Journal of Frontiers of Computer Science and Technology, 2015,9(8):914-912(in Chinese with English abstract).[doi:10.3778/j.jssn.1673-9418.1411052]
    附中文参考文献:
    [3] 段永颢,陈睿.基于启发式的静态中断数据竞争检测方法.计算机工程与设计,2013,34(1):140-145.[doi:10.3969/j.issn.1000-7024. 2013.01.027]
    [6] 李克清,陈莘萌,郑无疾.一种基于锁集的多线程数据竞争的动态探测算法.武汉大学学报(自然科学版),2000,46(3):289-292.[doi:10.3321/j.issn:1671-8836.2000.03.008]
    [7] 章隆兵,张福新,吴少刚,陈意云.基于锁集合的动态数据竞争检测方法.计算机学报,2003,26(10):1217-1223.[doi:10.3321/j.issn:0254-4164.2003.10.001]
    [10] 吴萍,陈意云,张健.多线程程序数据竞争的静态检测.计算机研究与发展,2006,43(2):329-335. http://crad.ict.ac.cn/CN/Y2006/V43/I2/329
    [19] 周筱羽,顾斌,赵建华,杨孟飞,李宣东.中断驱动系统模型检验.软件学报,2015,26(9):2221-2230. http://www.jos.org.cn/1000-9825/4713.htm[doi:10.13328/j.cnki.jos.004713]
    [21] 霍玮,于洪涛,冯晓兵,张兆庆.静态检测中断驱动程序的数据竞争.计算机研究与发展,2011,48(12):2290-2299. http://crad.ict.ac. cn/CN/Y2011/V48/I12/2290
    [22] 陈园军,石浚菁,王林章,李宣东.中断驱动的嵌入式系统数据竞争检测工具.计算机科学与探索,2015.[doi:10.3778/j.jssn.1673-9418.1411052]
    Cited by
    Comments
    Comments
    分享到微博
    Submit
Get Citation

陈睿,杨孟飞,郭向英.基于变量访问序模式的中断数据竞争检测方法.软件学报,2016,27(3):547-561

Copy
Share
Article Metrics
  • Abstract:5039
  • PDF: 8092
  • HTML: 2673
  • Cited by: 0
History
  • Received:July 14,2015
  • Revised:October 20,2015
  • Online: January 06,2016
Links:Institute of Software, CASChina Computer FederationCASNSFC
You are the first2035254Visitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address：4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code：100190
Phone：010-62562563 Fax：010-62562533 Email：jos@iscas.ac.cn
Technical Support：Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063