实时嵌入式系统并发程序检测方法研究

梁 昊, 艾云峰

(1.装备学院研究生管理大队,北京101416; 2.中国科学院大学工程管理与信息技术学院,北京100049)

实时嵌入式系统并发程序检测方法研究

梁 昊1, 艾云峰2

(1.装备学院研究生管理大队,北京101416; 2.中国科学院大学工程管理与信息技术学院,北京100049)

近年来随着实时嵌入式系统自动化程度的不断提升,其设计复杂度不断加大,在设计中大量的使用了并发程序设计方法。但目前在基于实时嵌入式系统应用程序开发以及测试的过程中,由于中断和线程的相互交叠,始终缺乏有效的针对实时嵌入式系统的并发程序测试方法。本文设计了面向实时嵌入式系统并发程序动态测试的算法,提出以标记迁移系统作为并发程序的系统模型,对常见的并发错误给出了形式化定义,使用偏序化简算法缩减程序的状态空间,实现了对多线程、多重中断的并发程序错误检测。

实时嵌入式系统;并发程序;多重中断;多线程;并发错误

1 问题的提出

近年来控制系统的自动化程度不断提升,对其数据处理能力、通信处理能力、系统集成能力提出的要求也越来越高。因此并发多线程、多重中断程序设计技术在嵌入式实时操作系统中得到了广泛的应用。然而并发程序由于其执行过程中并发交叠的随机性,给软件的测试工作带来了大量的困难。目前国内外并发程序测试方法主要包括静态分析和动态验证2大类。

静态分析的基本原理是不编译运行程序,对有程序抽象出的状态模型进行验证。如国防科技大学设计的MIDAC(multiple interruption C program data race and atomicity checker)[1]检测工具。MIDAC采用了函数摘要的技术来缩减静态分析过程中需要遍历的状态空间。文献[2-3]所采用了类线程测试方法,其主要原理是将中断程序改写为“语义”等价的多线程程序,然后对多线程程序进行静态或者动态测试。

动态验证的基本原理是对在给定测试数据驱动下执行的程序进行验证,它避免了可执行程序中代码(包括编译、运行时库等)与程序模型之间的不一致问题,典型的工具有：VeriSoft[4]、Cal-Fuzzer[5]和Inspect[6]。其中VeriSoft面向可执行程序,能够验证由C、C++、Tcl等任何程序编写的可执行代码,它还支持对包含多个进程的并发程序的验证;CalFuzzer,其可对Java程序的数据竞争、原子性违背、死锁进行测试;Inspect可发现多线程C程序中的“并行错误”,并保证在给定测试数据下没有数据竞争、死锁这2种并发错误。文献[7]提出的多重中断程序测试框架的主要设计思想是对中断进行两两对比测试,通过不断提高2个中断的触发频率来加速并发错误的出现。但是该方法只能针对2个外部中断进行独立测试,且需要人为干预,很难保证测试的覆盖率。

以上的测试方法均无法检测同时包含线程和中断的并发程序,而线程和中断产生并发交叠的情况在实时嵌入式系统的应用程序中是十分常见的,因此本文在参考了国内外相关技术的基础上,针对实时嵌入式操作系统程序的特点,在基于发生序关系的动态偏序化剑算法的基础上,引入了状态记录、sleep集合和线程、中断优先级判断等技术手段,设计了面向实时嵌入式系统并发程序的错误验证算法,该算法可以验证包括多线程、多重中断在内的并发程序,错误检测范围涵盖了数据竞争、死锁、原子性违背这3种常见的并发错误。

2 并发程序建模及错误定义

2.1 实时嵌入式系统的并发程序建模

