计算机科学 ›› 2020, Vol. 47 ›› Issue (6): 24-31.doi: 10.11896/jsjkx.191100187

• 智能软件工程 • 上一篇    下一篇

一种解决嵌入式软件并发缺陷的建模方法

崔凯1, 赵国亮2, 周宽久1, 李明楚1   

  1. 1 大连理工大学软件学院 辽宁 大连116620
    2 北京大学软件与微电子学院 北京102600
  • 收稿日期:2019-11-25 出版日期:2020-06-15 发布日期:2020-06-10
  • 通讯作者: 周宽久(zhoukj@dlut.edu.cn)
  • 作者简介:ck.dut@163.com
  • 基金资助:
    国家自然科学基金(61872052,61772113,61733002); 中央高校基本科研业务费专项资金(DUT2019ZD104)

Model of Embedded Software for Solving Concurrent Defects

CUI Kai1, ZHAO Guo-liang2, ZHOU Kuan-jiu1, LI Ming-chu1   

  1. 1 School of Software,Dalian University of Technology,Dalian,Liaoning 116620,China
    2 School of Software & Microelectronics,Peking University,Beijing 102600,China
  • Received:2019-11-25 Online:2020-06-15 Published:2020-06-10
  • About author:CUI Kai,born in 1983,Ph.D candidate.His main research interests include software testing,software reliability and formal method.
    ZHOU Kuan-jiu,born in 1966,PH.D,professor,is a member of China Computer Federation.His main research interests include formal method,model checking and software reliability.
  • Supported by:
    This work was supported by the National Natural Science Foundation of China (61872052,61772113,61733002) and Fundamental Research Funds for the Central Universities of Ministry of Education of China (DUT2019ZD104)

摘要: 嵌入式并发软件的中断嵌套和线程交织等程序的随机性和不确定性(Randomicity and Nondeterminism)会引起数据竞争(Data Race)和原子性违背(Atomicity Violations)等并发缺陷问题,并且这些问题很难被修复和重新构建。针对嵌入式软件中的数据竞争和原子性违背这类并发缺陷问题,文中提出了瘦中断处理(Thin Interrupt Service Routine,Thin ISR)方式。首先,利用状态迁移矩阵(State Transition Matrix,STM)进行建模,把中断处理程序中与访问共享变量相关的程序段移植到主程序中,即中断处理程序只负责将外界中断请求数据存到缓冲区中,中断的具体处理由主程序完成;然后,利用构建的STM模型生成对应的C代码,这样可以有效地避免原子性违背和数据竞争等并发缺陷;最后,利用排队方法对中断的到达时间与离开时间进行仿真。实验结果验证了本方法在解决数据竞争和原子性违背等并发缺陷问题方面的可行性与有效性。

关键词: 中断嵌套, 数据竞争, 原子性违背, 状态迁移矩阵, 瘦中断

Abstract: Randomicity and nondeterminism of programs such as interrupts nesting or threads interleaving in embedded software can lead to concurrent defects such as data race and atomicity violations.Meanwhile,the insidious programming errors are difficult to restore and rebuild.Aiming at the concurrent defects of data race and atomicity violations in embedded software,a thin interrupt service routine (thin ISR) method is proposed in this paper.By using the state transition matrix (STM) to model,the program segments relatedto accessing shared variables in the interrupt processing program are migrated to the main program.The interrupt handler is only responsible for storing the external interrupt request data in the buffer,and the function of interrupt services is executed in the main program.Then the corresponding C codes are generated by the STM model.This method can efficiently avoid the happening of concurrent defects,such as data race and atomicity violations.Finally,queuing theory method is used to simulatethe arrival time and the departure time of the interrupt.Experimental results verify that this approach is feasible and effective in solving data race and atomicity violations.

Key words: Interrupt nesting, Data race, Atomicity violation, State transition matrix, Thin interrupt service routine

中图分类号: 

  • TP306
