基于内存访问模式的并发程序缺陷检测方法

摘要

本发明公开了一种基于内存访问模式的并发程序缺陷检测方法，通过借助MAP‑coverage匹配并发程序执行中尚未被覆盖的内存访问模式，构建程序约束并利用约束求解器，求解出程序调度，来取得更高的MAP‑coverage。与现有技术相比，本发明将并发程序状态空间的探索问题转换为约束求解问题，使用约束求解方法可以确定性的探索并发程序的状态空间；2)避免约束求解对冗余约束的探索，加快并发程序缺陷检测的过程；3)利用定义的过滤规则，可以过滤掉在特定上下文中冗余的内存访问模式，减少探索的开销。

说明书

技术领域

本发明涉及软件工程和软件测试领域，尤其涉及一种并发程序缺陷检测方法。

背景技术

随着多核架构的普及以及众多编程语言对并发的支持，人们对并发处理的需求进一步提升。然而，并发程序缺陷很难被检测和调试，且并发程序缺陷会对软件的可靠性构成严重的威胁，因此必须对并发测试进行全面的测试。由于并发程序的状态空间随着线程及指令数的增长而呈现指数级增长，因此测试并发程序的基本挑战之一是如何有选择地探索庞大的线程交错空间。目前，现有的并发缺陷检测方法多集中于约减庞大线程交错空间中的无效线程交错。通过减少对无效线程交错的探索从而减少对并发程序状态空间探索的开销。对于给定的并发程序测试套件，如何去衡量状态空间探索的充分性同样至关重要。在传统的软件工程中，可以通过不同种类的代码覆盖度量来衡量测试的充分性。例如代码行覆盖(statement coverage)分支覆盖(ranch coverage)及路径覆盖(path coverage)等等。然而这些代码覆盖度量都是为顺序程序而设计的，因此很难去衡量并发程序的特性。

目前已有部分研究工作在尝试为并发程序设计新的代码覆盖度量，例如，Valerio等人提出的Sequential Coverage、Lu等人提出的Method-Pair Coverage。然而这些工作一方面设计的代码覆盖度量粒度较粗，很难捕捉并发测试的特性，另一方面从测试用例的角度去衡量充分性会丢失很多运行时信息。最近，研究人员提出了一种MAP-coverage(内存访问模式的简称，Memory-Access Pattern)的多线程程序的代码覆盖标准。不同于现有的研究工作，MAP-coverage尝试衡量一组测试执行的覆盖率而不是测试用例的覆盖率。且已有研究工作表明，内存访问模式在一定程度上揭示了并发错误的本质，如表1所示，为内存访问模式。直观地，内存访问模式是描述多个线程如何访问共享变量的模式。内存访问模式可以看作是测试执行的抽象，它使并发缺陷的分析可以忽略不相关的细节，同时保留多线程错误的原因。一个内存访问模式有一组字节码指令组成，如表1所示，为十七种内存访问模式。例如，表1中第四个内存访问模式是一个包含三个步骤的执行：首先，线程t读取变量x。其次，另一个线程写入x。最后，线程t再次读取变量x。基于MAP-coverage不仅可以衡量并发程序探索的充分性，同时还可以以此为指导生成可以覆盖尚未被覆盖的内存访问模式的测试用例。大量的实验表明MAP-coverage对衡量并发程序测试的充分性有效。MAPTest是基于MAP-coverage的并发程序测试代码生成工具。MAPTest根据MAP-coverage指导，优先生成尚未被探索或很少被探索的内存访问模式测试代码，并利用控制执行方法指导程序的测试运行，以此提高并发程序的MAP-Coverage。然而，现MAPTest基于随机测试，这种做法很难触发罕见的线程交错才能导致的并发错误。

表1

现有并发程序缺陷检测技术包含以下缺点和不足：

(1)基于随机生成测试代码的方法不确定性太高，很难触发罕见的线程交错才能导致的并发错误；(2)现有的内存访问模式在特定上下文环境中仍存在冗余内存访问模式，对此类内存访问模式的探索会增加运行成本，降低测试效率；(3)现有基于约束求解对状态空间确定性探索的方法存在对不可解约束重复求解的问题，从而增加了测试成本。

发明内容

