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

Efficient Concurrent Program Model Checking Based on Grouping

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

In the era of parallel, model checking { also commonly referred as state-space search ） is an effective way to verify the cor- rectness of parallel programs. Because of the non-determinism of the threads scheduling, changing the order of the interleaving among the threads execution lead to the states increases exponentially. The state explosion problem is to be solved urgently when using the state-space searching method search program. To alleviate this phenomenon, this paper propose a group-based model checking method. Adding the directive-based language in the verified program, and let the thread grouping with different variable operation. During the verification process, real-time monitor whether the group is completed, and search the state space with the completed group information to avoid redundant states. The experimental results show that our scheme have a good effect to alleviate the state explosion problem,af- ter the directive grouping, the state set of testing program reduced on average by 67%, and improved the efficiency of the parallel pro- gram verification.