University of Illinois at Urbana-Champaign<EMAIL_ADDRESS>of Illinois at Urbana-Champaign,
USAumathur3@illinois.eduhttps://orcid.org/0000-0002-7610-0660Umang Mathur was
partially funded by a Google PhD Fellowship and by the Simons Institute for
the Theory of Computing Aarhus University<EMAIL_ADDRESS>Rucha
Kulkarni and Umang Mathur and Andreas Pavlogiannis [500]Software and its
engineering Software testing and debugging [500]Theory of computation
Parameterized complexity and exact algorithms John Q. Open and Joan R. Access
2 42nd Conference on Very Important Topics (CVIT 2016) CVIT 2016 CVIT 2016
December 24–27, 2016 Little Whinging, United Kingdom 42 23

# Dynamic Data-Race Detection through the Fine-Grained Lens

Rucha Kulkarni  Umang Mathur  Andreas Pavlogiannis

###### Abstract

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 _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
$\sigma$ with $\mathcal{N}$ events, $\mathcal{T}$ threads and $\mathcal{L}$
locks. Our main results are as follows. First, we show that _happens-before
(HB) races_ can be detected in
$O(\mathcal{N}\cdot\min(\mathcal{T},\mathcal{L}))$ time, improving over the
standard $O(\mathcal{N}\cdot\mathcal{T})$ bound when
$\mathcal{L}=o(\mathcal{T})$. Moreover, we show that even reporting an
$\operatorname{\textsf{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
$\mathcal{T}=\Omega(\mathcal{N})$. This establishes a complexity separation
from $\operatorname{\textsf{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 $\mathcal{T}=2$ and
$\mathcal{L}=\omega(\log\mathcal{N})$. The similar notion of _lock-set races_
is known to be detectable in $O(\mathcal{N}\cdot\mathcal{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
$\mathcal{L}=\Theta(\mathcal{N})$, and thus also have a quadratic lower bound,
when the input is sufficiently complex. To our knowledge, this is the first
work that characterizes the complexity of well-established dynamic race-
detection techniques, allowing for a rigorous comparison between them.

###### keywords:

dynamic analyses, data races, fine-grained complexity

###### category:

##  1 Introduction

Concurrent programs that communicate over shared memory are prone to _data
races_. Two events are _conflicting_ if they access the same memory location
and one (at least) modifies that location. Data races occur when conflicting
access happen concurrently between different threads, and form one of the most
common bugs in concurrency. In particular, data races are often symptomatic of
bugs in software like data corruption [5, 20, 26], and they have been deemed
_pure evil_ [6] due to the problems they have caused in the past [43].
Moreover, many compiler optimizations are unsound in the presence of data
races [36, 40], while data-race freeness is often a requirement for assigning
well-defined semantics to programs [7].

The importance of data races in concurrency has led to a multitude of
techniques for detecting them efficiently [4, 39]. By far the most standard
approach is via _dynamic analyses_. Instead of analyzing the full program,
dynamic analyzers try to _predict_ the existence of data races by observing
and analyzing concurrent executions [37, 21, 28]. As full dynamic data race
prediction is NP-hard in general [24], researchers have developed several
approximate notions of dynamic races, accompanied by efficient techniques for
detecting each notion.

Happens-before races. The most common technique for detecting data races
dynamically is based on Lamport’s _happens-before (
$\operatorname{\textsf{HB}}$)_ partial order [22]. Two conflicting events form
an $\operatorname{\textsf{HB}}$ race if they are unordered by
$\operatorname{\textsf{HB}}$, as the lack of ordering between them indicates
the fact that they may execute concurrently, thereby forming a data race. The
standard approach to $\operatorname{\textsf{HB}}$ race detection is via the
use of vector clocks [19], and has seen wide success in commercial race
detectors [35]. As vector clock computation is known to require
$\Theta(\mathcal{N}\cdot\mathcal{T})$ time on traces of $\mathcal{N}$ events
and $\mathcal{T}$ threads [10], $\operatorname{\textsf{HB}}$ race detection is
often assumed to suffer the same bound, and has thus been a subject of further
practical optimizations [29, 16].

Synchronization preserving races. HB races were recently generalized to
sync(hronization)-preserving races [25]. Intuitively, two conflicting events
are in a sync-preserving race if the observed trace can be soundly reordered
to a witness trace in which the two events are concurrent, but without
reordering synchronization events (e.g., locking events). Similar to HB races,
sync-preserving races can be detected in linear time when the number of
threads is constant. However, the dependence on the number of threads is cubic
for sync-preserving races, as opposed to the linear dependence for HB races.
On the other hand, sync-preserving races are known to offer better precision
in program analysis.

Races based on the locking discipline. The locking discipline dictates that
threads that access a common memory location must do so inside _critical
sections_ , using a common lock, when performing the access [39]. Although
this discipline is typically not enforced, it is considered good practice, and
hence instances that violate this principle are often considered indicators of
erroneous behavior. For this reason, there have been two popular notions of
data races based on the locking discipline, namely _lock-cover races_ [14] and
_lock-set races_ [33]. Both notions are detectable in linear time when the
number of locks is constant, however, lock-set race detection is typically
faster in practice, which also comes at the cost of being less precise.

Observe that, although techniques for all aforementioned notions of races are
generally thought to operate in linear time, they only do so assuming certain
parameters, such as the number of threads, are constant. However, as these
techniques are deployed in runtime, often with extremely long execution
traces, they have to be as efficient as absolutely possible, often in
scenarios when these parameters are very large. When a data-race detection
technique is too slow for a given application, the developers face a dilemma:
do they look for a faster algorithm, or for a simpler abstraction (i.e., a
different notion of dynamic races)? For these reasons, it is important to
understand the _fine-grained_ complexity of the problem at hand with respect
to such parameters. Fine-grained lower bounds can rule out the possibility of
faster algorithms, and thus help the developers focus on new abstractions that
are more tractable for the given application. Motivated by such questions, in
this work we settle the fine-grained complexity of dynamically detecting
several popular notions of data races.

###  1.1 Our Contributions

Here we give a full account of the main results of this work, while we refer
to later sections for precise definitions and proofs. We also refer to
Appendix A for relevant notions in fine-grained complexity and popular
hypotheses. The input is always a concurrent trace $\sigma$ of length
$\mathcal{N}$, consisting of $\mathcal{T}$ threads, $\mathcal{L}$ locks, and
$\mathcal{V}$ variables.

#### Happens-before races.

We first study the fine-grained complexity of $\operatorname{\textsf{HB}}$
races, as they form the most popular class of dynamic data races. The task of
most techniques is to report all events in $\sigma$ that participate in an
$\operatorname{\textsf{HB}}$ race, which is known to take
$O(\mathcal{N}\cdot\mathcal{T})$ time [19]. Note that the bound is quadratic
when $\mathcal{T}=\Theta(\mathcal{N})$, and multiple heuristics have been
developed to address it in practice (see e.g., [16]). Our first result shows
that polynomial improvements below this quadratic bound are unlikely.

######  Theorem 1.1.

For any $\epsilon>0$, there is no algorithm that detects even a single
$\operatorname{\textsf{HB}}$ race that involves a read in time
$O(\mathcal{N}^{2-\epsilon})$, unless the OV hypothesis fails.

Orthogonal vectors (OV) is a well-studied problem with a long-standing
quadratic worst-case upper bound. The associated hypothesis states that there
is no sub-quadratic algorithm for the problem [42]. It is also known that the
strong exponential time hypothesis (SETH) implies the Orthogonal Vectors
hypothesis [41]. Thus, under the OV hypothesis, Theorem 1.1 establishes a
quadratic lower bound for $\operatorname{\textsf{HB}}$ race detection.

Note that the hardness of Theorem 1.1 arises out of the requirement to detect
$\operatorname{\textsf{HB}}$ races that involve a read. A natural follow-up
question is whether detecting if the input contains _any_
$\operatorname{\textsf{HB}}$ race (i.e., not necessarily involving a read) has
a similar lower bound based on SETH. Our next theorem shows that under the
non-deterministic SETH (NSETH) [9], there is no fine-grained reduction from
SETH that proves any lower bound for this problem above $\mathcal{N}^{3/2}$.

######  Theorem 1.2.

For any $\epsilon>0$, there is no
$(2^{\mathcal{N}},\mathcal{N}^{3/2+\epsilon})$-fine-grained reduction from SAT
to the problem of detecting any $\operatorname{\textsf{HB}}$ race with bound,
unless NSETH fails.

Given the impossibility of Theorem 1.2, it would be desirable to at least show
a super-linear lower bound for detecting any $\operatorname{\textsf{HB}}$ data
race. To tackle this question, we show that detecting any
$\operatorname{\textsf{HB}}$ race is hard for the general problem of model
checking first-order formulas quantified by $\forall\exists\exists$ on
structures of size $n$ with $m$ relational tuples (denoted
FO($\mathsf{\forall\exists\exists}$)).

######  Theorem 1.3.

For any $\epsilon>0$, if there is an algorithm for detecting any
$\operatorname{\textsf{HB}}$ race in time $O(\mathcal{N}^{1+\epsilon})$, then
there is an algorithm for FO($\mathsf{\forall\exists\exists}$) formulas in
time $O(m^{1+\epsilon})$.

It is known that FO($\mathsf{\forall\exists\exists}$) can be solved in
$O(m^{3/2})$ time [17], which yields a bound $O(n^{3})$ for dense structures
(i.e., when $m=\Theta(n^{2})$). Theorem 1.3 implies that if $m^{3/2}$ is the
best possible bound for FO($\mathsf{\forall\exists\exists}$), then detecting
any $\operatorname{\textsf{HB}}$ race cannot take
$O(\mathcal{N}^{1+\epsilon})$ time for any $\epsilon<1/2$. Although
improvements for FO($\mathsf{\forall\exists\exists}$) over the current
$O(m^{3/2})$ bound might be possible, we find that a truly linear bound $O(m)$
would require major breakthroughs 111Even the well-studied problem of testing
triangle freeness, which is a special case of the similarly flavored
FO($\mathsf{\exists\exists\exists}$), has the super-linear bound
$O(n^{\omega})$.. Under this hypothesis, Theorem 1.3 implies a super-linear
bound for $\operatorname{\textsf{HB}}$ races.

Finally, we give an improved upper bound for this problem when
$\mathcal{L}=o(\mathcal{T})$.

######  Theorem 1.4.

Deciding whether $\sigma$ has an $\operatorname{\textsf{HB}}$ race can be done
in time $O(\mathcal{N}\cdot\min(\mathcal{T},\mathcal{L}))$.

In fact, similar to existing techniques [16], the algorithm behind Theorem 1.4
detects _all_ variables that participate in an $\operatorname{\textsf{HB}}$
race (instead of just reporting $\sigma$ as racy).

#### Synchronization-preserving races.

Next, we turn our attention to the recently introduced sync-preserving races
[24]. It is known that detecting sync-preserving races takes
$O(\mathcal{N}\cdot\mathcal{V}\cdot\mathcal{T}^{3})$ time. As sync-preserving
races are known to be more expressive than $\operatorname{\textsf{HB}}$ races,
the natural question is whether sync-preserving races can be detected more
efficiently, e.g., by an algorithm that achieves a bound similar to Theorem
1.4 for $\operatorname{\textsf{HB}}$ races. Our next theorem answers this
question in negative.

######  Theorem 1.5.

For any $\epsilon>0$, there is no algorithm that detects even a single sync-
preserving race in time $O(\mathcal{N}^{3-\epsilon})$, unless the 3-OV
hypothesis fails. Moreover, the statement holds even for traces over a single
variable.

As $\operatorname{\textsf{HB}}$ races take at most quadratic time, Theorem 1.5
shows that the increased expressiveness of sync-preserving races incurs a
complexity overhead that is unavoidable in general.

#### Races based on the locking discipline.

We now turn our attention to data races based on the locking discipline,
namely _lock-cover races_ and _lock-set races_. It is known that lock-cover
races are more expressive than lock-set races. On the other hand, existing
algorithms run in $O(\mathcal{N}^{2}\cdot\mathcal{L})$ time for lock-cover
races and in $O(\mathcal{N}\cdot\mathcal{L})$ time for lock-set races, and
thus hint that the former are computationally harder to detect. Our first
theorem makes this separation formal, by showing that even with just two
threads, having slightly more that logarithmically many locks implies a
quadratic hardness for lock-cover races.

######  Theorem 1.6.

For any $\epsilon>0$, any $\mathcal{T}\geq 2$ and any
$\mathcal{L}=\omega(\log\mathcal{N})$, there is no algorithm that detects even
a single lock-cover race in time $O(\mathcal{N}^{2-\epsilon})$, unless the OV
hypothesis fails.

Observe that the $O(\mathcal{N}\cdot\mathcal{L})$ bound for lock-set races
also becomes quadratic, when the number of locks is unbounded (i.e.,
$\mathcal{L}=\Theta(\mathcal{N}))$. Is there a SETH-based quadratic lower
bound similar to Theorem 1.6 for this case? Our next theorem rules out this
possibility, again under NSETH.

######  Theorem 1.7.

For any $\epsilon>0$, there is no
$(2^{\mathcal{N}},\mathcal{N}^{1+\epsilon})$-fine-grained reduction from SAT
to the problem of detecting any lock-set race, unless NSETH fails.

Hence, even though we desire a quadratic lower bound, Theorem 1.7 rules out
any super-linear lower-bound based on SETH. Alas, our next theorem shows that
a quadratic lower bound for lock-set races does exist, based on the hardness
of the hitting set (HS) problem.

######  Theorem 1.8.

For any $\epsilon>0$ and any $\mathcal{T}=\omega(\log n)$, there is no
algorithm that detects even a single lock-set race in time
$O(\mathcal{N}^{2-\epsilon})$, unless the HS hypothesis fails.

Hitting set is a problem similar to OV, but has different quantifier
structure. Just like the OV hypothesis, the HS hypothesis states that there is
no sub-quadratic algorithm for the problem [3]. Although HS implies OV, the
opposite is not known, and thus Theorem 1.8 does not contradict Theorem 1.7.
In conclusion, we have that both lock-cover and lock-set races have
(conditional) quadratic lower bounds, though the latter is based on a stronger
hypothesis (HS), and requires more threads and locks for hardness to arise.

Finally, on our way to Theorem 1.7, we obtain the following theorem.

######  Theorem 1.9.

Deciding whether a trace $\sigma$ has a lock-set race on a variable $x$ can be
performed in $O(\mathcal{N})$ time. Thus, deciding whether $\sigma$ has a
lock-set race can be performed in
$O(\mathcal{N}\cdot\min(\mathcal{L},\mathcal{V}))$ time.

Hence, Theorem 1.9 strengthens the $O(\mathcal{N}\cdot\mathcal{L})$ upper
bound for lock-set races when $\mathcal{V}=o(\mathcal{L})$.

###  1.2 Related Work

#### Dynamic data-race detection.

There exists a rich literature in dynamic techniques for data race detection.
Methods based on vector clocks (Djit algorithm [19]) using Lamport’s Happens
Before ($\operatorname{\textsf{HB}}$) [22] and the lock-set principle in
Eraser [33] were the first ones to popularize dynamic analysis for detecting
data races. Later work attempted to increase the performance of these notions
using optimizations as in [29] and FastTrack [16], altogether different
algorithms (e.g., the GoldiLocks algorithm [15]), and hybrid techniques [27].
$\operatorname{\textsf{HB}}$ and lock-set based race detection are
respectively sound (but incomplete) and complete (but unsound) variants of the
more general problem of data-race _prediction_ [34]. While earlier work on
data race prediction focused on explicit [34] or symbolic [31, 32]
enumeration, recent efforts have focused on scalability [37, 23, 21, 28, 30,
38]. The more recent notion [25] of sync-preserving races generalizes the
notion of $\operatorname{\textsf{HB}}$. As the complexity of race prediction
is prohibitive (NP-hard in general [24]), this work characterizes the fine-
grained complexity of popular, more relaxed notions of dynamic races that take
polynomial time.

#### Fine-grained complexity.

Traditional complexity theory usually shows a problem is intractable by
proving it NP-hard, and tractable by showing it is in P. For algorithms with
large input sizes, this distinction may be too coarse. It becomes important to
understand, even for problems in P, whether algorithms with smaller degree
polynomials than the known are possible, or if there are fine-grained lower
bounds making this unlikely. Fine-grained complexity involves proving such
lower bounds, by showing relationships between problems in $\textsf{P},$ with
an emphasis on the degree of the complexity polynomial, and is nowadays a
field of very active study. We refer to [8] for an introductory, and to [42]
for a more extensive exposition on the topic. Fine-grained arguments have also
been instrumental in characterizing the complexity of various problems in
concurrency, such as bounded context-switching [11], safety verification [12],
data-race prediction [24] and consistency checking [13].

##  2 Preliminaries

###  2.1 Concurrent Program Executions and Data Races

Traces and Events. We consider execution traces (or simply _traces_) generated
by concurrent programs, under the sequential consistency memory model. Under
this memory model, a trace $\sigma$ is a sequence of events. Each event $e$ is
labeled with a tuple $\mathsf{lab}(e)=\langle t,op\rangle$, where $t$ is the
(unique) identifier of the thread that performs the event $e$, and $op$ is the
operation performed in $e$. We will often abuse notation and write $e=\langle
t,op\rangle$ instead of $\mathsf{lab}(e)=\langle t,op\rangle$. For the purpose
of this presentation, an operation can be one of  (a) read ($\texttt{r}(x)$)
from, or write ($\texttt{w}(x)$) to, a shared memory variable $x$,  (b)
$\texttt{acq}(\ell)$or $\texttt{rel}(\ell)$ of a lock $\ell$.

For an event $e=\langle t,op\rangle$, we use $\operatorname{\mathsf{tid}}(e)$
and $\operatorname{op}(e)$ to denote respectively the thread identifier $t$
and the operation $op$. For a trace $\sigma$, we use
$\mathsf{Events}_{\sigma}$ to denote the set of events that appear in
$\sigma$. Similarly, we will use $\mathsf{Threads}_{\sigma}$,
$\mathsf{Locks}_{\sigma}$ and $\mathsf{Vars}_{\sigma}$ to denote respectively
the set of threads, locks and shared variables that appear in trace $\sigma$.
We denote by $\mathcal{N}=|\mathsf{Events}_{\sigma}|$,
$\mathcal{T}=|\mathsf{Threads}_{\sigma}|$,
$\mathcal{L}=|\mathsf{Locks}_{\sigma}|$, and
$\mathcal{V}=|\mathsf{Vars}_{\sigma}|$. The set of read events and write
events on variable $x\in\mathsf{Vars}_{\sigma}$ will be denoted by
$\mathsf{Reads}_{\sigma}(x)$ and $\mathsf{Writes}_{\sigma}(x)$, and further we
let
$\mathsf{Accesses}_{\sigma}(x)=\mathsf{Reads}_{\sigma}(x)\cup\mathsf{Writes}_{\sigma}(x)$.
Similarly, we let $\mathsf{Acquires}_{\sigma}(\ell)$ and
$\mathsf{Releases}_{\sigma}(\ell)$ denote the set of lock-acquire and lock-
release events, respectively, of $\sigma$ on lock $\ell$. The _trace order_ of
$\sigma$, denoted $\leq^{\sigma}_{\mathsf{\operatorname{\textsf{tr}}}}$, is
the total order on $\mathsf{Events}_{\sigma}$ induced by the sequence
$\sigma$. Finally, the _thread-order_ of $\sigma$, denoted
$\leq^{\sigma}_{\mathsf{\operatorname{\textsf{TO}}}}$ is the smallest partial
order on $\mathsf{Events}_{\sigma}$ such that for any two events
$e_{1},e_{2}\in\mathsf{Events}_{\sigma}$, if
$e_{1}\leq^{\sigma}_{\mathsf{\operatorname{\textsf{tr}}}}e_{2}$ and
$\operatorname{\mathsf{tid}}(e_{1})=\operatorname{\mathsf{tid}}(e_{2})$, then
$e_{1}\leq^{\sigma}_{\mathsf{\operatorname{\textsf{TO}}}}e_{2}$.

Traces are assumed to be well-formed in that critical sections on the same
lock do not overlap. For a lock $\ell\in\mathsf{Locks}_{\sigma}$, let
$\sigma|_{\ell}$ be the projection of the trace $\sigma$ on the set of events
$\\{e\,|\,\operatorname{op}(e)\in\\{\texttt{acq}(\ell),\texttt{rel}(\ell)\\}\\}$.
Also, let $t_{1},\ldots t_{k}$ be the thread identifiers in
$\mathsf{Threads}_{\sigma}$. Well-formedness then entails that for each lock
$\ell$, the projection $\sigma|_{\ell}$ is a prefix of some string in the
language of the grammar with production rules $S\rightarrow\varepsilon|S\cdot
S_{t_{1}}|S\cdot S_{t_{2}}|\cdots|S\cdot S_{t_{k}}$ and
$S_{t_{i}}\rightarrow\langle t_{i},\texttt{acq}(\ell)\rangle\cdot\langle
t_{i},\texttt{rel}(\ell)\rangle$ and start symbol $S$. Thus, every release
event $e$ has a unique matching acquire event, which we denote by
$\mathsf{match}_{\sigma}(e)$. Likewise for an acquire event $e$,
$\mathsf{match}_{\sigma}(e)$ denotes the unique matching release event if one
exists. For an acquire event $e$, the critical section of $e$ is the set of
events if $\mathsf{match}_{\sigma}(e)$ exists, and otherwise.

Data Races. Two events $e_{1},e_{2}\in\mathsf{Events}_{\sigma}$ are said to be
_conflicting_ if they are performed by different threads, they are access
events touching the same memory location, and at least one of them is a write
access. Formally, we have (i)
$\operatorname{\mathsf{tid}}(e_{1})\neq\operatorname{\mathsf{tid}}(e_{2})$,
(ii) $e_{1},e_{2}\in\mathsf{Accesses}_{\sigma}(x)$ for some
$x\in\mathsf{Vars}_{\sigma}$, and (iii)
$\\{e_{1},e_{2}\\}\cap\mathsf{Writes}_{\sigma}(x)\neq\varnothing$. An event
$e\in\mathsf{Events}_{\sigma}$ is said to be enabled in a prefix $\rho$ of
$\sigma$, if for every event $e^{\prime}\neq e$ with
$e^{\prime}\leq^{\sigma}_{\mathsf{\operatorname{\textsf{TO}}}}e$, we have
$e^{\prime}\in\mathsf{Events}_{\rho}$. A data race in $\sigma$ is a pair of
conflicting events $(e_{1},e_{2})$ such that there is a prefix $\rho$ in which
both $e_{1}$ and $e_{2}$ are simultaneously enabled. Depending on the type of
access of $e_{1}$ and $e_{2}$, we often distinguish between write-write races
and write-read races.

###  2.2 Notions of Dynamic Data Races

As the problem of determining whether a concurrent program has an execution
with a data race is undecidable, dynamic techniques observe program traces and
report whether certain events indicate the presence of a race. Depending on
the technique, such reports can be sound (i.e., they guarantee the presence of
a race in the program), Here we describe in detail some popular approaches to
dynamic race detection that are the subject of this work.

#### Happens-Before Races.

Given a trace $\sigma$, the _happens before_ order
$\leq^{\sigma}_{\mathsf{\operatorname{\textsf{HB}}}}$ is the smallest partial
order on $\mathsf{Events}_{\sigma}$ such that  (a)
$\leq^{\sigma}_{\mathsf{\operatorname{\textsf{TO}}}}\subseteq\leq^{\sigma}_{\mathsf{\operatorname{\textsf{HB}}}}$,
and  (b) for any lock $\ell\in\mathsf{Locks}_{\sigma}$ and for events
$e\in\mathsf{Acquires}_{\sigma}(\ell)$ and
$f\in\mathsf{Releases}_{\sigma}(\ell)$, if
$e\leq^{\sigma}_{\mathsf{\operatorname{\textsf{tr}}}}f$ then
$e\leq^{\sigma}_{\mathsf{\operatorname{\textsf{HB}}}}f$.  A pair of
conflicting events $(e_{1},e_{2})$ is an $\operatorname{\textsf{HB}}$-race in
$\sigma$ if they are unordered by $\operatorname{\textsf{HB}}$, i.e.,
$e_{1}\not\leq^{\sigma}_{\mathsf{\operatorname{\textsf{HB}}}}e_{2}$ and
$e_{2}\not\leq^{\sigma}_{\mathsf{\operatorname{\textsf{HB}}}}e_{1}$. The
associated decision question is, _given a trace $\sigma$, determine whether
$\sigma$ has an $\operatorname{\textsf{HB}}$ race_. Typically
$\operatorname{\textsf{HB}}$ race detectors are tasked to report all events
that form $\operatorname{\textsf{HB}}$ race with an earlier event in the trace
[35, 2, 1]). That is, they solve the following function problem:_given a trace
$\sigma$, determine all events $e_{2}\in\mathsf{Events}_{\sigma}$ for which
there exists an event $e_{1}\in\mathsf{Events}_{\sigma}$ such that
$e_{1}\leq^{\sigma}_{\mathsf{\operatorname{\textsf{tr}}}}e_{2}$, and
$(e_{1},e_{2})$ is an $\operatorname{\textsf{HB}}$ race of $\sigma$_. The
standard algorithm for solving both versions of the problem is a vector-clock
algorithm that runs in $O(\mathcal{N}\cdot\mathcal{T})$ time [19].

#### Synchronization Preserving Races.

Next, we present the notion of _sync(hronization)-preserving races_ [24]. For
a trace $\sigma$ and a read event $e$, we use $\mathsf{lw}_{\sigma}(e)$ to
denote the write event observed by $e$. That is,
$e^{\prime}=\mathsf{lw}_{\sigma}(e)$ is the last (according to the trace order
$\leq^{\sigma}_{\mathsf{\operatorname{\textsf{tr}}}}$) write event
$e^{\prime}$ of $\sigma$ such that $e$ and $e^{\prime}$ access the same
variable and $e^{\prime}\leq^{\sigma}_{\mathsf{\operatorname{\textsf{tr}}}}e$;
if no such $e^{\prime}$ exists, then we write $\mathsf{lw}_{\sigma}(e)=\bot$.
A trace $\rho$ is said to be a correct reordering of trace $\sigma$, if  (a)
$\mathsf{Events}_{\rho}\subseteq\mathsf{Events}_{\sigma}$ (b)
$\mathsf{Events}_{\rho}$is downward closed with respect to
$\leq^{\sigma}_{\mathsf{\operatorname{\textsf{TO}}}}$, and further
$\leq^{\rho}_{\mathsf{\operatorname{\textsf{TO}}}}\subseteq\leq^{\sigma}_{\mathsf{\operatorname{\textsf{TO}}}}$,
and  (c) for every read event $e\in\mathsf{Events}_{\rho}$,
$\mathsf{lw}_{\rho}(e)=\mathsf{lw}_{\sigma}(e)$.  We say that $\rho$ is _sync-
preserving_ with respect to $\sigma$ if for every lock $\ell$ and for any two
acquire events $e_{1},e_{2}\in\mathsf{Acquires}_{\rho}(\ell)$, we have
$e_{1}\leq^{\rho}_{\mathsf{\operatorname{\textsf{tr}}}}e_{2}$ iff
$e_{1}\leq^{\sigma}_{\mathsf{\operatorname{\textsf{tr}}}}e_{2}$. That is, the
order of two critical sections on the same lock is the same in $\sigma$ and
$\rho$.

A pair of conflicting events $(e_{1},e_{2})$ is a _sync-preserving race_ in
$\sigma$ if $\sigma$ has a sync-preserving correct reordering $\rho$ such that
$(e_{1},e_{2})$ is a data race of $\rho$. The associated decision question is,
_given a trace $\sigma$, determine whether $\sigma$ has a sync-preserving
race_. As with $\operatorname{\textsf{HB}}$ races, we are typically interested
in reporting all events $e_{2}\in\mathsf{Events}_{\sigma}$ for which there
exists an event $e_{1}\in\mathsf{Events}_{\sigma}$ such that
$e_{1}\leq^{\sigma}_{\mathsf{\operatorname{\textsf{tr}}}}e_{2}$, and
$(e_{1},e_{2})$ is an $\operatorname{\textsf{HB}}$ race of $\sigma$. It is
known one can report all such events $e_{2}$ in time
$O(\mathcal{N}\cdot\mathcal{V}\cdot\mathcal{T}^{3})$.

#### Lock-Cover and Lock-Set Races.

Lock-cover and lock-set races indicate violations of the _locking discipline_.
For an event $e$ in a trace $\sigma$, let
$\mathsf{locksHeld}_{\sigma}(e)=\\{\ell\,|\,\exists
f\in\mathsf{Acquires}_{\sigma}(\ell),\text{ such that }e\in$, i.e.,
$\mathsf{locksHeld}_{\sigma}(e)$ is the set of locks held by thread
$\operatorname{\mathsf{tid}}(e)$ when $e$ is executed. A pair of conflicting
events might indicate a data race if
$\mathsf{locksHeld}_{\sigma}(e_{1})\cap\mathsf{locksHeld}_{\sigma}(e_{2})=\varnothing$.
Although this condition does not guarantee the presence of a race, it
constitutes a violation of the locking discipline and can be further
investigated.

A pair of conflicting events $(e_{1},e_{2})$ is a _lock-cover race_ if
$\mathsf{locksHeld}_{\sigma}(e_{1})\cap\mathsf{locksHeld}_{\sigma}(e_{2})=\varnothing$.
The decision question is, _given a trace $\sigma$, determine if $\sigma$ has a
lock-cover race_. The problem is solvable in
$O(\mathcal{N}^{2}\cdot\mathcal{L})$ time, by checking the above condition
over all conflicting event pairs.

As the algorithm for lock-cover races takes quadratic time, developers often
look for less expensive indications of violations of locking discipline,
called lock-set races (as proposed by Eraser race detector [33]). A trace
$\sigma$ has a _lock-set race_ on variable $x\in\mathsf{Vars}_{\sigma}$ if

  1. (a)

there exists a pair of conflicting events
$(e_{1},e_{2})\in\mathsf{Writes}_{\sigma}(x)\times\mathsf{Accesses}_{\sigma}(x)$,
and

  2. (b)

$\bigcap_{e\in\mathsf{Accesses}_{\sigma}(x)}\mathsf{locksHeld}_{\sigma}(e)=\varnothing$.

The associated decision question is, _given a trace $\sigma$, determine if
$\sigma$ has a lock-set race_. Note that a lock-cover race implies a lock-set
race, but not the other way around. On the other hand, determining whether
$\sigma$ has a lock-set race is easily performed in
$O(\mathcal{N}\cdot\mathcal{L})$ time.

$t_{1}$$t_{2}$$1$$\texttt{acq}(\ell)$
$2$$\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{w}(x)$
$3$$\texttt{rel}(\ell)$
$4$$\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{w}(x)$
$5$$\texttt{acq}(\ell)$ $6$$\texttt{rel}(\ell)$

$t_{1}$$t_{2}$$1$$\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{w}(x)$
$2$$\texttt{acq}(\ell)$ $3$$\texttt{rel}(\ell)$ $4$$\texttt{acq}(\ell)$
$5$$\texttt{rel}(\ell)$
$6$$\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{w}(x)$

$t_{1}$$t_{2}$$1$$\texttt{acq}(\ell)$
$2$$\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{w}(x)$
$3$$\texttt{rel}(\ell)$ $4$$\texttt{acq}(\ell)$ $5$$\texttt{r}(x)$
$6$$\texttt{rel}(\ell)$
$7$$\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{w}(x)$

$t_{1}$$t_{2}$$1$$\texttt{acq}(\ell_{1})$ $2$$\texttt{acq}(\ell_{2})$
$3$$\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{w}(x)$
$4$$\texttt{rel}(\ell_{2})$ $5$$\texttt{rel}(\ell_{1})$
$6$$\texttt{acq}(\ell_{2})$ $7$$\texttt{acq}(\ell_{3})$
$8$$\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{w}(x)$
$9$$\texttt{rel}(\ell_{3})$ $10$$\texttt{rel}(\ell_{2})$
$11$$\texttt{acq}(\ell_{1})$ $12$$\texttt{acq}(\ell_{3})$
$13$$\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\texttt{w}(x)$
$14$$\texttt{rel}(\ell_{3})$ $15$$\texttt{rel}(\ell_{1})$

(a) HB-race

(b) Sync-preserving race

(c) Lock-cover race

(d) Lockset race

Figure 1: Types of data races.

#### Example.

We illustrate the different notions of races in Figure 1. We use $e_{i}$ to
denote the $i^{\text{th}}$ event of the trace in consideration. First consider
the trace $\sigma_{a}$ in Figure 1(a). The events $e_{2}$ and $e_{4}$ are
conflicting and unordered by
$\leq^{\sigma_{a}}_{\mathsf{\operatorname{\textsf{HB}}}}$, thus
$(e_{2},e_{4})$ is an $\operatorname{\textsf{HB}}$-race. Second, in trace
$\sigma_{b}$ of Figure 1(b), the pair $(e_{1},e_{6})$ is not an
$\operatorname{\textsf{HB}}$-race as
$e_{1}\leq^{\sigma_{b}}_{\mathsf{\operatorname{\textsf{HB}}}}e_{6}$. But this
is a sync-preserving race witnessed by the correct reordering $e_{4},e_{5}$,
as both $e_{1}$ and $e_{6}$ are enabled. Third, in trace $\sigma_{c}$ of
Figure 1(c), the pair $(e_{2},e_{7})$ is neither a sync-preserving race nor an
$\operatorname{\textsf{HB}}$ race, but is a lock-cover race as
$\mathsf{locksHeld}_{\sigma_{c}}(e_{2})\cap\mathsf{locksHeld}_{\sigma_{c}}(e_{7})=\varnothing$.
Finally, the trace $\sigma_{d}$ in Figure 1(d) has no
$\operatorname{\textsf{HB}}$, sync-preserving or lock-cover race, as all
$\texttt{w}(x)$ are protected by a common lock. But there is a lock-set race
on $x$ as there is no single lock that protects all $\texttt{w}(x)$.

##  3 Happens-Before Races

In this section we prove the results for detecting
$\operatorname{\textsf{HB}}$ races, i.e., Theorem 1.1 to Theorem 1.4.

###  3.1 Algorithm for $\operatorname{\textsf{HB}}$ Races

In this section, we outline our $O(\mathcal{N}\cdot\mathcal{L})$-time
algorithm for checking if a trace $\sigma$ has an
$\operatorname{\textsf{HB}}$-race, thereby proving Theorem 1.4. As with the
standard vector clock algorithm [19], our algorithm is based on computing
timestamps for each event. However, unlike the standard algorithm that assigns
thread-indexed timestamps, we use _lock-indexed_ timestamps, or _lockstamps_ ,
which we formalize next. We fix the input trace $\sigma$ in the rest of the
discussion.

#### Lockstamps

A lockstamp is a mapping from locks to natural numbers (including infinity)
$L:\mathsf{Locks}_{\sigma}\to\mathbb{N}\cup\\{\infty\\}$. Given lockstamps
$L,L_{1},L_{2}$ and lock $\ell$, we use the notation  (i) $L[\ell\mapsto c]$to
denote the the lockstamp $\lambda m{\cdot}\text{ if }m=\ell\text{ then
}c\text{ else }L(m)$,  (ii) $L_{1}\sqcup L_{2}$to denote the pointwise
maximum, i.e., $(L_{1}\sqcup L_{2})(\ell)=\max(L_{1}(\ell),L_{2}(\ell))$ for
every $\ell$,  (iii) $L_{1}\sqcap L_{2}$to denote the pointwise minimum, and
(iv) $L_{1}\sqsubseteq L_{2}$to denote the predicate
$\forall\ell{\cdot}L_{1}(\ell)\leq L_{2}(\ell)$.

Our algorithm computes _acquire_ and _release_ lockstamps
$\mathsf{AcqLS}^{\sigma}_{e}$ and $\mathsf{RelLS}^{\sigma}_{e}$ for every
event $e\in\mathsf{Events}_{\sigma}$. Let us formalize these next. For a lock
$\ell$ and acquire event $f\in\mathsf{Acquires}_{\sigma}(\ell)$ (resp. release
event $g\in\mathsf{Releases}_{\sigma}(\ell)$), let
$pos_{\sigma}(f)=|\\{f^{\prime}\in\mathsf{Acquires}_{\sigma}(\ell)\,|\,f^{\prime}\leq^{\sigma}_{\mathsf{\operatorname{\textsf{tr}}}}f\\}|$
(resp.
$pos_{\sigma}(g)=|\\{f^{\prime}\in\mathsf{Releases}_{\sigma}(\ell)\,|\,f^{\prime}\leq^{\sigma}_{\mathsf{\operatorname{\textsf{tr}}}}f\\}|$)
denote the relative position of $f$ (resp. $g$) among all acquire events
(resp. release events) of $\ell$. Then, for an event
$e\in\mathsf{Events}_{\sigma}$ the lockstamps $\mathsf{AcqLS}^{\sigma}_{e}$
and $\mathsf{RelLS}^{\sigma}_{e}$ are defined as follows (we assume that
$\max\varnothing=0$ and $\min\varnothing=\infty$.)

$\begin{array}[]{rcl}\mathsf{AcqLS}^{\sigma}_{e}(\ell)&=&\lambda\ell\cdot\max\\{pos_{\sigma}(f)\,|\,f\in\mathsf{Acquires}_{\sigma}(\ell),f\leq^{\sigma}_{\mathsf{\operatorname{\textsf{HB}}}}e\\}\\\
\\\
\mathsf{RelLS}^{\sigma}_{e}(\ell)&=&\lambda\ell\cdot\min\\{pos_{\sigma}(f)\,|\,f\in\mathsf{Releases}_{\sigma}(\ell),e\leq^{\sigma}_{\mathsf{\operatorname{\textsf{HB}}}}f\\}\end{array}$
(1)

Our $O(\mathcal{N}\cdot\mathcal{L})$ algorithm now relies on the following
observations. First, the $\operatorname{\textsf{HB}}$ partial order can be
inferred by comparing lockstamps of events (Lemma 3.1). Second, there is an
$O(\mathcal{N}\cdot\mathcal{L})$ time algorithm that computes the acquire and
release lockstamps for each event in the input trace. Third, the existence of
an $\operatorname{\textsf{HB}}$ race can be determined by examining only
$O(\mathcal{N})$ pairs of conflicting events (using their lockstamps), instead
of all possible $O(\mathcal{N}^{2})$ pairs (Lemma 3.2). Finally, we can also
examine all the $O(\mathcal{N})$ pairs in time
$O(\mathcal{N}\cdot\mathcal{L})$ (using $O(\mathcal{N})$ lockstamp
comparisons) and thus determine the existence of an
$\operatorname{\textsf{HB}}$ race in the same asymptotic running time. Let us
first state how we use lockstamps to infer the $\operatorname{\textsf{HB}}$
relation.

######  Lemma 3.1.

Let $e_{1}\leq^{\sigma}_{\mathsf{\operatorname{\textsf{tr}}}}e_{2}$ be events
in $\sigma$ such that
$\operatorname{\mathsf{tid}}(e_{1})\neq\operatorname{\mathsf{tid}}(e_{2})$. We
have,
$e_{1}\leq^{\sigma}_{\mathsf{\operatorname{\textsf{HB}}}}e_{2}\iff\neg(\mathsf{AcqLS}^{\sigma}_{e_{2}}\sqsubseteq\mathsf{RelLS}^{\sigma}_{e_{1}})$

Computing Lockstamps. We now illustrate how to compute the acquire lockstamps
for all events, by processing the trace $\sigma$ in a forward pass. For each
thread $t$ and lock $\ell$, we maintain lockstamp variables $\mathbb{C}_{t}$
and $\mathbb{L}_{\ell}$. We also maintain an integer variable
$\mathsf{p}_{\ell}$ for each lock $\ell$ that stores the index of the latest
$\texttt{acq}(\ell)$ event in $\sigma$. Initially, we set each
$\mathbb{C}_{t}$ and $\mathbb{L}_{m}$ to the _bottom_ map $\lambda\ell\cdot
0$, and $\mathsf{p}_{m}$ to $0$, for each thread $t$ and lock $m$. We traverse
$\sigma$ left to right, and perform updates to the data structures as
described in Algorithm 1, by invoking the appropriate _handler_ based on the
thread and operation of the current event $e=\langle t,op\rangle$. At the end
of each handler, we assign the lockstamp $\mathsf{AcqLS}^{\sigma}_{e}$ to $e$.
The computation of release lockstamps is similar, albeit in a reverse pass,
and presented in Appendix B.1. Observe that each step takes $O(\mathcal{L})$
time giving us a total running time of $O(\mathcal{N}\cdot\mathcal{L})$ to
assign lockstamps.

1

2 _acquire(_$t$ , $\ell$_)_:

3 $\mathsf{p}_{\ell}\leftarrow\mathsf{p}_{\ell}+1$

4
$\mathbb{C}_{t}\leftarrow\mathbb{C}_{t}[\ell\mapsto\mathsf{p}_{\ell}]\sqcup\mathbb{L}_{\ell}$

5 $\mathsf{AcqLS}^{\sigma}_{e}\leftarrow\mathbb{C}_{t}$

6 _release(_$t$ , $\ell$_)_:

7 $\mathbb{L}_{\ell}\leftarrow\mathbb{C}_{t}$

8 $\mathsf{AcqLS}^{\sigma}_{e}\leftarrow\mathbb{C}_{t}$

9 _read(_$t$ , $x$_)_:

10 $\mathsf{AcqLS}^{\sigma}_{e}\leftarrow\mathbb{C}_{t}$

11 _write(_$t$ , $x$_)_:

12 $\mathsf{AcqLS}^{\sigma}_{e}\leftarrow\mathbb{C}_{t}$

Algorithm 1 Assigning acquire lockstamps to events in the trace

We say that a pair of conflicting access events $(e_{1},e_{2})$ (with
$e_{1}\leq^{\sigma}_{\mathsf{\operatorname{\textsf{tr}}}}e_{2}$) to a variable
$x$ is a _consecutive conflicting pair_ if there is no event
$f\in\mathsf{Writes}_{\sigma}(x)$ such that
$e_{1}<^{\sigma}_{\mathsf{\operatorname{\textsf{tr}}}}f<^{\sigma}_{\mathsf{\operatorname{\textsf{tr}}}}e_{2}$.
We make the following observation.

######  Lemma 3.2.

A trace $\sigma$ has an $\operatorname{\textsf{HB}}$-race iff there is pair of
consecutive conflicting events in $\sigma$ that is an
$\operatorname{\textsf{HB}}$-race. Moreover, $\sigma$ has at most
$O(\mathcal{N})$ many consecutive conflicting pairs of events.

Checking for an $\operatorname{\textsf{HB}}$ race. We now describe the
algorithm for checking for an $\operatorname{\textsf{HB}}$ race in $\sigma$.
We perform a forward pass on $\sigma$ while storing the release lockstamps of
some of the earlier events. When processing an access event $e$, we check if
it is in race with an earlier event by comparing the acquire lockstamp of $e$
with a previously stored release lockstamp. More precisely, we maintain a
variable $\mathbb{W}_{x}$ to store the release lockstamp of the last write
event on $x$, a variable $t^{w}_{x}$ to store the thread that performed this
write and set $\mathsf{S}_{x}$ to store pairs $(t,L)$ of threads and release
lockstamps of all the read events performed since the last write on $x$ was
observed. Initially, $t^{w}_{x}=\texttt{NIL}$,
$\mathbb{W}_{x}=\lambda\ell\cdot\infty$ and $\mathsf{S}_{x}=\varnothing$. The
update performed at each event $e=\langle t,op\rangle$ are presented in the
corresponding handler in Algorithm 2.

1

_read(_$t$ , $x$_)_:

2 if
_$t^{w}_{x}\not\in\\{\texttt{NIL},t\\}\land\mathsf{AcqLS}^{\sigma}_{e}\sqsubseteq\mathbb{W}_{x}$_
then

3 declare ‘race’ and exit

4
$\mathsf{S}_{x}\leftarrow\mathsf{S}_{x}\cup\\{(t,\mathsf{RelLS}^{\sigma}_{e})\\}$

5 _write(_$t$ , $x$_)_:

6 if
_$t^{w}_{x}\not\in\\{\texttt{NIL},t\\}\land\mathsf{AcqLS}^{\sigma}_{e}\sqsubseteq\mathbb{W}_{x}$_
then

7 declare ‘race’ and exit

8 if  _$\exists(u,L)\in\mathsf{S}_{x},t\neq
u\land\mathsf{AcqLS}^{\sigma}_{e}\sqsubseteq L$_ then

9 declare ‘race’ and exit

10 $t^{w}_{x}=t$; $\mathsf{S}_{x}\leftarrow\varnothing$;
$\mathbb{W}_{x}\leftarrow\mathsf{RelLS}^{\sigma}_{e}$

Algorithm 2 Determining the existence of an $\operatorname{\textsf{HB}}$-race
using lockstamps

We refer to Appendix B.1 for the correctness, which concludes the proof of
Theorem 1.4.

###  3.2 Hardness Results for $\operatorname{\textsf{HB}}$

We now turn our attention to the hardness results for
$\operatorname{\textsf{HB}}$ race detection. To this end, we prove Theorem
1.1, Theorem 1.2, and Theorem 1.3. We start with defining the graph
$\textsf{G}(\leq^{\sigma}_{\mathsf{\operatorname{\textsf{HB}}}})$, which can
be thought of as a form of transitive reduction of the
$\operatorname{\textsf{HB}}$ relation.

The graph $\textsf{G}(\leq^{\sigma}_{\mathsf{\operatorname{\textsf{HB}}}})$.
Given a trace $\sigma$, the graph
$\textsf{G}(\leq^{\sigma}_{\mathsf{\operatorname{\textsf{HB}}}})$ is a graph
with node set $\mathsf{Events}_{\sigma}$, and we have an edge $(e_{1},e_{2})$
in $\textsf{G}(\leq^{\sigma}_{\mathsf{\operatorname{\textsf{HB}}}})$ iff  (i)
$e_{2}$is the immediate successor of $e_{1}$ wrt the thread order
$\leq^{\sigma}_{\mathsf{\operatorname{\textsf{TO}}}}$, or  (ii) $e_{1}$is a
$\texttt{rel}(\ell)$ event, $e_{2}$ is a $\texttt{acq}(\ell)$ event,
$e_{1}\leq^{\sigma}_{\mathsf{\operatorname{\textsf{tr}}}}e_{2}$, and there is
no intermediate event in $\sigma$ that accesses lock $\ell$.  It follows
easily that for any two distinct events $e_{1},e_{2}$, we have
$e_{1}\leq^{\sigma}_{\mathsf{\operatorname{\textsf{HB}}}}e_{2}$ iff $e_{2}$ is
reachable from $e_{1}$ in
$\textsf{G}(\leq^{\sigma}_{\mathsf{\operatorname{\textsf{HB}}}})$. Moreover,
every node has out-degree $\leq 2$ and thus
$\textsf{G}(\leq^{\sigma}_{\mathsf{\operatorname{\textsf{HB}}}})$ is sparse,
while it can be easily constructed in $O(\mathcal{N})$ time.

$A_{1}$101 100 010 $A_{2}$111 011 110

OV instance

$t_{(1,0)}$$1$$w(z)$ $2$$\texttt{cs}(\ell^{x})$

$t_{(1,1)}$$4$$\texttt{cs}(\ell^{x})$$6$$\texttt{cs}(\ell_{1})$

$t_{(1,2)}$$8$$\texttt{cs}(\ell^{x})$

$t_{(1,3)}$$10$$\texttt{cs}(\ell^{x})$$12$$\texttt{cs}(\ell_{3})$$14$$\texttt{cs}(\ell_{(y_{1},3)})$$16$$\texttt{cs}(\ell_{(y_{2},3)})$$18$$\texttt{cs}(\ell_{(y_{3},3)})$

Figure 2: Reducing OV to detecting a write-read
$\operatorname{\textsf{HB}}$-races. Illustration of the threads $t(x,i)$,
where $x$ is the first vector of $A_{1}$. $\texttt{cs}(\ell)$ denotes the
sequence $\texttt{acq}(\ell),\texttt{rel}(\ell)$. Event numbers indicate the
relative order in which these threads execute in $\sigma$.

####  OV hardness of write-read $\operatorname{\textsf{HB}}$ races.

Given a OV instance OV(n,d) on two vector sets $A_{1},A_{2}$, we create a
trace $\sigma$ as follows. For the part $A_{1}$ of OV, we introduce
$n\cdot(d+1)$ threads denoted by $t(x,i)$, for $x\in[n],i\in\\{0\\}\cup[d],$
and $d$ locks, each denoted by $l_{i}$, for $i\in[d]$. For the second part
$A_{2}$ we introduce $n\cdot d$ locks denoted by $l(y,i)$, for
$y\in[n],i\in[d],$ and $n$ threads, denoted by $t_{y}$, for $y\in[n]$.
Finally, we have a single variable $z$.

We first describe the threads $t(x,i)$. We order the vectors in $A_{1}$
arbitrarily. For each vector $x$, for each $i\in[d]$ with $x[i]=1$, we
introduce a critical section on the lock $l_{i}$. If $x$ is the last vector of
$A_{1}$ with $x[i]=1,$ we also insert the critical sections $l_{(y,i)}$ for
all $y\in[n]$, to $t(x,i)$ after the critical section of $l_{x}$. Finally, we
construct a thread $t_{x,0}$ which starts with a write event $\texttt{w}(z)$,
followed by a critical section on lock $l^{x}$. We also insert a critical
section on lock $l^{x}$ to all threads $t(x,i)$, for $i\in[d]$. Hence the
$\texttt{w}(z)$ event is ordered by $\operatorname{\textsf{HB}}$ before all
other events of $t(x,i)$. See Figure 2 for an illustration.

Now we describe the threads $t_{y}$. For each $i\in[d],$ if $y[i]=1$, we add a
critical section of the lock $l(y,i)$ in $t_{y}$. We end the thread with a
read event $\texttt{r}(z)$.

Finally, we construct $\sigma$ by first executing each thread $t(x,i)$ in the
pre-determined order of $x\in A_{1}$, followed by executing the traces $t_{y}$
in any order. See Figure 3 for an illustration. We refer to Appendix B for the
correctness, which concludes the proof of Theorem 1.1.

$w(z)$$\mathbf{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}w(z)}$$w(z)$$\texttt{cs}(l^{x_{1}})$$\texttt{cs}(l^{x_{2}})$$\texttt{cs}(l^{x_{3}})$$\texttt{cs}(l_{1})$$\texttt{cs}(l_{3})$$\texttt{cs}(l_{1,3})$$\texttt{cs}(l_{2,3})$$\texttt{cs}(l_{3,3})$$\texttt{cs}(l_{1})$$\texttt{cs}(l_{1,1})$$\texttt{cs}(l_{2,1})$$\texttt{cs}(l_{3,1})$$\texttt{cs}(l_{2})$$\texttt{cs}(l_{1,2})$$\texttt{cs}(l_{2,2})$$\texttt{cs}(l_{3,2})$$\texttt{cs}(l_{1,1})$$\texttt{cs}(l_{1,2})$$\texttt{cs}(l_{1,3})$$\texttt{cs}(l_{2,2})$$\texttt{cs}(l_{2,3})$$\texttt{cs}(l_{3,1})$$\texttt{cs}(l_{3,2})$$r(z)$$\mathbf{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}r(z)}$$r(z)$
For vectors in $Y,$ $n$ threads with $n\times d$ locks, where thread $i$ has
critical section of lock $(i,k)$ if $y_{i}[k]=1.$ We end each thread with
$\texttt{r}(z)$. Figure 3: Reducing OV to finding $\operatorname{\textsf{HB}}$
races using the instance of Figure 2. For simplicity, we show the graph
$\textsf{G}(\leq^{\sigma}_{\mathsf{\operatorname{\textsf{HB}}}})$ instead of
the trace $\sigma$. The $\operatorname{\textsf{HB}}$ race is marked in red,
corresponding to the orthogonal pair $(x_{2},y_{2})$.

We now turn our attention to the problem of detecting a single
$\operatorname{\textsf{HB}}$ race (i.e., not necessarily involving a read
event). We define a useful multi-connectivity problem on graphs.

######  Problem 3.3.

[MCONN] Given a directed graph $G$ with $n$ nodes and $m$ edges, and $k$ pairs
of nodes $(s_{i},t_{i}),i\in[k],$ decide if there is a path in $G$ from every
$s_{i}$ to the corresponding $t_{i}.$

Due to Lemma 3.2, detecting whether there is an $\operatorname{\textsf{HB}}$
race in $\sigma$ reduces to testing MCONN between all $O(\mathcal{N})$ pairs
of consecutive conflicting events in $\sigma$.

#### Short witnesses for $\operatorname{\textsf{HB}}$ races.

We now prove Theorem 1.2. Following [9, Corollary 2], it suffices to show that
deciding MCONN can be done in
$\textsf{NTIME}[\mathsf{\mathcal{N}^{3/2}}]\cap\textsf{coNTIME}[\mathsf{\mathcal{N}^{3/2}}]$.
At a first glance, the bound $\textsf{NTIME}[\mathsf{\mathcal{N}^{3/2}}]$ may
seem too optimistic, as there are $\Theta(\mathcal{N})$ paths $P_{i}\colon
s_{i}\rightsquigarrow t_{i}$, and each of them can have size
$\Theta(\mathcal{N})$. Hence even just guessing these paths appears to take
quadratic time. Our proof shows that more succinct witnesses exist.

######  Proof 3.4 (Proof of Theorem 1.2).

First consider the simpler case where $\sigma$ has an
$\operatorname{\textsf{HB}}$-race. Phrased as a MCONN problem on
$\textsf{G}(\leq^{\sigma}_{\mathsf{\operatorname{\textsf{HB}}}})$, it suffices
to show that there is a pair $(s_{i},t_{i})$ such that $s_{i}$ does not reach
$t_{i}$. We construct a non-deterministic algorithm for this task that simply
guesses the pair $(s_{i},t_{i})$, and verifies that there is no
$s_{i}\rightsquigarrow t_{i}$ path. Since
$\textsf{G}(\leq^{\sigma}_{\mathsf{\operatorname{\textsf{HB}}}})$ is sparse,
this can be easily verified in $O(\mathcal{N})$ time.

Now consider the case when there is no $\operatorname{\textsf{HB}}$-race.
Phrased as a MCONN problem on
$\textsf{G}(\leq^{\sigma}_{\mathsf{\operatorname{\textsf{HB}}}})$, it suffices
to verify that for every pair $(s_{i},t_{i})$, we have that $s_{i}$ reaches
$t_{i}$. We construct a non-deterministic algorithm for this task, as follows.
The algorithm operates in two phases, using a set $A$, initialized as
$A=\\{(s_{i},t_{i})\\}_{i\in k}$.

  1. 1.

In the first phase, the algorithm repeatedly guesses a node $u$ that lies on
at least $\mathcal{N}^{1/2}$ paths $s_{i}\rightsquigarrow t_{i}$, for
$(s_{i},t_{i})\in A$. It verifies this guess via a backward and a forward
traversal from $u$. The algorithm then removes all such $(s_{i},t_{i})$ from
$A$, and repeats.

  2. 2.

In the second phase, the algorithm guesses for every remaining
$(s_{i},t_{i})\in A$ a path $P_{i}\colon s_{i}\rightsquigarrow t_{i}$, and
verifies that $P_{i}$ is a valid path.

Phase 1 can be execute at most $\mathcal{N}^{1/2}$ iterations, while each
iteration takes $O(\mathcal{N})$ time since
$\textsf{G}(\leq^{\sigma}_{\mathsf{\operatorname{\textsf{HB}}}})$ is sparse.
Hence the total time for phase $1$ is $O(\mathcal{N}^{3/2})$. Phase 2 takes
$O(\mathcal{N}^{3/2})$ time, as every node of
$\textsf{G}(\leq^{\sigma}_{\mathsf{\operatorname{\textsf{HB}}}})$ appears in
at most $\mathcal{N}^{1/2}$ paths $P_{i}$. The desired result follows.

#### A super-linear lower bound for general $\operatorname{\textsf{HB}}$
races.

Finally, we turn our attention to Theorem 1.3. The problem
FO($\mathsf{\forall\exists\exists}$) takes as input a first-order formula
$\phi$ with quantifier structure $\forall\exists\exists$ and whose atoms are
tuples, and the task is to verify whether $\phi$ has a model on a structure of
$n$ elements and $m$ relational tuples. For simplicity, we can think of the
structure as a graph $G$ of $n$ nodes and $m$ edges, and $\phi$ a formula that
characterizes the presence/absence of edges (e.g., $\phi=\forall x\exists
y\exists z\leavevmode\nobreak\ e(x,y)\land\neg e(y,z)$).

The crux of the proof of Theorem 1.3 is showing the following lemma.

######  Lemma 3.5.

FO($\mathsf{\forall\exists\exists}$) reduces to MCONN on a graph $G$ with
$O(n)$ nodes in $O(n^{2})$ time.

Finally, we arrive at Theorem 1.3 by constructing in $O(n^{2})$ time a trace
$\sigma$ with $\mathcal{N}=\Theta(n^{2})$ such that
$\textsf{G}(\leq^{\sigma}_{\mathsf{\operatorname{\textsf{HB}}}})$ is similar
in structure to the graph $G$ of Lemma 3.5. In the end, detecting an
$\operatorname{\textsf{HB}}$ race in $\sigma$ in $O(\mathcal{N}^{1+\epsilon})$
time yields an algorithm for FO($\mathsf{\forall\exists\exists}$) in
$\Theta(n^{2+\epsilon^{\prime}})$ time. We refer to Appendix B for the
details, which conclude the proof of Theorem 1.3.

##  4 Synchronization-Preserving Races

In this section we discuss the dynamic detection of sync-preserving races, and
prove Theorem 1.5.

For notational convenience, we will frequently use the composite _sync_
events. A $\texttt{sync}(\ell)$ event represents the sequence
$\texttt{acq}(\ell),\texttt{r}(x_{\ell}),\texttt{w}(x_{\ell}),\texttt{rel}(\ell)$.
The key idea behind sync events is as follows. Assume that in a trace $\sigma$
we have two $\texttt{sync}(\ell)$ events $e_{1}$ and $e_{2}$ with
$e_{1}<^{\sigma}_{\mathsf{\operatorname{\textsf{tr}}}}e_{2}$. Then any correct
reordering $\rho$ of $\sigma$ with $e_{2}\in\mathsf{Events}_{\rho}$ satisfies
the following.

  1. (a)

We have $e_{1}\in\mathsf{Events}_{\rho}$, as the read event of $e_{2}$ must
read from the write event of $e_{1}$.

  2. (b)

For every $e^{\prime}_{1},e^{\prime}_{2}\in\mathsf{Events}_{\rho}$ such that
$e^{\prime}_{1}\leq^{\sigma}_{\mathsf{\operatorname{\textsf{TO}}}}e_{1}$ and
$e_{2}\leq^{\sigma}_{\mathsf{\operatorname{\textsf{TO}}}}e^{\prime}_{2}$, we
have
$e^{\prime}_{1}<^{\rho}_{\mathsf{\operatorname{\textsf{tr}}}}e^{\prime}_{2}$.

We hence use sync events to ensure certain orderings in any sync-preserving
correct reordering of $\sigma$ that exposes a sync-preserving data race.

#### Intuition.

Before we proceed with the detailed reduction, we provide a high-level
description. The input to 3-OV is three sets of vectors
$A_{1}=\\{x_{i}\\}_{i\in[n]}$, $A_{2}=\\{y_{i}\\}_{i\in[n]}$, and
$A_{3}=\\{z_{i}\\}_{i\in[n]}$. Every vector $x\in A_{1}$ is represented by a
thread $t_{x}$, ending with the critical section
$\texttt{acq}(X),\texttt{w}(z),\texttt{rel}(X)$. Similarly, every vector $y\in
A_{1}$ is represented by a thread $t_{y}$, ending with the critical section
$\texttt{acq}(Y),\texttt{r}(z),\texttt{rel}(Y)$. Notice that we can only have
a race between the write event of a thread $t_{x}$ and the read event of a
thread $t_{y}$. The search for such a race corresponds to the search of the
corresponding vectors $x\in A_{1}$ and $y\in A_{2}$ such that there is a
vector $z\in A_{3}$ which makes the triplet $x,y,z$ orthogonal.

To establish this correspondence, we insert in $t_{x}$ empty critical sections
on locks $l_{k}$, for $k\in[d]$ that represent the coordinates $k$ for which
$x[k]=1$. We use a similar encoding with locks $l^{\prime}_{k}$ for the
threads $t_{y}$, capturing that $y[k]=1$. To encode the vectors in $A_{3}$, we
use $k$ threads $t_{k}$, for $k\in[d]$, such that the $i^{th}$ segment of
$t_{k}$ encodes $z_{i}[k]$: we have two interleaved critical sections on locks
$l_{k}$ and $l^{\prime}_{k}$ iff $z_{i}[k]=1$.

Finally, we use some sync events to force all threads $t_{k}$ be partially
executed whenever we want to execute the write event of any thread $t_{x}$.
Hence, any correct reordering of $\sigma$ that exposes a data race in
$\sigma$, must execute all $t_{k}$ at least partially. We make all threads
$t_{k}$ execute before all $t_{x}$ and $t_{y}$ in $\sigma$. The notion of
sync-preservation ensures that if we have a correct reordering that exposes a
race between two threads $t_{x}$ and $t_{y}$, then the following holds. For
every coordinate $k\in[d]$ in which $x[k]=y[k]=1$, since the corresponding
threads $t_{x}$ and $t_{y}$ have critical sections on locks $l_{k}$ and
$l^{\prime}_{k}$, the thread $t_{k}$ must execute up to a point where it does
not have critical sections on these locks. This means that we have found a
vector $z$ with $z[k]=0$, and thus the triplet $x,y,z$ is orthogonal on that
coordinate.

$A_{1}$11 11 $A_{2}$11 01 $A_{3}$11 10

3-OV instance

$t_{x}$$34$$\texttt{acq}(l_{1})$$35$$\texttt{rel}(l_{1})$$36$$\texttt{acq}(l_{2})$$37$$\texttt{rel}(l_{2})$$50$$\texttt{acq}(X)$$51$$\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}w(z)$$52$$\texttt{rel}(X)$

$t_{y_{1}}$$42$$\texttt{sync}(s_{1})$$43$$\texttt{acq}(l^{\prime}_{1})$$44$$\texttt{rel}(l^{\prime}_{1})$$45$$\texttt{acq}(l^{\prime}_{2})$$46$$\texttt{rel}(l^{\prime}_{2})$$59$$\texttt{acq}(Y)$$60$$r(z)$$61$$\texttt{rel}(Y)$

$t_{y_{2}}$$47$$\texttt{sync}(s_{2})$$48$$\texttt{acq}(l^{\prime}_{2})$$49$$\texttt{rel}(l^{\prime}_{2})$$62$$\texttt{acq}(Y)$$63$$\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}r(z)$$64$$\texttt{rel}(Y)$

$t_{1}$$1$$\texttt{acq}(l_{1})$$2$$\texttt{sync}(\ell_{1})$$3$$\texttt{acq}(l^{\prime}_{1})$$4$$\texttt{rel}(l_{1})$$13$$\texttt{sync}(\ell_{1})$$14$$\texttt{rel}(l^{\prime}_{1})$-$z_{1}$
ends-
$20$$\texttt{acq}(l_{1})$$21$$\texttt{sync}(\ell_{1})$$22$$\texttt{acq}(l^{\prime}_{1})$$23$$\texttt{rel}(l_{1})$$28$$\texttt{sync}(\ell_{1})$$29$$\texttt{rel}(l^{\prime}_{1})$

$t_{2}$$5$$\texttt{acq}(l_{2})$$6$$\texttt{sync}(\ell_{2})$$7$$\texttt{acq}(l^{\prime}_{2})$$8$$\texttt{rel}(l_{2})$$15$$\texttt{sync}(\ell_{2})$$16$$\texttt{rel}(l^{\prime}_{2})$-$z_{1}$
ends- $24$$\texttt{sync}(\ell_{2})$$30$$\texttt{sync}(\ell_{2})$

$t_{Aux}$$9$$\texttt{sync}(\ell_{1})$$10$$\texttt{sync}(\ell_{2})$$11$$\texttt{sync}(s_{1})$$12$$\texttt{sync}(s_{2})$$17$$\texttt{acq}(Y)$$18$$\texttt{sync}(\ell_{1})$$19$$\texttt{sync}(\ell_{2})$$25$$\texttt{sync}(\ell_{1})$$26$$\texttt{sync}(\ell_{2})$$27$$\texttt{rel}(Y)$$31$$\texttt{acq}(Y)$$32$$\texttt{sync}(\ell_{1})$$33$$\texttt{sync}(\ell_{2})$$56$$\texttt{acq}(X)$$57$$\texttt{rel}(X)$$58$$\texttt{rel}(Y)$

Figure 5:  Example reduction from 3-OV to sync race detection. The trace
orders events as shown by their numbering. We only show one thread $t_{x}$, as
the two $x$ vectors are identical.

Reduction. Given an 3-OV instance OV(n, d, 3) on vector sets
$A_{1}=\\{x_{i}\\}_{i\in[n]}$, $A_{2}=\\{y_{i}\\}_{i\in[n]}$, and
$A_{3}=\\{z_{i}\\}_{i\in[n]}$, we create a trace $\sigma$ as follows (see
Figure 5). We have $\mathcal{T}=2\cdot n+d+1$ threads, while all access events
(not counting the sync events) are of the form $\texttt{w}(z)/\texttt{r}(z)$
in a single variable $z$. We first describe the threads, and then how they
interleave in $\sigma$.

Threads. We introduce a thread $t_{x}$ for every vector $x\in A_{1}$ and a
lock $l_{k}$ for every $k\in[d]$. Each thread $t_{x}$ consists of two segments
$t^{1}_{x}$ and $t^{2}_{x}$. We create $t^{1}_{x}$ as follows. For every
$k\in[d]$ where $x[k]=1,$ we add an empty critical section
$\texttt{acq}(l_{k}),\texttt{rel}(l_{k})$ in $t^{1}_{x}$. We create
$t^{2}_{x}$ as the sequence $\texttt{acq}(X),\texttt{w}(z),\texttt{rel}(X)$,
where $X$ is a new lock, common for all $t^{2}_{x}$.

For the vectors in $A_{2}$, we introduce threads similar to those of part
$A_{1},$ as follows. We have a thread $t_{y}$ for every vector $y\in A_{2}$
and a lock $l^{\prime}_{k}$ for every $k\in[d]$. Each thread $t_{y}$ consists
of two segments $t^{1}_{y}$ and $t^{2}_{y}$. For every $k\in[d]$ where
$y[k]=1,$ we add an empty critical section
$\texttt{acq}(l^{\prime}_{k}),\texttt{rel}(l^{\prime}_{k})$ in $t^{1}_{y}$. In
contrast to the $t^{1}_{x}$, every $t^{1}_{y}$ also has an event
$\texttt{sync}(s_{y})$ at the very beginning. We create $t^{2}_{y}$ as the
sequence $\texttt{acq}(Y),\texttt{r}(z),\texttt{rel}(Y)$, where $Y$ is a new
lock, common for all $t^{2}_{y}$.

The construction of the threads corresponding to the vectors in $A_{3}$ is
more involved. We have one thread $t_{k}$ for every $k\in[d]$. Each thread has
some fixed sync events, as well as critical sections corresponding to one
coordinate of all $n$ vectors in $A_{3}$. In particular, we construct each
$t_{k}$ as follows. We iterate over all $z_{i}$, and if $z_{i}[k]=0$, we
simply append two events $\texttt{sync}(\ell_{k}),\texttt{sync}(\ell_{k})$ to
$t_{k}$. On the other hand, if $z_{i}[k]=1$, we interleave these sync events
with two critical sections, by appending the sequence
$\texttt{acq}(l_{k}),\texttt{sync}(\ell_{k}),\texttt{acq}(l^{\prime}_{k}),\texttt{rel}(l_{k}),\texttt{sync}(\ell_{k}),\texttt{rel}(l^{\prime}_{k})$.

Lastly, we have a single auxiliary trace $t$ that consists of three parts
$t^{1}$, $t^{2}$ and $t^{3}$, where

$\displaystyle t^{1}$
$\displaystyle=\texttt{sync}(\ell_{1}),\dots,\texttt{sync}(\ell_{k}),\texttt{sync}(s_{y_{1}}),\dots\texttt{sync}(s_{y_{n}})$
$\displaystyle t^{2}$
$\displaystyle=\left(\texttt{acq}(Y),\texttt{sync}(\ell_{1}),\dots,\texttt{sync}(\ell_{k}),\texttt{sync}(\ell_{1}),\dots,\texttt{sync}(\ell_{k}),\texttt{rel}(Y)\right)^{n-1}$
$\displaystyle t^{3}$
$\displaystyle=\texttt{acq}(Y),\texttt{sync}(\ell_{1}),\dots,\texttt{sync}(\ell_{k}),\texttt{acq}(X),\texttt{rel}(X),\texttt{rel}(Y)$

Concurrent trace. We are now ready to describe the interleaving of the above
threads in order to obtain the concurrent trace $\sigma$.

  1. 1.

We execute the auxiliary trace $t$ and all traces $t_{k}$, for $k\in[d]$
(i.e., the threads corresponding to the vectors of $A_{3}$) arbitrarily, as
long as for every $k\in[d]$, every sequence of $\texttt{sync}(\ell_{k})$
events  (a) starts with the $\texttt{sync}(\ell_{k})$ event of $t_{k}$ and
proceeds with the $\texttt{sync}(\ell_{k})$ event of $t$,  (b) strictly
alternates in every two $\texttt{sync}(\ell_{k})$ events between $t$ and
$t_{k}$, and  (c) ends with the last $\texttt{sync}(\ell_{k})$ event of
$t_{k}$.

  2. 2.

We execute all $t^{1}_{x}$ and $t^{1}_{y}$ (i.e., the first parts of all
threads that correspond to the vectors in $A_{1}$ and $A_{2}$) arbitrarily,
but after all traces $t_{k}$, for $k\in[d]$.

  3. 3.

We execute all $t^{2}_{x}$ (i.e., the second parts of all traces that
correspond to the vectors in $A_{1}$) arbitrarily, but before the segment
$\texttt{acq}(X),\texttt{rel}(X),\texttt{rel}(Y)$ of $t$.

  4. 4.

We execute all $t^{2}_{y}$ (i.e., the second parts of all traces that
correspond to the vectors in $A_{2}$) arbitrarily, but after the segment
$\texttt{acq}(X),\texttt{rel}(X),\texttt{rel}(Y)$ of $t$.

We refer to Appendix C for the correctness of the reduction and thus the proof
of Theorem 1.5.

##  5 Violations of the Locking Discipline

###  5.1 Lock-Cover Races

We start with a simple reduction from OV to detecting lock-cover races. Given
a OV instance OV(n,d) on two vector sets $A_{1},A_{2}$, we create a trace
$\sigma$ as follows. We have a single variable $x$ and two threads
$t_{1},t_{2}$. We associate with each vector of the set $A_{i}$ a write access
event $e=\langle t_{i},\texttt{w}(x)\rangle$. Moreover, each such event holds
up to $d$ locks, so that $e$ holds the $k^{th}$ lock iff $k^{th}$ coordinate
of the vector corresponding to the event is $1$. The trace $\sigma$ is formed
by ordering the sequence of events corresponding to vectors of $A_{1}$ of OV
first, in a fixed arbitrary order, followed by the sequence of events
corresponding to $A_{2}$, again in arbitrary order. We refer to Appendix D for
the correctness, which concludes the proof of Theorem 1.6.

###  5.2 Lock-Set Races

We now turn our attention to lock-set races. We first prove Theorem 1.9, i.e.,
that determining whether a trace $\sigma$ has a lock-set race on a specific
variable $x$ can be performed in linear time.

#### A linear-time algorithm per variable.

Verifying that there are two conflicting events on $x$ is straightforward by a
single pass of $\sigma$. The more involved part is in computing the lock-set
of $x$, i.e., the set
$\bigcap_{e\in\mathsf{Accesses}_{\sigma}(x)}\mathsf{locksHeld}_{\sigma}(e)$,
in linear time. Indeed, each intersection alone requires $\Theta(\mathcal{L})$
time, resulting to $\Theta(\mathcal{N}\cdot\mathcal{L})$ time overall.

Here we show that a somewhat more involved algorithm achieves the task. The
algorithm performs a single pass of $\sigma$, while maintaining three simple
sets $A$, $B$, and $C$. While processing an event $e$, the sets are updated to
maintain the invariant

$\displaystyle
A=\mathsf{locksHeld}_{\sigma}(e)\quad\;B=\mathsf{Locks}_{\sigma}\cap\bigcap_{e^{\prime}\in\mathsf{Accesses}_{\sigma}(x),e^{\prime}\leq^{\sigma}_{\mathsf{\operatorname{\textsf{tr}}}}e}\mathsf{locksHeld}_{\sigma}(e^{\prime})\quad\;C=\overline{A}\cap
B$ (2)

The sets are initialized as $A=\varnothing$, $B=C=\mathsf{Locks}_{\sigma}$.
Then the algorithm performs a pass over $\sigma$ and processes each event $e$
according to the description of Algorithm 3.

1

_acquire(_$t$ , $\ell$_)_:

2 $A\leftarrow A\cup\\{\ell\\}$

3 if  _$\ell\in B$_ then

4 $C\leftarrow C\setminus\\{\ell\\}$

5 _release(_$t$ , $\ell$_)_:

6 $A\leftarrow A\setminus\\{\ell\\}$

7 if  _$\ell\in B$_ then

8 $C\leftarrow C\cup\\{\ell\\}$

9 _read(_$t$ , $y$_)_:

10 if  _$x=y$_ then

11 $B\leftarrow B\setminus C$

12 $C\leftarrow\varnothing$

13 _write(_$t$ , $y$_)_:

14 if  _$x=y$_ then

15 $B\leftarrow B\setminus C$

16 $C\leftarrow\varnothing$

Algorithm 3 Computing lock-set of variable $x$

The correctness of Algorithm 3 follows by proving the invariant in Equation 2.
We refer to Appendix D for the details, which concludes the proof of Theorem
1.9.

#### Short witnesses for lock-set races.

Besides the advantage of a faster algorithm, Theorem 1.9 implies that lock-set
races have short witnesses that can be verified in linear time. This allows us
to prove that detecting a lock-set race is in
$\textsf{NTIME}[\mathsf{\mathcal{N}}]\cap\textsf{coNTIME}[\mathsf{\mathcal{N}}]$,
and we can thus use [9, Corollary 2] to prove Theorem 1.7.

######  Proof 5.1 (Proof of Theorem 1.7).

First we argue that the problem is in $\textsf{NTIME}[\mathsf{\mathcal{N}}]$.
Indeed, the certificate for the existence of a lock-set race is simply the
variable $x$ on which there is a lock-set race. By Theorem 1.9, verifying that
we indeed have a lock-set race on $x$ takes $O(\mathcal{N})$ time.

Now we argue that the problem is in $\textsf{coNTIME}[\mathsf{\mathcal{N}}]$,
by giving a certificate to verify in linear time that $\sigma$ does not have a
race of the required form. The certificate has size
$O(|\mathsf{Vars}_{\sigma}|)$, and specifies for every variable, either the
lock that is held by all access events of the variable, or a claim that there
exist no two conflicting events on that variable. The certificate can be
easily verified by one pass over $\sigma$.

#### Lock-set races are Hitting-Set hard.

Finally we prove Theorem 1.8, i.e., that determining a single lock-set race is
HS-hard, and thus also carries a conditional quadratic lower bound. We
establish a fine-grained reduction from HS. Given a HS instance HS(n,d) on two
vector sets $X,Y$, we create a trace $\sigma$ using $d+1$ threads
$\\{t_{j}\\}_{j\in\\{0\\}\cup[d]}$, $n$ locks $\\{\ell_{i}\\}_{i\in[n]}$, and
$n$ variables $\\{z_{i}\\}_{k\in[n]}$. Thread $t_{0}$ that executes
$\texttt{acq}(\ell_{1}),\dots,\texttt{acq}(\ell_{n}),\texttt{w}(z_{1}),\dots\texttt{w}(z_{n}),\texttt{rel}(\ell_{n}),\dots\texttt{rel}(\ell_{1})$.
Each of the threads $t_{j}$, for $j\in[d]$, has a single nested critical
section consisting of the locks $\ell_{i}\in[n]$ such that the $i^{th}$ vector
of $Y$ has its $j^{th}$ coordinate $0$, i.e, $y_{i}[j]=0$. The events in the
critical section are all write events of all variables $z_{k}\in[n]$ with
$x_{k}[j]=1$. The trace orders all events of each thread $t_{d}$
consecutively, and all the events overall in increasing order of $d$. See
Figure 6 for an illustration. We refer to Appendix D for the correctness,
which concludes the proof of Theorem 1.8.

$X$$1$001 $2$100 $3$101 $4$011 $Y$001 010 111 110

HS instance: $n=4,d=3$

$t_{1}$$1$$\texttt{acq}(\ell_{1})$ $2$$\texttt{acq}(\ell_{2})$ $3$$w(z_{2})$
$4$$w(z_{3})$ $5$$\texttt{rel}(\ell_{2})$ $6$$\texttt{rel}(\ell_{1})$

$t_{2}$$7$$\texttt{acq}(\ell_{1})$$8$$\mathbf{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}w(z_{4})}$$9$$\texttt{rel}(\ell_{1})$

$t_{3}$$10$$\texttt{acq}(\ell_{2})$$11$$\texttt{acq}(\ell_{4})$$12$$w(z_{1})$$13$$w(z_{3})$$14$$\mathbf{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}w(z_{4})}$$15$$\texttt{rel}(\ell_{4})$$16$$\texttt{rel}(\ell_{2})$

