| 引用本文: | 李硕川,王赞,马明旭,陈翔,赵英全,王海弛,王昊宇.GC-MCR:有向图约束指导的并发缺陷检测方法.软件学报,2023,34(8):3485-3506 |
| |
|
| 摘要: |
| 约束求解应用到程序分析的多个领域，在并发程序分析方面也得到了深入的应用.并发程序随着多核处理器的快速发展而得到广泛使用，然而并发缺陷对并发程序的安全性和可靠性造成了严重的影响，因此，针对并发缺陷的检测尤为重要.并发程序线程运行的不确定性导致的线程交织爆炸问题，给并发缺陷的检测带来了一定挑战.已有并发缺陷检测算法通过约减无效线程交织，以降低在并发程序状态空间内的探索开销.比如，最大因果模型算法把并发程序状态空间的探索问题转换成约束求解问题.然而，其在约束构建过程中会产生大量冗余和冲突的约束，大幅度增加了约束求解的时间以及约束求解器的调用次数，降低了并发程序状态空间的探索效率.针对上述问题，提出了一种有向图约束指导的并发缺陷检测方法GC-MCR （directed graph constraint-guided maximal causality reduction）.该方法旨在通过使用有向图对约束进行过滤和约减，从而提高约束求解速度，并进一步提高并发程序状态空间的探索效率.实验结果表明：GC-MCR方法构建的有向图可以有效优化约束的表达式，从而提高约束求解器的求解速度并减少求解器的调用次数.与现有的J-MCR方法相比，GC-MCR的并发程序缺陷检测效率可以取得显著提升，且不会降低并发缺陷的检测能力，在现有研究方法广泛使用的38组并发测试程序上的测试时间可以平均减少34.01%. |
| 关键词: 并发程序 最大因果约减 约束求解 有向图 冲突约束过滤 |
| DOI：10.13328/j.cnki.jos.006865 |
| 分类号: |
| 基金项目:国家自然科学基金（61872263）；天津市智能制造专项资金（20201180） |
|
| GC-MCR: Directed Graph Constraint-guided Concurrent Bug Detection Method |
|
LI Shuo-Chuan1, WANG Zan1, MA Ming-Xu1, CHEN Xiang2, ZHAO Ying-Quan1, WANG Hai-Chi1, WANG Hao-Yu1
|
|
1.College of Intelligence and Computing, Tianjin University, Tianjin 300350, China;2.School of Information Science and Technology, Nantong University, Nantong 226019, China
|
| 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. |
| Key words: concurrent program maximum causality reduction constraint solving directed graph conflict constraint filtering |
