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

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