为了解决现有并发缺陷检测技术在探索过程中存在的随机探索不确定性高、检测效率低等问题，本发明提出了一种基于内存访问模式的并发程序缺陷检测方法，通过将包含并发缺陷的程序抽象成内存访问模式以及路径条件进行迭代编码表示成程序约束，并采用优化的约束求解，生成获得高MAP-coverage的线程交错，以此来达到更快检测出并发缺陷的目的。

本发明的一种基于内存访问模式的并发程序缺陷检测方法，该方法包括以下步骤：

步骤1、对给定的被检测并发程序进行程序插桩，以记录被检测并发程序的执行轨迹，至少包括记录被检测并发程序在运行过程中所发生的事件，这些事件包含线程启动事件，共享变量读取、写入；

步骤2、进行内存访问模式匹配，即结合对内存访问模式的查询进行被检测并发程序执行轨迹中尚未被覆盖的内存访问模式匹配；其中，将动态执行轨迹中的每一步操作定义成一个元组

在获取到测试用例的动态执行之后，匹配已经被覆盖的内存访问模式，进而从已经覆盖的内存访问模式中推断出尚未被覆盖的内存访问模式；

程序执行轨迹由测试用例执行过程中产生的各种事件所组成，包含线程启动事件、线程结束事件、线程Join事件、Lock事件、UnLock事件、Wait事件、Notify事件以及对变量的读事件和写事件；每个事件中包含事件全局发生ID，事件操作的变量ID、变量地址、变量标签以及对应的变量的值，给定这些信息便可以从中匹配出相关的内存访问模式；根据以下规则对内存模式进行约减处理，包括：

NONDEFINED规则定义为给定的内存访问模式类型不存在；

COVERED规则定义为给定的内存访问模式已被覆盖；

VIOLATION规则定义为给定的内存访问模式违背Happens-before关系；

INVARIANT规则定义为给定的内存访问模式不能触发新的程序状态；

INTERRUPTED规则定义为给定的内存访问模式被其它写指令所打断；

REDUNDANT规则定义为给定的内存访问模式是冗余的；

约减后得到尚未被覆盖的内存访问模式，从而实现了新的程序状态的触发；

步骤3、构建程序约束，即将排序后的内存访问模式以及动态执行轨迹将作为输入，生成新的线程调度，并对测试用例进行重复的探索，直至触发并发程序错误或到达设置的停止时间，根据被检测并发程序执行轨迹以及匹配出的执行轨迹中尚未被覆盖的内存访问模式构建对应于完备调度的程序约束，在这些程序约束中定义了并发程序该如何执行；

步骤4、进行约束求解，即以构建好的约束以文件形式作为本步骤的输入，求解出新的程序调度，随后实现对并发程序进行重复的探索，实现对被检测并发程序进行完备的探索，对程序进行再调度以覆盖尚未被覆盖的内存访问模式，具体实现过程如下：

使用Z3约束求解器求解构建的程序约束，具体包括根据构建的程序事件发生顺序约束，求解出一条可满足约束可线程调度，该线程调度以指定线程切换覆盖尚未被覆盖的内存访问模式，以此来增加并发程序的MAP-coverage；

所述步骤1中，被检测并发程序在运行过程中所发生的事件，具体包括线程的起始以及终止事件、线程对变量的读或者写事件、线程获取以及释放锁事件、由当前线程创建一个新线程′事件、当前线程等待另外的线程执行终止事件。

所述步骤3中，新生成的线程调度同时满足以下条件的并发程序：

条件一、读一致性条件，即前缀中的读操作必须与原有执行轨迹中读取的值相同；

条件二、互斥条件，即每个释放锁事件必须有相应的获取锁事件与之相对应；

条件三、先发生于条件：即一个线程的begin事件必须是当前线程的第一个事件，线程的join事件是当前线程的最后一个事件，其它对应的读写事件只能发生在begin事件之后，以及join事件之前。

所述步骤3中，程序约束包括Start-Join约束、Happens-Before约束、数据有效性约束以及Pattern约束。

与现有技术相比，本发明能够达成的有益技术效果如下：

1)实现了将并发程序状态空间的探索问题转换为约束求解问题，使用约束求解方法可以确定性的探索并发程序的状态空间；

2)避免约束求解对冗余约束的探索，加快并发程序缺陷检测的过程；

3)利用定义的过滤规则过滤掉在特定上下文中冗余的内存访问模式，减少探索的开销；

4)利用确定性的探索庞大的并发程序状态空间，减少了探索过程的随机性，且不会重复探索冗余的线程交错，可以更快的取得更高的MAP-coverage，效率更高。

