计算机科学 ›› 2020, Vol. 47 ›› Issue (6): 24-31.doi: 10.11896/jsjkx.191100187
崔凯1, 赵国亮2, 周宽久1, 李明楚1
CUI Kai1, ZHAO Guo-liang2, ZHOU Kuan-jiu1, LI Ming-chu1
摘要: 嵌入式并发软件的中断嵌套和线程交织等程序的随机性和不确定性(Randomicity and Nondeterminism)会引起数据竞争(Data Race)和原子性违背(Atomicity Violations)等并发缺陷问题,并且这些问题很难被修复和重新构建。针对嵌入式软件中的数据竞争和原子性违背这类并发缺陷问题,文中提出了瘦中断处理(Thin Interrupt Service Routine,Thin ISR)方式。首先,利用状态迁移矩阵(State Transition Matrix,STM)进行建模,把中断处理程序中与访问共享变量相关的程序段移植到主程序中,即中断处理程序只负责将外界中断请求数据存到缓冲区中,中断的具体处理由主程序完成;然后,利用构建的STM模型生成对应的C代码,这样可以有效地避免原子性违背和数据竞争等并发缺陷;最后,利用排队方法对中断的到达时间与离开时间进行仿真。实验结果验证了本方法在解决数据竞争和原子性违背等并发缺陷问题方面的可行性与有效性。
中图分类号:
[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. |
|