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

来源：软件学报杂志2016年第3期北京时间：

作者：陈睿,杨孟飞,郭向英

单位：陈睿，北京控制工程研究所, 北京 100190;北京轩宇信息技术有限公司, 北京 10019011,杨孟飞，中国空间技术研究院, 北京 10009402,郭向英，北京控制工程研究所, 北京 100190;北京轩宇信息技术有限公司, 北京 10019003

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

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

基金资助：国家自然科学基金(91118007)