软件学报

作者：李硕川，王赞，马明旭，陈翔，赵英全，王海弛，王昊宇

单位：李硕川，天津大学 智能与计算学部, 天津 30035011,王赞，天津大学 智能与计算学部, 天津 30035002,马明旭，天津大学 智能与计算学部, 天津 30035003,陈翔，南通大学 信息科学技术学院, 江苏 南通 22601904,赵英全，天津大学 智能与计算学部, 天津 30035005,王海弛，天津大学 智能与计算学部, 天津 30035006,王昊宇，天津大学 智能与计算学部, 天津 30035007

关键词：并发程序;最大因果约减;约束求解;有向图;冲突约束过滤

基金：国家自然科学基金（61872263）；天津市智能制造专项资金（20201180）

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

来源：2023年第8期

《软件学报》期刊编辑部

查看软件学报杂志2023年第8期