附图说明

图1为本发明的基于内存访问模式的并发程序缺陷检测方法流程图；

图2为插桩流程图；

图3为动态执行轨迹序列示意图；

图4为VIOLATION约减规则示意图；

图5为INVARIANT约减规则示意图；

图6为INTERRUPTED约减规则示意图；

图7为INTERRUPTED约减规则示意图；

图8为REDUNDANT约减规则示意图；

图9为示例Java程序示意图；

图10为并发程序测试用例示意图；

图11为调度分析及内存访问模式匹配示意图。

具体实施方式

下面结合附图和具体实施例对本发明技术方案作进一步详细描述。

本发明一种基于内存访问模式的并发程序缺陷检测方法，该方法是一种模式约束减少(Pattern Constraint Reduction，PCR)的新方法，通过借助MAP-coverage匹配并发程序执行中尚未被覆盖的内存访问模式，构建程序约束并利用约束求解器，求解出程序调度，来取得更高的MAP-coverage，采用优化的约束求解来生成高MAP-coverage的线程交错。

如图1所示，为本发明的基于内存访问模式的并发程序缺陷检测方法流程图。该流程的具体实施由即程序插桩模块、匹配内存访问模式模块、构建程序约束模块、约束求解模块和调度执行模块5个模块来实现。

步骤1、对给定的被检测并发程序进行程序插桩，记录被检测并发程序的执行轨迹，主要记录被检测并发程序在运行过程中所发生的事件，这些事件包含线程启动事件，共享变量读取、写入等；

本步骤以针对线程安全类的并发测试程序作为输入，每个并发测试程序包含两个部分：前缀和后缀。前缀是顺序执行的一条线程，用来声明当前测试类的对象以及随机调用一些类方法改变当前对象的状态。后缀则是两条不同的线程并发执行，潜在的并发程序错误往往隐藏在后缀并发执行的线程交错中。然而，输入的并发测试程序是未经任何处理的，直接将其加载至JVM执行无法获得准确的线程执行信息，更无法为后续模块提供准确的输入。现有研究方法中记录程序执行轨迹主要采用程序插桩的方法，例如PECAN、LEAP、MCR等。使用字节码增加工具ASM对并发程序进行插桩。ASM是针对Java字节码的代码分析和修改工具，无需项目的源代码即可对被测项目插入所需的执行代码，通常被用来动态生成类或增强现有类的功能。ASM可以直接生成二进制Java字节码文件，也可以在Java类被加载至JVM之前动态修改类的行为。

如图2所示，为插桩过程的流程图。其中，对Java类的插桩发生在Java类编译之后加载之前。因此插桩操作需要对加载至JVM的文件进行拦截，如果不对其进行拦截，如图中的虚线所示，Java程序再编译成字节码文件之后便直接加载至JVM执行。然而，ASM是Java字节码修改工具，不具备拦截功能，因此使用Java在Java SE 5中引入的新特性JavaInstrumentation。Instrumentation可以构建独立于应用程序的代理程序，在代理程序中指定检测或协助JVM中运行的应用程序。Instrumentation通过JAR包指定插桩类，在类中重写premain函数。在premain函数中拦截加载至JVM中的类文件，再通过ASM解析，插入记录和调度代码后将修改后的字节码文件再加载至JVM运行。被插桩的并发程序在动态执行的过程中记录下运行的轨迹，以此为后续流程提供输入。

并发程序的错误往往是因为脏读、数据可见性等问题造成。考虑到并发程序庞大的状态空间，记录所有调度信息是不可能的，而且记录无用的调度信息还会增加后续分析的成本。与此同时，内存访问模式即对变量读/写操作的组合，因此插桩操作主要记录与并发程序错误相关的读/写节点，例如主要包括对变量的读操作，在字节码中对应的指令为GETFIELD、GETSTATIC；对变量的写操作，在字节码中对应的指令为PUTFIELD、PUTSTATIC。当分析对变量的读操作时，当ASM分析到GETFIELD或GETSTATIC指令，插桩操作在此指令前插入记录代码，记录代码的内容主要包含变量ID、变量对象、变量语句ID、变量的值以及变量是否为写操作。对变量的写操作分析过程相似；

步骤2、进行内存访问模式匹配，即结合对表1的查询进行被检测并发程序执行轨迹中尚未被覆盖的内存访问模式匹配；

