基于约束依赖图的并发程序模型检测工具  

Model Checking Tool for Concurrent Program Based on Constrained Dependency Graph

作　　者：苏杰 杨祖超 田聪[1,2] 段振华[1,2] SU Jie;YANG Zu-Chao;TIAN Cong;DUAN Zhen-Hua(Institute of Computing Theory and Technology,Xidian University,Xi’an 710071,China;State Key Laboratory of Integrated Service Networks(Xidian University),Xi’an 710071,China)

机构地区：[1]西安电子科技大学计算机理论与技术研究所,陕西西安710071 [2]综合业务网理论及关键技术国家重点实验室(西安电子科技大学),陕西西安710071

出　　处：《软件学报》2023年第7期3064-3079,共16页Journal of Software

基　　金：国家自然科学基金(62192730,62192734,61732013,62172322);科技创新2030——“新一代人工智能”重大项目(2018AAA0103202)。

摘　　要：模型检测是一种基于状态空间搜索的自动化验证方法,可以有效地提升程序的质量.然而,由于并发程序中线程调度的不确定性以及数据同步的复杂性,对该类程序验证时存在更为严重的状态空间爆炸问题.目前,大多采用基于独立性分析的偏序约简技术缩小并发程序探索空间.针对粗糙的独立性分析会显著增加需探索的等价类路径问题,开发了一款可细化线程迁移依赖性分析的并发程序模型检测工具CDG4CPV.首先,构造了待验证可达性性质对应的规约自动机;随后,根据线程迁移边的类型和共享变量访问信息构建约束依赖图;最后,利用约束依赖图剪裁控制流图在展开过程中的独立可执行分支.在SV-COMP 2022竞赛的并发程序数据集上进行了对比实验,并对工具的效率进行比较分析.实验结果表明,该工具可以有效地提升并发程序模型检测的效率.特别是,与基于BDD的程序分析算法相比,该工具可使探索状态数目平均减少91.38%,使时间和空间开销分别平均降低86.25%和69.80%.Model checking is an automatic verification approach based on the state-space exploration strategy,which can effectively improve the quality of a program.However,due to the non-deterministic of thread scheduling and the complexity of data synchronization,the state-space explosion problem in concurrent program verification is more serious.At present,the independence analysis based partial-order reduction techniques have been widely applied to reduce the exploration space of concurrent program verification tasks.In the face of the problem that imprecise independence analysis will significantly increase the number of equivalent trace classes to be explored,a concurrent program model checking tool CDG4CPV that can refine the dependencies between thread transitions has been developed.Firstly,specification automata are constructed corresponding to the reachability property.Then,a constrained dependency graph is constructed according to the types of transition edges of threads and the access information of shared variables.Finally,the constrained dependency graph is utilized to prune the independent and enabled branches when unwinding the control-flow graph.The experiments have been carried out on the concurrency track of SV-COMP 2022 benchmark suite,and the efficiency of the proposed tool is also compared and analyzed.Empirical results show that the proposed tool can effectively improve the efficiency of model checking for concurrent programs.Specially,compared with the BDD-based program analysis algorithm,the proposed tool reduces the number of explored states by 91.38%,and the time and memory overheads are reduced by 86.25%and 69.80%,respectively.

关 键 词：约束依赖图 偏序约简 并发程序 模型检测 工具 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]