计算机科学与探索2011，Vol.5Issue(12)：1085-1093,9.DOI:10.3778/j.issn.1673-9418.2011.12.003
多重中断C程序中数据竞争及原子性检测
Data Race and Atomicity Checking for C Programs with Multiple Interruptions
摘要
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 semantics for C programs under multiple interruptions, gives an atomicity definition based on the access of shared variables, presents the data race and atomicity checking algorithms based on the atomicity definition, and adopts function 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,9.基金项目
The National Natural Science Foundation of China under Grant No.90818024(国家自然科学基金) （国家自然科学基金）
the National Science Foundation for Distinguished Young Scholars of China under Grant No.60725206(国家杰出青年科学基金). （国家杰出青年科学基金）
