1 引言

随着互联网、物联网、云计算等新计算平台、新应用模式以及智能化等新软件模式的广泛运用, 软件系统内外各种来源的非确定性(uncertainty)不断增强.如何面向非确定性, 保障相关软件系统的质量, 逐渐成为了国内外学术界关注的焦点.从软件系统内部的不确定性来看, 并发程序是一类典型的非确定性软件程序.并发程序由于其随机性高, 容易导致难以调试的并发缺陷.其中, 数据竞争就是一种典型的并发缺陷.数据竞争发生在两个或以上的线程并发地访问相同的内存位置, 并且其中至少一个是写访问.此外, 这些线程未采取任何机制来防止访问操作同时进行^[1].数据竞争带来的影响从轻微的内存数据损坏到许多并发相关的缺陷, 包括原子性及顺序违反.例如, 在2018年共公开了52个数据竞争相关的CVE^[2].数据竞争需要经过复杂的线程切换才能显露, 因此它是软件系统中最难检测的漏洞之一.随着近年来软件并行化程度不断提高, 竞争检测技术正变得前所未有地重要.尽管已经取得了巨大的研究进展^[3-8], 但工业级的静态数据竞争检测技术仍远远不能令人满意.

数据竞争可以通过静态和动态方式来检测.动态分析^{[3, 9-12]}能够检测出程序中实际存在的漏洞, 但难以推断线程间存在的所有可能的交织情况.静态工具^{[4, 5, 8, 13]}通常能够达到很高的代码覆盖, 但现有的前沿静态数据竞争检测技术在精度和可扩展性之间陷入了两难.一类方法^{[5, 6, 8, 13-15]}通过放弃上下文或路径敏感达到了很高的可扩展性, 但这不可避免地带来了高误报率的问题.例如, 本文对一种近期提出的路径敏感的数据竞争检测技术LDruid^[8]进行了评估, 它的误报率在70%以上.另一类方法^{[4, 5]}追求高精度, 但不可避免地存在可扩展性方面的问题.如LOCKSMITH^[4]为程序生成部分约束并求解, 这限制了它的可扩展性.本文的实验结果表明, 它无法在1小时内完成对1万行以上规模项目的分析.

本文解决这种矛盾的思路是基于这样一种观察: 在实际程序中, 使用部分程序路径来识别数据竞争就已足够了.尽管这可能会引入误报(例如程序入口到该路径的约束不可达), 但因为对于每个数据竞争都至少存在一条局部路径, 所以不会产生漏报.相比之下, 传统的竞争检测方法^{[4-6, 8]}会分析整个程序路径(即从程序入口点开始的路径)来检测竞争, 而对整个程序路径进行路径敏感分析是代价高昂的.所以, 本文只对以两次变量访问为起止的子路径进行分析, 因为这样的子路径是重要的数据竞争候选路径.

由于子路径总体上比整个程序路径更简单、明了, 实行重量级分析, 例如流敏感、上下文敏感、路径敏感分析是可行的.但是这些分析技术代价很高, 路径敏感分析尤为如此, 因为路径条件可能会错综庞杂且计算成本高昂^[16].因此, 现有的静态数据竞争检测技术都不能同时实现流、上下文和路径敏感分析.为了解决重量级分析(即路径敏感分析)所带来的分析开销问题, 我们设计了一种分段分析的方法.首先进行值流分析^{[17, 18]}识别出候选的数据竞争子路径, 接着进行可能并行执行(may-happen-in-parallel, 简称MHP)分析筛除不可行的竞争子路径.最后, 对于可能并发的数据访问子路径, 采用一种更精确且更重量级的方法求解路径的可行性, 以此来实现路径敏感.

MHP分析对于GUARD的总体性能是至关重要的, 这需要以很高的精度识别非并发的访问对.然而, 前沿的MHP分析技术^{[8, 19-23]}面临着精度问题.例如, 大多数工作^[19-23]聚焦于简单的线程模型(即缺少丰富的并行化模型), 且都未考虑路径约束.为了克服这种局限性, GUARD引入了一种称作线程流图(TFG)的线程信息表示形式, 用于高效且精确地编码并发信息.TFG中的每个节点按线程标签总结了其过程内的MHP信息.为了最小化计算开销, 线程标签将每个线程操作(例如thread_create)编码为一个三元组.根据实验结果, 这一步会筛除大约99.5%的数据访问对.为了保证精度以及可扩展性, MHP分析和数据访问分析都采用了一种自定义的约束求解器来筛除“简单但矛盾”的路径, 以此进一步减少不会导致数据竞争的路径.最后, GUARD对于剩余的候选项调用一个完整的SMT求解器(例如Z3).基于该分段分析方法, GUARD能够精确地为程序行为建模, 同时也保证了效率.

为了对GUARD的有效性以及效率进行评估, 我们选取12个现实世界中的开源项目.评估工作显示GUARD能够在1 870s内完成对130万行代码的工业规模项目的检测, 平均误报率为16.0%.并且, GUARD比现有的前沿技术平均快6.08倍, 与此同时取得了更低的误报率及更高的召回率.

本文的贡献总结如下:

● 提出了GUARD, 一种检测数据竞争的分段分析方法.GUARD与其他前沿技术相比具有更高的扩展性及精度.

● 评估了GUARD在多线程测试基准以及现实世界C/C++应用程序上的性能, 结果表明, 它能够在短时间内以可观的精度检测数据竞争.

● GUARD已经发现12个真实程序中存在的漏洞, 并且其中的8个已得到确认.

本文第2节通过一个示例程序阐述GUARD, 并介绍GUARD的分析基础.第3节详细描述GUARD.第4节、第5节为实现和实验, 评估GUARD的效率和有效性.第6节介绍相关工作.最后第7节给出结论.

2 GUARD概览和分析基础