$t_{0}$$17$$\texttt{acq}(\ell_{1})$$18$$\vdots$$19$$\texttt{acq}(\ell_{4})$$20$$w(z_{1})$$21$$\vdots$$22$$w(z_{4})$$23$$\texttt{rel}(\ell_{4})$$24$$\vdots$$25$$\texttt{rel}(\ell_{1})$

Figure 6: Reducing HS to detecting a lock-set race on trace $\sigma$ with $d$
threads. Thread $t_{k}$ uses lock $l_{i}$ if $y_{i}[k]=0$, and $w(z_{j})$ if
$x_{j}[k]=1$. Vector $x_{4}$ hits all vectors in $Y$, implying a lock-set race
on $z_{4}$.

##  6 Conclusion

In this work we have taken a fine-grained view of the complexity of popular
notions of dynamic data races. We have established a range of lower bounds on
the complexity of detecting $\operatorname{\textsf{HB}}$ races, sync-
preserving races, as well as races based on the locking discipline (lock-
cover/lock-set races). Moreover, we have characterized cases where lower
bounds based on SETH are not possible under NSETH. Finally, we have proven new
upper bounds for detecting $\operatorname{\textsf{HB}}$ and lock-set races. To
our knowledge, this is the first work that characterizes the complexity of
well-established dynamic race-detection techniques, allowing for a rigorous
characterization of their trade-offs between expressiveness and running time.

