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:[phone] 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%,而冲突的约束在求解过程中甚至存在不可解的问题并消耗了大量时间,大幅度降低并发缺陷的检测效率.针对上述问题,本文以最大因果约减算法中的约束为研究对象,通过过滤冲突约束并约减冗余约束,以提高并发缺陷检测的效率,最终设计了一种有向图约束指导的并发缺陷检测方法 GC-MCR(directed graph 李硕川 等:GC-MCR:有向图约束指导的并发缺陷检测方法 3487 constraint-guided maximal causality reduction).GC-MCR 首先根据程序基本约束关系(即 happens-before 约束、锁互斥约束等)来构建有向图;然后,对基于最大因果约减算法18生成的读写约束进行解析与拆分,即将读写约束构建成读写约束树,根据程序基本约束关系的有向图,获得读写约束树中每个节点的值,该值表示以当前节点为根节点的子树是否与程序基本约束冲突;最后,根据读写约束树中每个节点的值,判断是否过滤或约减约束.GC-MCR 通过对冲突约束进行过滤,并约减冗余约束的表达式,有效降低单次约束的求解时间甚至减少约束求解器的调用次数,因此能够保证并发缺陷的检测能力,并提高并发缺陷效率.本文选择在已有研究工作中广泛使用的 38 组并发程序作为实验对象,这 38 组并发程序包含的缺陷类型覆盖了死锁、数据竞争、原子性违背、顺序违背等.实验结果表明:GC-MCR 方法无论是在约束求解器的调用次数以及单次调用时间方面,还是从探索并发程序状态空间的效率方面,都显著优于现有方法,与 J-MCR 相比,在总的调度数量没有损失的情况下,即并发缺陷的检测能力没有任何损失,程序的约束求解次数和总调用时间可平均减少 34.01%.本文的主要贡献总结如下.基于有向图设计并发约束的表示方法,从有向图结构上识别出潜在的不可解并发约束,优化冗余并发约束,提高并发约束表示的准确性;提出一种新的有向图约束指导的并发缺陷检测方法 GC-MCR.GC-MCR 基于本文提出的有向图表示方法构建完整的并发程序约束,并对其进行过滤和约减,可以有效减少约束求解成本,从而提高探索并发程序状态空间的效率;实现并开源了 GC-MCR(https:/ 38 个并发测试程序上进行了验证.实验结果表明:相比于现有研究方法,GC-MCR 可以更快地找出并发程序中的缺陷,其平均性能可提升 34.01%.1 背景知识 本文的主要目标是通过有向图表示的方法构建完整的并发程序约束,并对其进行过滤和约减,减少约束求解成本,提高探索并发程序状态空间的效率.与本文方法相关的理论和方法包括:作为 GC-MCR 的基础模型最大因果模型(maximal causal model,MCM)5,19、在最大因果模型的基础上提出的最大因果约减算法18以及约束的构建与求解的工具 Z320.1.1 最大因果模型 最大因果模型5,19根据给定的程序执行轨迹构建出最大且合理的因果模型,其包含所有能生成原始轨迹的并发程序所生成的所有轨迹,即:假如并发程序 P 能够生成原始轨迹,则 P 生成的所有轨迹都包含在最大因果模型中.因此,最大因果模型可以发现在庞大的状态空间中尚未被执行到的线程交织.在 MCM 中,事件(event)是线程在并发对象上执行的原子操作,其中,事件的属性包括:访问一个并发对象的线程 Thread、对该并发对象进行的操作类型 OP、该事件访问的并发对象 Target、对并发对象执行的操作值 Data.对于两个事件s1和 s2,当且仅当 s1和 s2所对应的全部属性都相等,称事件 s1和 s2相等.MCM 事件的类型和对应描述如下所示.begin(t):线程 t 中的第 1 个事件;end(t):线程 t 中最后一个事件;read(t,x,v):线程 t 读到 x 的值为 v;write(t,x,v):线程 t 写入变量 x 的值为 v;lock(t,l):线程 t 获取锁 l;unlock(t,l):线程 t 释放锁 l;fork(t,t):线程 t 创建新线程 t;join(t,t):阻塞线程 t 直到 t运行结束.在MCM中,程序的一条执行轨迹(execution trace)可以被抽象为一组事件的序列,并且规定执行轨迹需要 3488 软件学报 2023 年第 34 卷第 8 期 满足顺序一致性,即读写一致性、锁互斥和先发生于原则(happens-before).其中,读写一致性需要保证读(read)的值是执行轨迹在该读事件之前,且距离其最近,且与其访问同一个共享内存地址的写(write)的值.锁互斥需要保证每个释放(release)锁事件之前都有同一个线程且同一个锁变量的获得(acquire)锁事件与其匹配,且对每一个 Acquire-Release 锁对都不可与其他访问同一锁变量的锁对产生交织.happens-before 原则需要保证程序按照代码的顺序执行;对 volatile 修饰的变量进行的写操作要先发生于对其进行的读操作;对同一个锁的解锁操作要先发生于对其的加锁操作;如果操作 A 先发生于操作 B,操作 B 先发生于操作 C,那么 A 应该先发生于操作 C;在线程 A 中调用 B.start()之前的所有操作先发生于线程 B 的所有操作;在线程 A 中调用 B.join()会先执行线程 B,即线程 B 中的所有操作先发生于在线程 A 中的 join 后面的所有操作.在 MCM 中,feasible()是由能够产生执行轨迹的所有由程序的执行产生的顺序一致性轨迹构成最小的集合,feasible()也是最大因果模型的最终结果.feasible()需要满足前缀闭合性(prefix closedness)和局部确定性(local determinism).前缀闭合性假设事件是独立、不可分割的,且是根据程序的执行按顺序生成的,因此,feasible()必须是前缀闭合的.局部确定性假设并发操作的执行是由同一线程中的之前发生的事件确定的,并且可以在它们之后的任意时刻发生.1.2 最大因果约减算法 最大因果约减算法通过构建并发程序的最大因果模型,将探索程序状态空间问题转换为约束求解问题.最大因果约减算法如图 1 所示,先输入一个被测程序,通过模型检查器(model checker)按照指定的线程交织得到程序的执行轨迹(trace).在模型检查器中的调度器通过控制线程的调度探索指定线程交织.然后,通过最大因果引擎(maximal causality engine)生成新的种子线程交织,并将其添加到被测程序的状态空间中,使得该交织之后可以被模型检查器再次使用,并通过运行获取新的种子交织.对于一个线程交织 s,通过前文介绍的最大因果模型,可以获得一组唯一且规模最大的可行性交织集合,记作 MaxCausal(s).且每个 MCR 程序运行产生的新的种子交织都是 MaxCausal(s)中的可行交织.图 1 最大因果约减算法执行流程 在并发程序的运行过程中,不同线程的交错执行会产生一系列线程交织.而每个被触发的线程交织都会使程序到达某一种状态(state).这里规定:当程序执行之前产生新交织时,如果从同一个变量上读到和之前不同的值从而使得程序进入了一个新的状态,那么算法需要将这一状态加入到被测程序的状态空间中.当被测程序的状态空间已满,即所有的种子交织都已经被探索过,且没有新的种子交织生成时,即可以认为被测程序的状态空间已经被完全覆盖了.这里,MCR 提出了一个新的约束 Race 约束,即假设 COP(x,y)表示一个全局变量在不同线程中的读写对,那么对于程序中每一个存在的 COP 关系的全局变量,需要对这些变量的每一个读事件 R 进行约束,即所有 happens-before 于 R 的读事件读到与之前一样的值,且 R 应当读到一个与之前完全不一样的值.由于每次程序读到新值都可能导致程序到达一个与之前不同的状态,因此,通过在程序的约束求解的过程中不断地读到新值,可以获得一棵程序的状态树,而这棵树就可以覆盖程序中所有可能的程序状态.输入:测试程序线程交织程序执行轨迹线程交织 1 线程交织 2 模型检查器种子交织错误报告 输出:最大因果引擎 李硕川 等:GC-MCR:有向图约束指导的并发缺陷检测方法 3489 导致并发程序的状态空间庞大的原因有两方面:一是由于线程的组合可以是多种多样的,且其中大部分都是可行的以及线程的调度是不确定的;另一方面,并发程序的状态空间存在大量等价的线程交织,除线程的调度顺序不同,读取到的数据是一致的,即这些等价的线程是不能够使程序到达一个新的不同的状态.大量等价线程交织使其他算法执行时间相对较长.而最大因果约减算法虽然也会重复地执行被测程序,通过干预线程调度,执行所有调度并检查当前调度的可行性,产生新的种子交织.然而,该算法仅当读到新值时才会识别程序到达了一个新的状态,并将当前线程调度加入到当前程序的状态空间中,从而能够最大化约减状态空间.1.3 约束的构建与求解 本文将最大因果约减算法中的约束分为程序基本约束和读写约束:程序基本约束是程序中对 happens-before 原则的约束体现,其中包括程序顺序约束、线程约束、锁约束等;读写约束则是约束不同线程对同一共享变量按照指定读写要求进行读写,其中,读写要求是程序中所有线程的读事件中有且只有一个读事件 R 读到新的值,而发生在 R 前的读事件需要读到旧的值.如图 2 程序所示:T1 和 T2 是两个线程,则图中程序基本约束是 x1x2,x3x4,x4x5,x5x6,即同一线程中程序按照代码的顺序执行;假如第 4 行 x 应读到值 1,则读写约束为 x3x1,x1x1 x9)(x1 x9)是一个约束单元,实际意义为事件 x1 在事件 x9 之后发生;图 3 中,(x1 x2)既是一个约束单元,又是一个子约束.每个 assert 语句之间是 and 关系,即当且仅当每个约束都为真,才能表示整体约束是满足的.图 3 程序基本约束示例 (a)冲突约束 (b)冗余约束 图 4 读写约束示例 冲突约束 图 4 中,读写约束(a)中的 x8x9,x3x7,x9x4,x3x6 冲突,而其他约束与程序基本约束一致.通过逻辑运算判断,其最终结果为 false,与程序基本约束冲突,即满足程序基本约束的条件下读写约束不成立.故定义这类与程序基本约束冲突的读写约束为冲突约束.冲突约束即不可解约束.并发测试程序 dekker 中存在 150 个冲突,在使用约束求解器求解前,识别并过滤这类冲突约束,则能够节省大量计算资源.冗余约束 进一步分析发现:读写约束(b)中的 x3x6 冲突;而另一部分 x1x9 与程序基本约束不冲突,且在满足程序基本约束的条件下读写约束(b)成立.故定义这类部分子约束与程序基本约束冲突,且约束整体与基本约束不冲突的读写约束为冗余约束.冗余约束能够根据程序基本约束进行约减,图4中的冗余约束就可以被约减为(x1 x9).而对于约减后的约束,约束求解器可以更快地进行求解,节省程序在约束求解步骤中的求解计算资源.而且对约束进行过滤与约减产生的时间开销远小于求解器求解原约束的时间开销.基于上述分析,本文提出了一种有向图约束指导的并发缺陷检测方法 GC-MCR.首先,把约束分为读写约束和程序基本约束.然后,先将程序基本约束构建成有向图,再将读写约束构建成前缀树.最后,根据有向图判断读写约束中是否存在冲突约束和冗余约束:若存在冲突约束,则过滤掉当前约束;若存在冗余约束,则将其约减后,再次调用约束求解器进行求解,从而提高并发缺陷检测效率.2.2 方法流程 2.2.1 整体框架:输入/输出及整体流程简介 GC-MCR 方法的输入是并发测试程序,输出是程序的并发缺陷错误报告.首先,模型检查器执行并发测试程序,获取程序的初始执行轨迹.最大因果引擎分析处理执行轨迹,生成满足MCM和Race约束的约束.然后,GC-MCR 方法将约束分为读写约束和程序基本约束:程序基本约束被分析并重构成有向图,读写约束被 李硕川 等:GC-MCR:有向图约束指导的并发缺陷检测方法 3491 分析、拆分并重组成读写约束树.随后,约束过滤器根据有向图计算读写约束树中每个节点的值,并根据读写约束树根节点的值判断:是否跳过当前求解或约减当前约束.假如进行约束求解,求解得到的线程交织会存储到线程交织集合中.最后,模型检查器通过依次执行线程交织集合中的线程交织,获取程序执行轨迹并检测程序是否存在并发缺陷:假如检测到并发缺陷,则输出错误报告;反之,则重复上述操作.GC-MCR 方法的具体工作流程如图 5 所示.图 5 基于有向图构建约束的并发缺陷检测方法流程图 2.2.2 基于有向图的程序基本约束重构 图 3 中约束为 GC-MCR 生成的程序基本约束,程序基本约束都满足 happens-before 原则.根据顺序一致性模型的定义,程序中的约束必须遵循 happens-before 原则,因此不应该存在违背程序基本约束的约束.图 6是本方法生成的有向图,表示程序中各个调度点在满足 happens-before 原则下的顺序关系.图 6 基本约束的有向图 由于程序基本约束中的顺序不等式存在传递性关系,且不是所有调度点都存在这些顺序关系,因此,通过数轴上的大小表示难于归纳出所有调度点的顺序关系.而为了清晰表明调度点的顺序关系,本方法将这些顺序关系转化为有向图来表示.具体实现时,使用邻接表构建有向图,并定义新的节点类,其中包含当前节点对应的调度点和在有向图中直接指向该调度点的节点的集合.在图 3 中,若存在约束 x1x2,则在有向图中构建 x1 指向 x2 的边.不断重复该过程,直至最终构建出该有向图.如算法 1 所示:首先分析程序基本约束中每对调度点间的关系,然后在图中找到对应节点,最后将节点间指向关系存储在邻接表中.通过上述步骤,使用有向图表示程序基本约束关系,仅通过遍历该有向图,即可获得程序中线程调度点间的关系,用于后续处理读写约束.测试程序 错误报告 输入 输出 模型检查器验证 执行 程序执行轨迹 是否触发错误最大因果引擎 线程交织线程交织集合约束求解器 选择求解 构造输入 基本约束有向图基本约束过滤分类读写约束冗余约束读写约束树解析构造冲突约束约束过滤器约减后约束 x3 x5 x1 x2x6x7x8x4x9约减 3492 软件学报 2023 年第 34 卷第 8 期 算法 1.基于有向图的程序基本约束重构.输入:base:程序基本约束;输出:G:由邻接表构成的有向图.1 G;2 for i in base do 3 option,target,nextanalysisConstraint(i);4 targetNode,nextNodefindNode(target,next,G);5 targetNode.largeNodes.add(nextNode);6 end for 7 return G 2.2.3 读写约束的解析与拆分 读写约束的生成是 GC-MCR 的核心步骤,该步骤确保所有共享变量的每一个读事件 R 需要满足两个条件:读事件 R 要读到一个之前没有读到过的值;所有发生在读事件 R 之前的读事件要读到和原来一样的值.这样保证只有一个读事件读到新值,其余读事件仍读到原值.例如:对于变量 x,若需要读取新值,则让其中一个具有新的写值的写 x 事件排在该读 x 事件之前;若需要保持读取到原值,则应当保证新的 x 写事件在该读事件之后.因此,GC-MCR 能够通过控制读写事件,改变调度点的顺序排布.然而,令一个读事件读到新值有多种限制和可能情况,其中既包含保证新的x的写入值的约束,又包含保证其他读事件的值保持不变的约束,因此读写约束颇为复杂.如图 4 所示,读写约束(a)是由多个 or 和 and 组合表示的约束.现有方法将这类读写约束和先前生成的程序基本约束传入约束求解器中进行求解,获得调度点的顺序关系后再解析成新的线程调度序列,进行线程定向调度,最终探索程序整个状态空间.然而,现有方法忽视了读写约束和程序基本约束之间的关系,其中包含明显冲突的约束和冗余的约束,冲突约束不需要调用约束求解器进行求解,冗余约束可以约减后进行求解.通过过滤冲突约束和约减冗余约束,能够有效减少单次求解时间甚至减少约束求解器的调用次数,显著提高并发缺陷检测效率.因此,GC-MCR 对读写约束进行解析.图 7 是根据图 4 中的读写约束(a)构造的前缀树,其中:非叶子节点皆是 and/or 的逻辑运算符,叶子节点则是调度点的顺序关系.后续用于遍历程序基本约束有向图进行冲突分析.具体算法见算法 2.图 7 读写约束树 算法 2.读写约束的解析与拆分.输入:rw:程序的一条读写约束;G:程序基本约束的有向图;输出:T:以前缀表达式表示的读写约束树,树中的每个节点包含当前节点的布尔值以及从叶子节点到当前节点的约束表达式.1 T;2 listsplit(rw);3 for s in list do x8x7x9x8 x3x5x1x4x1x6x3x6orororandand and 李硕川 等:GC-MCR:有向图约束指导的并发缺陷检测方法 3493 4 if s then 5 target,nextanalysisConstraint(s);6 isConf lictisConflictWithOrderMap(target,next,G);7 expressiongetConstraintExpression(s,target,next,isConf lict);8 T.add(Pair(isConf lict,expression);9 else 10 T.add(Pair(s,s);11 end if 12 end for 13 return T;例如,其中一个叶子节点中 x3x9,查看在图 6 中是否存在 x9x3,即是否存在一条由 x9 到 x3 的路径(第6 行):若存在,则设该叶子节点为 false,表示该子表达式中存在冲突;反之,该叶子节点为 true,表示该子表达式中不存在冲突.然后,对每个叶子节点执行该操作,将全部叶子节点的结果替换为 true/false;同时,每个叶子节点还应存储当前节点的约束表达式(第 7 行、第 8 行),后续用于约束表达式约减.最终,经过冲突分析后,叶子节点应全部变为 true/false.此时,整棵树为一个由 and/or 和 true/false 组成的运算树.最终,只需将该运算树进行运算即可.若结果为 false,则表示该读写约束与程序基本约束冲突,直接跳过此次对约束求解器的调用即可;反之,则约减当前约束.被过滤约束没有调用约束求解器,这部分时间被过滤算法优化,从而提高并发缺陷检测效率.2.2.4 约束表达式约减 对冗余约束的约减,GC-MCR 将约减其中冲突的子表达式,最后对约减后的约束表达式及程序基本约束的表达式调用约束求解器进行求解.本文中,读写约束树的每个节点既包含以当前节点为根节点的子树是否满足程序基本约束的值,又包含子树的约束表达式,称约束表达式前缀树中的叶子节点中的约束表达式为子表达式.首先,将子表达式与程序基本约束冲突的叶子节点的值置为 false,其余叶子节点的值置为 true.如图 8 所示,赋值后的前缀树的叶子结点为 true/false,在图中使用 T 表示 true,F 表示 false.然后,根据父节点的操作符及其两个子节点的值,考虑以下 5 种情况.a)父节点为 and,两个子节点皆为 true,如图 9(a)所示:将父节点的值置为 true,并将父节点的约束表达式置为 and 关系的两个子节点的约束表达式;b)父节点为 or,两个子节点皆为 true,如图 9(b)所示:将父节点的值置为 true,并将父节点的约束表达式置为 or 关系的两个子节点的约束表达式;c)父节点为 or,两个子节点皆为 false,如图 9(c)所示:将父结点的值置为 false,并将父节点的约束表达式置为空;d)父节点为 and,两个子节点中至少一个为 false,如图 9(d)所示:将父节点的值置为 false,并将父节点的约束表达式置为空;e)父节点为 or,两个子节点中仅一个为 true,如图 9(e)所示:将父结点的值置换为 true,并将父节点的约束表达式置为值为 true 子节点的约束表达式.重复上述操作,直至读写约束树中仅存在根节点.此时,根据根节点的值判断是否使用约束求解器进行约束求解:若值为 false,则不需要;反之,使用根节点的约束表达式,即最简的读写约束表达式,结合程序基本约束的表达式使用约束求解器进行求解,在当前例子中,最终根节点的值为 false,因此可以直接跳过约束求解步骤.执行 GC-MCR 方法的后续操作,检测并发程序中的并发缺陷.3494 软件学报 2023 年第 34 卷第 8 期 图 8 前缀树替换的示例 (a)父节点为 and,两个子节点皆为 true (b)父节点为 or,两个子节点皆为 true (c)父节点为 or,两个子节点皆为 false (d)父节点为 and,两个子节点中至少一个为 false (e)父节点为 or,两个子节点中仅一个为 true 图 9 前缀树简化的示例 andand oror TF F F TTTFF andand orandand andandand oror ororororTTT TTT F F FFF andand andand TT TTTF oror orororTF F F FFF andand andand andorororF F FF F F F FTTTTTandand and and andor orand or oror FFF TTT T x8x7 x9x8 x3x5x1x4x1x6 x3x6 李硕川 等:GC-MCR:有向图约束指导的并发缺陷检测方法 3495 3 实验设计与结果分析 3.1 研究问题 为了验证 GC-MCR 方法的有效性,本文从程序约束求解次数、程序运行时间和程序调度次数的角度设计了 3 个研究问题.(1)RQ1:GC-MCR 方法是否有效减少程序约束求解的次数,减少约束求解器的计算资源消耗?由于调用约束求解器进行约束求解相比于程序调度更加耗时,如果可以减少程序的约束求解次数,降低约束求解器的计算资源消耗,对并发缺陷检测有着重要意义.现有方法18在约束进行约束求解前没有对约束进行任何处理,使得许多可以提前被过滤的冲突约束被约束求解器求解,增加约束求解的次数,降低探索并发程序状态空间的效率.因此,本研究问题中,本文希望分析与现有方法相比,GC-MCR 方法能否有效减少程序调用约束求解器进行约束求解的次数,降低约束求解器的计算资源消耗.(2)RQ2:GC-MCR 方法能否有效减少并发缺陷检测的时间,提高探索并发程序状态空间的效率?程序检测到并发缺陷所需时间是评估并发缺陷检测效率的一个重要指标.通过统计程序约束求解的次数以及程序的运行时间,还可以分析两者之间的关系,即是否可以通过减少约束求解次数以降低并发缺陷检测所消耗的时间,以及影响并发缺陷检测的因素.因此,在本研究问题中,本文希望从多种角度来分析与现有方法相比,GC-MCR 方法能否有效减少并发缺陷检测的时间,提高并发程序状态空间的探索效率.(3)RQ3:GC-MCR 方法是否可以保证现有方法的并发缺陷检测能力?现有的研究方法在并发缺陷检测上已取得一定的效果,即可以使用最少的调度次数准确找到并发程序中的缺陷.而并发程序的调度次数同时也是衡量并发缺陷检测能力的一个主要指标.如果 GC-MCR 方法的调度次数与现有方法的调度次数相等甚至更少,且发现相同缺陷,则并发缺陷检测能力没有下降.因此,在本研究问题中,本文希望验证与现有方法相比,GC-MCR 方法能否拥有相同甚至更优的并发缺陷检测能力.3.2 实验配置 测试对象 本文通过从现有研究18,22,23广泛使用的并发数据集中收集一组包含 38 个含有并发缺陷的测试程序作为测试对象.表 1 显示了这些类的详细信息,其中,?ID 列表示测试程序的实验序号;?测试程序的列表示测试程序的名称;?代码行数的列表示测试程序中的代码行数(使用 Statistic 工具统计);?线程数量的列表示测试程序中线程的数量;?变量数量的列表示测试程序中定义的变量数量,其中包含来自它