本文使用标记迁移系统(LTS)[8]对并发程序进行建模。假定一个并发程序包含α个并发单元(本文将线程和中断服务程序通称为“并发单元”),其中包括n个线程,m个中断服务程序,α= n+m,将线程标志集合定义为Ithread=[1,n],中断服务程序标志集合定义为Iinterrupt=[n+1,α],则并发单元标志集合IF=Ithread∪Iinterrupt=[1,α], f∈F表示每一个并发单元的唯一标志。假定实时嵌入式操作系统中线程的优先级为[0,i],中断优先级为[0,j],则可将整个系统的并发单元优先级映射到集合P⊆[0,β](β=i+j),其中[0,i]为线程优先级空间,[i+1,β]为中断优先级空间,中断服务函数比线程拥有更高的优先级。

定义1并发单元的LTS模型为：Mpf=(Sf, s0f,Tpf,Rf,Lf),其中f为该并发单元的唯一标识;Sf表示并发单元的状态集合;s0f∈Sf表示并发单元的初始状态;Tpf表示并发单元迁移集合; Rf表示并发单元迁移关系集合;Lf表示允许中断发生的标志(如果该并发单元为线程,则此Lf始终都处于允许的状态);p∈P表示并发单元的优先级。

定义2通过对Mf的并发合并,可以得到实时嵌入式系统的并发LTS统模型为

下文中将并发合并后的程序模型简记为M= (S,s0,T,R,L),并使用s∈S表示程序的全局状态,t∈T表示程序的迁移,s0=init表示程序的初始状态。

定义3并发单元对全局共享对象的读写操作为可见操作,对本地对象的读写操作为不可见操作。

由于不可见操作对程序的并发执行不产生影响,因此下文中只对可见操作进行讨论。

2.2 并发错误定义

在描述实时嵌入式系统并发错误之前,需要先介绍2个相关概念：

定义4对于一个全局状态s=(s1,s2,…, sn),当且仅当其上的迁移t在全局状态s上的局部状态si上是可执行的,此时si之外的局部状态有sj=s′j(i≠j),则迁移t在全局状态上才是可执行的,记作t∈s.enabled即s→ts′。

定义5R∈T×T是独立关系,当且仅当如果对于每一个〈t1,t2〉∈R,如果他们是相互独立的,则必须满足下面2个关系：

1)若t1∈s.enabled,且有s→t1s′,当且仅当t2在状态s′是可执行的,则t2∈s.enabled。

2)如果t1、t2在状态s是可执行的,则存在一个唯一的状态s′,有并且。

独立关系的定义反映了2个迁移t1、t2作用于同一个全局状态的2个不同的局部状态;或者是2个作用于同一个局部变量上的2个读操作,此时交换他们的执行次序对程序的运行无影响。

定义6当且仅当并发系统中所有非空迁移序列,满足迁移ti∉TP, 1≤i≤n,tn与集合TP中的所有迁移是相互独立的,则在状态s上可执行的迁移集合PP∈T是一个Persistent集合。

2.2.1 死 锁

死锁的定义[9]：所谓死锁是指2个或2个以上的进程在执行过程中,因争夺资源而造成的一种互相等待的现象,若无外力作用,它们都将无法推进下去。

死锁的形式化描述：若存在一个状态sdead,有该状态的sdead·enabled=Ø,即该状态没有后续的迁移则在该状态上存在死锁,且状态sdead在偏序化简中是可达的,从初始状态s0到死锁状态sdead的迁移序列为Tdead,则可表示为：。

证明：首先当Tdead的长度为0时,即length (Tdead)=0,此时结论显然是成立的。

假设length(Tdead)=n,设迁移序列T′dead=t0, t1,…,tn,从s开始的迁移序列sdead。设状态s的Persistent集合TP非空,且t0, t1,…,tn∉TP即TP∩T′dead=Ø。那么根据定义6可知T′dead中的所有迁移与TP的迁移都存在独立关系,所以TP中的迁移仍然可在状态sdead上执行,而这一结果与死锁的状态相违背。因此必然有TP∩T′dead≠Ø。

