基于多线程程序约束构建的数据竞争检测与证据生成方法

摘要

一种基于多线程程序约束构建的数据竞争检测与证据生成方法，根据多线程程序语义构建约束表达式，将数据竞争检测问题转化为约束求解问题，采用约束求解器检测可能存在的数据竞争，并生成触发数据竞争的程序执行路径，首先插桩被检测程序，执行此程序并得到执行路径；其次根据多线程程序执行语义将执行路径转化为无量词一阶逻辑表达式，此约束表达式涵盖所有可行的线程交织；然后根据发生数据竞争时语句间时序关系构建数据竞争候选集合，生成候选发生竞争的条件；最后遍历候选集合判定是否存在数据竞争，如有则生成对应的证据序列，本方法可找出一次执行中所有的数据竞争且不存在误报情况，对每一个数据竞争都生成一个展示了数据竞争触发过程的证据序列。

说明书

技术领域

本发明涉及可信软件及软件测试领域，特别涉及一种基于多线程程序约束 构建的数据竞争检测与证据生成方法。

背景技术

随着处理器多核化的普及，多线程技术已经成为软件编程中提高CPU利 用率不可或缺的技术。然而，由于线程之间交织的不确定性，多线程程序执 行过程中可能会出现一些难以预料的行为导致程序出错，例如对临界区没有 做好同步工作而导致的数据竞争问题。数据竞争是两个不同的线程在没有同 步保护的情况同时访问一个内存，并且至少有一个写操作。数据竞争不一定 导致程序错误，因为有些程序员故意让程序有数据竞争以提高运行的效率， 但是有调查表明5-24％的数据竞争会对程序产生坏影响。数据竞争很难以被 发现，因为它们经常发生在一些低概率出现的交织序列中，在现实中往往需 要花很多时间去定位，其引起的错误如同“corner error”，即使在软件发布 时也未必能够完全清除它们。因此，数据竞争检测是多线程程序测试领域最 受关注的研究点之一。

过去几十年中数据竞争检测已有大量研究，设计出很多杰出的自动化检 测工具，主要分为静态与动态分析技术。静态方法通过静态检测程序所有的 路径来推断程序中的所有数据竞争，可以检测出大部分数据竞争；但由于使 用大量假设，静态分析方法会产生无效的数据竞争，导致误报率较高。动态 方法通过监控一次执行中内存与同步信息以确定是否存在数据竞争，能够提 供较高精度的检测结果；但是动态分析方法受到交织与路径的影响，往往要 通过多次执行来提高覆盖率。本文将静态代码分析与程序执行过程监测相结 合，以提高覆盖率且尽可能消除误报。

现有的动态检测技术主要分为三种：基于lockset、基于happens-before 与二者结合的方法。1)基于lockset的方法对线程交织不敏感，但是存在误 报情况，即无效竞争。2)基于happens-before的方法只检测某特定交织序列 上的数据竞争，检测结果虽可靠，但敏感于线程交织。3)混合方法结合了两 者的优点，并且试图减小各自的缺点，但也面临如不能够搜索出隐藏的错误、 lockset高误报引起的无效报警等问题。

发明内容

为了克服上述现有技术的缺点，本发明的目的在于提供一种基于多线程程 序约束构建的数据竞争检测与证据生成方法，根据多线程程序语义构建约束表 达式，将数据竞争检测问题转化为约束求解问题，采用约束求解器检测可能存 在的数据竞争，并生成触发数据竞争的程序执行路径。

为了实现上述目的，本发明采用的技术方案是：

一种基于多线程程序约束构建的数据竞争检测与证据生成方法，包括如下 步骤：

S1)在给定输入下，通过执行已插桩的待测程序以生成路径记录文件，且 识别出执行路径中公有变量的访问点以便于约束构建；

S2)根据程序执行语义将执行路径中状态转移、线程交织关系转化为无量 词一阶逻辑表达式，构建蕴含了所有可能的交织序列的多线程程序执行路径约 束模型F；

S3)将路径中所有线程上可能发生数据竞争的两点视为数据竞争候选，收 集所有候选并构建数据竞争候选集合DRCS，同时根据数据竞争的定义构建每个 候选的竞争发生条件ρ；

S4)针对每一个候选竞争发生条件ρ，利用约束求解器验证F∧ρ是否有解；

S5)如果有解，则表示此竞争条件会触发真实的数据竞争；如果无解，则 表示此候选不会触发数据竞争；

S6)当存在数据竞争时，输出该数据竞争的证据序列；

S7)对于数据竞争候选集合DRCS，如果遍历结束，则输出所有结果；否则， 继续遍历下一个竞争候选；

S8)验证结束后，输出检测到的所有数据竞争以及对应的证据序列。

