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

作     者：苏杰 杨祖超 田聪 段振华 SU Jie;YANG Zu-Chao;TIAN Cong;DUAN Zhen-Hua

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

出 版 物：《软件学报》 (Journal of Software)

年 卷 期：2023年第34卷第7期

页      面：3064-3079页

核心收录：

学科分类：08[工学] 0812[工学-计算机科学与技术（可授工学、理学学位）] 081202[工学-计算机软件与理论] 

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

主　　题：约束依赖图 偏序约简 并发程序 模型检测 工具 

摘      要：模型检测是一种基于状态空间搜索的自动化验证方法,可以有效地提升程序的质量.然而,由于并发程序中线程调度的不确定性以及数据同步的复杂性,对该类程序验证时存在更为严重的状态空间爆炸问题.目前,大多采用基于独立性分析的偏序约简技术缩小并发程序探索空间.针对粗糙的独立性分析会显著增加需探索的等价类路径问题,开发了一款可细化线程迁移依赖性分析的并发程序模型检测工具CDG4CPV.首先,构造了待验证可达性性质对应的规约自动机;随后,根据线程迁移边的类型和共享变量访问信息构建约束依赖图;最后,利用约束依赖图剪裁控制流图在展开过程中的独立可执行分支.在SV-COMP 2022竞赛的并发程序数据集上进行了对比实验,并对工具的效率进行比较分析.实验结果表明,该工具可以有效地提升并发程序模型检测的效率.特别是,与基于BDD的程序分析算法相比,该工具可使探索状态数目平均减少91.38%,使时间和空间开销分别平均降低86.25%和69.80%.