基于约束依赖图的并发程序模型检测工具
作者:
作者单位:

作者简介:

苏杰(1993-),男,博士生,CCF学生会员,主要研究领域为并发程序模型检测,形式化验证;田聪(1981-),女,博士,教授,CCF杰出会员,主要研究领域为软件安全,形式化方法,模型检测;杨祖超(1997-),男,博士生,主要研究领域为软件安全,形式化方法,并发程序数据竞争检测;段振华(1948-),男,博士,教授,博士生导师,CCF会士,主要研究领域为高可信软件开发及验证.

通讯作者:

田聪,E-mail:ctian@mail.xidian.edu.cn

中图分类号:

基金项目:

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


Model Checking Tool for Concurrent Program Based on Constrained Dependency Graph
Author:
Affiliation:

Fund Project:

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

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

    Abstract:

    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.

    参考文献
    相似文献
    引证文献
引用本文

苏杰,杨祖超,田聪,段振华.基于约束依赖图的并发程序模型检测工具.软件学报,2023,34(7):3064-3079

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2022-09-04
  • 最后修改日期:2022-10-08
  • 录用日期:
  • 在线发布日期: 2022-12-30
  • 出版日期: 2023-07-06
文章二维码
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号