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

• 作者: 杨孟飞 郭向英 陈睿
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 中断驱动型程序 数据竞争 抽象解释
• 年，卷（期）: 2016,（3）
• 所属期刊栏目: 软件形式化方法与应用专题
• 页码范围: 547-561
• 页数: 15页
• 分类号: TP311
• 字数: 12838字
• 语种: 中文
• DOI: 10.13328/j.cnki.jos.004980

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	杨孟飞		45	222	10.0	12.0
2	郭向英		7	46	4.0	6.0
4	陈睿		7	30	3.0	5.0