简述
本文将会介绍 JMCR 中约束求解的算法。
提纲
- 约束求解的定义
- 约束求解的目的
- JMCR 中基本的概念
- JMCR 中约束的实现
本文中的图片和文字参考于源码在 github Readme中提供的论文。本文仅供学习参考使用，如有侵权，请联系删除。
系列文章：
1. JMCR 简介
2. JMCR 字节码插桩（一）
3. JMCR 字节码插桩（二）
4. JMCR 约束求解原理
5. JMCR 线程调度
一、什么是约束求解
约束求解是通过一个已知的程序运行记录（以下简称 trace），生成约束并通过 smt 求解技术得出新的线程可行的调度序列的过程。
二、约束求解的目标
回顾一下在 JMCR 学习笔记 中的内容
如果要测试多线程的程序，我们需要 “多跑几遍”，将程序中所有可能的操作序列复现一遍，看看是否可以触发错误，这样才能保证我们的测试不会漏过每一种可能。随之而来的问题是，如何计算出来所有可能的操作集合序列？对于每一次执行，怎么驱动程序按照制定操作序列进行调度，又如对于多线程程序爆炸性增长的探索空间进行剪枝呢？
首先，为了保证测试的 completeness ，要覆盖程序过程中每一个可能的状态。其次，由于多线程程序的测试具有随着测试规模增长而爆炸性增长的趋势，对于不合法的和冗余的测试样例在约束阶段就删除掉，提高测试程序的运行效率
三、一些基本的概念
- trace：程序调度序列，由一系列 event 组成。
- event：多线程程序中发生的事件，包括：
- begin(t)/end(t)：线程 t 中的第一个/最后一个事件
- read(t, x, v)/write(t, x, v)：线程 t 读到/写变量 x 值为 v
- lock(t, l)/unlock(t, l)：线程 t 获取/释放锁 l
- fork(t, t')：线程 t 创建新线程 t'
- join(t, t')：线程 t 阻塞直到 t' 运行结束
运行程序，通过之前提到过的字节码插装技术，我们可以获取到整个测试程序中的变量、线程以及trace 信息。
四、约束
程序中每一行都是一个 event，我们对其进行了标号，在本小节将对以下程序增加约束来产生新的调度序列
（一）保证生成合法的调度序列
合法在这里有三个部分：读一致性、锁互斥以及 Must Happens-Before 原则。
- 读一致性
A read event contains the value written
by the most recent write event on the same memory location.
指的是每一个 read(t, x, v0) 事件和之前距离其最近的 write(t, x, v1) 事件，v0 = v1。
2.锁互斥原则
Each release event is preceded by an acquire event on the same lock by the same thread, and each pair is not interleaved by any other acquire or release event on the same lock
每个 unlock(t, l) 事件之前都应该有一个 lock(t, l) 事件，且两个不同线程对于同一个锁 l 的 lock unlock 对之间不能有交错的时间序列。
- Must Happens-Before 原则
A begin event can happen only as a first event in a thread and only after the thread is forked by another thread. An end event can happen only as the last event in a thread, and a join event can happen only after the end event of the joined thread.
begin 事件只能作为线程中的第一个事件发生，并且只能在该线程被另一个线程 fork 之后发生。 end 事件只能作为线程中的最后一个事件发生，而 join 事件只能在被 join 线程的 end 事件之后发生。
线程内串行
对于线程内的事件顺序，序号为n的事件一定 happens-before 于序号 n+1 的事件。线程间的顺序以及 happens-before 传递性
这里借用了 Lamport 算法思想：因为begin 事件只能在该线程被另一个线程 fork 之后发生。所以 fork 是因，begin是果。而 end 事件只能在被 join 线程的 end 事件之后发生，所以 end 是因，join 是果。而每个线程内的事件可以把前一个事件作为因，后面的是果， 这样一来，我们可以参照分布式系统因果一致性，来对于程序的线程之间的通信（fork、start、end、join）进行建模。而因果关系是具有传递性的，同样的happens-before 也具有传递性。
（二）程序状态模型
来给程序执行的过程建立一个模型：
- 程序状态：
程序的状态是由当前的所有线程的局部变量和所有线程的共享的全局变量的集合。特别的，每个线程的 pc 计数器也是局部变量的一部分。 -
程序执行：
程序执行的过程就是程序从初始状态经过一系列的事件，也就是 trace，程序的状态状态不断地变化的一个过程。
程序执行模型
当一个事件的操作对象是局部变量的时候，取决于当前程序的状态，事件所在线程的局部变量到达了一个新的状态，而不会改变全局变量；而当一个时间的操作对象是全局变量 s 的时候，取决于当前程序的状态，s 和事件所在线程的局部状态会发生改变。
（三） Race 约束
基于之前的程序状
态模型和之前提出的程序合法性。
不同的程序状态会导致程序中某些直接判断语句if 和间接判断 (例如全局变量 x 作为数组的下标) 产生不一样的新的程序状态。所以，我们的目标就是探究所有可能的程序状态序列。提出了 Race 约束
定义：COP(a,b) 是不同线程中对于同一个全局变量的读-写对。
对于每一个存在 COP 的变量，对于该变量的每一个读事件R，定义以下约束：
- 所有 happens-before 于
R的读事件读到和之前一样的值 - 读事件
R读到和之前不一样的值。
以下面这个程序为例
图中的每一个线程中的代码都会循环两次执行，给出了事件的编号，以及事件在 trace 中的表示方法，其中 中上标
表示的是第几次循环，而下标
给出的是在图中的行号(1-14)。
假设我们第一次运行中读写的状态如图：
这个图的含义为：第一个黑点表示 T2 线程中第八行第一次循环
if(x>0) 读到的值是 T2 线程第一次循环第六行写 x = 0 的值。第二个黑点表示T2 线程第二次循环中第八行 if(x>0) 读到的值是 T2 线程第二次循环第六行写 x = 0 的值。后面两个黑点表示 T3 线程第一次循环和第二次循环中第十一行 if(x>1) 都是读到的T2 线程第二次循环第六行写 x = 0 的值。同时，由于两次 T3 中 if(x>1) 的判断结
果都是false，因此没有对于 y 的读时间，y 的读写表为空。
接下来对于，添加 Race 约束，使
读到一个与之前不同的值 1。并保证所有 happens-before 于这个事件的读事件（此处为空集合）都可以读到。运行的程序可得到以下的读写表。
不断读到一个新值，可以获得一颗树。
这颗树便覆盖了程序中所有可能的程序状态。
（四）示例的约束求解：
- 锁互斥
- Must Happens-Before 与线程内串行
- Race 约束（满足其中之一即可）
使第八行的读到 0
或
使第十行的读到 0
通过这一系列约束，我们可以通过 z3 来进行求解，得到新的事件顺序（这里满足了 Race 约束中的第二个）：
转换到线程，我们也得到了一个调度序列前缀：