本节从一个示例程序开始, 结合GUARD框架介绍GUARD各个模块的作用.之后再介绍整个分析过程基于的线程模型.最后是提出所需的基础结构, 即线程流图(TFG).

2.1 启发性案例

图 1是一个示例程序.图中函数foo创建了一个线程执行函数writer(第4行).接着, 它将变量arg自增(第7行), 然后等待线程结束(第8行).最后, 它再一次将arg自增.在第14行和第7行存在数据竞争, 因为函数writer和arg++指令能够并行执行.但是第14行和第9行不存在数据竞争, 因为writer线程在第8行被执行了等待终止操作.此外, 静态分析工具在报告数据竞争漏洞时也应附带路径信息作为佐证, 在此例中可能发生数据竞争的路径是第4行~第14行、第6行~第7行.

总的来说, 检测数据竞争漏洞存在许多挑战.第1个挑战在于检查数据访问是否可能并行发生.第2个挑战在于通过识别出不可行路径来消除误报.通过分析路径约束, 可以避免在分析现实世界应用程序时产生误报.与此同时, 静态分析工具应该提供路径信息以指明每条数据竞争可能的执行轨迹.与此相对, 若工具只提供了所有可能的执行路径, 而没有考虑路径约束, 则需要更多的人力来确认数据竞争警报.最后一个挑战是由复杂的线程操作带来的, 这些操作为程序引入了不同的线程语义信息.在本文的示例中使用到thread_create和thread_join这两个典型的线程操作.除此之外, GUARD还建模了4个线程操作: thread_wait、thread_notify、thread_lock、thread_unlock.不同的线程操作会引入不同的线程语义, 这使得MHP分析变得更为复杂.

2.2 GUARD框架

为了更清晰地阐述GUARD的原理, 本文将该方法分为4个组件.图 2展示了GUARD及其4个组件的概况: (1) TFG构建.构建一个线程流图(TFG), 用于表示整个程序的线程信息.(2) MHP分析.利用TFG综合出MHP信息, 为进一步的MHP查询作准备.(3) Source-Sink框架.利用预定义的source-sink模式检测漏洞, 且根据值流找出从一次数据访问开始到另一次数据访问结束的子路径.(4) 数据竞争检查器.为数据竞争定义source-sink模式, 以此检测数据访问子路径.对于每条数据访问子路径, GUARD查询MHP关系以避免误报.换言之, 它会过滤掉无法并发访问相同内存位置的数据访问对.最后, 为了通过路径敏感达到更高精度, GUARD调用约束求解器来验证MHP分析和数据竞争检测器所得到的路径的可行性.

TFG构建.这一部分会构建TFG.TFG是一个全局的图结构, 它连接了不同的函数调用、线程操作以及控制流.GUARD直接从程序指令构建函数级的TFG, TFG中的节点根据函数调用及控制流来构造.接着, 基于线程操作及函数调用信息连接各个函数级的TFG.这与控制流图(CFG)的构建方式有些类似, 所不同的是, GUARD为线程操作设计了一些特殊的语义, 而不是将它们当作普通的函数调用进行处理.例如, 对于一个thread_create函数调用, GUARD在TFG中创建一条从调用点指向被创建线程入口的边.另外, 根据函数调用, GUARD将一系列指令(CFG中的一个块)分割为2个或以上的节点, 这是因为, 在一次函数调用前后, MHP关系可能会有所不同.与CFG相比, TFG拥有3个特性: CFG中的多个基本块如果有相同的MHP关系就可以合并为TFG中的一个节点; 一个块中的任意函数调用或线程操作都会将该块分为两个节点, 且以函数调用或线程操作为分界; 各个函数级的TFG通过函数调用或线程操作连接在一起.因此, TFG关注线程相关的操作以及部分控制流, 而非仅仅是控制流.上述特征使得MHP信息的计算更为高效.图 3是对图 1中案例的简化分析过程.该TFG包含2个函数级TFG, 它们的入口节点以其函数名为开始, 出口节点用(0)标出.图 3(a)是示例所对应的TFG, 节点中的$({l_i}, \ldots , {l_j})$代表示例中相应的代码行.因为foo中创建了一个新的执行writer函数的线程, 所以foo所对应的TFG中的节点(2, 3, 4)连到writer对应的TFG入口节点.节点(6, 7, 8)被writer所对应的TFG的出口节点所指向, 这是因为, 它对线程执行了join操作.值得注意的是, 由于第6行和第7行的分支拥有相同的MHP关系, TFG将它们合并为了一个节点.除此之外, 在第4行和第8行的函数调用前后MHP关系发生了改变, 于是GUARD根据这两个函数调用将程序指令划分为了不同节点.其后继节点(即node(9))包含指令arg++.鉴于函数可能存在多条return指令, 每个函数中的终节点将函数的所有出口点进行了合并.总体而言, 构建TFG的目的在于实行精确的MHP分析并且避免冗余分析.

MHP分析.GUARD通过为TFG节点构建线程标签来表示MHP信息.首先提取出线程相关的信息(即thread_create和thread_join), 并用线程标签对它们建模.然后基于线程标签分析两条路径的MHP关系.图 3(b)中展现了每个节点简化的线程标签.初始标签集是Ø, 然后thread_create函数创建了一个新的线程标签.线程标签包含两种标签, 一类以〈1, T, Ø〉表示, 分配给刚创建的线程.它所对应的标签是〈1, C, 1〉, 在thread_create调用点之后被赋给节点.在thread_join的调用点处, 添加一个标签(1, C, 1), 表明这个标签执行了等待线程终止这个操作.线程标签中的第1个元素是thread_create的标识, 第2个元素表明了标签类型, 最后一个元素用于区分不同的调用上下文.〈〉和()分别表示thread_create和thread_join所对应的标签集.有关线程标签的详细讨论见第3.1.1节.