## References

  * [1] Helgrind: a thread error detector.  https://valgrind.org/docs/manual/hg-manual.html.  Accessed: 2021-04-30.
  * [2] Intel Inspector.  https://software.intel.com/content/www/us/en/develop/tools/oneapi/components/inspector.html.  Accessed: 2021-04-30.
  * [3] Amir Abboud, Virginia Vassilevska Williams, and Joshua Wang.  Approximation and fixed parameter subquadratic algorithms for radius and diameter in sparse graphs.  In Proceedings of the Twenty-Seventh Annual ACM-SIAM Symposium on Discrete Algorithms, SODA ’16, page 377–391, USA, 2016. Society for Industrial and Applied Mathematics.
  * [4] Utpal Banerjee, Brian Bliss, Zhiqiang Ma, and Paul Petersen.  A theory of data race detection.  In Proceedings of the 2006 Workshop on Parallel and Distributed Systems: Testing and Debugging, PADTAD ’06, pages 69–78, New York, NY, USA, 2006\. ACM.  URL: http://doi.acm.org/10.1145/1147403.1147416, doi:10.1145/1147403.1147416.
  * [5] Hans-J. Boehm.  How to miscompile programs with “benign” data races.  In Proceedings of the 3rd USENIX Conference on Hot Topic in Parallelism, HotPar’11, page 3, USA, 2011. USENIX Association.
  * [6] Hans-J. Boehm.  Position paper: Nondeterminism is unavoidable, but data races are pure evil.  In Proceedings of the 2012 ACM Workshop on Relaxing Synchronization for Multicore and Manycore Scalability, RACES ’12, page 9–14, New York, NY, USA, 2012. Association for Computing Machinery.  URL: https://doi.org/10.1145/2414729.2414732, doi:10.1145/2414729.2414732.
  * [7] Hans-J. Boehm and Sarita V. Adve.  Foundations of the C++ Concurrency Memory Model.  In Proceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’08, page 68–78, New York, NY, USA, 2008. Association for Computing Machinery.  URL: https://doi.org/10.1145/1375581.1375591, doi:10.1145/1375581.1375591.
  * [8] Karl Bringmann.  Fine-Grained Complexity Theory (Tutorial).  In Rolf Niedermeier and Christophe Paul, editors, 36th International Symposium on Theoretical Aspects of Computer Science (STACS 2019), volume 126 of Leibniz International Proceedings in Informatics (LIPIcs), pages 4:1–4:7, Dagstuhl, Germany, 2019. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik.  URL: http://drops.dagstuhl.de/opus/volltexte/2019/10243, doi:10.4230/LIPIcs.STACS.2019.4.
  * [9] Marco L Carmosino, Jiawei Gao, Russell Impagliazzo, Ivan Mihajlin, Ramamohan Paturi, and Stefan Schneider.  Nondeterministic extensions of the strong exponential time hypothesis and consequences for non-reducibility.  In Proceedings of the 2016 ACM Conference on Innovations in Theoretical Computer Science, pages 261–270, 2016.
  * [10] Bernadette Charron-Bost.  Concerning the size of logical clocks in distributed systems.  Information Processing Letters, 39(1):11 – 16, 1991.  URL: http://www.sciencedirect.com/science/article/pii/002001909190055M, doi:https://doi.org/10.1016/0020-0190(91)90055-M.
  * [11] Peter Chini, Jonathan Kolberg, Andreas Krebs, Roland Meyer, and Prakash Saivasan.  On the Complexity of Bounded Context Switching.  In Kirk Pruhs and Christian Sohler, editors, 25th Annual European Symposium on Algorithms (ESA 2017), volume 87 of Leibniz International Proceedings in Informatics (LIPIcs), pages 27:1–27:15, Dagstuhl, Germany, 2017. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik.  URL: http://drops.dagstuhl.de/opus/volltexte/2017/7873, doi:10.4230/LIPIcs.ESA.2017.27.
  * [12] Peter Chini, Roland Meyer, and Prakash Saivasan.  Fine-grained complexity of safety verification.  In Dirk Beyer and Marieke Huisman, editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 20–37, Cham, 2018. Springer International Publishing.
  * [13] Peter Chini and Prakash Saivasan.  A Framework for Consistency Algorithms.  In Nitin Saxena and Sunil Simon, editors, 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020), volume 182 of Leibniz International Proceedings in Informatics (LIPIcs), pages 42:1–42:17, Dagstuhl, Germany, 2020. Schloss Dagstuhl–Leibniz-Zentrum für Informatik.  URL: https://drops.dagstuhl.de/opus/volltexte/2020/13283, doi:10.4230/LIPIcs.FSTTCS.2020.42.
  * [14] Anne Dinning and Edith Schonberg.  Detecting access anomalies in programs with critical sections.  In Proceedings of the 1991 ACM/ONR Workshop on Parallel and Distributed Debugging, PADD ’91, pages 85–96, New York, NY, USA, 1991. ACM.  URL: http://doi.acm.org/10.1145/122759.122767, doi:10.1145/122759.122767.
  * [15] Tayfun Elmas, Shaz Qadeer, and Serdar Tasiran.  Goldilocks: A race and transaction-aware java runtime.  In Proceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’07, pages 245–255, New York, NY, USA, 2007. ACM.  URL: http://doi.acm.org/10.1145/1250734.1250762, doi:10.1145/1250734.1250762.
  * [16] Cormac Flanagan and Stephen N. Freund.  Fasttrack: Efficient and precise dynamic race detection.  In Proceedings of the 30th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’09, pages 121–133, New York, NY, USA, 2009. ACM.  URL: http://doi.acm.org/10.1145/1542476.1542490, doi:10.1145/1542476.1542490.
  * [17] Jiawei Gao, Russell Impagliazzo, Antonina Kolokolova, and Ryan Williams.  Completeness for first-order properties on sparse structures with algorithmic applications.  ACM Trans. Algorithms, 15(2), December 2018.  URL: https://doi.org/10.1145/3196275, doi:10.1145/3196275.
  * [18] Russell Impagliazzo and Ramamohan Paturi.  On the complexity of k-sat.  Journal of Computer and System Sciences, 62(2):367–375, 2001.
  * [19] Ayal Itzkovitz, Assaf Schuster, and Oren Zeev-Ben-Mordehai.  Toward integration of data race detection in dsm systems.  J. Parallel Distrib. Comput., 59(2):180–203, November 1999.  URL: http://dx.doi.org/10.1006/jpdc.1999.1574, doi:10.1006/jpdc.1999.1574.
  * [20] Baris Kasikci, Cristian Zamfir, and George Candea.  Racemob: Crowdsourced data race detection.  In Proceedings of the Twenty-Fourth ACM Symposium on Operating Systems Principles, SOSP ’13, page 406–422, New York, NY, USA, 2013. Association for Computing Machinery.  URL: https://doi.org/10.1145/2517349.2522736, doi:10.1145/2517349.2522736.
  * [21] Dileep Kini, Umang Mathur, and Mahesh Viswanathan.  Dynamic race prediction in linear time.  In Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017, pages 157–170, New York, NY, USA, 2017. ACM.  URL: http://doi.acm.org/10.1145/3062341.3062374, doi:10.1145/3062341.3062374.
  * [22] Leslie Lamport.  Time, clocks, and the ordering of events in a distributed system.  Commun. ACM, 21(7):558–565, July 1978.  URL: http://doi.acm.org/10.1145/359545.359563, doi:10.1145/359545.359563.
  * [23] Umang Mathur, Dileep Kini, and Mahesh Viswanathan.  What happens-after the first race? enhancing the predictive power of happens-before based dynamic race detection.  Proc. ACM Program. Lang., 2(OOPSLA):145:1–145:29, October 2018\.  URL: http://doi.acm.org/10.1145/3276515, doi:10.1145/3276515.
  * [24] Umang Mathur, Andreas Pavlogiannis, and Mahesh Viswanathan.  The complexity of dynamic data race prediction.  In Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’20, page 713–727, New York, NY, USA, 2020. Association for Computing Machinery.  URL: https://doi.org/10.1145/3373718.3394783, doi:10.1145/3373718.3394783.
  * [25] Umang Mathur, Andreas Pavlogiannis, and Mahesh Viswanathan.  Optimal prediction of synchronization-preserving races.  Proc. ACM Program. Lang., 5(POPL), January 2021.  URL: https://doi.org/10.1145/3434317, doi:10.1145/3434317.
  * [26] Satish Narayanasamy, Zhenghao Wang, Jordan Tigani, Andrew Edwards, and Brad Calder.  Automatically classifying benign and harmful data races using replay analysis.  In Proceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’07, page 22–31, New York, NY, USA, 2007. Association for Computing Machinery.  URL: https://doi.org/10.1145/1250734.1250738, doi:10.1145/1250734.1250738.
  * [27] Robert O’Callahan and Jong-Deok Choi.  Hybrid dynamic data race detection.  SIGPLAN Not., 38(10):167–178, June 2003.  URL: http://doi.acm.org/10.1145/966049.781528, doi:10.1145/966049.781528.
  * [28] Andreas Pavlogiannis.  Fast, sound, and effectively complete dynamic race prediction.  Proc. ACM Program. Lang., 4(POPL), December 2019.  URL: https://doi.org/10.1145/3371085, doi:10.1145/3371085.
  * [29] Eli Pozniansky and Assaf Schuster.  Efficient on-the-fly data race detection in multithreaded c++ programs.  SIGPLAN Not., 38(10):179–190, June 2003.  URL: http://doi.acm.org/10.1145/966049.781529, doi:10.1145/966049.781529.
  * [30] Jake Roemer, Kaan Genç, and Michael D. Bond.  High-coverage, unbounded sound predictive race detection.  In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, pages 374–389, New York, NY, USA, 2018. ACM.  URL: http://doi.acm.org/10.1145/3192366.3192385, doi:10.1145/3192366.3192385.
  * [31] Grigore Rosu.  RV-Predict, Runtime Verification.  https://runtimeverification.com/predict/, 2018.  Accessed: 2018-04-01.
  * [32] Mahmoud Said, Chao Wang, Zijiang Yang, and Karem Sakallah.  Generating data race witnesses by an smt-based analysis.  In Proceedings of the Third International Conference on NASA Formal Methods, NFM’11, pages 313–327, Berlin, Heidelberg, 2011. Springer-Verlag.  URL: http://dl.acm.org/citation.cfm?id=1986308.1986334.
  * [33] Stefan Savage, Michael Burrows, Greg Nelson, Patrick Sobalvarro, and Thomas Anderson.  Eraser: A dynamic data race detector for multithreaded programs.  ACM Trans. Comput. Syst., 15(4):391–411, November 1997.  URL: http://doi.acm.org/10.1145/265924.265927, doi:10.1145/265924.265927.
  * [34] Koushik Sen, Grigore Roşu, and Gul Agha.  Detecting errors in multithreaded programs by generalized predictive analysis of executions.  In Martin Steffen and Gianluigi Zavattaro, editors, Formal Methods for Open Object-Based Distributed Systems, pages 211–226, Berlin, Heidelberg, 2005. Springer Berlin Heidelberg.
  * [35] Konstantin Serebryany and Timur Iskhodzhanov.  ThreadSanitizer: Data Race Detection in Practice.  WBIA ’09, 2009.
  * [36] Jaroslav Ševčík and David Aspinall.  On validity of program transformations in the java memory model.  In Jan Vitek, editor, ECOOP 2008 – Object-Oriented Programming, pages 27–51, Berlin, Heidelberg, 2008. Springer Berlin Heidelberg.
  * [37] Yannis Smaragdakis, Jacob Evans, Caitlin Sadowski, Jaeheon Yi, and Cormac Flanagan.  Sound predictive race detection in polynomial time.  In Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’12, pages 387–400, New York, NY, USA, 2012. ACM.  URL: http://doi.acm.org/10.1145/2103656.2103702, doi:10.1145/2103656.2103702.
  * [38] Martin Sulzmann and Kai Stadtmüller.  Efficient, near complete, and often sound hybrid dynamic data race prediction.  In Proceedings of the 17th International Conference on Managed Programming Languages and Runtimes, MPLR 2020, page 30–51, New York, NY, USA, 2020. Association for Computing Machinery.  URL: https://doi.org/10.1145/3426182.3426185, doi:10.1145/3426182.3426185.
  * [39] Christoph von Praun.  Race Detection Techniques, pages 1697–1706.  Springer US, Boston, MA, 2011.  URL: https://doi.org/10.1007/978-0-387-09766-4_38, doi:10.1007/978-0-387-09766-4_38.
  * [40] Jaroslav Ševčík.  Safe optimisations for shared-memory concurrent programs.  SIGPLAN Not., 46(6):306–316, June 2011.  URL: https://doi.org/10.1145/1993316.1993534, doi:10.1145/1993316.1993534.
  * [41] Ryan Williams.  A new algorithm for optimal 2-constraint satisfaction and its implications.  Theoretical Computer Science, 348(2-3):357–365, 2005.
  * [42] Virginia Vassilevska Williams.  On some fine-grained questions in algorithms and complexity.  In Proceedings of the ICM, volume 3, pages 3431–3472. World Scientific, 2018.
  * [43] M. Zhivich and R. K. Cunningham.  The real cost of software errors.  IEEE Security and Privacy, 7(2):87–90, March 2009.  URL: https://doi.org/10.1109/MSP.2009.56, doi:10.1109/MSP.2009.56.

