Abstract: In C programs with multiple interruptions, the interleaving of interruptions may cause some unexpected interleaving executions and even wrong execution results. A kind of frequently occurred error is that the atomicity of programs is violated because of data race. To solve this problem, this paper introduces the abstract execution seman-tics for C programs under multiple interruptions, gives an atomicity definition based on the access of shared vari-ables, presents the data race and atomicity checking algorithms based on the atomicity definition, and adopts func-tion abstraction technique to reduce the traversed state space. At last, it designs and implements a prototype checker named MIDAC (multiple interruption C program data race and atomicity checker), and the experimental results demonstrate its effectiveness on several practical programs.

Key words: multiple interruption, data race, atomicity

摘要： 在多重中断C程序中, 中断嵌套可能会导致一些非期望的交叠执行, 从而造成错误的程序执行结果。典型的问题是共享变量引起的数据竞争破坏了程序的原子性。针对此类问题, 对多重中断C程序的运行时语义进行建模, 根据共享变量的访问给出了一种原子性的定义, 提出了相应的数据竞争及原子性检测方法, 并采用函数摘要技术缩减静态分析过程中所需遍历的程序状态。最后, 设计并实现了一个数据竞争及原子性检测原型工具MIDAC(multiple interruption C program data race and atomicity checker),实验结果表明, 该工具能够针对一定规模的实际程序得到很好的检测效果。

关键词: 多重中断, 数据竞争, 原子性