基于程序约束构建的多线程程序输出唯一性检测与证据生成方法

摘要

一种基于程序约束构建的多线程程序输出唯一性检测与证据生成方法，根据多线程程序语义构建约束表达式，将输出唯一性验证问题转化为约束求解问题，采用约束求解器检测是否存在不同的输出，并生成说明不同输出的反例执行路径，首先，插桩被检测程序，执行此程序并得到执行路径；其次，根据多线程程序执行语义，将执行路径转化为无量词一阶逻辑表达式，此约束表达式涵盖所有可行的线程交织；然后，针对一次运行的输出结果，构建唯一性验证条件；最后，利用约束求解器验证是否存在一条路径使得输出值与运行结果不一致，本方法可以检测出在给定输入下，多线程程序的输出是否唯一；如果存在输出不唯一的情况，则展示出反例序列以说明其触发过程。

说明书

技术领域

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

背景技术

随着多核处理器被普遍应用，编写性能与结构良好的多线程程序成为释 放多核处理器潜能的重要途径。调试多线程程序中的隐晦错误成为当务之急。 对于串行程序，同一输入，多次执行下输出必定唯一。但是同一输入下对， 于多线程程序的多次执行，未必就能产生唯一的输出。因为多线程程序在每 次执行过程中都可能会产生不同的线程交织，对程序的执行结果也会有不同 的影响。所以，如何验证多线程程序的输出唯一性，是一个亟待解决的问题。

然而，验证多线程程序存在一定的难度，难以重现并行错误。多线程程 序具有以下几个特征：1)用户难以控制所有线程之间的执行顺序；2)在调 试器中使用插装技术或者断点调试方法会产生副作用，导致某些错误消失；3) 由于操作系统与运行时环境的原因，导致错误发生的序列很少再次发生；4) 线程交织导致的空间状态爆炸，例如，对于有n个线程，每个线程执行k指 令的程序，其交织序列数量可达(nk)！/(k！)n＞＝(n！)k。即使在可控制线程调度的 假设下，程序员也无法用穷举所有线程交织。

目前，对于多线程程序的测试与验证已有大量工作，其中包括不确定性 测试与模型检验等。基于覆盖标准指导的不确定测试方法，通过检查每次执 行中的覆盖标准集合以确定尚未覆盖的元素，向程序中插入随机延迟以增大 下次执行中覆盖其他元素的可能性。此外，模型检验通过符号化程序状态以 及遍历整个状态空间，以查找程序中的错误状态。虽然模型检验在一定程度 解决了多线程程序的验证问题，但其具有状态空间爆炸问题，导致难以扩展 应用到大型复杂软件系统。

发明内容

为了克服上述现有技术的缺点，本发明的目的在于提供一种基于程序约束 构建的多线程程序输出唯一性检测与证据生成方法，根据多线程程序语义构建 约束表达式，将输出唯一性的验证问题转化为约束求解问题，采用约束求解器 检测是否存在不同的输出，并生成说明不同输出的反例执行路径。

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

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

S1)将监控代码植入待测程序，以记录程序的执行过程；

S2)在给定输入下，执行已插桩程序，生成路径记录文件；

S3)预处理执行路径以便于约束构建；

S4)在程序运行结尾处自动添加属性条件，针对多线程程序的运行输出， 将输出唯一性条件ρ以assert的格式插入程序；

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

S6)针对唯一性条件ρ，利用约束求解器验证是否有解。

S7)如果有解，则表示存在多种不同的输出，并生成证据序列；如果无解， 则表示此输出在此输入下唯一。

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

本发明进一步的改进在于：所述步骤S3)中预处理包括提取共享变量以识 别出执行路径中公有变量的访问点以及切片以去除与验证属性无关的执行语句。

本发明进一步的改进在于：所述步骤S4)中自动识别出输出变量且对其构 建输出唯一性验证条件ρ。

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

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

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

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

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

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

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

本发明进一步的改进在于：所述步骤S5)中多线程程序执行路径约束模 型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_j为线程终止事件；last(e_j)为e_j所结束的线程末尾事件的顺序；

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

本发明进一步的改进在于：所述步骤S6)中给定约束模型与输出唯一性 属性条件，利用约束求解器求解属性条件；如果存在不同的输出，则生成反 例以说明此不同输出的触发过程。

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

(1)提出一种多线程程序约束构建模型，将多线程程序的输出唯一性验证 问题转化为约束求解问题。此模型按照程序语义进行约束构建，所构建的表达 式包含了所有可能的交织序列，利用约束求解器检查所有交织是否会产生不同 的输出。

(2)如果存在不同的输出时，产生一个证据序列，以给用户展示此不同的 结果是如何被生成的。

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

附图说明

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

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

具体实施方式

以下结合附图和实例详细说明本发明的实施方式。待测程序如下所示，x 与y为共享变量，线程0在第1行与第2行创建了线程1与线程2。

如图1所示，一种基于多线程程序约束构建的输出唯一性验证方法，包括 如下步骤：

步骤S1)：将监控代码植入被测程序，以对程序的执行过程进行记录。 在LLVM字节码的层面上，插装完成之后所呈现的代码样式如下；

其中，函数clap_inst_pre为被插入的监控语句，监控其后的一行语句， 执行过程中会输出后一行的线程ID、指令ID、状态值以及返回值。

步骤S2)：给定输入下，执行示例程序，记录下路径 ＝[1，2，3，4，5，6，7，8，9，10，11，12，13，14]；

步骤S3)：预处理路径以便于S4)的约束构建，提取全局变量访问点， 包括行：5，6，8，9，12，13；将路径转化为SSA格式。线程0转化为轨迹0，线 程1转化为轨迹1，线程2转化为轨迹2，如下所示：

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

步骤S4)：在此，针对全局变量x与y，预期结果分别为6与5，在末 尾处插入断言x＝6与y＝5。同时，令x＝6与y＝5作为输出唯一性验证条件， 如下所示，

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

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

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

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

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

o(e₅)＜o(e₆)＜o(e₇)＜o(e₈)＜o(e₉)＜o(e₁₀)∧

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

其中，o(e_i)表示第i行语句交织序列中的排列序号。

S503)计算读写顺序约束，使共享变量的读来自于最近的写。对于同一 共享变量，令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之后。

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

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

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

1)构建锁同步语义约束(lock/unlock操作)时，要求在同一互斥锁的 lock/unlock集合中，对于任意两个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操作与之匹配。

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

o(e₁₀)＜o(e₁₁)∨o(e₁₄)＜o(e₇)

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

S505)计算偏序约束，其规定：如果事件创建一个线程，那么被创建线 程的所有事件都要在此事件之后执行。如果事件执行线程终止操作，那么被 终止线程的所有事件都要在此事件之前。令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₁₁)∧

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

其中，约束o(e₁)＜o(e₅)表示线程创建语句e₁在其被创建线程1的首个事件 e₅前执行，约束o(e₁₀)＜o(e₃)表示线程等待语句e₃在线程1的末尾事件e₁₀后执 行。

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

步骤S6)在本示例中，输出唯一性验证条件分别为ρ₁∶x＝6、ρ₂∶y＝5， 利用约束求解器求解与，两者皆有解；ρ₁的反例为 {1，2，5，11，12，13，14，6，7，8，9，10}，ρ₂的反例为{1，2，5，6，11，12，13，14，7，8，9，10}。

步骤S7)输出验证结果以及反例序列。