动态数据竞争验证方法（一）

动态数据竞争检测算法可以在不知道程序中是否存在数据竞争前提下执行，而动态数据竞争验证方法则是在知道程序中可能存在的数据竞争前提下，对这部分可疑的数据竞争进行验证，看这些数据竞争是否真的发生，同时也可以验证这些数据竞争是否对程序造成有害的影响。

Reference http://web2.cs.columbia.edu/~junfeng/09fa-e6998/papers/racefuzz.pdf 这篇文章提出的RaceFuzzer采取随机调度的方式来验证数据竞争是否是有害的，主要分为如下几个阶段：

Phase1 首先利用hybrid的动态数据竞争检测方法找到程序中所有的数据竞争，这些数据竞争将会构成一个数据竞争语句对集合。之前的文章已经分析很多hybrid的动态数据竞争检测方法，这里就不再重复。

Phase2 根据Phase1中得到的数据竞争语句对，在动态的时候调度线程尽量让这些数据竞争语句对能够临时地相遇（同时发生）。相关的算法如下所示，为了方便描述，这里给出相关的一些定义： • s：程序在执行过程中的状态 • Enabled(s)：当前状态s下可用的线程集合，线程不可用表明当先线程阻塞在一些同步操作上 • Alive(s)：当前状态s下还没有结束的线程集合 • Execute(s,t)：返回线程t在当前状态s下执行语句之后的状态 • NextStmt(s,t)：返回线程t在当前状态s下即将要执行的语句

首先输入RaceSet为Phase1中的竞争语句对集合，并且程序当前状态为s为初始状态s0。其中postponed集合用来保存认为干预中止的线程，初始的时候同样是空集。

从while循环也可以发现，只要当前有可用的线程，那么就会一直执行下去。否则的话，一旦当前状态存在没有结束的线程就表明程序陷入了死锁(L30)。

该算法调度线程的核心就是每次只让一个线程执行，并且是随机的挑选可用的线程(L5)。

当被选择的线程即将执行的语句在RaceSet中，也就是数据竞争语句。 • 如果此时postponed中存在其他的线程即将访问的操作和当前线程t即将访问的操作构成数据竞争，那么此时机会随机是否当当前的线程继续执行还是让postponed中的线程继续执行（如果有多个阻塞的线程那么会让所有参与数据竞争的被阻塞的线程都继续执行）。 • 否则的话，当前线程就会被阻塞中止执行。 下图展示的是一个数据竞争的例子：

其中存在两个数据竞争[5,7]和[1,10]。对于数据竞争[1,10]来说，如果线程1先到达1，那么此时会被阻塞等待线程2到达10，线程1被加入到postponed中，但是由于y初始为0，因此线程2会一直执行到结束，此时线程1就会从postponed中被移除。对于数据竞争[5,7]来说，如果线程1先到达5，此时就会被阻塞，当线程到达7时，此时就会被验证为一个数据竞争。而一旦随机挑选线程1继续执行，那么此时就会执行6导致程序出现错误，此时，数据竞争[5,7]就是一个有害的数据竞争。

上述数据竞争验证方法每次只能够允许一个线程执行，使得数据竞争验证较慢。并且由于其使用确定性阻塞来中止线程的执行，因此可能会引入新的死锁。同时该方法每次执行程序能够验证的数据竞争很少。