GC-MCR：有向图约束指导的并发缺陷检测方法.pdf

软件学报 ISSN 1000-9825,CODEN RUXUEW E-mail: Journal of Software,2023,34(8):34853506 doi:10.13328/ki.jos.006865 http:/ 中国科学院软件研究所版权所有.Tel:+86-10-62562563 GC-MCR:有向图约束指导的并发缺陷检测方法 李硕川1,王 赞1,马明旭1,陈 翔2,赵英全1,王海弛1,王昊宇1 1(天津大学 智能与计算学部,天津 300350)2(南通大学 信息科学技术学院,江苏 南通 226019)通信作者:王赞,E-mail: 摘 要:约束求解应用到程序分析的多个领域,在并发程序分析方面也得到了深入的应用.并发程序随着多核处理器的快速发展而得到广泛使用,然而并发缺陷对并发程序的安全性和可靠性造成了严重的影响,因此,针对并发缺陷的检测尤为重要.并发程序线程运行的不确定性导致的线程交织爆炸问题,给并发缺陷的检测带来了一定挑战.已有并发缺陷检测算法通过约减无效线程交织,以降低在并发程序状态空间内的探索开销.比如,最大因果模型算法把并发程序状态空间的探索问题转换成约束求解问题.然而,其在约束构建过程中会产生大量冗余和冲突的约束,大幅度增加了约束求解的时间以及约束求解器的调用次数,降低了并发程序状态空间的探索效率.针对上述问题,提出了一种有向图约束指导的并发缺陷检测方法 GC-MCR(directed graph constraint-guided maximal causality reduction).该方法旨在通过使用有向图对约束进行过滤和约减,从而提高约束求解速度,并进一步提高并发程序状态空间的探索效率.实验结果表明:GC-MCR 方法构建的有向图可以有效优化约束的表达式,从而提高约束求解器的求解速度并减少求解器的调用次数.与现有的 J-MCR 方法相比,GC-MCR 的并发程序缺陷检测效率可以取得显著提升,且不会降低并发缺陷的检测能力,在现有研究方法广泛使用的38组并发测试程序上的测试时间可以平均减少 34.01%.关键词:并发程序;最大因果约减;约束求解;有向图;冲突约束过滤 中图法分类号:TP311 中文引用格式:李硕川,王赞,马明旭,陈翔,赵英全,王海弛,王昊宇.GC-MCR:有向图约束指导的并发缺陷检测方法.软件学报,2023,34(8):34853506.http:/ 英文引用格式:Li SC,Wang Z,Ma MX,Chen X,Zhao YQ,Wang HC,Wang HY.GC-MCR:Directed Graph Constraint-guided Concurrent Bug Detection Method.Ruan Jian Xue Bao/Journal of Software,2023,34(8):34853506(in Chinese).http:/ 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 基金项目:国家自然科学基金(61872263);天津市智能制造专项资金(20201180)本文由“约束求解与定理证明”专题特约编辑蔡少伟研究员、陈振邦教授、王戟研究员、詹博华副研究员、赵永望教授推荐.收稿时间:2022-09-04;修改时间:2022-10-13;采用时间:2022-12-14;jos 在线出版时间:2022-12-30 3486 软件学报 2023 年第 34 卷第 8 期 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 目前,约束求解作为符号执行的重要组成部分,已在软件验证、程序分析等领域得到了广泛应用,其在并发程序分析领域的贡献尤为突出.并发程序以计算速度快且资源利用率高为特点,在当今多核架构广泛应用的硬并发时代,其应用越发普遍.从微观角度看,并发程序的线程调度(即某一时刻每个线程是否运行)是由CPU 决定的,而不是由用户决定的1.因此,在程序默认配置下,线程的执行顺序具有一定的不确定性.这种不确定性导致开发者难以预料程序的状态,使得程序内部易出现并发缺陷,可能会造成严重事故.例如,2012年,Facebook 上市当天,纳斯达克的交易程序出现并发缺陷(即由于大量的撤单导致程序一直重新运行并进入死循环,出现了数据竞争问题),导致20分钟无法开盘,给Facebook造成了巨大损失.故而在实际项目开发中,需要对并发程序进行充分的测试,以避免并发缺陷可能造成的不良影响.因此,针对并发软件的自动缺陷检测技术研究具有重大意义,其研究成果有助于快速有效地检测出各类并发缺陷,以保证并发软件的质量和可靠性.近些年来,针对并发程序的测试在软件工程领域得到了广泛的关注,并发缺陷检测的相关技术逐渐成为研究热点.目前,国内外已经发表多篇与并发缺陷检测相关的综述论文13,现有研究从不同角度对并发缺陷检测进行了深入探索并取得了丰富的研究成果,在此基础上,也开发了一些成熟的并发检测工具.目前常见的并发缺陷可以分为 4 种:死锁4、数据竞争5、原子性违背6和顺序违背7.为检测这 4 种并发缺陷,研究人员提出了动态分析8、静态分析9以及动静结合分析10这 3 类方法.其中,动态分析通过动态执行被测程序,旨在触发程序异常,且触发的异常问题都是真实存在的;静态分析基于缺陷模式的规则,提取和对比分析代码中的模式以检测缺陷11.符号执行作为静态分析的主要方式,通过对符号化的程序路径约束进行约束求解,探索程序状态空间;动静结合分析则充分利用动态分析和静态分析的优点,即动态分析可以提升静态分析可靠性,静态分析可以降低动态分析的验证负载2,3.并发程序的测试和验证面临的主要挑战是线程交织(thread interleaving)空间爆炸问题,即:可能的线程交织数量随着线程数量和程序执行时间的增加而呈指数级增长,使并发缺陷难以被检测.解决线程交织爆炸的关键是识别冗余的线程交织12.为解决这一问题,研究人员提出了偏序约减方法(partial order reduction,POR)1315,即:通过检查程序各个状态和行为间的独立性,以减小整体状态空间规模.首先,POR 会将所有线程交织划分为不同的 Mazurkiewicz 轨迹16,即所有线程交织被分成的不同等价类;然后,POR 从每个Mazurkiewicz 轨迹中选取一个线程交织进行探索.由于 Mazurkiewicz 轨迹基于 happens-before 关系17,且happens-before 关系依赖于所有锁的释放和获取以及冲突的写事件和读事件,POR 在识别冗余线程的交织方面存在局限性,即仅符合 happens-before 关系的线程交织中大部分线程交织存在冗余18.针对这一问题,Huang等人提出了最大因果约减算法(maximal causality reduction,MCR)18.MCR 基于 Mazurkiewicz 轨迹制定了新标准:最大因果关系(maximal causality relation),即根据读和写事件的值划分 Mazurkiewicz 轨迹中的最大可能等效线程交织集合.MCR 将探索并发程序状态空间的问题转换成约束求解问题,稳定高效地检测并发缺陷.然而,异常庞大的并发程序状态空间会导致MCR为事件添加的约束极其严格且复杂,复杂的约束构建易产生大量冗余甚至存在冲突的约束,这些约束会导致约束求解耗时较长.据实验统计,MCR 在约束求解上的耗时约占 MCR 运行总时间的 89.21%,而冲突的约束在求解过程中甚至存在不可解的问题并消耗了大量时间,大幅度降低并发缺陷的检测效率.针对上述问题,本文以最大因果约减算法中的约束为研究对象,通过过滤冲突约束并约减冗余约束,以提高并发缺陷检测的效率,最终设计了一种有向图约束指导