设ti为第一个出现在集合TP中的迁移, T″dead=ti,t0,t1,…,ti-1,ti+1,…,tn。根据Persistent集合的定义∀tj,0≤j≤i与ti相独立,所以ti可以在T′dead中与前面的迁移连续交换次序得到T″dead,即同时存在,由于ti∈ TP,因此对于长度为n+1的迁移序列亦成立。

2.2.2 原子性与原子性违背

原子性的定义[9]：一个事务中的所有操作,要么全部完成,要么全部不完成,不会结束或中断在某一个环节,事物在执行的过程中发生错误会被回滚到初始状态。

多重中断中C语言程序的原子性违背的形式化描述：给定一个原子块A,迁移序列为：TA= {t1,t2,…,tn},∃i∈[1,n],ti∈TA,即ti处在原子块A中,原子块中所有写操作的集合OPW(A)={op|op∈OP(A),and,op(A)= write},原子块中所有读操作的集合OPR(A)= {op|op∈OP(A),and,op(A)=read},其中op的含义为操作;OP(A)为原子块A中所有可见操作的集合。如果∃t∉TA并且t与ti是非相互独立且可同时执行的迁移,若(OPR(A)∩opw(t))∪(opr(t)∩OPW(A))∪(OPW(A)∩opw(t))≠Ø,则会引发原子性违背错误。其中opw(t),opr(t)分别表示op(t)=write,op(t)= read。

2.2.3 数据竞争

数据竞争的定义[10-11]：2个线程在没有同步操作保护的前提下同时访问一块共享内存,且至少有其中一个访问为写操作。

多重中断中C语言程序数据竞争的形式化描述：对于程序中的任意一个状态s,在其上的所有写操作的集合为：OPW(s)={op|op∈OP(s), and,op(s)=write},所有读操作的集合为：OPR(s)={op|op∈OP(s),and,op(s)=read},如果存在2个迁移t和t′在状态s上都是可执行且非相互独立的,若t和t′分别属于2个优先级不同的中断函数,t和t′有一个操作在集合OPW(s)中,则状态s存在数据竞争错误。

3 动态检测算法设计

3.1 动态偏序化简思想

实时嵌入式系统并发程序由于其状态空间在动态执行的过程中会变得极其巨大,甚至出现状态空间爆炸的问题。为此本文将基于happensbefore关系的多线程程序动态偏序化简(dynamic partial-order reduction,DPOR)[12-13]方法引入到多重中断程序的状态空间化简中。

DPOR算法的主要思想就是计算各个状态的Persistent集合,剔除由独立关系所带来的冗余路径。传统的DPOR算法在处理包含多线程、多中断的并发程序中有3个缺陷：① 无法对包含无限循环的程序进行化简;②DPOR算法也无法对中断服务程序进行处理;③ 没有对中断允许标志位和优先级的处理。下文中将针对以上3点不足提出对算法的改进。

3.2 基于DPOR算法的实时嵌入式系统并发程序检测算法

针对3.1节中提出的问题,本文设计了如下的检测算法。

算法将程序的并发单元划分为2个集合：线程集合Ithread,中断服务程序集合Iinterrupt,并规定Ithread的优先级取值范围为[0,n],Iinterrupt的优先级取值范围为[n+1,α],集合IF=Iinterrupt∪Ithread来代表被测试程序的并发单元集合,f∈F即为并发单元的唯一标志。pre(s,t)返回到达状态s之前的迁移,fid(t)∈F返回该迁移所在的并发单元标志,算法中使用fid(t).p来记录迁移t所在的并发单元的优先级,Tid即为Ithread,Iid即为Iinterrupt。S为全局对象的搜索堆栈,s为动态执行中当前的全局状态,s.enabled为每一个状态s的可执行迁移集合,s.backtrack为回溯集合表示需要搜索的状态s的函数集合。s.done表示被检测过的状态s的函数集合。