##  Appendix A Fine-Grained Complexity and Popular Hypotheses

In this section we present notions of fine-grained complexity theory that are
relevant to our work. We refer to the survey [42] for a detailed exposition on
the topic.

This theory relates the computational complexity of problems under the
following, more refined, notion of reduction than the standard ones used in
traditional complexity theory. Informally, the definition says that if there
is an algorithm for some problem B faster than its assumed lower bound, then
such a reduction from some problem A to B gives an algorithm for A thatis
faster than its conjectured lower bound.

#### Fine-grained Reductions.

Assume that A and B are computational problems and $a(n)$ and $b(n)$ are their
conjectured running time lower bounds, respectively. Then we say A
$(a,b)$-reduces to B, denoted by A
${}_{(\mathsf{a})}\\!\\!\preceq_{(\mathsf{b})}$ B, if for every $\epsilon>0,$
there exists $\delta>0$, and an algorithm R for A that runs in time
$a(n)^{(1-\delta)}$ on inputs of length $n$, making $q$ calls to an oracle for
B with query lengths $n_{1},\dotsc,n_{q}$, where,

$\sum_{1}^{q}(b(n))^{(1-\epsilon)}\leq(a(n))^{(1-\delta)}.$

Problems that can be reduced to each other such that the lower bounds for each
problem are the same in both reductions, i.e.,
A${}_{(\mathsf{a})}\\!\\!\preceq_{(\mathsf{b})}$B and
B${}_{(\mathsf{b})}\\!\\!\preceq_{(\mathsf{a})}$A, are intuitively thought to
have the same underlying ‘reason’ for hardness, and are said to be fine-
grained equivalent.