本发明进一步的改进在于：所述步骤S1)中插桩工作并非在源码或者二 进制的层面上进行，而是在字节码的层面上完成，具体实施方法为：首先将 待测多线程程序源码转化为中间字节码格式，即LLVM字节码；然后将具有 监控功能的语句植入待测程序；最后将植入监控代码的字节码链接成可执行 程序。

本发明进一步的改进在于：所述步骤S2)中多线程程序执行路径约束模型 F蕴含了执行路径所有可能的交织序列，包括五种约束：路径表达式、内存 模型约束、读写关系约束、偏序约束以及同步语义约束，定义分别如下：

1)路径表达式：描述线程内部的定义-使用链，以及控制线程内部状态 转换；

2)内存模型约束：表示程序中语句、变量之间的关系，采用顺序一致性 的语义，顺序一致性规定CPU按照代码中语句的顺序来执行程序；

3)读写关系约束：定义线程间的定义-使用链，规定共享变量所读取到 的值，必须来自初始值以及最近的写值；

4)偏序约束：定义线程之间创建线程与终止线程操作语句于被操作线程 语句之间的时序关系；

5)同步语义约束：定义线程之间同步控制操作语句之间的时序关系；

其中，定义-使用链为：将每一个线程序列转化为SSA格式，对于每一 个SSA格式的执行序列，除去共享访问点都是一个完整的定义-使用链。

本发明进一步的改进在于：所述步骤S2)中多线程程序执行路径约束模 型F的构建方法包括以下操作：

1)计算路径表达式，以控制线程内部状态转移；

2)计算内存模型约束，以线程内限制语句之间的关系；

3)计算读写关系约束，以建立线程间的定义-使用链；

4)计算同步语义约束，以定义线程间同步关系；

5)计算偏序约束，以描述线程创建与终止的语义；

最后，结合以上五种约束，构成约束模型F。

本发明进一步的改进在于：定义执行路径事件集合其中k为线程数量，T_i＝{e₁，e₂，…，e_n}作为线程i的执行序列，e_n表示T_i的第n 个事件，O(e_n)表示事件e_n的顺序，n表示T_i的事件数量，则：

所述路径表达式的计算方法：

将每一个线程序列转化为SSA格式，类似于路径条件(Path Condition) 的收集，直接将SSA格式序列转化为路径表达式；

所述内存模型约束的计算方法：

采用顺序一致性模型，所有操作完全按程序的顺序执行，线程内的事件 顺序符合约束：

其中e_i与e_i+1表示同一线程内连续的两个事件，τ表示所有线程序列；

所述读写关系约束的计算方法：

使共享变量的读来自于最近的写，对于同一共享变量v，令R作为所有对 其进行读操作的事件集合，令W作为所有对其进行写操作的事件集合，给出 以下公式：

其中，e_r为读事件，e_w与e_x为写事件，v_r和v_w为事件e_r与e_w所操作的变 量，公式所表达的意思是，如果事件e_r中的v_r取值来自于事件e_w中的v_w，首 先要满足e_r在e_w之后，即O(e_w)＜O(e_r)；然后要满足所有的写要么在e_w之前， 要么在e_r之后；

所述同步语义约束的计算方法包括lock/unlock与wait/signal两类操作：

1)lock/unlock操作的目的为构建锁同步语义约束，要求在同一互斥锁的 lock/unlock集合L中，对于任意两个lock/unlock事件对：l_i/u_i与l_k/u_k，须满 足公式：

其中，锁对l_i/u_i要么发生在锁对l_k/u_k之前，要么发生在其后；

2)wait/signal操作的目的是构建条件变量同步语义约束，要满足条件： 每一个wait操作必须对应一个signal操作，而一个signal操作至多唤醒一个 wait操作，对于同一条件变量cond，令WT作为在cond上所有wait操作的集 合，令SG作为在cond上所有signal操作的集合，如要满足之上的条件，须 有以下公式：

其中，e_wt为WT中的任一元素，SG_wt表示e_wt可以匹配的signal操作的集 合，e_sg为SG_wt中任一signal操作事件，利用变量是否等于1来表示e_sg是 否与e_wt相匹配。子公式表示，对于每一个wait操作e_wt必 须有一个signal操作与之匹配；

所述偏序约束的计算方法：

首先规定：如果事件创建一个线程，那么被创建线程的所有事件都要在 此事件之后执行；如果事件执行线程终止操作，那么被终止线程的所有事件 都要在此事件之前；令C为create/fork操作的事件集合，令J作为join操作的 事件集合；给定约束：

其中，e_c为线程创建事件，first(e_c)为e_c所创建的线程首个事件的顺序； e_i为线程终止事件；last(e_j)为e_j所结束的线程末尾事件的顺序；

最终将以上五种约束相与构成约束模型F。

