计算机科学与探索 ›› 2011, Vol. 5 ›› Issue (12): 1085-1093.

• 学术研究 • 上一篇    下一篇

多重中断C程序中数据竞争及原子性检测

吴学光, 文艳军, 王 戟, 傅秀涛, 綦艳霞, 顾 斌   

  1. 1. 国防科学技术大学 计算机学院, 长沙 410073
    2. 中国航天科技集团 北京控制工程研究所, 北京 100080

  • 收稿日期:1900-01-01 修回日期:1900-01-01 出版日期:2011-12-01 发布日期:2011-12-01

Data Race and Atomicity Checking for C Programs with Multiple Interruptions

WU Xueguang, WEN Yanjun, WANG Ji, FU Xiutao, QI Yanxia, GU Bin

  

  1. 1. School of Computer, National University of Defense Technology, Changsha 410073, China 2. Beijing Institute of Control Engineering, China Aerospace Science and Technology Corporation, Beijing 100080, China
  • Received:1900-01-01 Revised:1900-01-01 Online:2011-12-01 Published:2011-12-01

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

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

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