A reduction A${}_{(\mathsf{a})}\\!\\!\preceq_{(\mathsf{b})}$B would be
interesting for B if $a(n)$ was a proven or well-believed conjectured lower
bound on A, thus implying a believable lower bound on B. One such well-
believed conjecture in complexity theory is SETH [18] for the classic CNF-SAT
problem, originally defined for deterministic algorithms, but now widely
believed for randomized algorithms as well.

######  Hypothesis 1 (Strong Exponential Time Hypothesis (SETH)).

For every $\epsilon>0$ there exists an integer $k\geq 3$ such that CNF-SAT on
formulas with clause size at most $k$ and $n$ variables cannot be solved in
$O(2^{(1-\epsilon)n})$ time even by a randomized algorithm.

SETH implies a lower bound conjecture, denoted by OVH, on the Orthogonal
Vectors problem OV, as shown by a reduction from CNF-SAT to k-OV [41]. Thus, a
conditional lower bound under OVH implies one under SETH as well, leading to
numerous conditional lower bound results under OVH [See [42] for a detailed
literature review]. This paper will also prove such results on several data
race detection problems, hence we now state k-OV and OVH formally.

An instance of k-OV is an integer $d=\omega(\log n)$ and $k$ sets
$A_{i}\subseteq\\{0,1\\}^{d},\ i\in[n]$ such that $|A_{i}|=n,$ and denoted by
$\textsf{OV}(n,d){}$.