本发明进一步的改进在于：所述步骤S3)中竞争发生条件ρ的构建方法 如下：如果有一条路径τ＝<τ₁e_ie_jτ₂>，其中τ₁是前缀，τ₂是后缀，事件e_i与 e_j属于不同的线程并且都访问同一内存，至少有一个写，那么二者之间发生 了数据竞争，而τ看作是e_i与e_j数据竞争的证据序列；对于访问同一变量的事 件e_i与ek，e′_i与e″_i分别表示e_i的前一个事件与后一个事件；同样，e′_k与e″_k分别 表示e_k的前一个事件与后一个事件，那么两者发生数据竞争即同时访问同一 内存的条件ρ为：

O(e′_i)＜O(e_k)＜O(e″_i)∧O(e′_k)＜O(e_i)＜O(e″_k)。

本发明进一步的改进在于：所述步骤S7)中对于每一个数据竞争都会生 成证据序列，以描述其触发过程。

与现有技术相比，本发明的有益效果是：

(1)提出一种多线程程序约束构建模型，将一次执行中的数据竞争检测问 题转化为约束求解问题。此模型按照程序语义进行约束构建，所构建的表达式 包含了所有可能的交织序列，进而检测出执行路径中的所有数据竞争。

(2)对所有数据竞争都产生一个证据序列，以给用户提供数据竞争是如何 被触发的信息。

(3)对执行序列进行事后分析，不存在on-the-fly技术所产生的巨大运行 时开销。

附图说明

图1为本发明方法整体流程图。

图2为多线程程序路径约束构建方法流程图。

具体实施方式

以下结合附图和实例详细说明本发明的实施方式。

待测程序如下所示，x与y为共享变量，线程0创建了线程1与线程2。

如图1所示，本发明数据竞争检测与证据生成方法，包括如下步骤：

步骤S1)：将监控代码植入被测程序，以对程序的执行过程进行记录。 给定输入下，执行示例程序，记录下路径π＝[1，2，3，4，5，6，7，8，9，10，11]；然后， 识别出共享变量访问点，包括{1，5，7，9，10}。

步骤S2)：根据程序执行语义将执行路径中状态转移、线程交织关系转 化为无量词一阶逻辑表达式，构建执行路径π的约束模型F，包括路径表达式、 内存模型约束、读写关系约束、偏序约束、同步语义约束。整个约束模型F 蕴含了执行路径所有可能的交织序列。具体地，如图2所示，按照以下步骤 生成对应的逻辑表达式：

S201)首先，根据识别出的共享访问点，将路径π转化为SSA格式，如 下所示：

$\mathrm{initialization}:x_w^0=0,y_w^0=0$

$1:x_w^1=0;$

2：create(1)；

3：create(2)；

4：lock(m)；

$5:x_w^2=a+b;$

6：unlock(m)；

$7:y_w^1=y_r^1+1;$

8：lock(m)；

$9:x_w^3=x_r^0+1;$

$10:y_w^2=y_r^2+1;$

11：unlock(m)；

其中，对于全局变量x与y的下角标表示读(r)或写(w)，上角标区 分不同的读或写操作，上角标为0表示为初始赋值。

然后，根据路径的SSA格式，直接计算出路径π的路径表达式，如下公 式：

S202)构建内存模型约束，采用顺序一致性模型，规定所有操作按程序 的顺序执行。按照公式：

计算出路径π的内存模型约束，如以下公式：

o(e₁)＜o(e₂)＜o(e₃)∧

o(e₄)＜o(e₅)＜o(e₆)＜o(e₇)∧

o(e₈)＜o(e₉)＜o(e₁₀)＜o(e₁₁)

其中，o_i表示第i行语句交织序列中的排列序号。

S203)计算读写顺序约束，使共享变量的读来自于最近的写。对于同一 共享变量v，令R作为所有对其进行读操作的事件集合，令W作为所有对其进 行写操作的事件集合。给出以下公式：

其中，e_r为读事件，e_w与e_x为写事件。公式所表达的意思是，如果事件e_r中 的v_r取值来自于事件e_w中的v_w，首先要满足e_r在e_w之后，即O(e_w)＜O(e_r)； 然后要满足所有的写要么在e_w之前，要么在e_r之后。

在路径π中，对于全局变量x，R＝{e₉}，W＝{e₀，e₁，e₅，e₉}，其读写关系 表达式如下公式：

其中，对变量x的读写可能进行了罗列，当第9行x的读来自于第1行 x的写时，应该满足：第1行在第9行之前，且第5行对x的写不能发生在 两者之间。y变量的情况类似于x。

S204)计算同步语义约束，包括lock/unlock与wait/signal两类操作：