[1]ENGLER D,ASHCRAFT K.RacerX:effective,static detection of race conditions and deadlocks[C]//ACM SIGOPS Operating Systems Review.ACM,2003:237-252.
[2]NETZER R H,MILLER B P.What are race conditions?:Some issues and formalizations[J].ACM Letters on Programming Languages and Systems (LOPLAS),1992,1(1):74-88.
[3]VON P C,GROSS T R.Static Detection of Atomicity Violations in Object-Oriented Programs[J].Journal of Object Technology,2004,3(6):103-122.
[4]LAMPORT L.Time,clocks,and the ordering of events in a distributed system[J].Communications of the ACM,1978,21(7):558-565.
[5]SAVAGE S,BURROWS M,NELSON G,et al.Eraser:A dynamic data race detector for multithreaded programs[J].ACM Transactions on Computer Systems (TOCS),1997,15(4):391-411.
[6]KAHLON V,SANKARANARAYANAN S,GUPTA A.Static analysis for concurrent programs with applications to data race detection[J].International Journal on Software Tools for Technology Transfer,2013,15(4):321-336.
[7]ZHANG W,LIM J,OLICHANDRAN R,et al.ConSeq:detecting concurrency bugs through sequential errors[C]//ACM SIGARCH Computer Architecture News.ACM,2011:251-264.
[8]SACK P,BLISS B E,MA Z,et al.Accurate and efficient filtering for the intel thread checker race detector[C]//Proceedings of the 1st workshop on Architectural and system support for improving software dependability.ACM,2006:34-41.
[9]BISWAS S,CAO M,ZHANG M,et al.Lightweight data race detection for production runs[C]// Proceedings of the 26th International Conference on Compiler Construction.ACM,2017:11-21.
[10]SEREBRYANY K,ISKHODZHANOV T.ThreadSanitizer:data race detection in practice[C]//Proceedings of the Workshop on Binary Instrumentation and Applications.ACM,2009:62-71.
[11]ZHANG W,SUN C,LU S.ConMem:detecting severe concurrency bugs through an effect-oriented approach[J].ACM Sigplan Notices,2010,45(3):179-192.
[12]CHEN Y,CHEN Y.An efficient algorithm for answering graph reachability queries[C]//2008 IEEE 24th InternationalConfe-rence on Data Engineering.IEEE,2008:893-902.
[13]SIMON K.An improved algorithm for transitive closure on acyclic digraphs[J].Theoretical Computer Science,1988,58(1):325-346.
[14]TRIβL S,LESER U.Fast and practical indexing and querying of very large graphs[C]//Proceedings of the 2007 ACM SIGMOD International Conference on Management of Data.ACM,2007:845-856.
[15]CHATARASI P,SHIRAKO J,KONG M,et al.An extended polyhedral model for SPMD programs and its use in static data race detection[C]//International Workshop on Languages and Compilers for Parallel Computing.Springer,2016:106-120.
[16]COHEN E,HALPERIN E,KAPLAN H,et al.Reachability and distance queries via 2-hop labels[J].SIAM Journal on Computing,2003,32(5):1338-1355.
[17]RODITTY L,ZWICK U.A fully dynamic reachability algorithm for directed graphs with an almost linear update time[J].SIAM Journal on Computing,2016,45(3):712-733.
[18]SAKURAI Y,ARAHORI Y,GONDOW K.POI:Skew-Aware Parallel Race Detection[C]//2018 IEEE 18th International Working Conference on Source Code Analysis and Manipulation (SCAM).IEEE,2018:215-224.
[19]ZHOU J,ZHOU S,YU J X,et al.DAG reduction:Fast answering reachability queries[C]//Proceedings of the 2017 ACM International Conference on Management of Data.ACM,2017:375-390.
[20]YILDIRIM H,CHAOJI V,ZAKI M J.Grail:Scalable reachability index for large graphs[J].Proceedings of the VLDB Endowment,2010,3(1/2):276-284.
[21]JANSSEN J,CORPORAAL H.Making graphs reducible with controlled node splitting[J].ACM Transactions on Programming Languages and Systems (TOPLAS),1997,19(6):1031-1052.
[22]LUCIA B,CEZE L,STRAUSS K.ColorSafe:architectural support for debugging and dynamically avoiding multi-variable atomicity violations[C]// ACM SIGARCH computer architecture news.New York:ACM,2010:222-233.
[23]LU S,TUCEK J,QIN F,et al.Avio:Detecting atomicity violations via access-interleaving invariants[J].IEEE Micro,2007,27(1):26-35.
[24]KONG W,HOU G,HU X,et al.ZipPath:A Simple-But-Useful Path Finder for HSTM Designs in ZIPC[C]//2016 IEEE International Conference on Agents (ICA).IEEE,2016:154-157.
[25]CUI K,WANG J,ZHOU K J,et al.Reliability of interrupt services for embedded systems[J].Journal of Tsinghua University (Science and Technology),2016,56(8):878-884.
[1] 李梦珂, 郑秋生, 王磊. 基于采样技术的动态混合数据竞争检测算法[J]. 计算机科学, 2020, 47(10): 315-321.
[2] 杨璐,余守文,严建峰. 基于二型模糊逻辑的多线程数据竞争检测方法研究[J]. 计算机科学, 2017, 44(12): 135-143.
[3] 佘艺,唐弘胤,吴国全,陈伟,魏峻,黄涛. 基于测试例生成的Android应用数据竞争验证方法[J]. 计算机科学, 2017, 44(11): 27-32.
[4] 周宽久,任龙涛,王小龙,勇嘉伟,侯刚. 基于层次化时间STM软件设计的形式化验证[J]. 计算机科学, 2014, 41(8): 42-46.
[5] 李国徽 王洪亚 刘云生. 一种高效的合作实时事务并行检验点算法[J]. 计算机科学, 2005, 32(7): 69-71.
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
[1] 雷丽晖,王静. 可能性测度下的LTL模型检测并行化研究[J]. 计算机科学, 2018, 45(4): 71 -75 .
[2] 孙启,金燕,何琨,徐凌轩. 用于求解混合车辆路径问题的混合进化算法[J]. 计算机科学, 2018, 45(4): 76 -82 .
[3] 张佳男,肖鸣宇. 带权混合支配问题的近似算法研究[J]. 计算机科学, 2018, 45(4): 83 -88 .
[4] 伍建辉,黄中祥,李武,吴健辉,彭鑫,张生. 城市道路建设时序决策的鲁棒优化[J]. 计算机科学, 2018, 45(4): 89 -93 .
[5] 史雯隽,武继刚,罗裕春. 针对移动云计算任务迁移的快速高效调度算法[J]. 计算机科学, 2018, 45(4): 94 -99 .
[6] 周燕萍,业巧林. 基于L1-范数距离的最小二乘对支持向量机[J]. 计算机科学, 2018, 45(4): 100 -105 .
[7] 刘博艺,唐湘滟,程杰仁. 基于多生长时期模板匹配的玉米螟识别方法[J]. 计算机科学, 2018, 45(4): 106 -111 .
[8] 耿海军,施新刚,王之梁,尹霞,尹少平. 基于有向无环图的互联网域内节能路由算法[J]. 计算机科学, 2018, 45(4): 112 -116 .
[9] 崔琼,李建华,王宏,南明莉. 基于节点修复的网络化指挥信息系统弹性分析模型[J]. 计算机科学, 2018, 45(4): 117 -121 .
[10] 王振朝,侯欢欢,连蕊. 抑制CMT中乱序程度的路径优化方案[J]. 计算机科学, 2018, 45(4): 122 -125 .