本算法在传统的DPOR算法中加入了一个hash表H用来记录检索过的状态,所有被检索过的状态都会被加入到H中。若算法检索的状态已存在于表H中,则会首先搜索可见关系依赖图,以此来减少系统的消耗;若算法检测到的状态不存在于表H中,则会更新可见关系依赖图。可见关系依赖图记作G。详细的描述如下,令M= (S,s0,T,R,L)为一个并发程序的模型。可见操作依赖关系图G=〈V,E〉为模型M中的有向图,其中V,E表示有向图中2个迁移的节点,它包含了遍历状态空间中所有可见操作之间的发生前关系。对于G中的每一个节点v∈V是一个可见操作,即∀v∈V：∃t∈T：tg=v;同样的有e∈E是一个可见操作,即∀e∈E：∃t′∈T：t′g=e。对于在动态搜索中执行的每一个迁移序列s3,算法都会在图中加入一个方向边(tg,t′g),这样在除程序的第一次动态执行以外,之后的执行过程会首先搜索可见关系依赖图并执行回溯,进一步提高了状态空间搜索效率。

本文引入了sleep集合的概念,s.sleep表示在状态s上可以执行但没有必要执行的迁移的集合。状态s上s.sleep的初始值为存在独立关系的迁移集合,将已经检索过的迁移加入到s.sleep中,同时在s.enabled集合中减去s.sleep,这样做不仅可以减少状态s上需要遍历的迁移数量,更重要的是随着s.enabled集合的不断缩小,在所有迁移都被检索之后s.enabled=Ø,解决了在无限循环中出现的迁移空间的无限增长问题。

算法1第11行,为对中断允许标志位的判断,即对回溯集合中存在的路径在实际执行过程中是否可以到达的判断,如果下一个迁移处在一个中断服务程序中,且中断的允许标志位没有使能,则改路径不可达,算法将不搜索这条路径。算法1第16行中BUGDETECT函数为并发错误检测函数,小节3.3给出了该函数的具体描述。

算法2给出了函数PriorityJudgments()的具体算法：

1.PriorityJudgments(state s,transition t){

2. If(fie(t)∈Tid and fid(pre(s,t))∈Tid)return true;

3. else if(fie(t)∈Iid and fid(pre(s,t))∈Tid)return true;

4. else if(fie(t)∈Iid and fid(pre(s,t))∈Iid and fid (pre(s,t))∈Tid.PRI＜fid(t).PRI)

5. return true;

6. else return false;

7.}

由于线程在执行的过程中存在被阻塞的可能性,因此即便高优先级的线程在执行的过程中也可能会放弃CPU的使用权限,从而使低优先级的线程进入到运行状态,而中断在执行的过程中是无法被阻塞的,只有高优先级的中断打断低优先级中断执行的过程,而任何的中断都可以打断线程的执行。

函数UPDATEBACKTRACESETS(s)作用是动态计算persistent集合,其算法设计如下。

其算法与经典DPOR的回溯算法有2个不同点：在第6行中引入了对优先级的判断,以此决定这个回溯点在实际执行的过程中是否存在;在回溯算法的第8行中,引入了在文献[12]发生前关系的基础上的一个变种,对于一条迁移序列π,且π的长度为n,如果∃ti,tj∈π(1,≤i≤j≤n),则存在关系,进而如果有fid(tj)=q,则存在关系;关于DPOR的算法的详细理论与数学证明请参考文献[13]。

3.3 并发错误检测算法

函数BUGDETECT的作用是检测状态上是否存在并发错误。

