| 多重中断C程序中数据竞争及原子性检测 |
| |
| 引用本文： | 吴学光,文艳军,王戟,傅秀涛,綦艳霞,顾斌.多重中断C程序中数据竞争及原子性检测[J].计算机科学与探索,2011,5(12):1085-1093. |
| |
| 作者姓名： | 吴学光 文艳军 王戟 傅秀涛 綦艳霞 顾斌 |
| |
| 作者单位： | 1. 国防科学技术大学计算机学院,长沙,410073
2. 中国航天科技集团北京控制工程研究所,北京,100080 |
| |
| 基金项目： | 国家自然科学基金No.90818024; 国家杰出青年科学基金No.60725206~~ |
| |
| 摘 要： | 在多重中断C程序中,中断嵌套可能会导致一些非期望的交叠执行,从而造成错误的程序执行结果。典型的问题是共享变量引起的数据竞争破坏了程序的原子性。针对此类问题,对多重中断C程序的运行时语义进行建模,根据共享变量的访问给出了一种原子性的定义,提出了相应的数据竞争及原子性检测方法,并采用函数摘要技术缩减静态分析过程中所需遍历的程序状态。最后,设计并实现了一个数据竞争及原子性检测原型工具MIDAC(multiple interruption C program data race and atomicity checker),实验结果表明,该工具能够针对一定规模的实际程序得到很好的检测效果。
|
| 关 键 词： | 多重中断 数据竞争 原子性 |
| 修稿时间： | |
Data Race and Atomicity Checking for C Programs with Multiple Interruptions |
| |
| 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 Frontier of Computer Science and Technology,2011,5(12):1085-1093. |
| |
| Authors: | WU Xueguang WEN Yanjun WANG Ji FU Xiutao QI Yanxia GU Bin |
| |
| Affiliation: | 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 |
| |
| 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. |
| |
| Keywords: | multiple interruption data race atomicity |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
| 点击此处可从《计算机科学与探索》浏览原始摘要信息 |
|
点击此处可从《计算机科学与探索》下载全文 |
|
