基于变量访问序模式的中断数据竞争检测方法

摘要：

在航天嵌入式软件等中断驱动型软件中,中断数据竞争问题十分突出.然而,中断在并发语义、同步机制、调度机制等方面与线程(任务)有诸多不同,具有Ad-hoc特征,难以统一刻画,因此,主流的数据竞争检测方法并不适用.以航天嵌入式软件数据竞争案例库为基础进行了系统分析,提出刻画有害中断数据竞争的7种缺陷模式.针对其中最常见且最难解决的单变量访问序模式,基于抽象解释,提出一种支持过程间分析、中断并发分析的高效检测方法.设计并实现了相应的检测工具SpaceDRC.实验结果表明,SpaceDRC能够在145ms内检测出约21 400行程序中的真实数据竞争.SpaceDRC已经在多个航天重点型号中进行了应用,使得中断数据竞争专项分析的效率提高了至少5倍,并且降低了问题遗漏率.

关键词：中断驱动型程序、数据竞争、抽象解释

所属期刊栏目：27

分类号：TP311(计算技术、计算机技术)

资助基金：国家自然科学基金91118007National Natural Science Foundation of China 91118007

在线出版日期：2016-08-19（万方平台首次上网日期，不代表论文的发表时间）

页数：共15页

页码：547-561