1.BUGDETECT(state s){

2. if(s.enabled==Øand s.sleep==Ø)

3. return a deadlock;

4. else if(∃A：which is a atomic block such that state s is a state in a atomic block A){

5. let SAtombe the sequence of state in atomic block A;

6. let TAtombe the sequence of transition with SAtom;

7. let OPW be the write operations in TAtom;

8. let OPR be the read operations in TAtom;

9. for(each t∈TAtom{

10. if(∃t's.t.fid(t').PRI＞fid(t).PRI and t'is co_enabled at the same state with t){

11. if(op(t')==write and op(t')∪OPR!=Ø) return an atom write mistake;

12. if(op(t')==read and op(t')∪OPW!=Ø) return an atom read mistake;

13. if(op(t')==write and op(t')∪OPW!=Ø) return an atom Dual write mistake;

14. }

15. }

16. }

17. else if(∃t,t's.t.t,t'∈s.enabled and(fid(t'). PRI!=fid(t).PRI)and(t,t')is dependent){

18. if(op(t')==write or op(t)==write)return maybe a write out of sync;

19. }

20. else return False;

21.}

算法4中第2、3行为对死锁算法的检测,第4行至第16行为对目标程序的原子性违背错误的检测方法;第17、18行主要是检测程序中不同优先级下,高优先级中断打断低优先级中断时,程序是否存在数据竞争的情况。

4 实验平台与实验结果分析

4.1 实验平台

实时嵌入式系统并发程序检测工具主要包括5个部分：程序分析器、线程分析器、中断分析器、控制执行器、中断发生器。

程序分析器的重要作用是建立并发的程序的LTS模型;线程分析器的主要作用是识别程序中的线程以及线程的相关操作;中断分析器的主要作用是识别程序的内部和外部中断,建立中断触发机制;控制执行器的主要工作是接收由插装、编译后的被测试程序得到共享变量、函数注册信息,并根据以上信息控制中断发生器的中断产生时间和阻塞、允许线程的执行,根据目标程序的执行情况判断并发交叠中是否包含并发错误;中断发生器的作用是在控制执行器给定的信号驱使下,产生相应的中断,对于内部中断不进行触发,而是等待条件允许后,内部中断自身完成触发执行。

图1 多重中断测试工具设计框架图

被测试程序方面,我们在ARM平台上选用了基于RT-Linux系统通讯加密编码程序,在PPC平台上选用了基于Vx Works系统的无人飞行器控制程序。

4.2 实验结果与分析

实验首先对并发错误检测算法的执行效率进行了评估,之后对算法的准确性进行了验证。

1)算法执行效率评估。本文分别使用了verisoft和inspect软件与本文所设计的测试工具进行对比,如表1所示。其中verisoft使用了无状态的动态偏序化简算法,因此执行效率相对较低;在inspect工具的测试对比环节中,由于其只能针对多线程程序进行测试,因此本文对中断服务程序采用了类线程的测试方法[2-3],同时由于都采用了有状态的动态偏序化简算法,因此在执行效率上相近,但是本文所设计的算法还引入了sleep集合和对中断服务程序和线程优先级的判断,可以进一步地缩减被测试程序并发模型的状态空间,所以在执行效率上有了进一步地提升。

2)动态验证测试结果分析。表2显示了具体的并发错误的数量与类型。这里需要说明一点的是verisoft和inspect都不支持对于原子性违背的检测,因此仅有本文所设计的算法找到一个原子性违背错误。由于同是基于发生序关系的测试方法,因此在死锁检测方面(仅涉及线程的交叠,中断服务函数中不可能有锁的出现),三者检测结果是完全相同的;数据竞争方面,inspect由于使用了类线程的测试方法,但线程和中断的执行方式依然存在本质的不同,因此在数据竞争方法出现了误报。

表1 执行效率对比

表2 动态验证错误说明

5 结束语

本文根据实时嵌入式系统中并发C语言程序的相关特点,使用LTS模型对并发程序进行建模,在DPOR算法的基础上,对中断服务程序进行了功能扩展,实现了对包含多线程、多重中断状态空间的化简。本文根据常见的3种并发错误的经典定义,给出了在标记迁移系统中的形式化描述和具体的检测算法,最终实现了对于包含多线程、多重中断的C语言并发错误检测。目前在数据竞争的检测方面,可以报告出可能存在的数据竞争,但是还无法区分良性的数据竞争还是恶性的数据竞争,最终结果还需要人为判断。

References)

[1]吴学光,文艳军,王戟,等.多重中断数据竞争及原子性检测[J].计算机科学与探索,2011,12(3)：1086-1093.