######  Problem A.1 (Orthogonal Vectors (k-OV)).

Given an instance $\textsf{OV}(n,d,k)$, the k-OV problem is to decide if there
are $k$ vectors $a_{i}\in A_{i}$ for all $i\in[n]$ such that the sum of their
point wise product is zero, i.e., $\sum_{j=1}^{d}\prod_{i=1}^{k}a_{i}[j]=0.$

For ease of exposition, we denote $\textsf{OV}(n,d,2)$ and 2-OV by OV(n,d) and
OV respectively.

######  Hypothesis 2 (Orthogonal Vectors Hypothesis (OVH)).

No randomized algorithm can solve k-OV for an instance $\textsf{OV}(n,d,k)$ in
time $O(n^{(k-\epsilon)}\cdot\operatorname{poly}(d))$ for any constant
$\epsilon>0$.

There is an impossibility result from [9] that proves that a reduction under
SETH, and hence under OVH, is not possible unless the following NSETH
conjecture is false.

######  Hypothesis 3 (Non-deterministic SETH (NSETH)).

For every $\epsilon>0$, there exists a $k$ so that k-TAUT is not in
$\textsf{NTIME}[\mathsf{2^{n(1-\epsilon)}}]$, where k-TAUT is the language of
all k-DNF formulas which are tautologies.

The impossibility result [9, Corollary 2] is as follows.

######  Theorem A.2.

If NSETH holds and a problem C
$\in\textsf{NTIME}[\mathsf{T_{C}}]\cap\textsf{coNTIME}[\mathsf{T_{C}}],$ then
for any problem B that is SETH-hard under deterministic reductions with time
$T_{B},$ and $\gamma>0,$ we cannot have a fine-grained reduction B
${}_{(\mathsf{T_{B}})}\\!\\!\preceq_{(\mathsf{c})}$ C where
$c=T_{C}^{(1+\gamma)}.$

We show some of our problems satisfy the conditions of Theorem A.2, and hence
show lower bounds for these conditioned on one of two other hypotheses called
HSH and FOPH($\mathsf{\forall\exists\exists}$), described below.

An instance of the hitting set problem, denoted by HS, is an integer
$d=\omega(\log n)$ and sets $X,Y\subseteq\\{0,1\\}^{d},\ i\in[n]$ such that
$|X|=|Y|=n,$ and denoted by HS(n,d).

######  Problem A.3 (Hitting Sets (HS)).

Given an instance HS(n,d), the HS problem is to decide if there is a vector
$x\in X$ such that for all $y\in Y$ we have $x\cdot y\neq 0,$ or informally,
some vector in $X$ hits all vectors in $Y.$

######  Hypothesis 4 (Hitting Sets Hypothesis (HSH)).

No randomized algorithm can solve HS for an instance HS(n,d) in time
$O(n^{(2-\epsilon)}\cdot\operatorname{poly}(d))$ for any constant
$\epsilon>0.$

HSH implies OVH, but the reverse direction is not known.

Finally we consider a subclass of first order formula over structures of size
$n$ and with $m$ relational tuples [17].

######  Problem A.4 (FO($\mathsf{\forall\exists\exists}$)).

Decide if a given a first-order formula quantified by $\forall\exists\exists$
has a model on a structure of size $n$ with $m$ relational tuples.

It is known that FO($\mathsf{\forall\exists\exists}$) can be solved in
$O(m^{3/2})$ time using ideas from triangle detection algorithms [17]. For
dense structures ($m=\Theta(n^{2}))$, this yields the bound $O(n^{3})$.
Although sub-cubic algorithms might be possible, achieving a truly quadratic
bound seems unlikely or at least highly non-trivial.

##  Appendix B Proofs of Section 3

###  B.1 Proofs from Section 3.1

See 3.1

######  Proof B.1.

