论文部分内容阅读
在并行时代,系统正确性验证越来越受到关注。在并行系统中,由于线程之间执行次序的不确定性,错误往往很难通过测试的方法重现,从而研究人员提出模型检测技术验证并行程序。模型检测一般利用状态空间搜索的方法验证系统的正确性,随着被验证系统规模的增大,各线程之间交互次序的改变导致被搜索的状态集越来越大,因此,这种状态爆炸现象是亟需解决的难题。本文致力于缓解验证过程中出现的状态爆炸现象,在现有的模型检测框架Spin基础上,重新生成新的模型检测器GSpin。结合新的状态空间搜索算法,减少搜索的状态集,提高并行验证效率。本文的研究工作及创新之处主要包括以下两个方面：1.编译制导分组,结合分组压缩算法搜索状态空间本文在Bell实验室开发的模型检测器Spin的基础上,在验证程序中添加制导分组语句,重新改写新的词法语法规则文件,添加对制导语句的分析处理,生成新的模型检测器GSpin。利用GSpin生成的分组信息,结合分组压缩算法搜索系统状态。新的验证框架能有效减少验证系统的状态空间大小,提高验证效率。本文选取了8组测试程序,平均减少56.7%的状态空间大小,有效提高了验证效率。2.优化的分组压缩算法为了进一步提高程序的验证效率,考虑到各个分组之间的不相关性,本文提出两种优化的分组压缩算法,分别为局部并行化的Native算法及完全并行化的Entirely算法。Native算法将分组与多线程一一对应,使得每个线程顺序搜索相应的组,同步各组第一次到达自己的最终状态后,利用主线程将各线程的搜索路径合并,在串行模式下继续搜索系统状态。Entirely算法认为每个组都是一个独立的整体,并不仅仅在第一条完整路径上,还包括回溯等过程。该算法更能缩短验证时间,进一步提高验证效率。利用局部并行化算法Native算法搜索程序状态空间,随着被验证程序规模的增加,并行化效果也随之加强,验证时间平均减少了41.7%,但以消耗内存为代价,内存是顺序模式下的分组压缩算法的1.47倍。完全并行搜索的Entirely算法平均搜索时间减少了70%。由于程序中使用的是静态内存申请策略,使得Entirely算法的内存消耗与Native算法申请的内存差别不大,是顺序模式下的分组压缩算法的1.5倍。