Page 131 - 《软件学报》2021年第7期

高凤娟 等:高精度的大规模程序数据竞争检测方法 2049

局变量以函数参数在函数调用之间传播的方式,使得被调用者的分析结果能够包括全局变量.以这种方式,通过
分析函数参数来分析全局变量,统一并简化了分析过程.
简化的 source-sink 模式.为数据竞争检测所设计的 source 和 sink 是对变量的读写访问操作.但是,由于读-
读访问并不会导致数据竞争,所以这样的设计模式会导致冗余分析.为了避免多余的分析,GUARD 实际上将
source 设为写操作而将 sink 设为读或写操作.这样,如果一个 source 是写而 sink 是读,就不必检查 source 和 sink
的顺序.朴素的 source-sink 模式会检查 source 和 sink 的顺序,否则,当一个访问是写而另一个访问是读时就会报
告两遍警告.所以,改进后的 source-sink 模式能够减少分析变量的数量以及检查 source 和 sink 顺序的时间.
4.2 程序中的循环
由于本文方法需要为两个分析步骤收集路径约束(即 MHP 查询和 source-sink 检测),必须使得两个分析步
骤中的约束条件保持一致.然而,当分析一个循环时,线程标签流难以确定循环执行的次数.尽管通过对 TFG 应
用转换规则能够使得 MHP 分析到达不动点,但是,由于整体分析需要结合 MHP 分析和基于 source-sink 的值流
分析,计算 MHP 的定点会存在两部分路径不一致的问题.例如,有可能出现 MHP 分析中经过 2 次某个循环但是
source-sink 则是 3 次该循环.因此,尽管 GUARD 的线程流分析和检测框架能够将各个循环分开分析,我们还是
采取了一个折中方案,即将一个循环展开 2 次,以此达到两个目的:(1) 避免计算定点;(2) 避免不一致的路径约
束.此外,根据 Saturn [30] 和 Pinpoint [17] 等工具,在基于约束条件的分析过程中,展开循环是可行的,并且将循环展开
2 次是权衡精度和效率的常用举措.

5 实验评估

为了对 GUARD 进行评估,我们考虑如下研究问题.
RQ1:GUARD 检测数据竞争的效率如何?
RQ2:GUARD 检测数据竞争的有效性如何?
RQ1 评估 GUARD 方法的性能表现,RQ2 就检测到的数据竞争数量、其减少误报率的能力对 GUARD 方
法的有效性进行评估.RQ1 和 RQ2 也能评估 GUARD 和其他工具相比总体性能的差异.本文实验选取 4 种可以
[6]
[4]
[8]
[5]
公开获得的前沿的静态数据竞争检测工具:Relay 、LOCKSMITH 、Goblint 和 LDruid .其中,Relay 和
LOCKSMITH 是经典数据竞争检测工具,Goblint 和 LDruid 是近期提出的技术,其中,LDruid 同样采用了 MHP
分析.所有这些工具都是上下文敏感和流敏感的,且 Goblint 额外支持路径敏感的分析,这是为了处理在分支中
的锁操作或可能失败的加解锁操作.相比之下,GUARD 是上下文、流、路径敏感的.
所有实验都在 Ubuntu 16.04、Intel Core i7-8700k 处理器、32GB 物理内存条件下完成.该实验将每个
程序的检测时限设为 1 小时.此外,无法在限定时间内求解的约束条件会被视为可满足的.这是为了避免漏
报,因为 GUARD 会丢弃不可行路径,如果将超时约束视为不可满足会导致相应的路径被丢弃,从而可能引
入漏报.

5.1 评估对象
由于 GUARD 需要待测程序的源代码,因此随机选取 Github 中比较流行的开源项目作为评估对象.这些项
目涵盖,如下载工具、文件系统、数据库等不同的领域.具体信息见表 1.在选定评估对象后,使用 GUARD 对它
们进行分析.最后通过人工查验报告统计其效率和有效性.表 1 列出了被测程序的相关信息,第 1 列和第 2 列分
别代表它们的名称和规模,最后两列则是被测程序的描述和源码地址.
为了保证公平性,我们不把通过 GUARD 检测出来的数据竞争的项目(即表 1)作为基准去评估其他工具的
效果.所以,用于比较的基准程序是基于 LDruid 和 LOCKSMITH 所提供的 7 个程序.如果分析过程在 1 小时内
未完成,则被认为超时.如果警报总数小于 100,我们就会手动确认数据竞争警报.否则,随机从中选取 100 个进行
确认.实验结果已经公开在 figshare 中(https://figshare.com/articles/GURAR-Experiment/9724055).