动态数据竞争验证和检测方法

之前提到的动态数据竞争验证方法尽管相比RaceFuzzer提高了验证的效率，但是仍然存在一个比较致命的问题就是执行程序一次只能够验证很少的一部分数据竞争。



图(a)中存在两个数据竞争[S1,S3]和[S2,S4]，S1在S2之前执行，S3在S4之前执行，因此如果对这两个数据竞争进行验证，那么都能够被验证成为数据竞争。

图(b)中同样也是存在两个数据竞争[S1,S4]和[S2,S3]，S1在S2之前执行，S3在S4之前执行，因此这两个数据竞争之间存在相互干扰。当线程T1阻塞并被中止在S1时，线程T2也会被阻塞中止在S3。此时就必须随机唤醒其中一个线程，如果T1被唤醒继续执行，那么最终只有[S2,S3]会被验证成功，[S1,S4]就被遗漏了；如果T2被唤醒继续执行，那么最终只有[S1,S4]会被验证成功，[S2,S3]就被遗漏了。

图(c)中存在两个数据竞争[S1,S2]和[S1,S3]，S2在S3之前执行，这两个数据竞争有相同的一个竞争语句，因此也存在相互干扰。当[S1,S2]被验证为数据竞争之后，如果随机选择线程T1继续执行，那么最终[S1,S3]就会被遗漏。

事实上，程序中存在的数据竞争绝大部分都是相互干扰的，有些是类似于上图中简单的干扰，有些则是依赖于输入或是控制条件存在的比较复杂的干扰。如果仅仅使用前面提到的动态数据竞争验证方法那么就会有大量的漏报。

为了能够找到在验证过程中遗漏的数据竞争，我们提出了一种简单的动态数据竞争验证和检测方法。该方法的核心就是在动态数据竞争验证之后，利用比较精确地动态数据竞争检测方法找到被遗漏的数据竞争。



我们可以完全在之前提出的动态数据竞争验证的方法框架上加入动态数据竞争检测，根据前面的文章对于动态数据竞争检测方法进行的实验分析，我们选择ML作为动态数据竞争检测方法。这样的话，如果在验证过程中被遗漏的数据竞争，就会通过ML进行数据竞争检测。ML作为比较精确地动态数据竞争检测器，因此基本不会遗漏数据竞争。

本质上，动态数据竞争验证和检测方法是利用动态数据竞争验证来改变线程调度触发一些隐藏的数据竞争条件，验证一部分数据竞争，而对于不能验证的数据竞争或是遗漏的数据竞争，则交给动态数据竞争检测来分析。

后序文章将会介绍动态数据竞争验证和检测并行化的方法。