一种基于约束求解的原子违背探测方法

摘要

本发明提供一种基于约束求解的原子违背探测方法，利用并发程序的原始执行轨迹确定原子性区域，结合原子违背的各种错误模式，建立原始执行轨迹中事件之间执行先后顺序的约束关系，利用Z3求解器进行约束求解，将原子违背的探测问题转化为约束等式的求解问题。本方法属于运行时预测技术，可根据约束求解出隐藏在原始执行轨迹中没有暴露出的原子违背错误，具有更好的探测原子违背的能力；对原始程序轨迹和每个不可序列化的执行交织建立一组约束，将探测原子违背问题转化为约束的求解问题，能够提高原子违背探测的精度。

说明书

所属技术领域

本发明涉及软件测试技术领域，具体涉及一种基于约束求解的原子违背探测方法。

背景技术

随着多核处理器的普及，并发编程技术得到了广泛的应用。由于并发程序的执行交织空间大、运行不确定，并发程序错误的测试、调试以及修复十分困难。其中，原子违背是其中最常见的并发错误，约占非死锁类型并发错误的65％。现有的原子违背探测技术大致分为三类：静态探测技术、运行时监测技术和运行时预测技术。其中，静态探测技术可在程序源代码级别识别出潜在的原子违背错误，但其无法处理锁以外的其他类型的同步原语，误检率高。运行时监测技术监测并发程序执行，探测在程序实际执行中暴露出的原子违背错误，其误检率低，但漏检率高。运行时预测技术通过对程序执行序列进行分析和处理，可探测出隐藏在程序执行序列中尚未暴露的原子违背。然而，现有很多运行时预测技术或者由于采用了保守的并发程序模型，其探测结果具有较高的误检率，或者由于搜索交织空间有限，具有较高的漏检率。

若某执行轨迹至少满足Happened-Before和锁保护两个约束，则称其为合法轨迹。其中，Happened-Before关系约束，包含以下三个方面：

●若事件e_i,e_j属于同一线程，且e_i发生在e_j之前，那么在任何情况下e_i都在e_j之前执行；

●若事件e_i开启了e_j所在的线程，那么e_i必须在e_j前发生；

●若事件e_j等待来在e_i发送的信息，那么e_i在e_j前发生；

锁约束(Lock Constraint)：每一个锁对(acquire-release)都不能与其他操作同一锁变量的锁对产生交织，即在任何情况下对于任何一个锁只能被一个线程拥有，以保证互斥访问。

对同一共享变量进行访问的原子违背有如下五种模式，如表1，其中t_i表示线程，R_i,W_j分别表示线程t_i的读事件与写事件，m表示事件所存取的内存位置。

表1：原子违背的各种模式

发明内容

针对现有技术的不足，本发明提出一种基于约束求解的原子违背探测方法，将原子违背的探测问题转化为约束等式的求解问题，可有效降低原子违背探测的误检率，提高其探测能力。

为实现上述方面目的，本发明采用如下技术方案：

一种基于约束求解的原子违背探测方法，利用并发程序原始执行轨迹，结合原子违背的各种错误模式，建立原始执行轨迹中事件之间执行先后顺序的约束关系，并求解，当约束有解时，该解对应的新的执行轨迹中存在原子违背现象，当约束无解时，则不存在原子违背现象。

进一步的，包括以下步骤：

步骤1)：记录原始执行轨迹：

步骤11)：对原始程序进行插桩，以便在运行时记录需要的执行轨迹信息；

步骤12)：执行原始程序，记录执行轨迹，一个执行轨迹是一个事件序列，表示为δ＝<e₁,e₂,…e_i,…,e_n>，其中每个事件e_i包含下列属性：

t_i：事件e_i所属的线程；

m_i：事件e_i所存取的内存位置；

l_i：当事件e_i执行时，其所拥有的锁；

a_i：事件e_i的存取类型，包括读、写、获取锁、释放锁、等待、通知、创建线程和等待线程结束等八种类型；

步骤2)：由步骤1)所得的原始执行轨迹和预定义的原子区域模式确定原子性区域，并利用原子区域和原子违背的各种错误模式收集潜在的可能会引起不可序列化交织的事件序列：

