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

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

Model of Embedded Software for Solving Concurrent Defects

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 related to 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 simulate the 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.