软件学报ISSN1000-9825,CODENRUXUEWE-mail:jos@iscas.ac.cnJournalofSoftware,2023,34(8):3485−3506[doi:10.13328/j.cnki.jos.006865]http://www.jos.org.cn©中国科学院软件研究所版权所有.Tel:+86-10-62562563GC-MCR:有向图约束指导的并发缺陷检测方法∗李硕川1,王赞1,马明旭1,陈翔2,赵英全1,王海弛1,王昊宇11(天津大学智能与计算学部,天津300350)2(南通大学信息科学技术学院,江苏南通226019)通信作者:王赞,E-mail:wangzan@tju.edu.cn摘要:约束求解应用到程序分析的多个领域,在并发程序分析方面也得到了深入的应用.并发程序随着多核处理器的快速发展而得到广泛使用,然而并发缺陷对并发程序的安全性和可靠性造成了严重的影响,因此,针对并发缺陷的检测尤为重要.并发程序线程运行的不确定性导致的线程交织爆炸问题,给并发缺陷的检测带来了一定挑战.已有并发缺陷检测算法通过约减无效线程交织,以降低在并发程序状态空间内的探索开销.比如,最大因果模型算法把并发程序状态空间的探索问题转换成约束求解问题.然而,其在约束构建过程中会产生大量冗余和冲突的约束,大幅度增加了约束求解的时间以及约束求解器的调用次数,降低了并发程序状态空间的探索效率.针对上述问题,提出了一种有向图约束指导的并发缺陷检测方法GC-MCR(directedgraphconstraint-guidedmaximalcausalityreduction).该方法旨在通过使用有向图对约束进行过滤和约减,从而提高约束求解速度,并进一步提高并发程序状态空间的探索效率.实验结果表明:GC-MCR方法构建的有向图可以有效优化约束的表达式,从而提高约束求解器的求解速度并减少求解器的调用次数.与现有的J-MCR方法相比,GC-MCR的并发程序缺陷检测效率可以取得显著提升,且不会降低并发缺陷的检测能力,在现有研究方法广泛使用的38组并发测试程序上的测试时间可以平均减少34.01%.关键词:并发程序;最大因果约减;约束求解;有向图;冲突约束过滤中图法分类号:TP311中文引用格式:李硕川,王赞,马明旭,陈翔,赵英全,王海弛,王昊宇.GC-MCR:有向图约束指导的并发缺陷检测方法.软件学报,2023,34(8):3485–3506.http://www.jos.org.cn/1000-9825/6865.htm英文引用格式:LiSC,WangZ,MaMX,ChenX,ZhaoYQ,WangHC,WangHY.GC-MCR:DirectedGraphConstraint-guidedConcurrentBugDetectionMethod.RuanJianXueBao/JournalofSoftware,2023,34(8):3485−3506(inChinese).http://www.jos.org.cn/1000-9825/6865.htmGC-MCR:DirectedGraphConstraint-guidedConcurrentB...
