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

摘要：

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

关键词：制导语言、源到源编译、模型检测、分组

所属期刊栏目：37

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

资助基金：国家自然科学基金项目60970023;国家“九七三”重点基础研究发展计划项目2011CB302501;国家“八六三”高技术研究发展计划项目2012AA010902,2012AA010901;国家科技重大专项项目2009ZX01036-001-002,2011ZX01028-001-002-3

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

页数：共6页

页码：1898-1903