1)构建锁同步语义约束(lock/unlock操作)时，要求在同一互斥锁的 lock/unlock集合L中，对于任意两个lock/unlock事件对：l_i/u_i与l_k/u_k，须满足 公式：

其中，锁对l_i/u_i要么发生在锁对l_k/u_k之前，要么发生在其后。

2)构建条件变量同步语义约束(wait/signal)时，要满足条件：每一个 wait操作必须对应一个signal操作，而一个signal操作至多唤醒一个wait操作。 对于同一条件变量cond，令WT作为在cond上所有wait操作的集合，令SG作 为在cond上所有signal操作的集合。如要满足之上的条件，须有以下公式：

其中，令e_wt为WT中的一个元素，SG_wt表示e_wt可以匹配的signal操作的 集合，WT_sg表示e_sg可以匹配的wait操作的集合。本文利用变量是否等 于1来表示e_sg是否与e_wt相匹配。子公式表示，对于每一个 wait操作e_wt必须有一个signal操作与之匹配。

在路径π中，只有锁m，同步语义约束公式如下：

o(e₆)＜o(e₈)∨o(e₁₁)＜o(e₄)

其中，约束表达式表示要么线程1先获取锁o₆＜o₈，要么线程2先获取 锁o₁₁＜o₄。

S205)计算偏序约束，其规定：如果事件创建一个线程，那么被创建线 程的所有事件都要在此事件之后执行。如果事件执行线程终止操作，那么被 终止线程的所有事件都要在此事件之前。令C为create/fork操作的事件集合， 令J作为join操作的事件集合。给定约束：

其中，e_c为线程创建事件，first(e_c)为e_c所创建的线程首个事件的顺序； e_j为线程终止事件；last(e_j)为e_j所结束的线程末尾事件的顺序。

在路径π中，线程创建语句为O₂，O₃，其偏序关系约束如下公式：

o(e₂)＜o(e₄)∧o(e₃)＜o(e₈)

其中，约束表示线程创建语句第2行在其被创建线程1的首个事件前执 行。

S206)将以上五种约束进行相与，得到约束模型F。

步骤S3)：构建数据竞争候选集合，以及生成每一个候选的竞争发生条 件。对于访问同一变量的事件e_i与e_k，e′_i与e″_i分别表示e_i的前一个事件与后一 个事件；同样，e′_k与e″_k分别表示e_k的前一个事件与后一个事件，那么两者发 生数据竞争(同时访问同一内存)的条件ρ为：

O(e′_i)＜O(e_k)＜O(e″_i)∧O(e′_k)＜O(e_i)＜O(e″_k)。

此示例中的候选集合以及竞争发生条件如下：

候选发生条件

<1，5> o(e₅)＜o(e₂)∧o(e₄)＜o(e₁)＜o(e₆)

<1，9> o(e₉)＜o(e₂)∧o(e₈)＜o(e₁)＜o(e₁₀)

<5，9> o(e₄)＜o(e₉)＜o(e₆)∧o(e₈)＜o(e₅)＜o(e₁₀)

<7，10> o(e₆)＜o(e₁₀)∧o(e₉)＜o(e₇)＜o(e₁₁)

数据竞争的定义为当两个线程同时访问同一内存，且至少有一个写操作。 以第4个候选为例说明，o(e₆)＜o(e₁₀)∧o(e₉)＜o(e₇)＜o(e₁₁)表示第7行与第10 行之间发生数据竞争的条件，其中o(e₉)＜o(e₇)＜o(e₁₁)表示第7行能够发生在 第10行的前一事件(第9行)与后一事件(第11行)之间；由于第7行为 线程末尾，故只用o(e₆)＜o(e₁₀)。此竞争条件成立说明第7行与第10行可以同 时访问同一变量y，则出现数据竞争。

步骤S4一S7)：针对每一个候选，利用求解器求解F∧ρ，验证数据竞争 候选集合DRCS中所有的候选是否为有效数据竞争。以下逐一验证每个候选：

验证F∧o(e₅)＜o(e₂)∧o(e₄)＜o(e₁)＜o(e₆)，结果得出第1行与第5行不发 生数据竞争；

验证F∧o(e₉)＜o(e₂)∧o(e₈)＜o(e₁)＜o(e₁₀)，结果得出第1行与第9行不发 生数据竞争；

验证F∧o(e₄)＜o(e₉)＜o(e₆)∧o(e₈)＜o(e₅)＜o(e₁₀)，结果得出第5行与第9 行不发生数据竞争；

验证F∧o(e₆)＜o(e₁₀)∧o(e₉)＜o(e₇)＜o(e₁₁)，结果得出第7行与第9行之间 数据竞争，且证据序列为：1，2，3，4，5，6，8，9，10，7，11。

遍历完DRCS之后，终止验证工作。

步骤S8)收集所有数据竞争以及对应的证据序列。