Source-Sink框架.该框架基于值流分析(value flow analysis), 自动依据与特定缺陷对应的source-sink模式分析缺陷.很多软件缺陷都可以被表达为如下的形式: 在任意一个程序中, 一个由程序事件A生成的值v一定能够流向另一个程序事件B中的一个值^[24].所以, 该框架检测任何一个能够被建模成基于source和sink模式的全局值流的缺陷.并且, 检测出的由source到sink的路径并不会由程序入口开始.

数据竞争检查器.如图 3(c)所示, 最后一步是竞争检测, 这依赖于Source-Sink框架以及MHP分析.首先, 它会基于source-sink框架检测读-写或写-写对.source和sink都被设定为对变量的读或写操作, 因此第7行、第9行和第14行的变量arg同时为sources和sinks.接着, GUARD分析程序的值流, 找到从source到sink的路径.在这一步中, 检测到的source-sink路径是〈14, 4, 7〉和〈14, 4, 9〉.然后根据这两条路径的子路径(即{〈4, 7〉, 〈4, 14〉}和{〈4, 9〉, 〈4, 14〉})提取出线程标签以及路径约束.最后一步是根据它们所对应的线程标签和路径约束检测数据竞争.由于第4行创建的线程在第8行执行了等待结束操作, 〈14, 4, 9〉并不是MHP的, 因此对于启发性示例, GUARD只会报告一个数据竞争对〈14, 4, 7〉.

前文展示的启发性示例描述了GUARD检测数据竞争的基本思路.接下来, 本文将介绍有关检测实际程序数据竞争时的分析细节.

2.3 线程模型

图 1的示例程序中只包含两种线程操作: thread_create和thread_join.现代编程语言提供了种类繁多的线程操作来实现不同的并行模式.本文考虑如下6种具有代表性的函数.

● $thread\_create(tid, routine, para)$接受3个参数: 一个线程标识号(线程ID)、一个指向所要执行任务的指针及其所需的单个参数值.

● $thread\_join(tid)$等待tid所指明的线程终止.

● $thread\_notify(c)$唤醒执行了$thread\_wait(c)$的线程.

● $thread\_lock(mutex)$和$thread\_unlock(mutex)$给mutex加锁或去锁.

2.4 线程流图

GUARD首先生成函数级TFG, 并根据线程操作和函数调用将函数级TFG连接起来构建起一个全局TFG.

TFG定义为$\mathcal{G} = (\mathcal{N}, \mathcal{E}), $它包含一个点集$\mathcal{N} = \{ {n_1}, \ldots , {n_m}\} $以及一个由有向边组成的边集$\mathcal{E} = \{ {E_1}, \ldots , {E_K}\} , $其中, K是边的种数, E_k是类型为k的边的集合.在一个函数级TFG中, 每个节点由指令序列构成, 彼此间以控制流指令或函数调用为分割.为了连接各节点, TFG引入用于指明控制流的边→_flow.与CFG类似, TFG也有一个入口节点和一个出口节点(在$\mathcal{N}$中).入口节点没有入边而出口节点没有出边.

在一个全局TFG中, 函数调用中的调用者和被调用者由6种边连接, 分别是: →_call、→_create、→_join、→_notify、→_lock和→_unlock.其中, →_create将thread_create的调用点连接至线程的入口点; →_join将线程的出口点连接至thread_ join的调用点; thread_notify的调用点通过→_notify与相应的thread_wait的调用点连接起来; 从n₁到n₂的同步边(即→_notify)表明: 一旦thread_wait在n₂处执行, n₂必定会接收到来自n₁的消息; thread_lock或thread_unlock的调用点通过→_lock或→_unlock连接至其后继节点.其他函数调用通过→_call将它们的调用点连接至对应的被调用者的入口点.除此之外, 后5种边需要通过线程标识符(thread ID)匹配对应的操作, 例如thread_join需要匹配与其参数(即线程标识符)对应的, 且由thread_create创建的线程.这一部分通过值流分析实现(见第3.2节).

从TFG中可以看出, 同一节点中的所有指令拥有相同的MHP关系.此外, 相邻节点可能也具有相同的MHP关系.为了提高MHP分析的效率, GUARD根据算法1将具有相同MHP信息的邻接节点合并为一个.对于按拓扑序排列的每个函数级TFG(第1行), 首先用函数调用对TFG节点进行标记(第3行).allMinimalLoopOrBranch抽取出循环及分支所对应的节点.如果存在嵌套的循环或分支, 它只获取最深层的循环或分支.换言之, 给定一个嵌套的分支或循环$\mathcal{L} = \{ {l_1}, \ldots , {l_n}\} , $其中, l_i包含点集$\mathcal{N}_l^i, $分析出${l_j}{\rm{ s}}{\rm{.t}}.{\rm{ }}\forall {l_i} \in \mathcal{L}, \mathcal{N}_l^j \in \mathcal{N}_l^i.$之后对于allMinimalLoopOrBranch抽取出的每个循环或分支, 对其相应的节点进行标记(第5行~第8行).在标记节点之后, 基于循环或分支对节点进行合并.该算法一直合并节点, 直到没有节点可以被合并(第10行~第14行).

算法1. Compressing Thread-flow Graph.

Input: TFG $\mathcal{G}; $

Output: Compact TFG $\mathcal{G}'.$