测试用例以及线程安全类插桩的目的包括记录测试用例的动态执行轨迹以及后续对测试用例进行确定性探索。在上个模块进行插桩之后，本发明便可在测试用例运行结束之后获得动态执行的轨迹。一个动态执行轨迹由不同的原子性指令在特定的线程交织下组成的调度序列，如图3所示。这里将动态执行轨迹中的每一步定义成一个元组

在获取到测试用例的动态执行之后，可从中匹配已经被覆盖的内存访问模式，进而从已经覆盖的内存访问模式中推断出尚未被覆盖的内存访问模式。程序执行轨迹主要由测试用例执行过程中产生的各种事件所组成，这些事件主要包含线程启动事件、线程结束事件、线程Join事件、Lock事件、UnLock事件、Wait事件、Notify事件以及最重要的对变量的读事件和写事件。每个事件主要包含事件全局发生ID，事件操作的变量ID、变量地址、变量标签以及对应的变量的值。给定这些信息便可以从中匹配出相关的内存访问模式。

然而，基于获得的未约减前的内存访问模式中包含大量冗余以及已经覆盖的内存访问模式。已经访问的内存访问模式被证明无法触发并发错误，除此之外还有冗余的内存访问模式，这类内存访问模式保留下来不仅不会对并发程序状态空间的约减起不到帮助作用，而且会增加PCR约束求解以及探索的运行时开销。因此，本发明需要对这类内存访问模式进行约减。通过对表1中的内存访问模式进行全面的分析总结出6种约减规则，如表2所示。首先检查集合中的内存访问模式类型是否在表1中定义，约减掉类型不匹配的内存访问模式，对应NONDEFINED规则。其次，根据COVERED规则约减掉已经被覆盖的内存访问模式，已经被覆盖的内存访问模式被证明是与错误无关的。表2中的1-2很好分析及理解，3-6约减规则从内存访问模式的行为分析，进一步约减冗余的内存访问模式。图4至图7给出了3-6约减规则中对应的例子说明，定义

表2

①VIOLATION约减规则：如图4所示，为VIOLATION约减规则示意图。根据表2中的定义，VIOLATION表示给定的内存访问模式违背Happens-before关系。具体来说，生成内存访问模式中来自同一线程的事件必须满足Happens-before关系，即来自同一线程的读写事件必须服从执行轨迹中的原始顺序。(4a)为给定执行轨迹，(4b)为匹配出的一个长度为3的包括操作

②INVARIANT约减规则：为了约减并发程序的状态空间，因此需要尽可能的减少探索在行为上表现一致的线程交错，进而探索可以产生新的程序状态的线程交错。这里新的程序状态表现为，通过改变原有执行轨迹中不同线程事件的执行顺序，使目标共享变量读取到不同的值或改变不同写事件的顺序(写事件对同一变量写的值必须不同)。如图5所示，为INVARIANT约减规则示意图。(5a)为原有的执行轨迹，在原有的执行轨迹中，操作

③INTERRUPTED约减规则：新生成的内存访问模式同样需要避免被其它写指令所打断，这里的打断是值当前内存访问模式中穿插这对相同变量的其它写操作。如图6所示，为INTERRUPTED约减规则示意图。其中，假设根据图6中的原有执行轨迹，匹配一个长度为3的内存访问模式，例如

④REDUNDANT约减规则：对于长度为4的内存访问模式，通常涉及到对两个共享变量的操作。这种情况下，如果内存访问模式中一个变量操作指令的变化既不能使自身到达一个新的状态，也不能改变另一个变量的行为，这种内存访问模式需要被约减掉。如图7所示，为INTERRUPTED约减规则示意图。(7a)为给定的执行轨迹；(7b)为匹配出的一个长度为4的内存访问模式包括操作

约减后的内存访问模式是尚未被覆盖的，可以触发新的程序状态。然而，不同的内存访问模式与触发错误的相关性是未知的，并且会因为程序特征而改变。本发明旨在探索更少的线程交错空间，来更快的触发并发错误。因此，如何将更容易出错的内存访问模式排在前面，优先生成此类内存访问模式的调度是本发明需要考虑的问题。然而，导致不同并发程序出错的内存访问模式并不同很难给定一个特定的内存访问模式顺序对所有的并发程序都适用。基于约束求解构建程序约束求解新的线程调度，因此，从约束求解的角度出发，约束越多的内存访问模式求解出来的结果更具有确定性。如图8所示，为REDUNDANT约减规则示意图。(8a)为给定的执行轨迹，(8b)为匹配出的一个长度为2的内存访问模式包括操作

