利用分组算法实现高效的并行程序模型检测

• 作者: 周军蕊 姚文军 安虹 王云云 陈俊仕 韩文廷
• 来源期刊: 小型微型计算机系统
• 学科: 工学
• 关键词: 制导语言 源到源编译 模型检测 分组
• 年，卷（期）: 2016,（9）
• 所属期刊栏目: 计算机软件与数据库研究
• 页码范围: 1898-1903
• 页数: 6页
• 分类号: TP311
• 字数: 7011字
• 语种: 中文

摘要

在并行时代,模型检测技术(通常也被称为状态空间搜索)是验证并行程序正确性的有效方法.由于线程执行次序的不确定性,线程之间交互次序的改变导致程序状态呈指数性增长,因此在利用状态空间搜索法搜索程序状态时,状态爆炸是亟需解决的难题.为了改善该问题,提出基于分组的模型检测方法.针对操作不同变量的线程,在程序中简单添加制导语句对其进行分组,之后利用该分组信息搜索状态空间,并实时记录已完成搜索的分组信息,从而避免搜索冗余状态.实验结果表明,本文提出的方案对于缓解状态爆炸问题有很好的效果,制导分组前后,测试程序的状态集平均减少了67％,有效提高了并行程序验证效率.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	安虹	中国科学技术大学计算机科学与技术学院	65	224	7.0	12.0
2	陈俊仕	中国科学技术大学计算机科学与技术学院	10	25	3.0	5.0
3	姚文军	中国科学技术大学计算机科学与技术学院	3	14	2.0	3.0
4	韩文廷	中国科学技术大学计算机科学与技术学院	6	7	1.0	2.0
5	王云云	中国科学技术大学计算机科学与技术学院	1	0	0.0	0.0
6	周军蕊	中国科学技术大学计算机科学与技术学院	2	2	1.0	1.0