(1) for ${\mathcal{G}'_f}$ in reversedTopologicalOrder($\mathcal{G}$) do

(2)  //It marks function calls, including thread operations.

(3)  markNodeWithFunctionCall(${\mathcal{G}_f}$);

(4)   $\mathcal{B}$=allMinimalLoopOrBranch(${\mathcal{G}_f}$);

(5)   for $\mathcal{L} \in \mathcal{B}$ do

(6)    if $\exists v \in \mathcal{L}, {\rm{ is }}\;Marked(v) = = {\rm{true}}$ then

(7)    for $v \in \mathcal{L}$ do

(8)     markNode($v$);

(9)   ${\mathcal{G}'_f} = {\mathcal{G}_f};$

(10)   while ${\mathcal{G}'_f}$ is unchanged do

(11)    $\mathcal{B}$=allMinimalLoopOrBranch(${\mathcal{G}'_f}$);

(12)    for $\mathcal{L} \in \mathcal{B}$ do

(13)     if $\forall v \in \mathcal{L}, {\rm{ is }}\;Marked(v) = = {\rm{false}}$ then

(14)      mergeNodes($\mathcal{L}$);

3 GUARD分析方法

本节将展示GUARD分析一个程序时的详细步骤.首先, 具体阐释GUARD如何通过TFG分析MHP关系.之后, 基于source-sink检测出数据访问对, 并根据MHP分析筛除不可行路径.最后, 通过约束求解器求解路径约束并得到最终的数据竞争警报.

3.1 MHP分析

GUARD应能快速、准确地查询query关系以减少潜在的数据竞争数量.为了实现这一点, 我们设计了线程流图(TFG), 用于为线程操作建模.基于TFG, 将MHP关系编码为线程标签, 并使用转换规则模拟由线程操作所引入的语义信息.最后, 根据TFG以及转换规则总结出MHP关系.

3.1.1 线程标签流

在构建完TFG之后, GUARD使用线程标签及预设的转换规则来建模线程操作所引入的语义信息.首先, 线程标签的定义如图 4所示.CT是一个调用序列, 它由一系列调用点CS_i拼接而成, $\mathcal{L}$是L的集合, 其中, L是由一个三元组$\langle ID, T, CT\rangle $表示的线程标签.ID指明何种线程操作, T表示标签种类, 可以是$ Thread、$CS或Other.$Thread$意味着该标签是由$thread\_create$创建的, 并且CS是$thread\_create$的调用点.$Other$代表不由$thread\_create$创建的标签.CT表示由调用点标识组成的调用轨迹.一个节点的MHP关系由一个五元组$\langle NodeID, {\mathcal{L}_c}, {\mathcal{L}_j}, {\mathcal{L}_{wn}}, {\mathcal{L}_l}\rangle $表示.$NodeID$是当前节点的标识, $\mathcal{L}$是线程标签集.$ {\mathcal{L}}_{c}、{\mathcal{L}}_{j}、{\mathcal{L}}_{wn}、{\mathcal{L}}_{l}$分别代表$thread\_create$、$thread\_join$、thread_wait、$thread\_notify$和$thread\_lock$所对应的线程标签集.

接下来, 对于每个函数, 根据图 5中的转换规则对线程标签进行转换.$TL(n)[t]$表示查找节点n对应的${\mathcal{L}_t}, $其中, $t \in \{ c, j, wn, l\} .$如果t未给出, 则通过$TL(n)$表示检索出节点n的NL(图 4中定义).N(CS)用于查找出具有调用点CS的节点.N_i(CS)和N_o(CS)代表CS所在函数级TFG的入口点和出口点.${n_i}{ \to _t}{n_j}$表示n_i通过类型为t的边连接至n_j.注意, n_i(或n_j)可能为N(CS)(即$N(CS){ \to _t}{n_j}$), 这时它表示一个具有调用点CS的节点通过类型为t的边连接至n_j.$ \stackrel{·}{N(CS)}$和$ \underset{·}{N(CS)}$分别表示节点N(CS)之前和之后的点.$Succ({n_i})$和$Pred({n_i})$表示TFG中节点n_i的后继和前驱.$Ob{j_i}Oper = Ob{j_j}$代表通过$Oper$的一次赋值, 例如$Ob{j_i}\mathop \cup \nolimits^ = Ob{j_j}$表示合并这两个集合并复制给Obj_i.

$Flow$规则表示一次基本的线程标签转换.如果有k个节点通过→_flow与点n_m相连, 它将来自前驱节点(例如分支)的${\mathcal{L}_c}$合并, 并取$ {\mathcal{L}}_{j}、{\mathcal{L}}_{wn}、{\mathcal{L}}_{l}$各自的交集.如果一个节点只有一个前驱节点, 其后继节点与前驱节点拥有相同的线程标签.

Call规则用于在函数调用处转换线程标签.当一个线程标签集合到达一处函数调用时, 调用点将其当前的标签集传递给被调用者, 调用点的输出标签集则是合并被调用者出口节点的标签集.

$Create$规则对应$thread\_create$操作的转换规则.注意, 线程的创建引入两个新的标签(L_CS和L_T), 这两个标签被添加至NL中对应的${\mathcal{L}_C}$内.在被创建的线程上, 该规则将标签传递给被创建线程并将它们合并.在thread_ create的调用点, 只将${\mathcal{L}_C}$中的标签合并, 而不是将4个集合中的标签都合并.这是线程创建和函数调用两个规则在标签传播上的核心区别.在一个函数调用中, 被调用者可被视为一个内联函数, 这意味着调用点之前的线程标签与被调用者出口节点之前的线程标签是相同的.类似地, 调用点之后的线程标签和被调用者出口节点之后的线程标签是相同的.相比之下, 线程的创建操作引入了不同的语义, 因而不能被视为内联函数, 所以GUARD为函数调用和线程创建定义了两种转换规则.

$ Join、Wait/Notify、Lock、Unlock、CallingContext$规则展现了剩余线程操作的线程标签流.Join规则表示, 如果一个标签L_j被等待终止, 则会将标签添加至join集中.$Wait/Notify$规则说明会将一个ID(即这两种操作的唯一标识)加入$thread\_notify$所有前驱节点以及$thread\_wait$所有后继节点(包括过程间节点)的标签集中.

$ Lock、Unlock$规则展现了GUARD是如何分析锁的.当$thread\_lock$函数被调用时, GUARD将一个标签添加至锁集L_l中, 对应地, 当$thread\_unlock$函数被调用时, 它将相应锁集中的锁去除.这两条转换规则模拟了加锁和去锁的语义.

$CallingContext$规则描述了GUARD实现上下文敏感的核心策略.对于NL中的所有标签, 按调用点ID将每个标签中的CS进行拼接.注意, 每个CS的ID是拼接而成的, 因此GUARD可以从一个CS中提取出一个调用链.按照这种方式, GUARD能够通过分析CS中的各ID识别出不同的调用上下文.

从图 5可以看出, GUARD将$thread\_join$或同步操作($thread\_wait$和$thread\_notify$)分别存储在$ {\mathcal{L}}_{j}和{\mathcal{L}}_{wn}$中, 而不是清除相应的线程标签.这么做的原因在于, 被清除的标签可能会隐含其他函数的MHP关系, 清除线程标签可能会带来漏报.

3.1.2 MHP分析

在定义线程标签和转换规则后, GUARD根据转换规则通过自底向上和自顶向下分析的方法进行MHP分析.自底向上分析会为每个节点计算线程标签, 自顶向下分析将调用者的线程标签传递给它们的被调用者.

在自底向上分析的过程中, GUARD以逆拓扑序分析函数.在此阶段, GUARD根据图 5所示的转换规则创建并更新线程标签.在此阶段后, GUARD可以通过路径查询两条指令的MHP关系.但这一阶段没有路径信息GUARD, 无法高效地查询MHP关系, 这是因为, GUARD需要从两条指令所能到达的路径中提取出所有标签.为了不失一般性, GUARD的目标是, 无论是否有路径信息都能查询MHP关系, 因为有些MHP关系的查询有路径信息而有些没有, 因此GUARD执行第2阶段的自顶向下分析.

在自顶向下分析的过程中, GUARD以函数的拓扑序分析函数标签.它将调用者的线程标签传递给被调用者, 从而每个函数都能知晓其全局线程标签.通过这种方式, GUARD总结出了全局线程标签, 并且不需要路径信息就能高效地查询两条指令的MHP关系.

3.2 基于Source-Sink的检测框架

该框架提供了两种基础分析: 一种需求驱动的、路径、上下文敏感的值流分析和一个基于Source-Sink的检测框架.值流分析提供了数据依赖信息, 以此来识别线程操作的标识.例如, 对$thread\_join(tid), $tid必须与被执行join操作的线程的标识相同.类似地, $thread\_notify$或$thread\_lock$的线程标识也应该通过值流分析传递给对应的$thread\_wait$或$thread\_unlock$.GUARD借助别名分析的方式解决这个问题, GUARD首先会进行完备但不精确的指针分析, 然后, 给定一条特定的路径, 它会收集该路径的约束条件来进行精确的指针分析.

算法2展示了基于Source-Sink的检测框架, 该框架提供了对source和sink的配置.setSource、setSink和checkSourceSinkPair函数是由特定的漏洞检测器定义的.setSource定义了哪些变量是source; setSink定义了哪些变量为sink; checkSourceSinkPair则依据缺陷类型分析每条source-sink路径, 如果该source-sink匹配特定的漏洞模式, GUARD就会将其报告出来.以内存泄露检测为例, source设为每个内存分配函数, sink设为内存回收函数.所以每个内存分配函数(source)应该对应某条路径中的内存回收函数(sink), 以此避免内存泄漏.关于数据竞争的source和sink, 我们在下一节给出定义.retrieveCalleeSummary函数将被调用者的source和sink信息传递给调用者, 因此sources和sinks包含了被调用者的source和sink信息.被调用者的source和sink通过参数传播(全局变量被视作参数, 详见第4.1节), 因此调用者需要能够获取被调用者已经分析的值流信息.由于source和sink可能不在同一函数中, buildPath函数通过调用链提取出从source到sink的路径.注意, 从source到sink可能不止一条路径, 因此, 变量paths可能会包含多条路径.最后, 如果漏洞路径是可达的, 那么, reportBugWithPath就会报告该漏洞.

该框架按逆拓扑序分析程序(第1行), 这意味着它将依据函数调用图自底向上地分析函数.在分析过程中收集source以及它们对应的sink, 当找到一个source-sink对时, 该算法会检查source和sink是否都满足特定的漏洞特征模式, 如果是, 报告此source-sink对以及路径信息, 否则, 忽略它(第7行~第12行).可以看出, GUARD总结source-sink信息(第6行)并检查每个source-sink对的可行性(第11行), 因而该步骤是上下文敏感、路径敏感的.值得注意的是, 一个source-sink路径p可以被分为两条路径p₁和p₂, 且p₁和p₂有相同的起点且分别在source和sink中结束, 即$p = \{ {p_1}, {p_2}\} , $其中, ${p_1} = ({n_j}, ..., {n_{source}}), {p_2} = ({n_j}, ..., {n_{sink}}).$

算法2. Source-Sink based detection algorithm.

Input: Program;

Output: Race Bugs.

(1) for fun in reversedTopologicalOrder(Program) do

(2)  sources=setSource(fun);

(3)  sinks=setSink(fun);

(4)  //The following function retrieves summarized sources

(5)  //and sinks from fun’s callees.

(6)  retrieveCalleeSummary(sources, sinks);

(7)  for source in sources do

(8)   for sink in sinks do

(9)    //verify each sink in variable sinks.

(10)    paths=buildPath(source, sink);

(11)    isFeasible=checkSourceSinkPair(source, sink, paths);

(12)    reportBugWithPath(source, sink, paths, isFeasible);

3.3 竞争检测

基于MHP分析和source-sink框架, GUARD使用算法3通过source-sink模式检测数据竞争.首先, GUARD会检查source和sink是否满足数据竞争的一个条件, 即其中至少有一个写操作(第1行).为了避免报告读-读的数据访问对, GUARD添加了一个访问检查(第2行~第3行).接下来, 通过isPathOrderReversed、isReachable和isMHP精化竞争检测.isPathOrderReversed检测一个source-sink路径(即p)是否是逆序的, 以此来消除重复的报告.GUARD将source和sink都设为读或写, 因而一个source可能也是一个sink, 反之亦然, 这将导致, 如果忽略顺序, 一个漏洞可能会被报告两次.在检测完路径顺序之后, GUARD会验证source-sink路径是否可达.isRechable提取出从source到sink的路径约束并调用自定义的约束求解器筛除“简单但矛盾”的路径, 之后, 通过如下规则确认source-sink路径是否是MHP的.

isMHP.令p₁和p₂是来自一个给定source-sink路径p的两条路径, 令NL₁和NL₂为从p₁和p₂中提取出来的节点标签.路径p₁和p₂是MHP的, 当:

(1) $N{L_1}[l] \cap N{L_2}[l] = \emptyset ;$

(2) $N{L_1}[wn] \cap N{L_2}[wn] = \emptyset ;$

(3)$\forall {L_{1c}} \in N{L_1}[c], {\mathcal{L}_2} = \{ {L_{2c}}:{L_{2c}} \in N{L_2}[c]\;{\rm{ where}}$

${L_{2c}}[ID] = {L_{1c}}[ID]\;{\rm{ and }}\;{L_{2c}}[T] \ne {L_{1c}}[T]\} , \exists {L_{2c}} \in {\mathcal{L}_2}, {L_{2c}} \notin N{L_1}[j] \cup N{L_2}[j].$

在本文所定义的线程模型下, 这3个条件是p₁和p₂为MHP的充分条件, 因为: (1) 它们没有被同一个锁所保护; (2) 它们没有通过wait或notify进行同步; (3) 根据它们的调用轨迹存在一个没有被join的线程.最后, 通过isFeasible检测路径是否可行, 它会提取出路径约束并调用一个常规的约束求解器来验证路径的可行性(第10行).对于一个数据竞争对, GUARD验证两个路径约束.第1个约束来自被识别为MHP的线程标签, 第2个是相应source和sink的路径.如果它们的两种路径约束都是可满足的, 则GUARD报告这一漏洞(第11行).

算法3. CheckSourceSinkPair.

Input: source, sink, paths;

Output: isFeasible.

(1) if $source \in \{ write, read\} $ and $sink \in \{ write, read\} $ then

(2)   if $source \in \{ read\} $ and $sink \in \{ read\} $ then

(3)    continue;

(4)   //Analyze every path in paths

(5)   for p in paths do

(6)    if isPathOrderReversed(p) or not isReachable(p) then

(7)     continue;

(8)    if not isMHP(source, sink, p) then

(9)     continue;

(10)    if not isFeasible(p) then

(11)    return true;

(12) return false;

4 工具实现

GUARD是基于LLVM3.6.2^[25]使用Z3^[26]作为SMT求解器来实现的.GUARD中所有的模块都由LLVM pass实现, LLVM pass用于在编译器中执行程序分析、转换和优化^[27].目前, GUARD支持C语言中的POSIX thread^[28]以及C++中的std: : thread^[29].

4.1 方法优化

为了提高效率, GUARD采取了多种优化方式.第1种是Thread escape分析, 它排除了那些不会与其他变量同时被访问的变量.第2种优化是将全局变量内联为函数参数来简化分析过程.第3种优化是为数据竞争检测优化source-sink的模式.

线程逃逸(thread escape)分析.众所周知, 一个程序可能包含数目繁多的变量, 更不用说与之相应的变量访问.尽管GUARD只会分析过程间的变量(即实际参数和全局变量), 但是变量的总数仍十分庞大.线程逃逸分析能够避免分析那些无法与其他变量同时被访问的变量, 即GUARD不会分析不带线程标签的变量.因为这样的变量不可能与其他变量一起被并行访问.这个过程是保守且高效的, 它能够尽快给出线程逃逸信息, 同时也不会产生漏报.例如, 在第1次线程调用前使用的变量不会与任何线程中的变量并发执行.

内联全局变量.过程内的变量包含两种类型: 函数实参以及全局变量.据我们所知, 这两种变量是过程内分析的两大挑战.对于能够获取函数体的所有函数, GUARD将全局变量当作函数实参.换言之, GUARD通过将全局变量以函数参数在函数调用之间传播的方式, 使得被调用者的分析结果能够包括全局变量.以这种方式, 通过分析函数参数来分析全局变量, 统一并简化了分析过程.

简化的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种可以公开获得的前沿的静态数据竞争检测工具: Relay^[6]、LOCKSMITH^[4]、Goblint^[5]和LDruid^[8].其中, 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).

5.2 GUARD的效率

表 2中第2列和第3列展示了构建TFG及分析线程标签的性能信息.第4列和第5列展现了查询MHP的性能表现.第4列是平均查找时间, 第5列是查询次数.从表 2中可以看出一半以上的程序都能在1s内完成分析, 所以GUARD是足够高效的.大多数测试程序所消耗的内存也很低.可以看到, 所有程序都能在3.6GB的内存消耗内完成MHP分析.在识别MHP关系方面, MHP查询所消耗的总时长的几何平均为0.331s.其中只有5个程序查询MHP关系的时间超过1s.通过表 2可以得出结论: GUARD是十分高效的.

表 2中第7行和第8行是程序的数据竞争检测结果.我们分析了每个程序的执行时间和内存需求.关于前12个程序, 它们的大小从4.6KLOC到491.4KLOC不等, 都在1小时内、11GB内存条件下完成了分析.数据竞争检测时长的几何平均为83.7s, 内存消耗的几何平均为2 734.0MB.最后一个程序需要相对更多的资源进行分析.可以看到, GUARD能够在1 870s内消耗36GB内存完成对1.3MLoC规模程序的分析.

表 3是不同工具所消耗的时间和内存的比较.T代表总执行时间, Mem是最大消耗内存.TO意为超时(TimeOut), Crash代表出现了段错误, OOM表示内存不足.在计算效率提升时, 我们忽略所有失败的分析结果(即TO、Crash和OOM), 因为它们的分析时间是未知的.从表中可以看出, 在分析小规模程序时, GUARD并不是最高效的.但是, GUARD在所有测试程序上平均加速为6.08倍.代码规模在10KLOC以上的程序为平均分析速度的提升提供了主要的贡献.具体而言, LOCKSMITH、LDruid、Relay、Goblint和GUARD分析时间的算数平均值为55.50s、80s、3.67s、79.83s和25.00s, 消耗内存的算数平均值为767MB、322.8MB、49.7MB、194.3MB和563.8MB.由于只有GUARD能够分析所有程序, 所以针对每个工具的平均分析提升只考虑GUARD和它都能分析的程序.例如, LOCKSMITH只能分析前4个程序, GUARD分析它们的平均时间为9.25s, 平均内存消耗是250.25MB, 所以GUARD针对LOCKSMITH的分析速度提升了5倍, 降低了2.1倍的内存开销.同理, GUARD针对LDruid、Relay、Goblint的分析速度分别提升了43倍、-0.72倍和1.8倍; 在内存开销上, GUARD针对LDruid、Relay、Goblint的内存开销增加了0.09倍、6.7倍和1.92倍.由于GUARD同时引入了上下文、流、路径敏感的分析方法, 所以GUARD的分析开销会高于较低精度的分析方法.虽然GUARD的内存开销只比LOCKSMITH低, 但是, 由于其分析速度超过了3个工具, 所以GUARD的整体分析效率依旧是比较高的.

GUARD在保证分析精度的前提下保持高分析效率的原因为: 首先, 它使用TFG并合并了具有相同MHP关系的节点, 从而缩短了MHP分析和查询的时间; 其次, 为数据竞争所使用的source-sink模式避免了从程序入口开始分析数据竞争; 最后, GUARD只在最后一步进行了重量级路径敏感分析以验证数据竞争的可能性.但是, 由于预处理部分(即构建TFG、收集路径约束等)需要时间, GUARD在检测小规模的项目时效率会有所降低.

总之, 从实验结果可以看出GUARD是高效的, 大部分程序都能在可接受的时间内完成分析.表 3中对不同工具的比较表明, GUARD在处理大规模程序时总体上比其他工具更快.

5.3 GUARD的有效性

表 2的最后两列列出了竞争检测结果.第9列是静态分析结果, 它展示了警报的数量.最后一列是人工核验的结果.在本次实验中, 误报率的几何平均为16.0%.此外, 我们向开发者报告了12个不同的数据竞争漏洞, 并且其中8个已经得到了确认, 其余正在等待确认.确认的漏洞中有7个已被开发者修复.

表 4列出了各种工具检测准确性的比较情况.#Warning是竞争检测器报告的警报数量, #Bug代表人工确认的漏洞数量.从表 4中可以看出, GUARD尽管不是最高效的检测工具, 但其检测数据竞争的精度是最高的.在大多数情况下, 5种工具都能检测出实际存在的数据竞争, 但是另外4种工具会产生更多的误报.GUARD的误报率相较而言是最低的.具体而言, LOCKSMITH、LDruid、Relay、Goblint和GUARD误报率的几何平均值(由于有0, 故每个值加1, 将求得几何平均值减1以得到最终的平均值)为84%、80%、93%、97%和37%.由此可见, GUARD的误报率是最低的, 而且报告的数目相对较少, 确认缺陷的人工开销也相对较少.值得一提的是, 除了GUARD和Relay以外, 其他工具会报告包含对一个共享变量所有可能的数据访问, 对这些数据方法的组合进行确认, 比只确认一条包含两个数据访问的路径需要花费更多的精力.对于所有人工确认的报告, 没有发现GUARD漏报.

从结果中也可以看出, GUARD仍然会产生误报.通过进一步检查测试用例程序, 我们发现了如下导致误报的原因.第1个原因是外部函数中存在位置的访问类型(读和写).第2个原因在于复杂的线程创建和等待终止操作.例如, 我们发现一个程序在循环过程中创建一个线程列表, 并通过按位和移位运算符连接这些线程.第3个原因是我们将求解超时的约束当作是可满足的.

因此, 对真实世界开源程序的评估肯定地回答了RQ2的问题, 即GUARD在检测漏洞方面是有效的.此外, 对不同竞争检测工具的对比评估也回答了RQ2——GUARD能够以更低的误报率检测出其他工具报告的数据竞争.

5.4 讨论以及未来工作

有效性威胁.对内在有效性的主要威胁与GUARD实现的正确性有关.为了减轻这种威胁, 我们在工具构建期间持续地对其进行测试.测试集包含38个回归测试用例以及28个实际应用程序.其中, 38个测试用例同时也用于检验其可靠性.外部有效性威胁涉及到GUARD对其他编程语言的通用性以及缺陷数据集的质量.由于所定义的线程模型是一个相对通用的模型, 所以GUARD也能够基于当前线程模型扩展到其他编程语言, 例如Java.关于缺陷数据集的质量, 由于目前没有找到满足本文实验的、权威的数据竞争缺陷数据集, 所以我们使用了LDruid和LOCKSMITH都使用的程序作为基准程序.基准程序中的数目、缺陷特征以及已知缺陷信息都会影响缺陷检测工具的评估结果.所以, 为了进一步保障评估的准确性, 收集数据竞争缺陷也是未来工作之一.

相关警告.在实验中我们发现, 尽管GUARD对于一些程序报告了很多警报, 其中的一部分涉及的是相同的变量.这是由于, 可能存在两条以上的路径到达同一个数据访问对, 在这种情况下, GUARD根据这个数据访问对会报告来自不同路径的警报.此外, 另一种类型的相关警报是由访问相关联位置的一个变量引起的.例如, 若一个基本块中存在对一个变量的2次写访问, 那么这个变量所对应的数据竞争会被重复识别2次.即使这些警报的特征是相似的, 开发者也必须手动检查这些相似警报.在理想状况下, 开发者只需确认其中的一个, 而不必每个都进行检查.一种避免产生这两种警报的有效方式是使用警报集群(warning cluster).如果具有相似模式特征的警报能被聚集起来, 那么开发者只需检查其中一个典型的警报即可, 从而可以避免在相似的警报上花费精力.

6 相关工作

本节调研MHP分析和数据竞争检测相关的方法.

MHP分析.先前已有许多工作分析了MHP关系, 特别是对于具有高级并发结构的语言, 如Java^{[21, 22]}和X10^{[19, 20, 23]}.此外, 也有工作聚焦于其他语言^{[8, 14, 31, 32]}.X10拥有内置的高级并发结构, 如async、atomic和finish, 以此来简化并行程序的分析和优化.基于这种语言, Agarwal等人^[19]提出的一种MHP分析算法仅遍历X10程序的程序结构树.Sanker等人^[23]对这种算法进行了扩展, 通过一种对MHP条件的更高效的表示形式改善了计算复杂度.Joshi等人^[31]提高了MHP分析的精度, 通过对动态屏障间距的推理推断出语句间的顺序.Naumovich等人^[22]提出了一种面向Java的使用数据流分析框架的MHP分析技术.该技术通过构建并行执行图(PEG)来表示Java并发程序, 并使用PEG推测不同指令间的MHP关系.Barik^[21]通过牺牲精度的方式换取效率, 其采用的算法基于线程创建树, 从线程层面计算MHP关系.高层次并发结构的MHP分析简化了复杂性, 最近的工作也分析了低层语言中的MHP关系.Di等人^[14]通过分析局部关系图(RRG)计算Pthreads程序的MHP关系.RRG是基于线程敏感的CFG而构建的, 具有相同happens-before性质的语句会被分到同一区域中.该工作只建模了thread_create和thread_join.而LDruid^[8]方法通过静态地计算时钟向量来建立happens-before关系, 并建模了4种线程操作(thread_create、thread_join、thread_wait和thread_notify).与之相比, GUARD建模了6种常见的线程操作.尽管LDruid声称使用了分离的锁集分析用于竞争检测, 但它也引入了锁集分析所需的额外计算开销.上述方法背后采用的主要思路与GUARD是相似的, 即将MHP关系编码为专有结构体从而通过分析该结构体识别出两个语句的MHP关系.但是, 如果没有调用上下文信息和路径敏感分析, 这些方法会产生更高的误报率.据我们所知, GUARD是第1个将上下文敏感和路径敏感应用于MHP分析和数据竞争检测的工具.

静态方法.静态方法聚焦于在不执行程序的情况下检测数据竞争, 这样可以消除漏报^{[4-6, 13, 15, 33-36]}.但是, 由于缺少运行时信息, 误报很难避免.Polyvios等人^[4]开发出的LOCKSMITH是一个针对数据竞争的上下文敏感的相关性分析工具.它使用基于约束的技术来计算描述保护左值的锁的关联.LOCKSMITH仅仅被应用于检测100K行代码的程序^[6].Goblint^[5]将指针和值分析相结合, 从而使其能够处理复杂的加锁情况.RELAY^[35]是一种使用自底向上分析方法的静态可扩展算法.它采用符号执行、指针分析、锁集分析、受保护访问分析的方法产生竞争警报.IteRace^[36]是一种针对Java并行循环的静态数据竞争检测工具, 它通过专门处理lambda式并行循环、跟踪、汇总, 实现了较低的误报率.但其只能分析并行循环.ECHO^[15]能够在编写代码期间在IDE中实时检测数据竞争.为了能够在IDE中得以使用, 它采用的指针分析在程序有修改时会增量分析.然而, 由于对分析速度存在一定的要求, 它不是上下文敏感和路径敏感的.RacerX^[33]使用流敏感的过程间分析检测数据竞争以及死锁.然而, 为了实现可扩展, 它丢弃了一些程序信息, 例如使用类型表示所有左值, 这就导致了它是不完善的.据我们所知, 这些静态分析技术都没有同时实现上下文、流、路径敏感, 大部分技术仅实现了其中的一部分.例如, Goblint^[5]在分析锁集时只实现了路径敏感分析.与先前的工作相比, GUARD编码MHP关系、上下文信息、路径信息, 从而构建起了一个完备、有效的数据竞争检测器.

7 结论

本文提出了一种阶段化的数据竞争检测技术GUARD.它首先基于值流分析检测出数据可能的数据竞争候选, 之后采用MHP分析, 基于新的程序表现形式(即线程流图)高效地筛除不可行的数据竞争路径.最后, GUARD使用路径敏感分析保护数据竞争检测过程, 进一步降低了误报率.我们通过多个程序评估了GUARD, 结果表明, 它能够精确、高效地检测已知和未知的数据竞争.未来, 我们计划进一步提高分析精度, 同时也扩展GUARD, 使其能够处理其他种类的并发错误.