步骤3、构建程序约束，即将排序后的内存访问模式以及动态执行轨迹将作为输入，生成新的线程调度，并对测试用例进行重复的探索，直至触发并发程序错误或到达设置的停止时间，根据被检测并发程序执行轨迹以及匹配出的执行轨迹中尚未被覆盖的内存访问模式构建对应于完备调度的程序约束，在这些程序约束中定义了并发程序该如何执行。

值得注意的是，传统并发程序的调度主要依赖延迟、注解等方法，然而这些方法一方面耗时，在程序调度上耗费了太多的时间成本。另一方面，再调度的准确性较低，很难将执行轨迹中的每一个事件都纳入考量。本发明采用程序插桩的方式通过全局调度器控制线程的执行，既解决了调度不精确问题，同时也减少了调度的成本。最终，新的程序调度将作为调度执行模块的输入对并发程序进行再探索。

本发明的程序约束规定了新的线程调度如何执行，并在此基础上添加内存访问模式的约束，使新生成的调度可以覆盖之前动态执行中尚未被覆盖的内存分访问模式。具体来说，这些约束规定了已有执行轨迹中不同事件的执行顺序，这些事件由插桩模块插入的记录点所记录，同时每个记录点对应有相应的调度点，因此可以在求解出新的调度后对相同测试用例进行重复的探索。

本发明所考虑的事件主要包括：

(1)线程t的起始以及终止事件；

(2)线程t对变量x的读或者写写事件，且读/写的值为v；

(3)线程t获取以及释放锁l事件；

(4)线程t创建一个新线程t′事件；

(5)线程t等待线程t′执行终止事件；

一个完成的执行轨迹可以抽象成上述事件所组成的序列，则是根据已有的执行序列构建新的线程调度来探索测试用例。具体来说，新生成的线程调度必须同时满足并发程序的以下条件：

条件一、读一致性条件：本发明生成的新线程调度是基于前缀的，需要构建对应给定内存访问模式之前的事件的执行顺序。新生成的调度尝试去覆盖尚未被覆盖的内存访问模式，然而这需要程序正确运行到对应内存访问模式的调度点。因此前缀中的读操作必须与原有执行轨迹中读取的值相同。

条件二、互斥条件：多线程程序中，所有的同步代码块必须是互斥的，这意外着当前线程持有的锁，其它线程如果想获取必须等待其释放锁。而每个释放锁事件必须有相应的获取锁事件与之相对应。

条件三、先发生于条件：多线程程序指不同线程之间的并发执行，然而线程内的执行方式是顺序执行，如此才符合顺序一致性模型的执行方式。因此线程内部的执行方式必须满足先发生于条件。例如，一个线程的begin事件必须是当前线程的第一个事件，线程的join事件必须是当前线程的最后一个事件。其它对应的读写事件只能发生在begin事件之后，以及join事件之前。

综上，本发明需要设定的程序约束主要包括

步骤4、进行约束求解，即以构建好的约束以文件形式作为本步骤的输入，求解出新的程序调度，随后实现对并发程序进行重复的探索，以确保对被检测并发程序进行完备的探索，实现对程序进行再调度以覆盖尚未被覆盖的内存访问模式，具体实现过程如下：

使用Z3约束求解器求解构建的程序约束，具体包括根据构建的程序事件发生顺序约束，求解出一条可满足约束可线程调度，该线程调度尝试以指定线程切换覆盖尚未被覆盖的内存访问模式，以此来增加并发程序的MAP-coverage。

由于约束求解是比较耗时的，因此将约束求解设置为离线计算可以节省一部分运行时开销。在根据内存访问模式生成约束文件求解的过程中，并不是所有约束文件都能有满足解。因此会出现不可解约束无法生成特定的内存访问模式覆盖调度，而特定内存访问模式又因无法被覆盖重复生成新的不可解约束。为了避免重复求解不可解约束，本发明采用Z3约束求解器的插值技术。当给定的约束文件不可解时，Z3的插值技术可分析得到约束中最小不可解核心(unsat-core)，该核心包含导致该模型不可解的对应最小约束集合。本发明通过记录unsat-core来在约束求解前过滤掉包含已经被求解证明是不可解约束的约束文件，进一步减少约束求解的时间开销。