[2]REGEHR J,COOPRIDER N.Interrutp verifition via thread verification[J].Electronic Notes in Theoretical Computer Science,2007,174(9)：139-150.

[3]HOFER W,LOH MANN D,SCHELER F,et al.Sloth：Threads as interrupts[C]//Proceedings of the 30th IEEE Real-Time Systems Symposium(RTSS'09).Washington, D.C.,USA：IEEE Computer Society Press,2009：215-228.

[4]DINGEL J.Computer-assisted assume/guarantee reasoning with verisoft[C]//In Proceedings of the 25th International Conference on Software Engineering(ICSE'03).Washington,D.C.,USA：IEEE Computer Society Press,2009：138-148.

[5]JOSHI P,NAIK M,PARK Chang-Seo,et al.Cal Fuzzer：an extensible active testing framework for concurrent programs [C]//In Proc.21st International Conference on Computer Aided Verification(CAV'09).Secaucus,NJ,USA：Springer-Verlag New York,Inc.,2009：675-681.

[6]YANG Y,CHEN X F,GOPALAKRISHNAN G,et al.KirbyInspect.A runtime model checker for multithreaded C programs[D].Salt Lake City U.S.A：School of Computing University of Utah,2009：2-4.

[7]傅修峰,陈丽容.多重中断程序测试框架[J].计算机工程与设计,2012,2(2)：617-623.

[8]CHAKI S,CLARKE E M,OUAKNINE J,et al.Automated, compositional and iterative deadlock detection[C]//Proc.of the 2nd ACM and IEEE International Conference on Formal Methods and Models for Co-design.Washington,D.C., USA：IEEE Press,2004：201-210.

[9]SILBERSCHATZ A,GALVIN P B,GAGNE G.Operating ststem concepts[M].8th ed.John Wiley&Sons,Inc.,2009：283,733-734.

[10]HARRY R,NETZER B.Race condition detection for debugging shared-memory parallel programs[D].Madison Madison,WI,USA：University of Wisconsin,1991：5-7.

[11]NETZER R H B,MILLER B P.What are race conditions? Some issues and formalizations[J].ACM Letters on Programming Languages and Systems,1992,1(1)：74-88.

[12]FLANAGAN C,GODEFROID P.Dynamic partial-order reduction for model checking software[C]//In proceedings of POPL'05.Long Beach,California,USA：ACM Press,2005：110-121.

[13]GODEFROID P.Partial-order methods for the verification of concurrent systems-an approach to the state-explosion problem[M].Secaucus,NJ,USA：Springer-Verlag New York,Inc.,1996：27-78.

(编辑：李江涛)

Research for Method of Real-time Embedded Systems Concurrent Program Testing

LIANG Hao1, AI Yunfeng2

(1.Department of Graduate Management,Equipment Academy,Beijing 101416,China; 2.College of Engineering&Information Technology,University of Chinese Academy of Sciences,Beijing 100049,China)

In recent years,with the improving degree of automation of real-time embedded systems,and increasing complexity of designing,concurrent programming methods have been widely used in designing.But due to overlaps between the interrupts and threads in real-time embedded system,there is always lack of an effective program testing method in the testing and checking process of real-time embedded system.So in the paper,a testing method for real-time embedded systems dynamic concurrent programs is designed,labeled transition systems(LTS)as a system of concurrent programming model is used,the formal definition for common concurrency error is defined,partial order reduction algorithm to reduce the state space of the program is used,and the testing tool which can detect multi-threaded and multi-interrupt program concurrent errors has been realized.

real-time embedded systems;concurrent program;multiple interrupts;multithread; concurrency errors

TP 311.5

2095-3828(2014)04-0094-07

ADOI10.3783/j.issn.2095-3828.2014.04.021

2014-04-22

部委级资助项目

梁 昊(1981-),男,博士研究生.主要研究方向：兵器发射理论与技术.mouse1292000@hotmail.com.