计算机科学 ›› 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: Atomicity violation, Data race, Interrupt nesting, 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] 赵静文, 付岩, 吴艳霞, 陈俊文, 冯云, 董继斌, 刘嘉琪.
多线程数据竞争检测技术研究综述
Survey on Multithreaded Data Race Detection Techniques
计算机科学, 2022, 49(6): 89-98. https://doi.org/10.11896/jsjkx.210700187
[2] 李梦珂, 郑秋生, 王磊.
基于采样技术的动态混合数据竞争检测算法
Dynamic Hybrid Data Race Detection Algorithm Based on Sampling Technique
计算机科学, 2020, 47(10): 315-321. https://doi.org/10.11896/jsjkx.190700079
[3] 杨璐,余守文,严建峰.
基于二型模糊逻辑的多线程数据竞争检测方法研究
Type-2 Fuzzy Logic Based Multi-threaded Data Race Detection
计算机科学, 2017, 44(12): 135-143. https://doi.org/10.11896/j.issn.1002-137X.2017.12.027
[4] 佘艺,唐弘胤,吴国全,陈伟,魏峻,黄涛.
基于测试例生成的Android应用数据竞争验证方法
Concurrency Bugs Verification in Android Applications Based on Test Case Generation
计算机科学, 2017, 44(11): 27-32. https://doi.org/10.11896/j.issn.1002-137X.2017.11.005
[5] 周宽久,任龙涛,王小龙,勇嘉伟,侯刚.
基于层次化时间STM软件设计的形式化验证
Modeling and Formal Verification for Software Designs Based on Hierarchical Timed State Transition Matrix
计算机科学, 2014, 41(8): 42-46. https://doi.org/10.11896/j.issn.1002-137X.2014.08.008
[6] 李国徽 王洪亚 刘云生.
一种高效的合作实时事务并行检验点算法

计算机科学, 2005, 32(7): 69-71.
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!