步骤21)：由步骤1)所得的执行轨迹和预定义的原子区域模式，确定原子性区域；将每个synchronized方法，synchronized代码块以及锁保护的代码块均视为原子区域；

步骤22)：给定a,b,c三个事件，其中thread(a)＝thread(b)≠thread(c)，若事件a,b属于步骤21)所得的同一原子性区域，且这三个事件的读写类型符合某个原子违背模式中对应的事件读写类型，则事件a,b,c是一个潜在的可能会引起不可序列化交织的事件序列；收集这些潜在的可能会引起不可序列化交织的事件序列，对这些收集的事件序列，进一步探测是否存在执行轨迹使这些事件序列中的三个事件的执行顺序符合不可序列化交织模式；

步骤3)：建立原子违背约束；

对步骤22)中得到的事件序列建立原子违背约束，其中(a，c，b)是某个事件序列中的三个事件，其中thread(a)＝thread(b)≠thread(c)，且事件a，b来自同一原子性区域，约束内容分为两部分：

第一部分：在求解出的执行轨迹中事件c要在事件a和事件b之间被执行；

第二部分：事件a，b，c在求解出的执行轨迹中一定会被执行，但不要求事件a，b，c读写的值与原执行轨迹中的事件a，b，c读写的值一样；

步骤4)：原子违背约束求解

使用Z3约束求解器进行约束求解，当约束有解时，该解对应的新的执行轨迹中存在原子违背现象，否则不存在。

本发明的有益效果为：1、对原始程序轨迹和每个不可序列化的执行交织建立一组约束，将探测原子违背问题转化为约束的求解问题，提高原子违背探测的精度；

2、本方法属于运行时预测技术，可根据约束求解出隐藏在原始执行轨迹中没有暴露出的原子违背错误，具有更好的探测原子违背的能力。

附图说明

图1为本发明方法的实施流程图。

具体实施方式

本发明利用并发程序原始执行轨迹，结合原子违背的各种错误模式，建立原始执行轨迹中事件之间执行先后顺序的约束关系，并求解，当约束有解时，该解对应的新的执行轨迹中存在原子违背现象，否则不存在，具体而言，包括以下步骤：

1.得到执行轨迹：

(1)对原始程序进行插桩，以便在运行时记录需要的轨迹执行信息；

顺序扫描被测程序中的每条语句，在特定的语句前后插桩代码，如：同步语句、赋值语句、分支语句等，在实际执行时收集与这些语句相关的信息以组合成事件并保存到数据库中；

(2)执行插桩后的原始并发程序，得到执行轨迹，一个执行轨迹是一个事件序列，表示为δ＝<e₁,e₂,…e_i,…,e_n>，其中每个事件e_i包含下列属性：

t_i：事件e_i所属的线程；

m_i：事件e_i所存取的内存位置；

l_i：当事件e_i执行时，其所拥有的锁；

a_i：事件e_i的存取类型，包括读，写，获取锁，释放锁，等待，通知，创建线程和等待线程结束8种类型。

2.利用所得执行轨迹和预定义的原子区域模式确定原子性区域，并利用原子区域和原子违背的各种错误模式收集潜在的可能会引起不可序列化交织的事件序列：

(1)本发明中将每个synchronized方法，synchronized代码块以及锁保护的代码块均看做原子区域；

执行轨迹中包含进入和退出synchronized方法，synchronized代码块和锁保护区域的acquire和release事件，通过分析执行轨迹得到每个线程访问每个锁变量的<acquire,release>对序列，对于每个<acquire,release>事件对，定位acquire和release事件在对应线程执行轨迹中的位置，并将acquire和release事件的位置作为原子区域边界；将每对原子区域边界之间的事件序列看作一个原子区域；

(2)a,b,c三个事件，其中thread(a)＝thread(b)≠thread(c)，事件a,b属于步骤21)所得的同一原子性区域，且这三个事件的读写类型符合某个原子违背模式中对应的事件读写类型，则事件a,b,c是一个潜在的可能会引起不可序列化交织的事件序列，收集这些潜在的可能会引起不可序列化交织的事件序列，对收集的这些事件序列，我们进行进一步探测是否存在执行轨迹能使得这些事件序列中的三个事件的执行顺序符合不可序列化交织模式；

