Computer Science

Computer Science ›› 2020, Vol. 47 ›› Issue (6): 24-31.doi: 10.11896/jsjkx.191100187

• Intelligent Software Engineering • Previous Articles     Next Articles

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)

PDF (PC)

1222

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

CLC Number: 

  • 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] ZHAO Jing-wen, FU Yan, WU Yan-xia, CHEN Jun-wen, FENG Yun, DONG Ji-bin, LIU Jia-qi. Survey on Multithreaded Data Race Detection Techniques [J]. Computer Science, 2022, 49(6): 89-98.
[2] LI Meng-ke, ZHENG Qiu-sheng, WANG Lei. Dynamic Hybrid Data Race Detection Algorithm Based on Sampling Technique [J]. Computer Science, 2020, 47(10): 315-321.
[3] YANG Lu, YU Shou-wen and YAN Jian-feng. Type-2 Fuzzy Logic Based Multi-threaded Data Race Detection [J]. Computer Science, 2017, 44(12): 135-143.
[4] SHE Yi, TANG Hong-yin, WU Guo-quan, CHEN Wei, WEI Jun and HUANG Tao. Concurrency Bugs Verification in Android Applications Based on Test Case Generation [J]. Computer Science, 2017, 44(11): 27-32.
[5] ZHOU Kuan-jiu,REN Long-tao,WANG Xiao-long,YONG Jia-wei and HOU Gang. Modeling and Formal Verification for Software Designs Based on Hierarchical Timed State Transition Matrix [J]. Computer Science, 2014, 41(8): 42-46.
Viewed
Full text


Abstract

Cited
  Shared   
  Discussed   
No Suggested Reading articles found!
渝ICP备16013121号-4
Add:18# Honghu West Rd., Yubei ,Chongqing,China    Post Code: 401121
Tel: 023-63500828/023-67039612/023-67039623
E-mail: jsjkx12@163.com
Powered by Beijing Magtech Co., Ltd.