GC-MCR:有向图约束指导的并发缺陷检测方法
作者:
作者单位:

作者简介:

李硕川(1999-),男,硕士生,CCF学生会员,主要研究领域为并发缺陷检测,系统软件分析;赵英全(1994-),男,博士生,主要研究领域为编译器测试,JVM测试,并发测试;王赞(1979-),男,博士,副教授,CCF专业会员,主要研究领域为软件测试,机器学习;王海弛(1996-),男,博士生,主要研究领域为系统软件分析;马明旭(1999-),男,学士,主要研究领域为并发测试;王昊宇(1999-),男,硕士生,CCF学生会员,主要研究领域为并发缺陷检测,编译器测试;陈翔(1980-),男,博士,副教授,CCF高级会员,主要研究领域为智能软件工程,软件仓库挖掘,软件测试与维护.

通讯作者:

王赞,E-mail:wangzan@tju.edu.cn

中图分类号:

基金项目:

国家自然科学基金(61872263);天津市智能制造专项资金(20201180)


GC-MCR: Directed Graph Constraint-guided Concurrent Bug Detection Method
Author:
Affiliation:

Fund Project:

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

    约束求解应用到程序分析的多个领域,在并发程序分析方面也得到了深入的应用.并发程序随着多核处理器的快速发展而得到广泛使用,然而并发缺陷对并发程序的安全性和可靠性造成了严重的影响,因此,针对并发缺陷的检测尤为重要.并发程序线程运行的不确定性导致的线程交织爆炸问题,给并发缺陷的检测带来了一定挑战.已有并发缺陷检测算法通过约减无效线程交织,以降低在并发程序状态空间内的探索开销.比如,最大因果模型算法把并发程序状态空间的探索问题转换成约束求解问题.然而,其在约束构建过程中会产生大量冗余和冲突的约束,大幅度增加了约束求解的时间以及约束求解器的调用次数,降低了并发程序状态空间的探索效率.针对上述问题,提出了一种有向图约束指导的并发缺陷检测方法GC-MCR (directed graph constraint-guided maximal causality reduction).该方法旨在通过使用有向图对约束进行过滤和约减,从而提高约束求解速度,并进一步提高并发程序状态空间的探索效率.实验结果表明:GC-MCR方法构建的有向图可以有效优化约束的表达式,从而提高约束求解器的求解速度并减少求解器的调用次数.与现有的J-MCR方法相比,GC-MCR的并发程序缺陷检测效率可以取得显著提升,且不会降低并发缺陷的检测能力,在现有研究方法广泛使用的38组并发测试程序上的测试时间可以平均减少34.01%.

    Abstract:

    Constraint solving has been applied to many domains of program analysis, and deeply applied in concurrent program analysis. Concurrent programs are specific domain software that has been widely used with the rapid development of multi-core processors. However, concurrent defects threaten the security and robustness of concurrent programs, thus it is of great importance to test concurrent programs. Due to the non-deterministic thread scheduling, one of the key challenges for concurrent program testing is how to reduce the thread interleaving space with exponential growth. The state-of-the-art approaches (i.e., J-MCR) tackle the challenge through constraint solving. However, it is found that there exist conflicts and redundancies inside constraints (i.e., the conflict of constraint clauses makes constraints unsatisfiable), solving those unsatisfiable constraints results in lower efficiency. Thus, a directed graph constraint-guided method called GC-MCR (directed graph constraint-guided maximal causality reduction) is proposed. By removing conflictive constraints and simplify redundant constraints, the times of constraint solving are reduced thereby further improving the efficiency. Comparing with state-of-the-art approach J-MCR, GC-MCR reduces the times of constraint solving by 19.36% on average and reduces the testing time on average by 34.01% on 38 concurrent programs.

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

李硕川,王赞,马明旭,陈翔,赵英全,王海弛,王昊宇. GC-MCR:有向图约束指导的并发缺陷检测方法.软件学报,2023,34(8):3485-3506

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

京公网安备 11040202500063号