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

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

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

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

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. 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

摘要/Abstract

摘要： 在多重中断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

吴学光, 文艳军, 王戟, 傅秀涛, 綦艳霞, 顾斌. 多重中断C程序中数据竞争及原子性检测[J]. 计算机科学与探索, 2011, 5(12): 1085-1093.

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

. Data Race and Atomicity Checking for C Programs with Multiple Interruptions[J]. Journal of Frontiers of Computer Science and Technology, 2011, 5(12): 1085-1093.

[1]	李兰英，孙建达，朱素霞. 线程交互不变量的原子性违例错误并发检测[J]. 计算机科学与探索, 2018, 12(7): 1087-1099.
[2]	苏辉，葛洪伟，张涛. 密度自适应的数据竞争聚类算法[J]. 计算机科学与探索, 2016, 10(10): 1439-1450.