Optimistic Prediction of Synchronization-Reversal Data Races

TL;DR

This work addresses the challenge of predicting data races under nondeterministic thread scheduling by introducing OSR, an optimistic synchronization-reversal race detector. OSR computes the smallest optimistic lock-closed set $\mathsf{OLClosure}(e_1,e_2)$, uses an abstract optimistic reordering graph to test acyclicity, and achieves a quadratic-time algorithm $\widetilde{O}(\mathcal{N}^2)$ that is optimal under the Strong Exponential Time Hypothesis. Empirically, OSR reports more races than prior predictors on a large suite of Java and C/C++ benchmarks, while maintaining scalable performance comparable to linear-time methods. By expanding predictive race detection beyond synchronization-preserving reorderings, OSR enhances practical reliability for concurrent software systems and lays groundwork for broader optimistic analyses of synchronization reversals.

Abstract

Dynamic data race detection has emerged as a key technique for ensuring reliability of concurrent software in practice. However, dynamic approaches can often miss data races owing to nondeterminism in the thread scheduler. Predictive race detection techniques cater to this shortcoming by inferring alternate executions that may expose data races without re-executing the underlying program. More formally, the dynamic data race prediction problem asks, given a trace σof an execution of a concurrent program, can σbe correctly reordered to expose a data race? Existing state-of-the art techniques for data race prediction either do not scale to executions arising from real world concurrent software, or only expose a limited class of data races, such as those that can be exposed without reversing the order of synchronization operations. In general, exposing data races by reasoning about synchronization reversals is an intractable problem. In this work, we identify a class of data races, called Optimistic Sync(hronization)-Reversal races that can be detected in a tractable manner and often include non-trivial data races that cannot be exposed by prior tractable techniques. We also propose a sound algorithm OSR for detecting all optimistic sync-reversal data races in overall quadratic time, and show that the algorithm is optimal by establishing a matching lower bound. Our experiments demonstrate the effectiveness of OSR on our extensive suite of benchmarks, OSR reports the largest number of data races, and scales well to large execution traces.

Figures (8)

• Figure 1: The two conflicting events $e_1 = \langle t_1, \mathsf{w}(x) \rangle$ and $e_{12} = \langle t_4, \mathsf{w}(x) \rangle$ is a predictable data race of $\sigma_1$ which is also an optimistic sync-reversal race, witnessed by the correct reordering$\rho_1$ that reverses critical sections.
• Figure 2: The two write events $e_1 = \langle t_1, \mathsf{w}(x) \rangle$ and $e_5 = \langle t_2, \mathsf{w}(x) \rangle$ in $\sigma_2$ are conflicting. $(e_1, e_5)$ is not a data race but a predictable data race of $\sigma_2$, witnessed by correct reorderings $\rho_2$ and $\rho'_2$.
• Figure 3: Two traces containing two predictable races. One of them (a) can be detected by SyncP, but not M2 nor OSR. (b) is the witness of race in (a). The other one (c) can be detected by M2, but not SyncP nor OSR. Trace in (c) is directly cited from M2 paper m2 without modification. (d) is the witness of race in (c).
• Figure 4: Optimistic and abstract optimistic reordering graphs of $\sigma_1$ from Figure \ref{['fig:ssp-race-trace']} are acyclic
• Figure 5: In $\sigma_3$, $(e_4, e_9)$ is not a predictable race. The optimistic reordering graph and the abstract optimistic reordering graph are cyclic.

Theorems & Definitions (21)

• Example 1
• Example 2
• Example 3
• Example 4
• Theorem 3.1
• Definition 1: Optimistic Sync-Reversal Race
• Example 5
• Example 6
• Example 7
• Example 8