步骤5、调度执行：新的线程调度之后需要对测试用例进行再调度，以探索新的线程调度是否能覆盖新的内存访问模式以及触发并发错误。传统线程调度方法通过注入延迟函数或注解尝试控制程序的执行，然而此类方法一方面对不同程序的适配性很差，另一方面调度的准确性也很低。本发明通过字节码插桩将调度代码插入至每个程序调度点，在全局使用调度类对线程进行监听和调度。在控制线程调度中，如何暂停当前线程以及在调度类根据线程调度选择执行线程后继续执行暂停线程是关键。本发明将在运行线程封装成新的线程对象ThreadInfo，并在其中初始化一个许可(permits)为0的信号量。信号量在多线程以及操作系统中有着广泛的应用，Java并发库中的Semaphore可以出色的完成对信号量的控制。信号量可以控制某个资源被被同时访问的次数，许可次数通常需要保持在0与设定最大值之间。使用过程中，通过调用acquire()方法获取一个许可，许可值减1，如果没有许可就等待；通过调用release()方法释放一个许可，许可值加1，此时等待的线程便可获得许可继续执行。本发明的调度需要阻塞当前正在执行的线程等待调度分配执行，因此需要在每个封装的线程对象中初始化一个许可为0的信号量。当程序运行到对应调度点时，调用acquire()方法尝试获取许可，因此许可初始为0，所以当前线程需要被阻塞。当线程被选择调度执行时，调用release()方法释放许可，之前阻塞的线程便可继续执行。通过上述方法，降低了线程调度的成本同时增加了调度的准确性。

如图9所示，为示例Java程序。如图10所示，为并发程序测试用例示意图。通过MAPTest生成的测试用例结合给定的并发程序P，该测试用例的具体流程描述如下：

步骤一：首先使用测试用例自动生成工具生成相关的测试用例如MAPTest：通过静态分析测试类的字节码指令，通过匹配潜在的内存访问模式来构建测试用例。图10展示了一个通过MAPTest生成的测试用例，该测试用例由一个前缀和两条后缀组成。从图中可以看出该测试用例首先在前缀中声明了测试类的实例对象var0，并随机调用其方法改变其状态。在两条后缀中分别调用var0的isAttached和removeAllAppenders方法，该测试用例隐含着并发错误。

步骤二：给定图10中的测试用例，本发明首先随机执行该测试用例以获得一条初始执行轨迹，如图11(a)所示，为了节省篇幅这里只展示两条线程的执行情况，因为前缀中的方法是顺序执行，在运行过程中不考虑其交织情况。在得到初始执行轨迹之后，首先本发明需要匹配其中的内存访问模式。根据表1中的内存访问模式类型可以匹配出9个内存访问模式如图11(b)所示。

步骤三：此时的内存访问模式包含有冗余的内存访问模式，因此需要根据约减规则对其进行进一步约减，例如p1，该内存访问模式满足约减规则中无法生成新的程序状态，因为线程t1在S6处对变量aL读取的值并没有发生任何改变，虽然线程t2中对aL的赋值可以导致后续指令读取不同的值，但这种情况可以被其它内存模式所覆盖。约减后剩下图中蓝色标记的内存访问模式为最终尚未被覆盖且可以触发新程序状态的内存访问模式。随后根据内存访问模式排序规则，本发明将长度为3的内存访问模式设置更高的优先级。

步骤四：在获取当前执行轨迹的所有内存访问模式之后，本发明首先选择优先级最高的内存访问模式并构建覆盖该内存访问模式所需要的约束，在当前的例子中本发明将优先选择p7构建程序约束。根据构建程序约束中的约束，在当前的例子中只需构建Happens-Before约束以及Pattern约束，同时针对线程t1本发明只构建i3对应事件之前的Happens-Before约束，因为PCR的调度是基于前缀的。最终构建的程序约束如公式(1)所示，公式的前两行为线程t1与线程t2的Happens-Before约束，公式的第三行为Pattern约束，随后P根据约束φ生成约束求解文件。

步骤五：在生成约束文件之后，本发明调用Z3约束求解器对其进行求解求解结果并基于求解结果提取出新的线程调度序列。设一个约束的可满足解为：i2

以上所述仅为本发明的较佳实施例，并不用以限制本发明，凡在本发明的精神和原则之内所作的任何修改、等同替换、改进等，均应包含在本发明的保护范围之内。