($\Rightarrow$) Let
$e_{1}\leq^{\sigma}_{\mathsf{\operatorname{\textsf{HB}}}}e_{2}$. Using the
definition of $\leq^{\sigma}_{\mathsf{\operatorname{\textsf{HB}}}}$, there
must be a sequence of events $f_{1},f_{2}\ldots f_{k}$ with $k>1$,
$f_{1}=e_{1}$, $f_{k}=e_{2}$, and for every $1\leq i<k$,
$f_{i}\leq^{\sigma}_{\mathsf{\operatorname{\textsf{tr}}}}f_{i+1}$ and either
$f_{i}\leq^{\sigma}_{\mathsf{\operatorname{\textsf{TO}}}}f_{i+1}$ or there is
a lock $\ell$, such that $f_{i}\in\mathsf{Releases}_{\sigma}(\ell)$ and
$f_{i+1}\in\mathsf{Acquires}_{\sigma}(\ell)$. Let $j$ be the smallest index
$i$ such that
$\operatorname{\mathsf{tid}}(f_{i})\neq\operatorname{\mathsf{tid}}(f_{i+1})$;
such an index exists as
$\operatorname{\mathsf{tid}}(e_{1})\neq\operatorname{\mathsf{tid}}(e_{2})$.
Observe that there must be a lock $\ell$ for which
$\operatorname{op}(f_{j})=\texttt{rel}(\ell)$ and
$\operatorname{op}(f_{j+1})=\texttt{acq}(\ell)$. Observe that
$pos_{\sigma}(f_{j})<pos_{\sigma}(f_{j+1})$,
$\mathsf{RelLS}^{\sigma}_{e_{1}}(\ell)\leq pos_{\sigma}(f_{j})$ and
$pos_{\sigma}(f_{j+1})\leq\mathsf{AcqLS}^{\sigma}_{e_{2}}$, giving us
$\mathsf{RelLS}^{\sigma}_{e_{1}}(\ell)<\mathsf{AcqLS}^{\sigma}_{e_{2}}(\ell)$.

($\Leftarrow$) Let $\ell$ be a lock such that
$\mathsf{RelLS}^{\sigma}_{e_{1}}(\ell)<\mathsf{AcqLS}^{\sigma}_{e_{2}}(\ell)$.
Then, there is a release event $f$ and an acquire event $g$ on lock $\ell$
such that
$pos_{\sigma}(f)<pos_{\sigma}(g)$,$e_{1}\leq^{\sigma}_{\mathsf{\operatorname{\textsf{HB}}}}f$
and $g\leq^{\sigma}_{\mathsf{\operatorname{\textsf{HB}}}}e_{2}$. This means
$f\leq^{\sigma}_{\mathsf{\operatorname{\textsf{HB}}}}g$ and thus
$e_{1}\leq^{\sigma}_{\mathsf{\operatorname{\textsf{HB}}}}e_{2}$.

For the sake of completeness, we present the computation of release
lockstamps. As with Algorithm 1, we maintain the following variables. For each
thread $t$ and lock $\ell$, we will maintain variables $\mathbb{C}_{t}$ and
$\mathbb{L}_{\ell}$ that take values from the space of all lockstamps. We also
additionally maintain an integer variable $\mathsf{p}_{\ell}$ for each lock
$\ell$ that stores the index (or relative position) of the earliest (according
to the trace order $\leq^{\sigma}_{\mathsf{\operatorname{\textsf{tr}}}}$)
release event of lock $\ell$ in the trace. Initially, we set each
$\mathbb{C}_{t}$ and $\mathbb{L}_{m}$ to $\lambda\ell\cdot\infty$, for each
thread $t$ and lock $m$. Further, for each lock $m$, we set $\mathsf{p}_{m}$
to $n_{m}+1$, where $n_{m}$ is the number of release events of $m$ in the
trace; this can be obtained in a linear scan (or by reading the value of
$\mathsf{p}_{m}$ at the end of a run of Algorithm 1). We traverse the events
according to the total trace order and perform updates to the data structures
as described in Algorithm 4, by invoking the appropriate _handler_ based on
the thread and operation of the event $e=\langle t,op\rangle$ being visited.
At the end of each handler, we assign the lockstamp
$\mathsf{RelLS}^{\sigma}_{e}$ to the event $e$.

1

2 _acquire(_$t$ , $\ell$_)_:

3 $\mathbb{L}_{\ell}\leftarrow\mathbb{C}_{t}$

4 $\mathsf{RelLS}^{\sigma}_{e}\leftarrow\mathbb{C}_{t}$

5 _release(_$t$ , $\ell$_)_:

6 $\mathsf{p}_{\ell}\leftarrow\mathsf{p}_{\ell}-1$

7
$\mathbb{C}_{t}\leftarrow\mathbb{C}_{t}[\ell\mapsto\mathsf{p}_{\ell}]\sqcap\mathbb{L}_{\ell}$

8 $\mathsf{RelLS}^{\sigma}_{e}\leftarrow\mathbb{C}_{t}$

9 _read(_$t$ , $x$_)_:

10 $\mathsf{RelLS}^{\sigma}_{e}\leftarrow\mathbb{C}_{t}$

11 _write(_$t$ , $x$_)_:

12 $\mathsf{RelLS}^{\sigma}_{e}\leftarrow\mathbb{C}_{t}$

Algorithm 4 Assigning release lockstamps to events in the trace

Let us now state the correctness of Algorithm 1 and Algorithm 4.

######  Lemma B.2.

On input trace $\sigma$, Algorithm 1 and Algorithm 4 correctly compute the
lockstamps $\mathsf{AcqLS}^{\sigma}_{e}$ and $\mathsf{RelLS}^{\sigma}_{e}$
respectively for each event $e\in\mathsf{Events}_{\sigma}$.

######  Proof B.3 (Proof Sketch).

We focus on the correctness proof of Algorithm 1; the proof for Algorithm 4 is
similar. The proof relies on the invariant maintained by Algorithm 1 the
variables $\mathbb{C}_{t}$, $\mathbb{L}_{\ell}$ and $\mathsf{p}_{\ell}$ for
each thread $t$ and lock $\ell$, which we state next. Let $\pi$ be the prefix
of the trace processed at any point in the algorithm. Let $C^{\pi}_{t}$,
$L^{\pi}_{\ell}$ and $p^{\pi}_{\ell}$ be the values of the variables
$\mathbb{C}_{t}$, $\mathbb{L}_{\ell}$ and $\mathsf{p}_{\ell}$ after processing
the prefix $\pi$. Then, the following invariants are true:

  * •

$C^{\pi}_{t}=\mathsf{AcqLS}^{\pi}_{e^{\pi}_{t}}=\mathsf{AcqLS}^{\sigma}_{e^{\pi}_{t}}$,
where $e^{\pi}_{t}$ is the last event in $\pi$ performed by thread $t$

  * •

$L^{\pi}_{\ell}=\mathsf{AcqLS}^{\pi}_{e^{\pi}_{\ell}}=\mathsf{AcqLS}^{\sigma}_{e^{\pi}_{\ell}}$,
where $e^{\pi}_{\ell}$ is the last acquire event on lock $\ell$ in $\pi$.

  * •

$p^{\pi}_{\ell}=pos^{\pi}_{\ell}(e^{\pi}_{\ell})$, where $e^{\pi}_{\ell}$ is
the last acquire event on lock $\ell$ in $\pi$.

These invariants can be proved using a straightforward induction, each time
noting the definition of
$\leq^{\sigma}_{\mathsf{\operatorname{\textsf{HB}}}}$.

######  Lemma B.4.

For a trace with $\mathcal{N}$ events and $\mathcal{L}$ locks, Algorithm 1 and
Algorithm 4 both take $O(\mathcal{T}\cdot\mathcal{L})$ time.

######  Proof B.5.

We focus on Algorithm 1; the analysis for Algorithm 4 is similar. At each
acquire event, the algorithm spends $O(1)$ time for updating
$\mathsf{p}_{\ell}$, $O(\mathcal{L})$ time for doing the $\sqcup$ operation,
and $O(\mathcal{L})$ time for the copy operation
(‘$\mathsf{AcqLS}^{\sigma}_{e}\leftarrow\mathbb{C}_{t}$’). For a release
event, we spend $O(\mathcal{L})$ for the two copy operations. At read and
write events, we spend $O(\mathcal{L})$ for copy operations. This gives a
total time of $O(\mathcal{N}\cdot\mathcal{L})$.

See 3.2

######  Proof B.6.

We first prove that if there is a an $\operatorname{\textsf{HB}}$-race in
$\sigma$, then there is a pair of consecutive conflicting events that is in
$\operatorname{\textsf{HB}}$-race. Consider the first
$\operatorname{\textsf{HB}}$-race, i.e., an $\operatorname{\textsf{HB}}$-race
$(e_{1},e_{2})$ such that for every other $\operatorname{\textsf{HB}}$-race
$(e^{\prime}_{1},e^{\prime}_{2})$, either
$e_{2}\leq^{\sigma}_{\mathsf{\operatorname{\textsf{tr}}}}e^{\prime}_{2}$ or
$e_{2}=e^{\prime}_{2}$ and
$e^{\prime}_{1}\leq^{\sigma}_{\mathsf{\operatorname{\textsf{tr}}}}e_{1}$. We
remark that such a race $(e_{1},e_{2})$ exists if $\sigma$ has any
$\operatorname{\textsf{HB}}$-race. We now show that $(e_{1},e_{2})$ are a
consecutive conflicting pair (on variable $x$). Assume on the contrary that
there is an event $f\in\mathsf{Writes}_{\sigma}(x)$ such that
$e_{1}<^{\sigma}_{\mathsf{\operatorname{\textsf{tr}}}}f<^{\sigma}_{\mathsf{\operatorname{\textsf{tr}}}}e_{2}$.
If either $(e_{1},f)$ or $(f,e_{2})$ is an $\operatorname{\textsf{HB}}$-race,
then this contradicts our assumption that $(e_{1},e_{2})$ is the first
$\operatorname{\textsf{HB}}$-race in $\sigma$. Thus,
$e_{1}\leq^{\sigma}_{\mathsf{\operatorname{\textsf{HB}}}}f$ and
$f\leq^{\sigma}_{\mathsf{\operatorname{\textsf{HB}}}}e_{2}$, which gives
$e_{1}\leq^{\sigma}_{\mathsf{\operatorname{\textsf{HB}}}}e_{2}$, another
contradiction.

We now turn our attention to the number of consecutive conflicting events in
$\sigma$. For every read or write event $e_{2}$, there is at most one write
event $e_{1}$ such that $(e_{1},e_{2})$ is a consecutive conflicting pair
(namely the latest conflicting write event before $e_{2}$) Further, for every
read event $e_{1}$, there is at most one write event $e_{2}$ such that
$(e_{1},e_{2})$ is a consecutive conflicting pair (namely the earliest
conflicting write event after $e_{1}$). This gives at most $2\mathcal{N}$
consecutive conflicting pairs of events.

Let us now state the correctness of Algorithm 2.

######  Lemma B.7.

For a trace $\sigma$, Algorithm 2 reports a race iff $\sigma$ has an
$\operatorname{\textsf{HB}}$-race.

######  Proof B.8 (Proof Sketch.).

The proof relies on the following straightforward invariants; we skip their
proofs as they are straightforward. In the following, $e^{\pi}_{x}$ is the
last event with $\operatorname{op}(e^{\pi}_{x})=\texttt{w}(x)$ in a trace
$\pi$.

  * •

After processing the prefix $\pi$ of $\sigma$,
$t^{w}_{x}=\operatorname{\mathsf{tid}}(e^{\pi}_{x})$ and
$\mathbb{W}_{x}=e^{\pi}_{x}$.

  * •

After processing the prefix $\pi$ of $\sigma$, the set $\mathsf{S}_{x}$ is
$\\{(t,L)\,|\,\exists
e\in\mathsf{Reads}_{\pi}(x),e^{\pi}_{x}\leq^{\pi}_{\mathsf{\operatorname{\textsf{tr}}}}e,\operatorname{\mathsf{tid}}(e)=t,\mathsf{RelLS}^{\sigma}_{e}=L\\}$.

The rest of the proof follows from Lemma B.4 and Lemma B.2.

Let us now characterize the time complexity of Algorithm 2.

######  Lemma B.9.

On an input trace with $\mathcal{N}$ events and $\mathcal{L}$ locks, Algorithm
2 runs in time $O(\mathcal{N}\cdot\mathcal{L})$.

######  Proof B.10 (Proof Sketch).

Each pair $(t,L)$ of thread identifier and lockstamp is added atmost once in
some set $\mathsf{S}_{x}$ (for some $x$). Also, each such pair is also
compared against another timestamp atmost once. Each comparison of timestamps
take $O(\mathcal{L})$ time. This gives a total time of
$O(\mathcal{N}\cdot\mathcal{L})$.

See 1.4

######  Proof B.11.

We focus on proving that there is an $O(\mathcal{N}\cdot\mathcal{L})$ time
algorithm, as the standard vector-clock algorithm [19] for checking for an
$\operatorname{\textsf{HB}}$-race runs in $O(\mathcal{N}\cdot\mathcal{T})$
time. Our algorithm’s correctness is stated in Lemma B.7 and its total running
time is $O(\mathcal{N}\cdot\mathcal{L})$ (Lemma B.9 and Lemma B.4).

###  B.2 Proofs from Section 3.2

See 1.1

######  Proof B.12.

Consider a pair of events $\texttt{w}(z)$ from the $d$ threads
$t(x,i),i\in[d],$ and $\texttt{r}(z)\in t_{y}$ for some $x,i,y$. We have
$\texttt{w}(z)\leq^{\sigma}_{\mathsf{\operatorname{\textsf{HB}}}}\texttt{r}(z)$
iff there is some path from $\texttt{w}(z)$ to $\texttt{r}(z)$ in
$\textsf{G}(\leq^{\sigma}_{\mathsf{\operatorname{\textsf{HB}}}})$. As
$\texttt{w}(z)$ and $\texttt{r}(z)$ are in different threads, such a path can
only be through lock events in a sequence of threads such that the first and
last threads are $t(x,i)$ for some $i\in[d]$ and $t_{y}$, and every
consecutive pair of threads in the sequence holds a common lock. Now all the
locks in $t_{y}$ are $l(y,i)$ for all $i$ where $y[i]=1$. Consider the lock
corresponding to any $i\in[d]$. The only thread $t(x^{\prime},i)$ that also
holds this lock corresponds to the last $x^{\prime}$ such that
$x^{\prime}[i]=1$. The only other lock held by $t(x^{\prime},i)$ is $l_{i}.$
If $\texttt{w}(z)$ is in $t(x^{\prime},i),$ we are done. Otherwise the only
common lock between these threads $t(x^{\prime},i)$ and those of
$\texttt{w}(z)$ can be one of the $l_{i}$. The threads of $\texttt{w}(z)$
contain all $l_{i}$ where $x[i]=1.$ Hence, for there to be a common lock
between these threads, there must be at least one $i$ such that
$x^{\prime}[i]=1$ and $x[i]=1$. As this thread also has the lock $l(y,i),$
$y[i]$ is also $1$.

Thus, there is a path from $\texttt{w}(z)$ to $\texttt{r}(z)$ if and only if
there is at least one $i\in[d]$ such that $x[i]=y[i]=1,$ hence $x$ and $y$ are
not orthogonal. A pair of orthogonal vectors of OV thus corresponds to a
write-read $\operatorname{\textsf{HB}}$-race in the reduced trace.

Finally we turn our attention to the complexity. In time $O(n\cdot d),$ we
have reduced an OV instance to determining whether there is a write-read
$\operatorname{\textsf{HB}}$ race in a trace of $\mathcal{N}=O(nd)$ events. If
there was a sub-quadratic i.e. $O((n\cdot
d)^{(2-\epsilon)})=n^{(2-\epsilon)}\cdot\operatorname{poly}(d)$ algorithm for
detecting a write-read $\operatorname{\textsf{HB}}$ race, then this would also
solve OV in $n^{(2-\epsilon)}\cdot\operatorname{poly}(d)$ time, refuting the
OV hypothesis.

See 3.5

######  Proof B.13.

For intuition, assume the first order property is on an undirected graph with
$n$ variables and $m$ edges. Let the property be specified in quantified
$3$-DNF form with a constant number of predicates, i.e., $\phi=\forall
x\exists y\exists z\ (\psi_{1}\vee\psi_{2}\vee\dotsc\psi_{k}),$ where $x,y,z$
represent nodes of the graph, and each $\psi_{i}$ is a conjunction of $3$
variables representing edges of the graph, for example $e(x,y)\wedge\neg
e(y,z)\wedge e(x,z)$. The property is then true if and only if some predicate
is satisfied, which is true if all of its variables are satisfied ($e(x,y)$ is
satisfied when edge $(x,y)$ is in the graph). Denote the graph on which $\phi$
is defined by $H(I,J),$ where $I$ and $J$ are respectively the sets of nodes
and edges of $H.$

The instance of MCONN is constructed given $H$ and $\phi$ as follows.
Construct a $(2k+2)$-partite graph $G(V,E)$ by first creating $2k+2$ copies of
$I.$ Denote these copies by $S,Y_{i},Z_{i},T,\ i\in[k],$ and the copy of each
node $x\in I$ in any part, say $S,$ by $x(S).$ $\psi_{i}=(e_{1}\wedge
e_{2}\wedge e_{3})$ is encoded by connecting the sets $(S,Y_{i})$ to represent
$e_{1}$, $(Y_{i},Z_{i})$ for $e_{2}$ and $(Z_{i},T)$ for $e_{3}$ as follows.
If $e_{i}$ is of the form $e(x,y)$ (and not its negation), then draw a copy of
$H$ between its corresponding sets, say $S$ and $Y_{i}$ without loss of
generality. That is, for every $x,y,$ $(x,y)\in
J\Leftrightarrow(x(S),y(Y_{i}))\in E$. If on the other hand $e_{i}$ is of the
form $\neg e(x,y)$ then connect a copy of the complement of $H$, i.e.,
$(x,y)\notin J\Leftrightarrow(x(S),y(Y_{i}))\in E.$