对每组由三个事件a,b,c组成的可能会引起不可序列化交织的事件序列进行快速检查，判断此事件序列是否满足构成原子违背的前提条件，快速检查的内容包括：检查事件c和事件a,b是否被同一把锁保护，事件c和事件a,b之间是否存在happened-before关系；若满足这两个条件的任意一条则表明事件c不会发生在事件a和b之间，即不会构成一个真正的原子违背，因此不需要对此事件序列建立约束。

3.约束的建立与求解，验证步骤2得到的潜在的可能会引起不可序列化交织的事件序列是否是真正的原子违背；

为验证步骤2得到的潜在的可能会引起不可序列化交织的事件序列是否是真正的原子违背，需求解是否存在执行轨迹能使所得事件序列中的三个事件的执行顺序符合不可序列化交织模式，对步骤1)中得到的执行轨迹和步骤22)中得到的事件序列建立约束并求解，需要建立的约束等式有：happened-before约束、锁互斥约束、原子违背约束，将原子违背的探测问题转化为约束等式的求解问题。

(1)建立原子违背约束：

对步骤2中得到的事件序列建立原子违背约束，其中(a,c,b)是某个事件序列中的三个事件，其中thread(a)＝thread(b)≠thread(c)，且事件a,b来自同一原子性区域，约束内容主要分为两部分：

(11)事件a,b,c执行的顺序约束，在原子违背模式中要求事件c在事件事件a和事件b之间被执行，因此c在事件a和事件b之间被执行是此事件序列构成原子违背的必要条件，因此在求解出的执行轨迹中事件c要在事件a和事件b之间被执行；

(12)需要保证事件a,b,c在求解出的执行轨迹中一定会被执行，但不要求事件a,b,c读写的值与原执行轨迹中的事件a,b,c读写的值一样；

由于不要求read和write事件读写特定的值，因此影响读写事件e的可行性因素除了Happened-before关系和锁一致性要求以外，还有一些必须发生在e之前的分支(branch)事件；若这些branch事件是不可行的，则事件e也是不可行的，即在事件e在求解出的执行轨迹中不会执行，因此需要保证这些branch事件的可行性；

对每个读写事件e只需考虑每个线程距离事件e最近，且和e有偏序关系的branch事件的具体可行性，“具体”表示某事件在求解出的执行轨迹中所有属性的值都和原执行轨迹中对应的事件相等；branch事件的可行性依赖于在同一线程内在branch事件之前的所有read事件，即约束branch事件所依赖的read事件的值在求解出的执行轨迹中与原执行轨迹中相等；branch事件的可行性约束进而转化为对read事件可行性的约束，read事件的可行性约束要求read事件读取的值与原执行轨迹中在此read事件之前发生、距离此read事件最近且与此read事件操作同一共享变量的write事件的值相同；

在对branch事件建立可行性约束时，若假定branch事件的可行性依赖于同一线程内部在branch事件之前所有的read事件，则会引入一些不必要的read事件的可行性约束；实际程序执行时，branch事件读取的共享变量的值来自同一线程内在branch事件之前且离branch事件最近，读同一共享共享变量的read事件的值；因此为确保branch事件读写共享变量的值不变，只需保证线程内在branch事件之前的所有read事件中，如果有多个read事件操作同一共享变量，则只需确保距离branch事件最近的read事件读的值不变，而不需要所有的read事件读的值不变；通过这种方法可以减少对于分支事件可行性建立约束的个数，从而减少约束求解的时间。

(2)约束求解

在本发明中我们借助约束求解器Z3实现约束的求解，将所有的约束组合并调用求解器求解方法，观察对步骤2中得到的事件序列建立的约束求解是否有解，若有解则说明存在执行轨迹可以按照这种不可序列化交错序列的顺序执行事件序列中的三个事件，即此潜在的可能会引起不可序列化交织的事件序列是一个真实的原子违背。

以上所述仅是本发明的优选实施方式，应当指出，对于本技术领域的普通技术人员来说，在不脱离本发明原理的前提下，还可以做出若干改进和润饰，这些改进和润饰也应视为本发明的保护范围。