通过细粒度透镜的动态数据竞争检测
Dynamic Data-Race Detection through the Fine-Grained Lens
摘要：
数据竞争是并发中最常见的错误之一。数据竞争检测的标准方法是通过动态分析，它在并发程序的执行上工作，而不是程序源代码。关于该主题的丰富文献已经创建了动态数据竞争的各种概念，已知当某些参数（例如，线程数）很小。然而，所有这些种族概念的\emph{fine-grained}复杂性仍然难以捉摸，使得不可能描述它们在精度和效率之间的权衡。在这项工作中，我们建立了几个细粒度的分离之间的许多流行的概念的动态数据竞争。输入是包含$N$事件、$T$线程和$L$锁的执行跟踪。我们的主要结果如下。首先，我们证明了在$O(N\cdot \min(T, L))$时间内可以检测到之前发生的（HB）种族，当$L=o(T)$结合时，其优于标准$O(N\cdot T)$。此外，我们表明，即使报告HB比赛，涉及读访问是很难为2-正交向量（2-OV）。这是第一次严格证明了检测HB竞赛的二次下界。其次，我们表明，最近推出的同步保持种族是很难检测到OV-3，因此有一个立方下界，当$T=Ω(N)$。这建立了一个复杂性分离HB种族是已知的表达较少。第三，我们表明，锁覆盖比赛是很难的2-OV，因此有一个二次下界，即使当$T=2$和$L = ω(\log N)$。锁集竞争的类似概念已知在$O(N\cdot L)$时间内是可检测的，因此我们实现了两者之间的复杂度分离。此外，我们表明，锁集种族成为击中集（HS）硬时，$L=Θ(N)$，因此也有一个二次下界，当输入是足够复杂的。
英文摘要：
Data races are among the most common bugs in concurrency. The standard approach to data-race detection is via dynamic analyses, which work over executions of concurrent programs, instead of the program source code. The rich literature on the topic has created various notions of dynamic data races, which are known to be detected efficiently when certain parameters (e.g., number of threads) are small. However, the \emph{fine-grained} complexity of all these notions of races has remained elusive, making it impossible to characterize their trade-offs between precision and efficiency. In this work we establish several fine-grained separations between many popular notions of dynamic data races. The input is an execution trace with $N$ events, $T$ threads and $L$ locks. Our main results are as follows. First, we show that happens-before (HB) races can be detected in $O(N\cdot \min(T, L))$ time, improving over the standard $O(N\cdot T)$ bound when $L=o(T)$. Moreover, we show that even reporting an HB race that involves a read access is hard for 2-orthogonal vectors (2-OV). This is the first rigorous proof of the conjectured quadratic lower-bound in detecting HB races. Second, we show that the recently introduced synchronization-preserving races are hard to detect for OV-3 and thus have a cubic lower bound, when $T=Ω(N)$. This establishes a complexity separation from HB races which are known to be less expressive. Third, we show that lock-cover races are hard for 2-OV, and thus have a quadratic lower-bound, even when $T=2$ and $L = ω(\log N)$. The similar notion of lock-set races is known to be detectable in $O(N\cdot L)$ time, and thus we achieve a complexity separation between the two. Moreover, we show that lock-set races become hitting-set (HS)-hard when $L=Θ(N)$, and thus also have a quadratic lower bound, when the input is sufficiently complex.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