Finally define $|I|$ pairs $(x(S),x(T))$ as the $(s,t)$ pairs for MCONN.

We now prove this reduction is correct. First, assume $\phi$ is true. Then for
every node $x,$ there exist nodes $y,z$ such that some predicate is true. If
$\psi_{i}$ is the predicate that is satisfied for some node $u,$ then there is
a path between $u(S)$ and $u(T)$ through the parts $S,Y_{i},Z_{i}$ and $T$ as
follows. As the first variable is satisfied, then if it is $e(x,y),$ then
$(x,y)\in J,$ and $x(S)$ is connected to $y(Y_{i}),$ and if it is $\neg
e(x,y),$ then $(x,y)\notin J$ and again $x(S)$ is connected to $y(Y_{i}).$
Similarly, $y(Y_{i})$ is connected to $z(Z_{i}),$ and $z(Z_{i})$ to $x(T).$
These edges form a $3$ length path between $x(S)$ and $x(T)$.

Now consider the reverse case, and assume the MCONN problem is true, that is ,
there is a path between every $(x(S),x(T))$ pair. Note that the construction
of edges in $G$ is such that any path from $x(S)$ to $x(T)$ has to be a $3$
length path, connecting the copy of $x$ in $S$ to its copy in some $Y_{i},$
from this $Y_{i}$ to its corresponding $Z_{i},$ and from $Z_{i}$ to $T.$ Also,
this path exists only if all variables of the corresponding $\psi_{i}$ are
true. Hence, as there is a path between every pair $(x(S),x(T)),$ and one pair
is defined for every variable $x,$ some predicate is satisfied for every $x.$
Thus $\phi$ is also true.

Finally, the time of the reduction is equal to the size of $G.$ This is
$2k+2=O(1)$ graphs, each of which is either $H$ or its complement. Hence
$|G|=O(m+n+(n^{2}-m)+n)=O(n^{2}).$

See 1.3

######  Proof B.14.

We first reduce the instance of FO($\mathsf{\forall\exists\exists}$) to MCONN
as in the proof of Lemma 3.5. Let $G(V,E)$ be the multi-partite graph for
MCONN and $S,T$ the first and last parts of nodes of $G$. We add a sufficient
number of nodes, referred as dummy nodes, to make G sparse. Let every node $x$
of $V\backslash T$ correspond to a distinct thread $t_{x}$ and form one write
access event to a distinct variable $v_{x}$ in the thread. Let each node $t$
in $T$ also correspond to a write access event of the variable corresponding
to the copy of $t$ in $S,$ and be in a new thread. Define $|E|$ locks, and for
every edge $(a,b)\in E,$ let the events corresponding to $v_{a}$ and $v_{b}$
hold the lock $l_{(a,b)}$ corresponding to $(a,b).$ The trace $\sigma$ for
first lists all threads corresponding to the dummy nodes in some fixed
arbitrary order, then the threads corresponding to nodes in $S,$ followed by
those in each $Y_{i},$ followed by those in each $Z_{i},$ in a fixed arbitrary
order, and finally those in $T$.

This reduction is seen to be correct by observing that $G$ was modified to be
the transitive reduction graph of $\sigma,$ and the only
$\operatorname{\textsf{HB}}$-race events can be the pairs of write events
corresponding to the pairs of nodes given as input to MCONN. Thus, each pair
of events does not form an $\operatorname{\textsf{HB}}$-race if and only if
$G$ has a path between its corresponding pair of nodes.

To analyze the time of the reduction, first we see that the size of $\sigma$
is the size of $G,$ with dummy nodes added to have $n=O(n^{2}),$ and hence
$O(n^{2}).$ There are $O(n^{2})$ variables, locks and threads in $\sigma.$ If
deciding if the given trace has an $\operatorname{\textsf{HB}}$-race has an
$O((n^{2})^{1+\epsilon})$ time algorithm, then
FO($\mathsf{\forall\exists\exists}$) can be solved in
$O(n^{2+\epsilon^{\prime}})$ time, which is $O(m^{1+\epsilon^{\prime}})$ time
for properties on dense structures.

##  Appendix C Proofs of Section 4

12dAux$t^{1}$$t^{2}$$t^{3}$ $A_{3}$ has $d+1$ threads. Events encoding
$z_{i}[k]$ interleaved with the $i^{th}$ sync events in thread $k$ $A_{3}$ $n$
threads each for $A_{1}$ and $A_{2}.$ Each thread has two parts. • $t_{x}^{1}$
and $t_{y}^{1}:$ events encoding vectors $x$ and $y.$ • $t_{x}^{2}$ and
$t_{y}^{2}:$ possible racy events.
$A_{1}$$t_{x}^{1}$$\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}t_{x}^{2}$$A_{2}$$t_{y}^{1}$$\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}t_{y}^{2}$
Nodes are sync events, lines are threads. • Red node $t^{3}$: If $t^{3}$ not
in reordering there is a race between $t_{x}^{2}$ and $t_{y}^{2}$. • Round
nodes: force us to add all $Z$ if we include possible race events. • square
nodes: force adding events of a $z$ from all threads, if we include any.
Figure 7: Intuition for the reduction from 3-OV to sync-preserving race
detection. Thread Aux allows forming a trace such that 3-OV has a solution iff
there is a sync-preserving race.

See 1.5

######  Proof C.1.

Consider any sync-preserving correct reordering $\rho$ of $\sigma$ that
exposes a data race $(\texttt{w}(z),\texttt{r}(z))$ on the local traces
$t_{x}$ and $t_{y}$. The following statements are straightforward to verify
based on the definition of sync-preserving correct reorderings.

  1. 1.

For every $k\in[d]$, the first $\texttt{sync}(\ell_{k})$ event the trace
$t_{k}$ is also in $\rho$.

  2. 2.

The auxiliary trace $t$ cannot have an open critical section in $\rho$. This
implies that for every trace $t_{k}$ with $k\in[d]$, the last event of $t_{k}$
in $\rho$ cannot be its $i^{th}$ $\texttt{sync}(\ell_{k})$ event, where $i$ is
even. Moreover, the number of $\texttt{sync}(\ell_{k})$ events in $\rho$ is
the same for every trace $t_{k}$ with $k\in[d]$.

First, consider that the 3-OV instance has a solution, i.e., there exist $x\in
A_{1}$, $y\in A_{2}$ and $z\in A_{3}$ such that $x,y,z$ are orthogonal, and we
argue that $\sigma$ has a data race that is also sync-preserving. We construct
a sync-preserving correct reordering $\rho$ of $\sigma$ that exposes the data
race. We only specify the local traces that exist in $\rho$, as their
interleaving that constructs $\rho$ will be identical to the one in $\sigma$
(in other words, we only specify the prefix up to which every local trace of
$\sigma$ is executed in $\rho$). We execute the traces $t_{x}$ and $t_{y}$ all
the way before the corresponding $\texttt{w}(z)$ and $\texttt{r}(z)$ events
(hence we are exposing a race between these two events). For every $k\in[d]$
if $z[k]=0$ or $x[k]=0$, we execute $t_{k}$ up to the $(2\cdot i)^{th}$
$\texttt{sync}(\ell_{k})$ event, where $i$ is such that $z$ is the $i^{th}$
vector of $A_{3}$. On the other hand, if $y[k]=0$, we execute $t_{k}$ up to
the first $\texttt{rel}(\ell_{k})$ event that appears after the $(2\cdot
i)^{th}$ $\texttt{sync}(\ell_{k})$ event in $t^{k}$. Finally, we execute
$t^{k}$ until its $(i-1)^{th}$ $\texttt{rel}(X)$ event.

It is easy to verify that $\rho$ is a valid correct reordering. Indeed, we
have two open critical sections in the threads $t_{x}$ and $t_{y}$, on the
locks $X$ and $Y$ respectively. Moreover, for every $k\in[d]$, we have the
following.

  1. 1.

If $z[k]=0$, there are no other open critical sections.

  2. 2.

If $z[k]=1$ and $x[k]=0$, there is one open critical section in the thread
$z[k]$ on lock $l_{k}$.

  3. 3.

If $z[k]=x[k]=1$ and $y[k]=0$, there is one open critical section in the
thread $z[k]$ on lock $l^{\prime}_{k}$.

We now consider the opposite direction, i.e., assume that there is a sync-
preserving race in $\sigma$, and we argue that there exist $x\in A_{1}$, $y\in
A_{2}$ and $z\in A_{3}$ such that $x,y,z$ are orthogonal. Consider any sync-
preserving correct reordering $\rho$ that exposes a race on the access events
of two local traces $t_{x}$ and $t_{y}$. Because of Item 1 above, every trace
$t_{k}$ is at least partially present in $\rho$. Because of Item 1 above,
every such trace executes the same number of $\texttt{sync}(\ell_{k})$ events
in $\rho$, and this number is odd. We argue that the triplet $x,y,z$ is
orthogonal, where $z$ is the $i^{th}$ vector of $A_{3}$ such that each $t_{k}$
executes $2\cdot(i-1)+1$ $\texttt{sync}(\ell_{k})$ events in $\rho$. Indeed,
consider any $k\in[d]$ and assume that $x[k]=y[k]=1$. If $z[k]=1$, then we
have a $\texttt{acq}(\ell)$ event in $t_{k}$ that immediately precedes its
last $\texttt{sync}(\ell_{k})$ event. Since $x[k]=1$, the trace $t_{x}$ also
has an $\texttt{acq}(l_{k})$ event. Since the $\texttt{acq}(l_{k})$ event of
$t_{x}$ is after the $\texttt{acq}(l_{k})$ event of $t_{k}$ in $\sigma$, the
matching $\texttt{rel}(l_{k})$ of $t_{k}$ must also be in $\rho$. This implies
that the $\texttt{acq}(l^{\prime}_{k})$ event of $t_{k}$ that immediately
succeeds its last $\texttt{rel}(l_{k})$ event is also in $\rho$. Since
$y[k]=1$, the trace $t_{y}$ also has an $\texttt{acq}(l^{\prime}_{k})$ event.
Since the $\texttt{acq}(l^{\prime}_{k})$ event of $t_{y}$ is after the
$\texttt{acq}(l^{\prime}_{k})$ event of $t_{k}$ in $\sigma$, the matching
$\texttt{rel}(l^{\prime}_{k})$ of $t_{k}$ must also be in $\rho$. However, we
now have another $\texttt{sync}(\ell_{k})$ event of $t_{k}$ in $\rho$, in
particular, the $\texttt{sync}(\ell_{k})$ event that immediately precedes its
last $\texttt{rel}(l^{\prime}_{k})$ event. But this results in an even number
of $\texttt{sync}(\ell_{k})$ events of $t_{x}$ being present in $\rho$, which
contradicts our observation in Item 2. Thus, if $x[k]=y[k]=1$, we necessarily
have that $z[k]=0$, and the triplet $x,y,z$ is orthogonal.

The desired result follows.

##  Appendix D Proofs of Section 5

See 1.6

######  Proof D.1 (Proof of Theorem 1.6).

To see why the reduction is correct, observe that if there a solution to OV,
that is, a pair of vectors $x,y$ such that for all $k\in[d],$ $x[k]=0$ or
$y[k]=0,$ implies that the corresponding events in $\sigma,$ say $e_{x}$ and
$e_{y},$ have for each lock $k\in[d]$ either $e_{x}$ does not hold the lock or
$e_{y}$ does not. As they have distinct thread ids too, $e_{x}$ and $e_{y}$
form two conflicting events with
$\mathsf{locksHeld}_{\sigma}(e_{1})\cap\mathsf{locksHeld}_{\sigma}(e_{2})=\varnothing.$
Similarly, a lock-cover race implies that for every lock, one of the events in
race do not hold the lock, hence have their corresponding coordinate in OV
$0.$ The events are thus orthogonal to each other.

Regarding the complexity, we have used $O(n\cdot d)$ time to construct a trace
$\sigma$ with $\mathcal{N}=O(n\cdot d)$ events. If we can detect a lock-cover
race in $\sigma$ in $O(\mathcal{N}^{(2-\epsilon)})$ time, then OV can be
solved in $O(n^{(2-\epsilon)}\cdot\operatorname{poly}(d))$ time, contradicting
the OV hypothesis.

See 1.9

######  Proof D.2.

We first argue that the algorithm maintains the invariant stated in Equation
2. The invariant for $A$ is trivial to verify. Moreover, it is easy to see
that, assuming that the invariant holds before processing an
$\texttt{acq}(\ell)$ or $\texttt{rel}(\ell)$ event, it also holds after
processing that event. Indeed, for an event $\texttt{acq}(\ell)$, we have
$\ell\in A$, and to maintain $C=\overline{A}\cap B$, we remove $\ell$ from $C$
if $\ell\in B$. Similarly for an event $\texttt{rel}(\ell)$. To see that the
invariant is maintained after processing an access event
$\texttt{w}(x)/\texttt{r}(x)$, note that we have

$B\setminus
C=B\cap\overline{C}=B\cap\left(\overline{B\cap\overline{A}}\right)=B\cap\left(\overline{B}\cup
A\right)=B\cap A$

and thus updating $B\leftarrow B\setminus C$ yields

$\mathsf{Locks}_{\sigma}\cap\bigcap_{\begin{subarray}{c}e^{\prime}\in\mathsf{Accesses}_{\sigma}(x)\\\
e^{\prime}<^{\sigma}_{\mathsf{\operatorname{\textsf{tr}}}}e\end{subarray}}\mathsf{locksHeld}_{\sigma}(e^{\prime})\cap\mathsf{locksHeld}_{tr}(e)=\mathsf{Locks}_{\sigma}\cap\bigcap_{\begin{subarray}{c}e^{\prime}\in\mathsf{Accesses}_{\sigma}(x)\\\
e^{\prime}\leq^{\sigma}_{\mathsf{\operatorname{\textsf{tr}}}}e\end{subarray}}\mathsf{locksHeld}_{\sigma}(e^{\prime})$

Finally, at this point we have $\overline{A}\cap B=\overline{A}\cap B\cap
A=\varnothing$, thus the invariant also holds for $C$.

We now turn our attention to complexity. Using a bit-set representation of the
sets $A$, $B$ and $C$, it is clear that each of the operations except
$\texttt{w}(x)/\texttt{r}(x)$ take constant time per event. Each
$\texttt{w}(x)/\texttt{r}(x)$ operation takes $O(|C|)$ time. Note, however,
that because of the previous invariant, every lock is removed from $B$ at most
once, hence the total time for performing all set differences $B\leftarrow
B\setminus C$ is $O(\mathcal{N}+\mathcal{L})=O(\mathcal{N})$. Thus the total
time is $O(\mathcal{N})$. The desired result follows.

See 1.8

######  Proof D.3.

First, assume there is a solution to HS, i.e., $\exists x_{k}\in X\ \forall
y_{i}\in Y\ \exists j\in[d]\ x_{k}[j]=y_{i}[j]=1$. Then for the variable
$z_{k}$, for every lock $\ell_{i}$, there is a thread $t_{j}$ that contains
$\texttt{w}(z_{k})$ (as $x_{k}[j]=1$) but does not contain lock $\ell_{i}$ (as
$y_{i}[j]=1$). Thus
$\bigcap_{e\in\mathsf{Accesses}_{\sigma}(z_{k})}\mathsf{locksHeld}_{\sigma}(e)=\varnothing$,
and we have a lock-set race on variable $z_{k}$ as there are at least two
$\texttt{w}(z_{k})$ conflicting events, one in the thread $t_{j}$ and the
other in thread $t_{0}$. For the opposite direction, assume that HS does not
have a solution, i.e., $\forall x_{k}\in X\ \exists y_{i}\in Y\ \forall
j\in[d]\ (x_{k}[j]=0\text{ or }y_{i}[j]=0)$. Then for each variable $z_{k}$,
there is some lock $\ell_{i}$ such that every thread that contains a write
event $\texttt{w}(z_{k})$ (thus $x_{k}[j]=1$) also contains the lock
$\ell_{i}$ (as necessarily $y_{i}[j]=0$). Hence, for every variable $z_{k},$
some lock $\ell_{i}$ is held by all its access events. Thus $\sigma$ does not
have a lock-set race.

Regarding the complexity, we have created a trace $\sigma$ with
$\mathcal{N}=O(n\cdot d)$ events in $O(n\cdot d)$ time. Thus, any
$O(\mathcal{N}^{(2-\epsilon)})$ time algorithm for HS implies an
$O(n^{(2-\epsilon)}\cdot\operatorname{poly}(d))$ time algorithm for HS,
contradicting the HS hypothesis.