1 pldi arxiv

# Sound Dynamic Deadlock Prediction in Linear Time

Hünkar Can Tunç  0000-0001-9125-8506 Aarhus UniversityDenmark<EMAIL_ADDRESS>,
Umang Mathur  0000-0002-7610-0660 National University of SingaporeSingapore
<EMAIL_ADDRESS>,  Andreas Pavlogiannis  0000-0002-8943-0722 Aarhus
UniversityDenmark<EMAIL_ADDRESS>and  Mahesh Viswanathan
0000-0001-7977-0080 University of Illinois, Urbana ChampaignUSA
<EMAIL_ADDRESS>
(2023; 2022-11-10; 2023-03-31)

###### Abstract.

Deadlocks are one of the most notorious concurrency bugs, and significant
research has focused on detecting them efficiently. _Dynamic predictive
analyses_ work by observing concurrent executions, and reason about
alternative interleavings that can witness concurrency bugs. Such techniques
offer scalability and sound bug reports, and have emerged as an effective
approach for concurrency bug detection, such as data races. Effective dynamic
deadlock prediction, however, has proven a challenging task, as no deadlock
predictor currently meets the requirements of _soundness_ , _high-precision_ ,
and _efficiency_.

In this paper, we first formally establish that this tradeoff is unavoidable,
by showing that (a) sound and complete deadlock prediction is intractable, in
general, and (b) even the seemingly simpler task of determining the presence
of _potential_ deadlocks, which often serve as unsound witnesses for actual
predictable deadlocks, is intractable. The main contribution of this work is a
new class of predictable deadlocks, called _sync(hronization)-preserving_
deadlocks. Informally, these are deadlocks that can be predicted by reordering
the observed execution while preserving the relative order of conflicting
critical sections. We present two algorithms for _sound_ deadlock prediction
based on this notion. Our first algorithm SPDOffline detects all sync-
preserving deadlocks, with running time that is linear per _abstract deadlock
pattern_ , a novel notion also introduced in this work. Our second algorithm
SPDOnline predicts all sync-preserving deadlocks that involve two threads in a
_strictly online_ fashion, runs in overall linear time, and is better suited
for a runtime monitoring setting.

We implemented both our algorithms and evaluated their ability to perform
offline and online deadlock-prediction on a large dataset of standard
benchmarks. Our results indicate that our new notion of sync-preserving
deadlocks is highly effective, as (i) it can characterize the vast majority of
deadlocks and (ii) it can be detected using an online, sound, complete and
highly efficient algorithm.

concurrency, runtime analyses, predictive analyses

††copyright: rightsretained††doi: 10.1145/3591291††journalyear:
2023††submissionid: pldi23main-p578-p††journal: PACMPL††journalvolume:
7††journalnumber: PLDI††article: 177††publicationmonth: 6††ccs: Software and
its engineering Software verification and validation††ccs: Theory of
computation Theory and algorithms for application domains††ccs: Theory of
computation Program analysis

##  1\. Introduction

The verification of concurrent programs is a major challenge due to the non-
deterministic behavior intrinsic to them. Certain scheduling patterns may be
unanticipated by the programmers, which may then lead to introducing
concurrency bugs. Such bugs are easy to introduce during development but can
be very hard to reproduce during in-house testing, and have been notoriously
called _heisenbugs_ (Musuvathi et al., 2008). Among the most notorious
concurrency bugs are deadlocks, occurring when the system blocks its execution
because each thread is waiting for another thread to finish a task in a
circular fashion. Deadlocks account for a large fraction of concurrency bugs
in the wild across various programming languages (Lu et al., 2008; Tu et al.,
2019) while they are often introduced accidentally when fixing other
concurrency bugs (Yin et al., 2011).

Deadlock-detection techniques can be broadly classified into static and
dynamic techniques. As usual, static techniques analyze source code and have
the potential to prove the absence of deadlocks (Naik et al., 2009; Ng and
Yoshida, 2016; Liu et al., 2021). However, as static analyses face
simultaneously two dimensions of non-determinism, namely in inputs and
scheduling, they lead to poor performance in terms of scalability and false
positives, and are less suitable when the task at hand is to help software
developers proactively find bugs. Dynamic analyses, on the other hand, have
the more modest goal of discovering deadlocks by analyzing program executions,
allowing for better scalability and few (or no) false positives. Although
dynamic analyses cannot prove the absence of bugs, they offer _statistical_
and _coverage_ guarantees. These advantages have rendered dynamic techniques a
standard practice in principled testing for various bugs, such as data races,
atomicity violations, deadlocks, and others (Flanagan and Freund, 2009;
Serebryany and Iskhodzhanov, 2009; Bensalem and Havelund, 2005; Flanagan et
al., 2008; Mathur and Viswanathan, 2020; Biswas et al., 2014; Savage et al.,
1997; Pozniansky and Schuster, 2003). A recent trend in this direction
advocates for _predictive analysis_ (Smaragdakis et al., 2012; Huang et al.,
2014; Kini et al., 2017; Flanagan et al., 2008; Huang, 2018; Kalhauge and
Palsberg, 2018; Genç et al., 2019), where the goal is to enhance coverage by
additionally reasoning about alternative reorderings of the observed execution
trace that _could_ have taken place and also manifest the bug.

Due to the difficulty of the problem, many dynamic deadlock analyses focus on
detecting _deadlock patterns_ , broadly defined as cyclic lock-acquisition
patterns in the observed execution trace. One of the earliest works in this
direction is the Goodlock algorithm (Havelund, 2000). As deadlock patterns are
necessary but insufficient conditions for the presence of deadlocks,
subsequent work has focused on refining this notion in order to reduce false-
positives (Bensalem and Havelund, 2005; Agarwal et al., 2006). Further
techniques reduce the size of the lock graph to improve scalability (Cai and
Chan, 2012; Cai et al., 2020). To further address the unsoundness (false
positives) problem, various works propose controlled-scheduling techniques
that attempt to realize deadlock warnings via program re-execution (Bensalem
et al., 2006; Joshi et al., 2009; Samak and Ramanathan, 2014b, a; Sorrentino,
2015) and exhaustive exploration of all reorderings (Joshi et al., 2010; Sen
et al., 2005).

Fully sound deadlock prediction has traditionally relied on explicitly (Joshi
et al., 2010; Sen et al., 2005) or symbolically (SMT-based) (Eslamimehr and
Palsberg, 2014; Kalhauge and Palsberg, 2018) producing all sound witness
reorderings. The heavyweight nature of such techniques limits their
applicability to executions of realistic size, which is often in the order of
millions of events. The first steps for sound, polynomial-time deadlock
prediction were made recently with SeqCheck (Cai et al., 2021), an extension
of M2 (Pavlogiannis, 2019) that targets data races.

This line of work highlights the need for a most-efficient sound deadlock
predictor, approaching the golden standard of _linear time_. Moreover, dynamic
analyses are often employed as runtime monitors, and must thus operate
_online_ , reporting bugs as soon as they occur. Unfortunately, most existing
online algorithms only report _deadlock patterns_ , thus suffering false
positives. The lack of such a deadlock predictor is even more pronounced when
contrasted to the problem of dynamic race prediction, which has seen a recent
surge of sound, online, _linear-time_ predictors (e.g., (Kini et al., 2017;
Roemer et al., 2020)), and highlights the bigger challenges that deadlocks
entail. We address these challenges in this work, by presenting the first
high-precision, sound dynamic deadlock-prediction algorithm that works online
and in linear time.

The task of checking if a potential deadlock is a real predictable deadlock,
in general, involves searching for the reordering of the original execution
that witnesses the deadlock. The first ingredient towards our technique is the
notion of _synchronization-preserving reorderings_ (Mathur et al., 2021) that
help systematize this search space. _Synchronization-preserving deadlocks_ are
then those predictable deadlocks that can be witnessed in some
synchronization-preserving reordering. We illustrate synchronization-
preserving deadlocks using an example in Section 1.1.

This notion of synchronization-preservation, by itself, is not sufficient when
it comes to deadlock detection as the prerequisite step towards predicting
deadlocks also involves identifying _potential deadlock patterns_. Unlike data
races, where _potential races_ can be identified in polynomial-time, the
identification of deadlock patterns is in general, intractable; we prove this
in Section 3. As a result, an approach that works by explicitly enumerating
cycles in a _lock graph_ and then checking if any of these cycles is
realizable to a deadlock is likely to be not scalable. To tackle this, we
propose the novel notion of _abstract deadlock patterns_ which, informally,
represent clusters of deadlock patterns of the same signature. Intuitively, a
set of deadlock patterns have the same signature if the threads and locks that
participate in the patterns are the same. Our next _key observation_ is that a
single abstract deadlock pattern can be checked for sync-preserving deadlocks
in _linear total time_ in the length of the execution, _regardless_ of how
many concrete deadlock patterns it represents. Our first deadlock prediction
algorithm SPDOffline builds upon this — it enumerates all abstract deadlock
patterns in a first phase and then checks their realizability in a second
phase, while running in linear time per abstract deadlock pattern. Since the
number of abstract deadlock patterns is typically _far smaller_ than the
number of (concrete) deadlock patterns (see Table 1 in Section 6), this
approach achieves high scalability. Our second algorithm SPDOnline works in a
single streaming pass — it computes abstract deadlock patterns that involve
only two threads and checks their realizability _on-the-fly_ simultaneously in
overall linear time in the length of the execution.

###  1.1. Synchronization-Preserving Deadlocks

$t_{1}$$t_{2}$$1$
$\mathtt{acq}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\ell_{1}})$$2$
$\mathtt{\bf
acq}({\color[rgb]{0.24,0.24,0.24}\definecolor[named]{pgfstrokecolor}{rgb}{0.24,0.24,0.24}\pgfsys@color@gray@stroke{0.24}\pgfsys@color@gray@fill{0.24}\ell_{2}})$$3$
$\mathtt{w}(x)$$4$
$\mathtt{rel}({\color[rgb]{0.24,0.24,0.24}\definecolor[named]{pgfstrokecolor}{rgb}{0.24,0.24,0.24}\pgfsys@color@gray@stroke{0.24}\pgfsys@color@gray@fill{0.24}\ell_{2}})$$5$
$\mathtt{rel}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\ell_{1}})$$6$
$\mathtt{acq}({\color[rgb]{0.24,0.24,0.24}\definecolor[named]{pgfstrokecolor}{rgb}{0.24,0.24,0.24}\pgfsys@color@gray@stroke{0.24}\pgfsys@color@gray@fill{0.24}\ell_{2}})$$7$
$\mathtt{r}(x)$$8$ $\mathtt{\bf
acq}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\ell_{1}})$$9$
$\mathtt{rel}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\ell_{1}})$$10$
$\mathtt{rel}({\color[rgb]{0.24,0.24,0.24}\definecolor[named]{pgfstrokecolor}{rgb}{0.24,0.24,0.24}\pgfsys@color@gray@stroke{0.24}\pgfsys@color@gray@fill{0.24}\ell_{2}})$

(a) A trace $\sigma_{1}$ with no
predictable deadlock.

$t_{1}$$t_{2}$$t_{3}$$t_{4}$$1$
$\mathtt{acq}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\ell_{1}})$$2$
$\mathtt{rel}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\ell_{1}})$$3$
$\mathtt{acq}({\color[rgb]{0.24,0.24,0.24}\definecolor[named]{pgfstrokecolor}{rgb}{0.24,0.24,0.24}\pgfsys@color@gray@stroke{0.24}\pgfsys@color@gray@fill{0.24}\ell_{2}})$$4$
$\mathbf{\mathtt{\bf
acq}({\color[rgb]{0.354,0.354,0.354}\definecolor[named]{pgfstrokecolor}{rgb}{0.354,0.354,0.354}\pgfsys@color@gray@stroke{0.354}\pgfsys@color@gray@fill{0.354}\ell_{3}})}$$5$
$\mathtt{w}(z)$$6$
$\mathtt{rel}({\color[rgb]{0.354,0.354,0.354}\definecolor[named]{pgfstrokecolor}{rgb}{0.354,0.354,0.354}\pgfsys@color@gray@stroke{0.354}\pgfsys@color@gray@fill{0.354}\ell_{3}})$$7$
$\mathtt{rel}({\color[rgb]{0.24,0.24,0.24}\definecolor[named]{pgfstrokecolor}{rgb}{0.24,0.24,0.24}\pgfsys@color@gray@stroke{0.24}\pgfsys@color@gray@fill{0.24}\ell_{2}})$$8$
$\mathtt{acq}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\ell_{1}})$$9$
$\mathtt{w}(y)$$10$ $\mathtt{r}(z)$

$t_{1}$$t_{2}$$t_{3}$$t_{4}$$11$$\mathtt{rel}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\ell_{1}})$$12$$\mathtt{acq}({\color[rgb]{0.354,0.354,0.354}\definecolor[named]{pgfstrokecolor}{rgb}{0.354,0.354,0.354}\pgfsys@color@gray@stroke{0.354}\pgfsys@color@gray@fill{0.354}\ell_{3}})$$13$$\mathtt{w}(x)$$14$$\mathtt{r}(y)$$15$$\mathtt{rel}({\color[rgb]{0.354,0.354,0.354}\definecolor[named]{pgfstrokecolor}{rgb}{0.354,0.354,0.354}\pgfsys@color@gray@stroke{0.354}\pgfsys@color@gray@fill{0.354}\ell_{3}})$$16$$\mathtt{acq}({\color[rgb]{0.354,0.354,0.354}\definecolor[named]{pgfstrokecolor}{rgb}{0.354,0.354,0.354}\pgfsys@color@gray@stroke{0.354}\pgfsys@color@gray@fill{0.354}\ell_{3}})$$17$$\mathtt{r}(x)$$18$$\mathtt{\bf
acq}({\color[rgb]{0.24,0.24,0.24}\definecolor[named]{pgfstrokecolor}{rgb}{0.24,0.24,0.24}\pgfsys@color@gray@stroke{0.24}\pgfsys@color@gray@fill{0.24}\ell_{2}})$$19$$\mathtt{rel}({\color[rgb]{0.24,0.24,0.24}\definecolor[named]{pgfstrokecolor}{rgb}{0.24,0.24,0.24}\pgfsys@color@gray@stroke{0.24}\pgfsys@color@gray@fill{0.24}\ell_{2}})$$20$$\mathtt{rel}({\color[rgb]{0.354,0.354,0.354}\definecolor[named]{pgfstrokecolor}{rgb}{0.354,0.354,0.354}\pgfsys@color@gray@stroke{0.354}\pgfsys@color@gray@fill{0.354}\ell_{3}})$

(b) A trace $\sigma_{2}$ with a sync-preserving deadlock, stalling $t_{2}$ on
$e_{4}$ and $t_{3}$ on $e_{18}$.

Figure 1.  Traces with no predictable deadlock (1(a)), and with a sync-
preserving deadlock (1(b)).

Consider the trace $\sigma_{1}$ in Figure 1(a) consisting of $10$ events and
two threads. We use $e_{i}$ to denote the $i$-th event of $\sigma_{1}$. The
events $e_{2}$ and $e_{8}$ form a _deadlock pattern_ : they respectively
acquire the locks
${\color[rgb]{0.24,0.24,0.24}\definecolor[named]{pgfstrokecolor}{rgb}{0.24,0.24,0.24}\pgfsys@color@gray@stroke{0.24}\pgfsys@color<EMAIL_ADDRESS>and
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\ell_{1}}$
while holding the locks
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\ell_{1}}$
and
${\color[rgb]{0.24,0.24,0.24}\definecolor[named]{pgfstrokecolor}{rgb}{0.24,0.24,0.24}\pgfsys@color@gray@stroke{0.24}\pgfsys@color<EMAIL_ADDRESS>and no common lock protects these operations.

A deadlock pattern is a necessary but insufficient condition for an actual
deadlock: a sound algorithm must examine whether it can be realized to a
deadlock via a witness. A witness is a reordering $\rho$ of (a slice of)
$\sigma_{1}$ that is also a valid trace, and such that $e_{2}$ and $e_{8}$ are
locally enabled in their respective threads at the end of $\rho$. In general,
the problem of checking if a deadlock pattern can be realized is intractable
(Theorem 3.3). In this work we focus on checking whether a given deadlock
pattern forms a _sync-preserving deadlock_ , which is a subclass of the class
of all predictable deadlocks.

A deadlock pattern is said to be sync-preserving deadlock if it can be
witnessed in a _sync-preserving reordering_. A reordering $\rho^{\sf SP}$ of a
trace $\sigma$ is said to be sync-preserving if it preserves the control flow
taken by the original observed trace $\sigma$, and further it preserves the
mutual order of any two critical sections (on the same lock) that appear in
the reordering $\rho^{\sf SP}$. Consider, for example, the sequence
$\rho_{1}=e_{1}..e_{3}\,e_{6}..e_{7}$ where $e_{i}..e_{j}$ denote the
contiguous sequence of events that starts from $e_{i}$ and ends at $e_{j}$. We
call $\rho_{1}$ a _correct reordering_ of $\sigma_{1}$, being a slice of
$\sigma_{1}$ closed under the thread order and preserving the writer of each
read in $\sigma_{1}$; the precise definition is presented in Section 2. In
this case, however, $\rho_{1}$ does not witness the deadlock as the event
$e_{2}$ is not _enabled_ in $\rho_{1}$. In fact, due to the dependency between
the events $e_{3}$ and $e_{7}$, there are no correct reorderings of
$\sigma_{1}$ which make both $e_{2}$ and $e_{8}$ enabled. This makes the
deadlock pattern $\langle e_{2},e_{8}\rangle$ non-predictable. Consider now
$\sigma_{2}$ in Figure 1(b), and the sequence
$\rho_{2}=e_{3}..e_{7}\,e_{8}..e_{11}\,e_{1}e_{2}$. Observe that $\rho_{2}$ is
also a correct reordering. However, $\rho_{2}$ is not sync-preserving as the
order of the two critical sections on lock $\ell_{1}$ in $\rho_{2}$ is
different from their original order in $\sigma_{2}$. On the other hand,
$\rho_{3}=e_{1}e_{2}e_{3}e_{8}e_{9}\,e_{12}..e_{15}\,e_{16}e_{17}$ is a
correct reordering that is also sync-preserving — all pairs of critical
sections on the same lock appear in the same order in $\rho_{3}$ as they did
in $\sigma_{2}$. Further, $\rho_{3}$ also witnesses the deadlock as the events
$e_{4}$ and $e_{18}$ are both _enabled_ in $\rho_{3}$. This makes the deadlock
pattern $\langle e_{4},e_{18}\rangle$ a sync-preserving deadlock.

In this work we show that sync-preserving deadlocks enjoy two remarkable
properties. First, all sync-preserving deadlocks of a given _abstract_
deadlock pattern can be checked in linear time. Second, our extensive
experimental evaluation on standard benchmarks indicates that sync-
preservation captures a vast majority of deadlocks in practice. In
combination, these two benefits suggest that sync-preservation is the right
notion of deadlocks to be targeted by dynamic deadlock predictors.

###  1.2. Our Contributions

In detail, the contributions of this work are as follows.

  1. (1)

Complexity of Deadlock Prediction. Perhaps surprisingly, the complexity of
detecting deadlock patterns, as well as predicting deadlocks has remained
elusive. Our first contribution resolves such questions. Given a trace
$\sigma$ of size $\mathcal{N}$ and $\mathcal{T}$ threads, we first show that
detecting even one deadlock _pattern_ of length $k$ is $\mathsf{W[1]}$-hard in
$k$. This establishes that the problem is $\mathsf{NP}$-hard, and further
rules out algorithms that are fixed-parameter-tractable in $k$, i.e., with
running time of the form $f(k)\cdot\text{poly}(\mathcal{N})$, for some
function $f$. We next show that even with just $\mathcal{T}=2$ threads, the
problem of detecting a single deadlock _pattern_ (of size $k=2$) admits a
quadratic lower bound, i.e., it cannot be solved in time
$O(\mathcal{N}^{2-\epsilon})$, no matter what $\epsilon>0$ we choose. These
two results shed light on the difficulty in identifying deadlock patterns — a
task that might otherwise appear easier than the core task of prediction.
These hardness results, in particular the fine-grained lower bound result, are
based on novel constructions, and results from fine-grained complexity
(Williams, 2018). Our third result is about confirming predictable deadlocks —
even for a deadlock pattern of size $k=2$, checking whether it yields a
_predictable deadlock_ is $\mathsf{W[1]}$-hard in the number of threads
$\mathcal{T}$ (and thus again $\mathsf{NP}$-hard), and is inspired from an
analogous result in the context of data race prediction (Mathur et al., 2020).
These results capture the intractability of deadlock prediction in general,
even for the class of parametrized algorithms.

  2. (2)

Sync-preserving Deadlock Prediction and Abstract Deadlock Patterns. Given the
above hardness of predicting arbitrary deadlocks, we define a novel notion of
sync(hronization)-preserving deadlocks, illustrated in Section 1.1. We develop
SPDOnline, an _online, sound_ deadlock predictor that takes as input a trace
and reports _all_ sync-preserving deadlocks of size $2$ in _linear time_
$\widetilde{O}(\mathcal{N})$***We use $\widetilde{O}$ to ignore _polynomial_
appearance of trace parameters typically much smaller than $\mathcal{N}$
(e.g., number of threads).. As most deadlocks in practice involve only two
threads (Lu et al., 2008), restricting SPDOnline to size $2$ deadlocks leads
to linear-time deadlock prediction with small impact on its coverage. We also
develop our more general algorithm, SPDOffline, that detects _all_ sync-
preserving deadlocks of all sizes. SPDOffline operates in two phases. In the
first phase, it detects all _abstract deadlock patterns_. An abstract deadlock
pattern is a novel notion that serves as a succinct representation of the
class of deadlock patterns having the same signature. In the second phase,
SPDOffline executes SPDOnline on each abstract pattern to decide whether a
deadlock is formed. The running time of SPDOffline remains linear in
$\mathcal{N}$, but increases by a factor proportional to the number of
abstract deadlock patterns in the lock graph.

  3. (3)

Implementation and Evaluation. We have evaluated SPDOnline and SPDOffline in
terms of performance and predictive power on a large dataset of standard
benchmarks. In the offline setting, SPDOffline finds the same number of
deadlocks as the recently introduced SeqCheck, while achieving a speedup of
$>200\times$ on the most demanding benchmarks, and $21\times$ overall. In the
online setting, SPDOnline achieved a significant improvement in deadlock
discovery and deadlock-hit-rate compared to the random scheduling based
controlled concurrency testing technique of DeadlockFuzzer (Joshi et al.,
2009). Our experiments thus support that the notion of sync-preserving
deadlocks is suitable: (i) it captures the vast majority of the deadlocks in
practice, and (ii) sync-preserving deadlocks can be detected online and
optimally — that is, soundly, completely and in linear time, (iii) it can
enhance the deadlock detection capability of controlled concurrency testing
techniques, (iv) with reasonable runtime overhead.

##  2\. Preliminaries

Here we set up our model and develop relevant notation, following related work
in predictive analyses of concurrent programs (Smaragdakis et al., 2012; Kini
et al., 2017; Roemer et al., 2020).

Execution traces. A dynamic analysis observes traces generated by a concurrent
program, and analyzes them to determine the presence of a bug. Each such trace
$\sigma$ is a linear arrangement of events $\mathsf{Events}_{\sigma}$. An
event $e\in\mathsf{Events}_{\sigma}$ is tuple $e=\langle i,t,o\rangle$, where
$i$ is a unique identifier of $e$, $t$ is the unique identifier of the thread
performing $e$, and $o$ is either a read or write ($o=\mathtt{r}(x)$ or
$o=\mathtt{w}(x)$) operation to some variable $x$, or an acquire or release
($o=\mathtt{acq}(\ell)$ or $o=\mathtt{rel}(\ell)$) operation on some lock
$\ell$. For the sake of simplicity, we often omit $i$ when referring to an
event. We use $\operatorname{thread}(e)$ and $\operatorname{op}(e)$ to
respectively denote the thread identifier and the operation performed in the
event $e$. We use $\mathsf{Threads}_{\sigma}$, $\mathsf{Vars}_{\sigma}$ and
$\mathsf{Locks}_{\sigma}$ to denote the set of thread, variable and lock
identifiers in $\sigma$.

We restrict our attention to _well-formed_ traces $\sigma$, that abide to
shared-memory semantics. That is, if a lock $\ell$ is acquired at an event $e$
by thread $t$, then any later acquisition event $e^{\prime}$ of the same lock
$\ell$ must be preceded by an event $e^{\prime\prime}$ that releases lock
$\ell$ in thread $t$ in between the occurrence of $e$ and $e^{\prime}$. Taking
$e^{\prime\prime}$ to be the earliest such release event, we say that $e$ and
$e^{\prime\prime}$ are matching acquire and release events, and denote this by
$e=\mathsf{match}_{\sigma}(e^{\prime\prime})$ and
$e^{\prime\prime}=\mathsf{match}_{\sigma}(e)$. Moreover, every read event has
at least one preceding write event on the same location, that it reads its
value from.

Functions and relations on traces. A trace $\sigma$ implicitly defines some
relations. The _trace-order_
$\leq^{\sigma}_{\mathsf{tr}}\subseteq\mathsf{Events}_{\sigma}\times\mathsf{Events}_{\sigma}$
orders the events of $\sigma$ in a total order based on their order of
occurrence in the sequence $\sigma$. The _thread-order_
$\leq^{\sigma}_{\mathsf{TO}}$ is the unique partial order over
$\mathsf{Events}_{\sigma}$ such that $e\leq^{\sigma}_{\mathsf{TO}}e^{\prime}$
iff $\operatorname{thread}(e)=\operatorname{thread}(e^{\prime})$ and
$e\leq^{\sigma}_{\mathsf{tr}}e^{\prime}$. We say
$e<^{\sigma}_{\mathsf{TO}}e^{\prime}$ if
$e\leq^{\sigma}_{\mathsf{TO}}e^{\prime}$ but $e\neq e^{\prime}$. The _reads-
from_ function $\mathsf{rf}_{\sigma}$ is a map from the read events to the
write events in $\sigma$. Under sequential consistency, for a read event $e$
on variable $x$, we have that $e^{\prime}=\mathsf{rf}_{\sigma}(e)$ be the
latest write event on the same variable $x$ such that
$e^{\prime}\leq^{\sigma}_{\mathsf{tr}}e$. We say that a lock
$\ell\in\mathsf{Locks}_{\sigma}$ is held at an event
$e\in\mathsf{Events}_{\sigma}$ if there is an event $e^{\prime}$ such that (i)
$\operatorname{op}(e^{\prime})=\mathtt{acq}(\ell)$, (ii)
$e^{\prime}<^{\sigma}_{\mathsf{TO}}e$, and (iii) either
$\mathsf{match}_{\sigma}(e^{\prime})$ does not exist in $\sigma$, or
$e\leq^{\sigma}_{\mathsf{TO}}\mathsf{match}_{\sigma}(e^{\prime})$. We use
$\mathsf{HeldLks}_{\sigma}(e)$ to denote the set of all the locks that are
held by $\operatorname{thread}(e)$ right before $e$. The lock nesting depth of
$\sigma$ is
$\max\limits_{e\in\mathsf{Events}_{\sigma}}|\mathsf{HeldLks}_{\sigma}(e)|+1$
where $\operatorname{op}(e)=\mathtt{acq}(\ell)$.

Deadlock patterns. A deadlock pattern†††Similar notions have been used in the
literature, sometimes under the term _deadlock potential(Havelund, 2000)._ of
size $k$ in a trace $\sigma$ is a sequence $D=\langle
e_{0},e_{1},\ldots,e_{k-1}\rangle$, with $k$ distinct threads
$t_{0},\ldots,t_{k-1}$ and $k$ distinct locks $\ell_{0},\ldots,\ell_{k-1}$
such that $\operatorname{thread}(e_{i})=t_{i}$,
$\operatorname{op}(e_{i})=\mathtt{acq}(\ell_{i})$,
$\ell_{i}\in\mathsf{HeldLks}_{\sigma}(e_{(i+1)\%k})$, and further,
$\mathsf{HeldLks}_{\sigma}(e_{i})\cap\mathsf{HeldLks}_{\sigma}(e_{j})=\varnothing$
for every $i,j$ such that $i\neq j$ and $0\leq i,j<k$. A deadlock pattern is a
necessary but insufficient condition of an actual deadlock, due to subtle
synchronization or control and data flow in the underlying program.

Dynamic predictive analysis and correct reorderings. Dynamic analyses aim to
expose bugs by observing traces $\sigma$ of a concurrent program, often
without accessing the source code. While such purely dynamic approaches enjoy
the benefits of scalability, simply detecting bugs that manifest on $\sigma$
offer poor coverage and are bound to miss bugs that appear in select thread
interleavings (Musuvathi et al., 2008). Therefore, for better coverage,
_predictive_ dynamic techniques are developed. Such techniques predict the
occurrence of bugs in alternate executions that can be _inferred_ from
$\sigma$, irrespective of the program that produced $\sigma$. The notion of
such inferred executions is formalized by the notion of correct reorderings
(Smaragdakis et al., 2012; Şerbănută et al., 2013; Sen et al., 2005).

A trace $\rho$ is a _correct reordering_ of a trace $\sigma$ if  (1)
$\mathsf{Events}_{\rho}\subseteq\mathsf{Events}_{\sigma}$,  (2) for every
$e,f\in\mathsf{Events}_{\sigma}$ with $e\leq^{\sigma}_{\mathsf{TO}}f$, if
$f\in\mathsf{Events}_{\rho}$, then $e\in\mathsf{Events}_{\rho}$ and
$e\leq^{\rho}_{\mathsf{TO}}f$, and  (3) for every read event
$r\in\mathsf{Events}_{\rho}$, we have
$\mathsf{rf}_{\sigma}(r)\in\mathsf{Events}_{\rho}$ and
$\mathsf{rf}_{\rho}(r)=\mathsf{rf}_{\sigma}(r)$.  Intuitively, a correct
reordering $\rho$ of $\sigma$ is a permutation of $\sigma$ that respects the
thread order and preserves the values of each read and write that occur in
$\rho$. This ensures a key property — every program that generated $\sigma$ is
also capable of generating $\rho$ (possibly under a different thread
schedule), and thus $\rho$ serves as a true witness of a bug.

Predictable deadlocks. We say that an event $e$ is $\sigma$-enabled in a
correct reordering $\rho$ of $\sigma$ if $e\in\mathsf{Events}_{\sigma}$,
$e\not\in\mathsf{Events}_{\rho}$ and for every $f\in\mathsf{Events}_{\sigma}$
if $f<^{\sigma}_{\mathsf{TO}}e$, then $f\in\mathsf{Events}_{\rho}$. A deadlock
pattern $D=\langle e_{0},e_{1}\ldots e_{k-1}\rangle$ of size $k$ in trace
$\sigma$ is said to be a predictable deadlock if there is a correct reordering
$\rho$ of $\sigma$ such that each of $e_{0},\ldots,e_{k-1}$ are
$\sigma$-enabled in $\rho$. This notion guarantees that the witness $\rho$ is
a valid execution of _any_ concurrent program that produced $\sigma$.
Analogous definitions have also been widely used for other predictable bugs
(Huang et al., 2014; Smaragdakis et al., 2012). We call a deadlock-prediction
algorithm _sound_ if for every input trace $\sigma$, all deadlock reports on
$\sigma$ are predictable deadlocks of $\sigma$ (i.e., no false positives), and
_complete_ if all predictable deadlocks of $\sigma$ are reported by the
algorithm (i.e., no false negatives). This is in line with the previous works
on the topic of predictive analyses (Cai et al., 2021; Kalhauge and Palsberg,
2018; Mathur et al., 2021; Pavlogiannis, 2019). We remark that other domains
sometimes use this terminology reversed.

###### Example 0.

Let us illustrate these definitions on the trace $\sigma_{2}$ in Fig. 1(b),
with $e_{i}$ denoting the $i^{\text{th}}$ event in the figure. The set of
events, threads, variables and locks of $\sigma_{2}$ are respectively
$\mathsf{Events}_{\sigma_{2}}=\\{e_{i}\\}_{i=1}^{20}$,
$\mathsf{Threads}_{\sigma_{2}}=\\{t_{1},t_{2},t_{3},t_{4}\\}$,
$\mathsf{Vars}_{\sigma_{2}}=\\{x,y,z\\}$ and
$\mathsf{Locks}_{\sigma_{2}}=\\{\ell_{1},\ell_{2},\ell_{3}\\}$. The trace
order yields $e_{i}\leq^{\sigma_{2}}_{\mathsf{tr}}e_{j}$ iff $i\leq j$, and
some examples of thread-ordered events are
$e_{1}<^{\sigma_{2}}_{\mathsf{TO}}e_{2}<^{\sigma_{2}}_{\mathsf{TO}}e_{15}$ and
$e_{16}<^{\sigma_{2}}_{\mathsf{TO}}e_{18}<^{\sigma_{2}}_{\mathsf{TO}}e_{20}$.
The reads-from function is as follows:
$\mathsf{rf}_{\sigma_{2}}(e_{10})=e_{5}$,
$\mathsf{rf}_{\sigma_{2}}(e_{14})=e_{9}$ and
$\mathsf{rf}_{\sigma_{2}}(e_{17})=e_{13}$. The lock nesting depth of
$\sigma_{2}$ is $2$. The sequence $D=\langle e_{4},e_{18}\rangle$ forms a
deadlock pattern because of the cyclic acquisition of locks $\ell_{2}$ and
$\ell_{3}$ without simultaneously holding a common lock. The trace
$\rho_{4}=e_{3}..e_{7}\,e_{8}..e_{11}\,e_{1}e_{2}e_{12}..e_{15}\,e_{16}e_{17}$
is a correct reordering of $\sigma_{2}$; even though it differs from
$\sigma_{2}$ in the relative order of the critical sections of lock
$\ell_{1}$, and contains only a prefix of thread $t_{3}$, it is consistent
with $\mathsf{rf}_{\sigma_{2}}$ and $<^{\sigma_{2}}_{\mathsf{TO}}$. However,
$\rho_{4}$ does not witness $\langle e_{4},e_{18}\rangle$ as a deadlock, as
only $e_{18}$ is $\sigma_{2}$-enabled in $\rho_{4}$. On the other hand, the
trace $\rho_{3}=e_{1}e_{2}e_{3}e_{8}e_{9}\,e_{12}..e_{15}\,e_{16}e_{17}$ is a
correct reordering of $\sigma_{2}$ in which $e_{4}$ and $e_{18}$ are
$\sigma_{2}$-enabled, witnessing $D$ as a predictable deadlock of
$\sigma_{2}$.

##  3\. The Complexity of Dynamic Deadlock Prediction

Detecting deadlock patterns and predictable deadlocks is clearly a problem in
$\mathsf{NP}$, as any witness for either problem can be verified in polynomial
time. However, little has been known about the hardness of the problem in
terms of rigorous lower bounds. Here we settle these questions, by proving
strong intractability results. Due to space constraints, we state and explain
the main results here, and refer to our technical report (arxiv) Appendix A
for the full proofs.

Parametrized hardness for detecting deadlock patterns. We show that the basic
problem of checking the existence of a deadlock _pattern_ is itself hard
parameterized by the size $k$ of the pattern.

###### Theorem 3.1.

Checking if a trace $\sigma$ contains a deadlock pattern of size $k$ is
$\mathsf{W[1]}$-hard in the parameter $k$. Moreover, the problem remains
$\mathsf{NP}$-hard even when the lock-nesting depth of $\sigma$ is constant.

###### Proof.

We show that there is a polynomial-time fixed parameter tractable reduction
from INDEPENDENT-SET(c) to the problem of checking the existence of deadlock-
patterns of size $c$. Our reduction takes as input an undirected graph $G$ and
outputs a trace $\sigma$ such that $G$ has an independent set of size $c$ iff
$\sigma$ has a deadlock pattern of size $c$.

$G$${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}a}$${\color[rgb]{0.24,0.24,0.24}\definecolor[named]{pgfstrokecolor}{rgb}{0.24,0.24,0.24}\pgfsys@color@gray@stroke{0.24}\pgfsys@color@gray@fill{0.24}b}$${\color[rgb]{0.354,0.354,0.354}\definecolor[named]{pgfstrokecolor}{rgb}{0.354,0.354,0.354}\pgfsys@color@gray@stroke{0.354}\pgfsys@color@gray@fill{0.354}c}$$t_{1}$$t_{2}$$t_{3}$$\mathtt{acq}(\ell_{\\{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}a},{\color[rgb]{0.354,0.354,0.354}\definecolor[named]{pgfstrokecolor}{rgb}{0.354,0.354,0.354}\pgfsys@color@gray@stroke{0.354}\pgfsys@color@gray@fill{0.354}c}\\}})$$\mathtt{acq}(\ell_{\\{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}a},{\color[rgb]{0.24,0.24,0.24}\definecolor[named]{pgfstrokecolor}{rgb}{0.24,0.24,0.24}\pgfsys@color@gray@stroke{0.24}\pgfsys@color@gray@fill{0.24}b}\\}})$$\mathtt{cs}(\ell_{1},\ell_{2})$$\mathtt{rel}(\ell_{\\{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}a},{\color[rgb]{0.24,0.24,0.24}\definecolor[named]{pgfstrokecolor}{rgb}{0.24,0.24,0.24}\pgfsys@color@gray@stroke{0.24}\pgfsys@color@gray@fill{0.24}b}\\}})$$\mathtt{rel}(\ell_{\\{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}a},{\color[rgb]{0.354,0.354,0.354}\definecolor[named]{pgfstrokecolor}{rgb}{0.354,0.354,0.354}\pgfsys@color@gray@stroke{0.354}\pgfsys@color@gray@fill{0.354}c}\\}})$$\mathtt{acq}(\ell_{\\{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}a},{\color[rgb]{0.24,0.24,0.24}\definecolor[named]{pgfstrokecolor}{rgb}{0.24,0.24,0.24}\pgfsys@color@gray@stroke{0.24}\pgfsys@color@gray@fill{0.24}b}\\}})$$\mathtt{cs}(\ell_{1},\ell_{2})$$\mathtt{rel}(\ell_{\\{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}a},{\color[rgb]{0.24,0.24,0.24}\definecolor[named]{pgfstrokecolor}{rgb}{0.24,0.24,0.24}\pgfsys@color@gray@stroke{0.24}\pgfsys@color@gray@fill{0.24}b}\\}})$$\mathtt{acq}(\ell_{\\{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}a},{\color[rgb]{0.354,0.354,0.354}\definecolor[named]{pgfstrokecolor}{rgb}{0.354,0.354,0.354}\pgfsys@color@gray@stroke{0.354}\pgfsys@color@gray@fill{0.354}c}\\}})$$\mathtt{cs}(\ell_{1},\ell_{2})$$\mathtt{rel}(\ell_{\\{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}a},{\color[rgb]{0.354,0.354,0.354}\definecolor[named]{pgfstrokecolor}{rgb}{0.354,0.354,0.354}\pgfsys@color@gray@stroke{0.354}\pgfsys@color@gray@fill{0.354}c}\\}})$$\mathtt{acq}(\ell_{\\{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}a},{\color[rgb]{0.354,0.354,0.354}\definecolor[named]{pgfstrokecolor}{rgb}{0.354,0.354,0.354}\pgfsys@color@gray@stroke{0.354}\pgfsys@color@gray@fill{0.354}c}\\}})$$\mathtt{acq}(\ell_{\\{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}a},{\color[rgb]{0.24,0.24,0.24}\definecolor[named]{pgfstrokecolor}{rgb}{0.24,0.24,0.24}\pgfsys@color@gray@stroke{0.24}\pgfsys@color@gray@fill{0.24}b}\\}})$$\mathtt{cs}(\ell_{2},\ell_{0})$$\mathtt{rel}(\ell_{\\{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}a},{\color[rgb]{0.24,0.24,0.24}\definecolor[named]{pgfstrokecolor}{rgb}{0.24,0.24,0.24}\pgfsys@color@gray@stroke{0.24}\pgfsys@color@gray@fill{0.24}b}\\}})$$\mathtt{rel}(\ell_{\\{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}a},{\color[rgb]{0.354,0.354,0.354}\definecolor[named]{pgfstrokecolor}{rgb}{0.354,0.354,0.354}\pgfsys@color@gray@stroke{0.354}\pgfsys@color@gray@fill{0.354}c}\\}})$$\mathtt{acq}(\ell_{\\{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}a},{\color[rgb]{0.24,0.24,0.24}\definecolor[named]{pgfstrokecolor}{rgb}{0.24,0.24,0.24}\pgfsys@color@gray@stroke{0.24}\pgfsys@color@gray@fill{0.24}b}\\}})$$\mathtt{cs}(\ell_{2},\ell_{0})$$\mathtt{rel}(\ell_{\\{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}a},{\color[rgb]{0.24,0.24,0.24}\definecolor[named]{pgfstrokecolor}{rgb}{0.24,0.24,0.24}\pgfsys@color@gray@stroke{0.24}\pgfsys@color@gray@fill{0.24}b}\\}})$$\mathtt{acq}(\ell_{\\{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}a},{\color[rgb]{0.354,0.354,0.354}\definecolor[named]{pgfstrokecolor}{rgb}{0.354,0.354,0.354}\pgfsys@color@gray@stroke{0.354}\pgfsys@color@gray@fill{0.354}c}\\}})$$\mathtt{cs}(\ell_{2},\ell_{0})$$\mathtt{rel}(\ell_{\\{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}a},{\color[rgb]{0.354,0.354,0.354}\definecolor[named]{pgfstrokecolor}{rgb}{0.354,0.354,0.354}\pgfsys@color@gray@stroke{0.354}\pgfsys@color@gray@fill{0.354}c}\\}})$$\mathtt{acq}(\ell_{\\{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}a},{\color[rgb]{0.354,0.354,0.354}\definecolor[named]{pgfstrokecolor}{rgb}{0.354,0.354,0.354}\pgfsys@color@gray@stroke{0.354}\pgfsys@color@gray@fill{0.354}c}\\}})$$\mathtt{acq}(\ell_{\\{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}a},{\color[rgb]{0.24,0.24,0.24}\definecolor[named]{pgfstrokecolor}{rgb}{0.24,0.24,0.24}\pgfsys@color@gray@stroke{0.24}\pgfsys@color@gray@fill{0.24}b}\\}})$$\mathtt{cs}(\ell_{0},\ell_{1})$$\mathtt{rel}(\ell_{\\{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}a},{\color[rgb]{0.24,0.24,0.24}\definecolor[named]{pgfstrokecolor}{rgb}{0.24,0.24,0.24}\pgfsys@color@gray@stroke{0.24}\pgfsys@color@gray@fill{0.24}b}\\}})$$\mathtt{rel}(\ell_{\\{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}a},{\color[rgb]{0.354,0.354,0.354}\definecolor[named]{pgfstrokecolor}{rgb}{0.354,0.354,0.354}\pgfsys@color@gray@stroke{0.354}\pgfsys@color@gray@fill{0.354}c}\\}})$$\mathtt{acq}(\ell_{\\{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}a},{\color[rgb]{0.24,0.24,0.24}\definecolor[named]{pgfstrokecolor}{rgb}{0.24,0.24,0.24}\pgfsys@color@gray@stroke{0.24}\pgfsys@color@gray@fill{0.24}b}\\}})$$\mathtt{cs}(\ell_{0},\ell_{1})$$\mathtt{rel}(\ell_{\\{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}a},{\color[rgb]{0.24,0.24,0.24}\definecolor[named]{pgfstrokecolor}{rgb}{0.24,0.24,0.24}\pgfsys@color@gray@stroke{0.24}\pgfsys@color@gray@fill{0.24}b}\\}})$$\mathtt{acq}(\ell_{\\{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}a},{\color[rgb]{0.354,0.354,0.354}\definecolor[named]{pgfstrokecolor}{rgb}{0.354,0.354,0.354}\pgfsys@color@gray@stroke{0.354}\pgfsys@color@gray@fill{0.354}c}\\}})$$\mathtt{cs}(\ell_{0},\ell_{1})$$\mathtt{rel}(\ell_{\\{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}a},{\color[rgb]{0.354,0.354,0.354}\definecolor[named]{pgfstrokecolor}{rgb}{0.354,0.354,0.354}\pgfsys@color@gray@stroke{0.354}\pgfsys@color@gray@fill{0.354}c}\\}})$

(a) Reduction of INDEPENDENT-SET(3) on $G$ to detecting a deadlock pattern of
size $3$.

[1, 1][1, 0]$A$[1, 0][0,
1]$B$$t_{A}$$t_{B}$$\mathtt{acq}({\color[rgb]{0.24,0.24,0.24}\definecolor[named]{pgfstrokecolor}{rgb}{0.24,0.24,0.24}\pgfsys@color@gray@stroke{0.24}\pgfsys@color@gray@fill{0.24}\ell_{2}})$$\mathtt{acq}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\ell_{1}})$$\mathtt{cs}(m_{0},m_{1})$$\mathtt{rel}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\ell_{1}})$$\mathtt{rel}({\color[rgb]{0.24,0.24,0.24}\definecolor[named]{pgfstrokecolor}{rgb}{0.24,0.24,0.24}\pgfsys@color@gray@stroke{0.24}\pgfsys@color@gray@fill{0.24}\ell_{2}})$$\mathtt{acq}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\ell_{1}})$$\mathtt{cs}(m_{0},m_{1})$$\mathtt{rel}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\ell_{1}})$$\mathtt{acq}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\ell_{1}})$$\mathtt{cs}(m_{1},m_{0})$$\mathtt{rel}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\ell_{1}})$$\mathtt{acq}_{1}({\color[rgb]{0.24,0.24,0.24}\definecolor[named]{pgfstrokecolor}{rgb}{0.24,0.24,0.24}\pgfsys@color@gray@stroke{0.24}\pgfsys@color@gray@fill{0.24}\ell_{2}})$$\mathtt{cs}(m_{1},m)$$\mathtt{rel}_{1}({\color[rgb]{0.24,0.24,0.24}\definecolor[named]{pgfstrokecolor}{rgb}{0.24,0.24,0.24}\pgfsys@color@gray@stroke{0.24}\pgfsys@color@gray@fill{0.24}\ell_{2}})$

(b) Reduction for OV-hardness proof from an instance of size $n=2$ and $d=2$.

Figure 2.  Construction of $\mathsf{W[1]}$-hardness (2(a)) and OV-hardness
(2(b)) results. We use the shortcut $\mathtt{cs}(\ell,\ell^{\prime})$ to
denote two nested critical sections on $\ell$ and $\ell^{\prime}$. That is,
$\mathtt{cs}(\ell,\ell^{\prime})=\mathtt{acq}(\ell)\cdot\mathtt{acq}(\ell^{\prime})\cdot\mathtt{rel}(\ell^{\prime})\cdot\mathtt{rel}(\ell)$.

Construction. Let $V=\\{v_{1},v_{2},\ldots,v_{n}\\}$. We assume a total
ordering $<_{E}$ on the set of edges $E$. The trace $\sigma$ we construct is a
concatenation of $c$ sub-traces:
$\sigma=\sigma^{(1)}\cdot\sigma^{(2)}\cdots\sigma^{(c)}$ and uses $c$ threads
$\\{t_{1},t_{2},\ldots t_{c}\\}$ and $|E|+c$ locks
$\\{\ell_{\\{u,v\\}}\\}_{\\{u,v\\}\in
E}\uplus\\{\ell_{0},\ell_{1}\ldots,\ell_{c-1}\\}$. The $i^{\text{th}}$ sub-
trace $\sigma^{(i)}$ is a sequence of events performed by thread $t_{i}$, and
is obtained by concatenation of $n=|V|$ sub-traces:
$\sigma^{(i)}=\sigma^{(i)}_{1}\cdot\sigma^{(i)}_{2}\cdots\sigma^{(i)}_{n}$.
Each sub-trace $\sigma^{(i)}_{j}$ with $(i\leq c,j\leq n)$ comprises of nested
critical sections over locks of the form $\ell_{\\{v_{j},u\\}}$, where $u$ is
a neighbor of $v_{j}$. Inside the nested block we have critical sections on
locks $\ell_{i\%c}$ and $\ell_{(i+1)\%c}$. Formally, let
$\\{v_{j},v_{k_{1}}\\},\ldots,\\{v_{j},v_{k_{d}}\\}$ be the neighboring edges
of $v_{j}$ (ordered according to $<_{E}$). Then, $\sigma^{(i)}_{j}$ is the
unique string generated by the grammar having $d+1$ non-terminals
$S_{0},S_{1},\ldots,S_{d}$, start symbol $S_{d}$ and the following production
rules:

  * •

$S_{0}\to\langle t_{i},\mathtt{acq}(\ell_{i\%c})\rangle\cdot\langle
t_{i},\mathtt{acq}(\ell_{(i+1)\%c})\rangle\cdot\langle
t_{i},\mathtt{rel}(\ell_{(i+1)\%c})\rangle\cdot\langle
t_{i},\mathtt{rel}(\ell_{i\%c})\rangle$.

  * •

for each $1\leq r\leq d$, $S_{r}\to\langle
t_{i},\mathtt{acq}(\ell_{\\{v_{j},v_{k_{r}}\\}})\rangle\cdot
S_{r-1}\cdot\langle t_{i},\mathtt{rel}(\ell_{\\{v_{j},v_{k_{r}}\\}})\rangle$.

Fig. 2(a) illustrates this construction for a graph with $3$ nodes and
parameter $c=3$. Finally, observe that the lock-nesting depth in $\sigma$ is
bounded by 2 + the degree of $G$. ∎

Theorem 3.1 implies that the problem is not only $\mathsf{NP}$-hard, but also
unlikely to be _fixed parameter tractable_ in the size $k$ of the deadlock
pattern. In fact, under the well-believed Exponential Time Hypothesis (ETH),
the parametrized problem INDEPENDENT-SET(c) cannot be solved in time
$f(c)\cdot n^{o(c)}$ (Chen et al., 2006). The above reduction preserves the
parameter $k=c$, thus under ETH, detecting deadlock patterns of size $k$ is
unlikely to be solvable in time complexity $f(k)\cdot\mathcal{N}^{g(k)}$,
where $g(k)$ is $o(k)$ (such as $g(k)=\sqrt{k}$ or even $g(k)=k/\log(k)$). The
problem of checking the existence of deadlock patterns is, intuitively, a
precursor to the deadlock prediction problem. Thus, an approach for deadlock
prediction that first identifies the existence of arbitrary deadlock patterns
and then verifying their feasibility is unlikely to be tractable. In practice,
the synchronization patterns corresponding to the hard instances are uncommon
in executions, and our proposed algorithms (Section 4 and Section 5) can
effectively expose predictable deadlocks (Section 6).

Fine-grained hardness for deadlock pattern detection. We next consider the
problem of detecting deadlock patterns of size $2$, as these form the most
common case in practice (Lu et al., 2008). Observe that Theorem 3.1 has no
implications on this case, as here $k$ is fixed. The problem admits a folklore
$O(\mathcal{N}^{2})$ time algorithm, by iterating over all pairs of lock-
acquisition events of the input trace, and checking whether any such pair
forms a deadlock pattern. Perhaps surprisingly, here we show that, despite its
simplicity, this algorithm is optimal, i.e., we cannot hope to improve over
this quadratic bound. This result is based on a reduction from the popular
Orthogonal Vectors (OV) problem. Given two sets of $d$-dimensional vectors
$A,B\subseteq\\{0,1\\}^{d}$ of cardinality $|A|=|B|=n$, the OV problem asks if
there are $a\in A,b\in B$ such that $a\cdot b=\sum_{i}a[i]\cdot b[i]=0$. The
OV hypothesis states that for any $\epsilon>0$, there is no
$O(n^{2-\epsilon}\cdot\text{poly}(d))$ algorithm for solving OV. This is also
a consequence of the famous Strong Exponential Time Hypothesis (SETH)
(Williams, 2005). We next show that detecting deadlock patterns of size $2$ is
at least as hard as solving OV.

###### Theorem 3.2.

Given a trace $\sigma$ of size $\mathcal{N}$ and $\mathcal{L}$ locks, for any
$\epsilon>0$, there is no algorithm that determines in
$O(\mathcal{N}^{2-\epsilon}\cdot\text{poly}(\mathcal{L}))$ time whether
$\sigma$ has a deadlock pattern of size $2$, under the OV hypothesis.

###### Proof.

We show a fine-grained reduction from the Orthogonal Vectors Problem to the
problem of checking for deadlock patterns of size $2$. For this, we start with
two sets $A,B\subseteq\\{0,1\\}^{d}$ of $d$-dimensional vectors with
$|A|=|B|=n$. We write the $i^{th}$ vector in $A$ as $A_{i}$ and that in $B$ as
$B_{i}$.

Construction. We will construct a trace $\sigma$ such that $\sigma$ has a
deadlock pattern of length $2$ iff $(A,B)$ is a positive OV instance. The
trace $\sigma$ is of the form $\sigma=\sigma^{A}\cdot\sigma^{B}$ and uses $2$
threads $\\{t_{A},t_{B}\\}$ and $d+2$ distinct locks
$\ell_{1},\ldots,\ell_{d},m_{0},m_{1}$. Intuitively, $\sigma^{A}$ and
$\sigma^{B}$ encode the given sets of vectors $A$ and $B$. The sub-traces
$\sigma^{A}=\sigma^{A}_{1}\cdot\sigma^{A}_{2}\cdots\sigma^{A}_{n}$ and
$\sigma^{B}=\sigma^{B}_{1}\cdot\sigma^{B}_{2}\cdots\sigma^{B}_{n}$ are defined
as follows. For each $i\in\\{1,2,\ldots,n\\}$ and $Z\in\\{A,B\\}$, the sub-
trace $\sigma^{Z}_{i}$ is the unique string generated by the grammar having
$d+1$ non-terminals $S_{0},S_{1},\ldots,S_{d}$, start symbol $S_{d}$ and the
following production rules:

  * •

$S_{0}\to\langle t_{Z},\mathtt{acq}(m)\rangle\cdot\langle
t_{Z},\mathtt{acq}(m^{\prime})\rangle\cdot\langle
t_{Z},\mathtt{rel}(m^{\prime})\rangle\cdot\langle
t_{Z},\mathtt{rel}(m)\rangle$, where $(m,m^{\prime})=(m_{0},m_{1})$ if $Z=A$,
and $(m,m^{\prime})=(m_{1},m_{0})$.

  * •

for each $1\leq j\leq d$, $S_{j}\to S_{j-1}$ if $Z_{i}[j]=0$. Otherwise (if
$Z_{i}[j]=1$), $S_{j}\to\langle t_{Z},\mathtt{acq}(\ell_{j})\rangle\cdot
S_{j-1}\cdot\langle t_{Z},\mathtt{rel}(\ell_{j})\rangle$.

In words, all events of $\sigma^{A}$ are performed by thread $t_{A}$ and those
in $\sigma^{B}$ are performed by $t_{B}$. Next, the $i^{th}$ sub-trace of
$\sigma^{A}$, denoted $\sigma^{A}_{i}$ corresponds to the vector $A_{i}$ as
follows — $\sigma^{A}_{i}$ is a nested block of critical sections, with the
innermost critical section being on lock $\ell^{\prime}$, which is immediately
enclosed in a critical section on lock $\ell$. Further, in the sub-trace
$\sigma^{A}_{i}$, the lock $\ell_{j}$ occurs iff $A_{i}[j]=1$. The sub-traces
$\sigma^{B}_{i}$ is similarly constructed, except that the order of the two
innermost critical sections is inverted. Fig. 2(b) illustrates the
construction for an OV-instance with $n=2$ and $d=2$. ∎

The complexity of deadlock prediction. Finally, we settle the complexity of
the prediction problem for deadlocks, and show that, even for deadlock
patterns of size $2$, the problem is $\mathsf{W[1]}$-hard parameterized by the
number of threads. In contrast, recall that the $\mathsf{W[1]}$-hardness of
Theorem 3.1 concerns deadlock patterns of arbitrary size. Our result is based
on a similar hardness that was established recently for predicting data races
(Mathur et al., 2020).

###### Theorem 3.3.

The problem of checking if a trace $\sigma$ has a predictable deadlock of size
$2$ is $\mathsf{W[1]}$-hard in the number of threads $\mathcal{T}$ appearing
in $\sigma$, and thus is also $\mathsf{NP}$-hard.

##  4\. Synchronization-Preserving Deadlocks and their Prediction

Having established the intractability of general deadlock prediction in
Section 3, we now define the subclass of predictable deadlocks called
synchronization-preserving (_sync-preserving_ , for short) in Section 4.1. The
key benefit of sync-preserving deadlocks is that, unlike arbitrary deadlocks,
they can be detected efficiently; we develop our algorithm SPDOffline for this
task in Sections 4.2-4.5. Our experiments later indicate that most predictable
deadlocks are actually sync-preserving, hence the benefit of fast detection
comes at the cost of little-to-no precision loss in practice.

Overview of the algorithm. There are several insights behind our algorithm.
First, given a deadlock pattern, one can verify if it is a sync-preserving
deadlock in linear time (Section 4.3); this is based on our sound and complete
characterization of sync-preserving deadlocks (Section 4.2). Next, instead of
verifying single deadlock patterns one-by-one, we consider _abstract deadlock
patterns_ , which are essentially collections of deadlock patterns that share
the same signature; the formal definition is given in Section 4.4. We show
that our basic algorithm can be extended to _incrementally_ verify _all_ the
concretizations of an abstract deadlock pattern in linear time (Section 4.4),
in a single pass (Lemma 4.8). Finally, we feed this algorithm all the abstract
deadlock patterns of the input trace, by constructing an _abstract lock graph_
and enumerating cycles in it (Section 4.5).

###  4.1. Synchronization-Preserving Deadlocks

Our notion of sync-preserving deadlocks builds on the recently introduced
concept of sync-preserving correct reorderings (Mathur et al., 2021).

###### Definition 0 (Sync-preserving Correct Reordering).

A correct reordering $\rho$ of a trace $\sigma$ is _sync-preserving_ if for
every lock $\ell\in\mathsf{Locks}_{\rho}$ and every two acquire events
$e_{1}\neq e_{2}\in\mathsf{Events}_{\rho}$ with
$\operatorname{op}(e_{1})=\operatorname{op}(e_{2})=\mathtt{acq}(\ell)$, the
order of $e_{1}$ and $e_{2}$ is the same in $\sigma$ and $\rho$, i.e.,
$e_{1}\leq^{\rho}_{\mathsf{tr}}e_{2}$ iff
$e_{1}\leq^{\sigma}_{\mathsf{tr}}e_{2}$.

A sync-preserving correct reordering preserves the order of those critical
sections (on the same lock) that actually appear in the reordering, but allows
intermediate critical sections to be dropped completely. This style of
reasoning is more permissive than the space of reorderings induced by the
Happens-Before partial order (Lamport, 1978), that implicitly enforces that
all intermediate critical sections on a lock be present. Sync-preserving
deadlocks can now be defined naturally.

###### Definition 0 (Sync-preserving Deadlocks).

Let $\sigma$ be a trace and $D=\langle e_{0},e_{1},\ldots,e_{k-1}\rangle$ be a
deadlock pattern. We say that $D$ is a sync-preserving deadlock of $\sigma$ if
there is a sync-preserving correct reordering $\rho$ of $\sigma$ such that
each of $e_{0},\ldots,e_{k-1}$ is $\sigma$-enabled in $\rho$.

$t_{1}$$t_{2}$$t_{3}$$1$
$\mathtt{acq}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\ell_{1}})$$2$
$\mathtt{acq}({\color[rgb]{0.24,0.24,0.24}\definecolor[named]{pgfstrokecolor}{rgb}{0.24,0.24,0.24}\pgfsys@color@gray@stroke{0.24}\pgfsys@color@gray@fill{0.24}\ell_{2}})$$3$
$\mathtt{rel}({\color[rgb]{0.24,0.24,0.24}\definecolor[named]{pgfstrokecolor}{rgb}{0.24,0.24,0.24}\pgfsys@color@gray@stroke{0.24}\pgfsys@color@gray@fill{0.24}\ell_{2}})$$4$
$\mathtt{acq}({\color[rgb]{0.24,0.24,0.24}\definecolor[named]{pgfstrokecolor}{rgb}{0.24,0.24,0.24}\pgfsys@color@gray@stroke{0.24}\pgfsys@color@gray@fill{0.24}\ell_{2}})$$5$
$\mathtt{w}(y)$$6$
$\mathtt{rel}({\color[rgb]{0.24,0.24,0.24}\definecolor[named]{pgfstrokecolor}{rgb}{0.24,0.24,0.24}\pgfsys@color@gray@stroke{0.24}\pgfsys@color@gray@fill{0.24}\ell_{2}})$$7$
$\mathtt{rel}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\ell_{1}})$$8$
$\mathtt{acq}({\color[rgb]{0.354,0.354,0.354}\definecolor[named]{pgfstrokecolor}{rgb}{0.354,0.354,0.354}\pgfsys@color@gray@stroke{0.354}\pgfsys@color@gray@fill{0.354}\ell_{3}})$$9$
$\mathtt{w}(x)$$10$ $\mathtt{r}(y)$$11$
$\mathtt{rel}({\color[rgb]{0.354,0.354,0.354}\definecolor[named]{pgfstrokecolor}{rgb}{0.354,0.354,0.354}\pgfsys@color@gray@stroke{0.354}\pgfsys@color@gray@fill{0.354}\ell_{3}})$$12$
$\mathtt{acq}({\color[rgb]{0.24,0.24,0.24}\definecolor[named]{pgfstrokecolor}{rgb}{0.24,0.24,0.24}\pgfsys@color@gray@stroke{0.24}\pgfsys@color@gray@fill{0.24}\ell_{2}})$$13$
$\mathtt{acq}({\color[rgb]{0.354,0.354,0.354}\definecolor[named]{pgfstrokecolor}{rgb}{0.354,0.354,0.354}\pgfsys@color@gray@stroke{0.354}\pgfsys@color@gray@fill{0.354}\ell_{3}})$$14$
$\mathtt{r}(x)$$15$
$\mathtt{rel}({\color[rgb]{0.354,0.354,0.354}\definecolor[named]{pgfstrokecolor}{rgb}{0.354,0.354,0.354}\pgfsys@color@gray@stroke{0.354}\pgfsys@color@gray@fill{0.354}\ell_{3}})$$16$
$\mathtt{acq}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\ell_{1}})$

$t_{1}$$t_{2}$$t_{3}$$17$$\mathtt{w}(v)$$18$$\mathtt{rel}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\ell_{1}})$$19$$\mathtt{acq}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\ell_{1}})$$20$$\mathtt{rel}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\ell_{1}})$$21$$\mathtt{rel}({\color[rgb]{0.24,0.24,0.24}\definecolor[named]{pgfstrokecolor}{rgb}{0.24,0.24,0.24}\pgfsys@color@gray@stroke{0.24}\pgfsys@color@gray@fill{0.24}\ell_{2}})$$22$$\mathtt{acq}({\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25}\ell_{4}})$$23$$\mathtt{acq}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\ell_{1}})$$24$$\mathtt{w}(z)$$25$$\mathtt{r}(v)$$26$$\mathtt{rel}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\ell_{1}})$$27$$\mathtt{rel}({\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25}\ell_{4}})$$28$$\mathtt{acq}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\ell_{1}})$$29$$\mathtt{acq}({\color[rgb]{0.24,0.24,0.24}\definecolor[named]{pgfstrokecolor}{rgb}{0.24,0.24,0.24}\pgfsys@color@gray@stroke{0.24}\pgfsys@color@gray@fill{0.24}\ell_{2}})$$30$$\mathtt{r}(z)$$31$$\mathtt{rel}({\color[rgb]{0.24,0.24,0.24}\definecolor[named]{pgfstrokecolor}{rgb}{0.24,0.24,0.24}\pgfsys@color@gray@stroke{0.24}\pgfsys@color@gray@fill{0.24}\ell_{2}})$$32$$\mathtt{rel}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\ell_{1}})$

$\eta_{1}=\langle
t_{1},{\color[rgb]{0.24,0.24,0.24}\definecolor[named]{pgfstrokecolor}{rgb}{0.24,0.24,0.24}\pgfsys@color@gray@stroke{0.24}\pgfsys@color@gray@fill{0.24}\ell_{2}},\\{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\ell_{1}}\\},[e_{2},e_{4},e_{29}]\rangle$$\eta_{2}=\langle
t_{2},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\ell_{1}},\\{{\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25}\ell_{4}}\\},[e_{23}]\rangle$$\eta_{3}=\langle
t_{3},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\ell_{1}},\\{{\color[rgb]{0.24,0.24,0.24}\definecolor[named]{pgfstrokecolor}{rgb}{0.24,0.24,0.24}\pgfsys@color@gray@stroke{0.24}\pgfsys@color@gray@fill{0.24}\ell_{2}}\\},[e_{16},e_{19}]\rangle$$\eta_{4}=\langle
t_{3},{\color[rgb]{0.354,0.354,0.354}\definecolor[named]{pgfstrokecolor}{rgb}{0.354,0.354,0.354}\pgfsys@color@gray@stroke{0.354}\pgfsys@color@gray@fill{0.354}\ell_{3}},\\{{\color[rgb]{0.24,0.24,0.24}\definecolor[named]{pgfstrokecolor}{rgb}{0.24,0.24,0.24}\pgfsys@color@gray@stroke{0.24}\pgfsys@color@gray@fill{0.24}\ell_{2}}\\},[e_{13}]\rangle$

${D}^{\textsf{abs}}=\langle\eta_{1},\eta_{3}\rangle$

$D_{1}=\langle e_{2},e_{16}\rangle$$D_{2}=\langle
e_{2},e_{19}\rangle$$D_{3}=\langle e_{4},e_{16}\rangle$$D_{4}=\langle
e_{4},e_{19}\rangle$$D_{5}=\langle e_{29},e_{16}\rangle$$D_{6}=\langle
e_{29},e_{19}\rangle$

Figure 3.  A trace $\sigma_{3}$, its abstract acquires $\eta_{i}$, unique
abstract deadlock pattern ${D}^{\textsf{abs}}$, concrete patterns
$D_{i}\in{D}^{\textsf{abs}}$.

###### Example 0.

Consider the trace $\sigma_{2}$ in Fig. 1(b). The deadlock pattern $D=\langle
e_{4},e_{18}\rangle$ is a sync-preserving deadlock, witnessed by the sync-
preserving correct reordering
$\rho_{3}=e_{1}e_{2}e_{3}e_{8}e_{9}\,e_{12}..e_{15}\,e_{16}e_{17}$. Now
consider the trace $\sigma_{3}$ from Fig. 3 and the deadlock pattern
$D_{5}=\langle e_{29},e_{16}\rangle$. This is a predictable deadlock,
witnessed by the correct reordering
$\rho_{5}=e_{1}..e_{7}e_{8}..e_{11}e_{12}..e_{15}\,e_{28}$. Observe that
$\rho_{5}$ is a sync-preserving reordering, which makes $D_{5}$ a sync-
preserving deadlock. A key aspect in $\rho_{5}$ is that the events
$e_{22}..e_{27}$ are dropped, as otherwise $e_{16}$ cannot be
$\sigma_{3}$-enabled. A similar reasoning applies for the deadlock pattern
$D_{6}$, and it is also a sync-preserving deadlock. The other deadlock
patterns ($D_{1},D_{2},D_{3},D_{4}$) are not predictable deadlocks.
Intuitively, the reason for this is that realizing these deadlock patterns
require executing the read event $e_{14}$, which then enforces to execute the
events $e_{8}..e_{11}$ and $e_{1}..e_{6}$. This prevents the deadlocks from
becoming realizable as the events $e_{2}$ or $e_{4}$ that appear in these
deadlock patterns are no longer $\sigma_{3}$-enabled. This point is detailed
in Example 4.7.

###  4.2. Characterizing Sync-Preserving Deadlocks

There are two fundamental tasks in searching for a correct reordering that
witnesses a deadlock — (i) determining the set of events in the correct
reordering, and (ii) identifying a total order on such events — both of which
are intractable (Mathur et al., 2020). On the contrary, for sync-preserving
deadlocks, we show that (a) the search for a correct reordering can be reduced
to the problem of checking if some well-defined set of events (Definition 4.4)
does not contain the events appearing in the deadlock pattern (Lemma 4.6), and
that (b) this set can be constructed efficiently.

###### Definition 0 (Sync-Preserving Closure).

Let $\sigma$ be a trace and $S\subseteq\mathsf{Events}_{\sigma}$. The sync-
preserving closure of $S$, denoted $\mathsf{SPClosure}_{\sigma}(S)$ is the
smallest set $S^{\prime}$ such that  (a) $S\subseteq S^{\prime}$,  (b) for
every $e,e^{\prime}\in\mathsf{Events}_{\sigma}$ such that
$e<^{\sigma}_{\mathsf{TO}}e^{\prime}$ or $e=\mathsf{rf}_{\sigma}(e^{\prime})$,
if $e^{\prime}\in S^{\prime}$, then $e\in S^{\prime}$, and  (c) for every lock
$\ell$ and every two distinct events $e,e^{\prime}\in S^{\prime}$ with
$\operatorname{op}(e)=\operatorname{op}(e^{\prime})=\mathtt{acq}(\ell)$, if
$e\leq^{\sigma}_{\mathsf{tr}}e^{\prime}$ then $\mathsf{match}_{\sigma}(e)\in
S^{\prime}$.

Definition 4.4 resembles the notion of correct reorderings (Definition 4.1).
Indeed, Lemma 4.5 justifies using this set — it is both a necessary and a
sufficient set for sync-preserving correct reorderings.

###### Lemma 4.5.

Let $\sigma$ be a trace and let $S\subseteq\mathsf{Events}_{\sigma}$. For any
sync-preserving correct reordering $\rho$ of $\sigma$, if
$S\subseteq\mathsf{Events}_{\rho}$, then
$\mathsf{SPClosure}_{\sigma}(S)\subseteq\mathsf{Events}_{\rho}$. Further,
there is a sync-preserving correct reordering $\rho$ of $\sigma$ such that
$\mathsf{Events}_{\rho}=\mathsf{SPClosure}_{\sigma}(S)$.

For an intuition, consider again Figure 3 and the sync-preserving correct
reordering $\rho_{5}=e_{1}..e_{7}e_{8}..e_{11}e_{12}..e_{15}\,e_{28}$ computed
in Example 4.3. According to Lemma 4.5,
$\mathsf{SPClosure}_{\sigma_{3}}(S)\subseteq\mathsf{Events}_{\rho_{5}}$ holds
for all $S$ such that $S\subseteq\mathsf{Events}_{\rho_{5}}$. For example, if
we take $S=\\{e_{1},e_{15}\\}$ then observe that
$S\subseteq\mathsf{Events}_{\rho_{5}}$ and
$\mathsf{SPClosure}_{\sigma_{3}}(S)=\\{e_{1},\ldots,e_{6},\,e_{8},\ldots
e_{15}\\}\subseteq\mathsf{Events}_{\rho_{5}}$ holds.

Based on Lemma 4.5, we present a sound and complete characterization of sync-
preserving deadlocks (Lemma 4.6). For a set
$S\subseteq\mathsf{Events}_{\sigma}$, we let $\textsf{pred}_{\sigma}(S)$
denote the set of immediate thread predecessors of events in $S$. That is,
$\textsf{pred}_{\sigma}(S)=\\{e\in\mathsf{Events}_{\sigma}\,|\,\exists f\in
S,e<^{\sigma}_{\mathsf{tr}}f\text{ and }\forall
e^{\prime}<^{\sigma}_{\mathsf{tr}}f,e^{\prime}\leq^{\sigma}_{\mathsf{TO}}e\\}$.

###### Lemma 4.6.

Let $\sigma$ be a trace and let $D=\langle e_{0},\ldots,e_{k-1}\rangle$ be a
deadlock pattern of size $k$ in $\sigma$. $D$ is a sync-preserving deadlock of
$\sigma$ iff $\mathsf{SPClosure}_{\sigma}(\textsf{pred}_{\sigma}(S))\cap
S=\varnothing$, where $S=\\{e_{0},\ldots,e_{k-1}\\}$.

###### Example 0.

Consider the trace $\sigma_{2}$ in Fig. 1(b), and the deadlock pattern
$D=\langle e_{4},e_{18}\rangle$. We have
$\mathsf{SPClosure}_{\sigma_{2}}(\textsf{pred}_{\sigma_{2}}(\\{e_{4},e_{18}\\}))=\\{e_{1},e_{2},e_{3},e_{8},e_{9},e_{12},\ldots,e_{17}\\}$.
Since we have that $e_{4},e_{18}\not\in$
$\mathsf{SPClosure}_{\sigma_{2}}(\textsf{pred}_{\sigma_{2}}(\\{e_{4},e_{18}\\}))$,
$D$ is a sync-preserving deadlock. Now consider the trace $\sigma_{3}$ in Fig.
3, and the deadlock patterns $D_{1}=\allowbreak\langle e_{2},e_{16}\rangle$,
$D_{5}=\allowbreak\langle e_{29},e_{16}\rangle$, and $D_{6}=\allowbreak\langle
e_{29},e_{19}\rangle$. We have
$\mathsf{SPClosure}_{\sigma_{3}}(\textsf{pred}_{\sigma_{3}}(\\{e_{2},e_{16}\\}))\allowbreak=\\{e_{1},\ldots,e_{6},e_{8},\ldots,e_{15}\\}$,
$\mathsf{SPClosure}_{\sigma_{3}}(\textsf{pred}_{\sigma_{3}}(\allowbreak\\{e_{29},e_{16}\\}))=\\{e_{1},\ldots,e_{15},e_{28}\\}$,
and
$\mathsf{SPClosure}_{\sigma_{3}}(\textsf{pred}_{\sigma_{3}}(\\{e_{29},e_{19}\\}))=\\{e_{1},\ldots,e_{18},e_{28}\\}$.
Since
$e_{2}\in\allowbreak\mathsf{SPClosure}_{\sigma_{3}}(\allowbreak\textsf{pred}_{\sigma_{3}}(\\{e_{2},e_{16}\\}))$,
$D_{1}$ is not a sync-preserving deadlock. However,
$e_{29},e_{16}\not\in\mathsf{SPClosure}_{\sigma_{3}}(\textsf{pred}_{\sigma_{3}}(\\{e_{29},e_{16}\\}))$,
and
$e_{29},e_{19}\not\in\mathsf{SPClosure}_{\sigma_{3}}(\textsf{pred}_{\sigma_{3}}(\\{e_{29},e_{19}\\}))$,
thus $D_{5}$ and $D_{6}$ are sync-preserving deadlocks (as we also concluded
in Example 4.3).

###  4.3. Verifying Deadlock Patterns

Given a deadlock pattern, we check if it constitutes a sync-preserving
deadlock by constructing the sync-preserving closure (Lemma 4.6) in linear
time. Based on Definition 4.4, this can be done in an iterative manner. We (i)
start with the set of $\leq_{\mathsf{TO}}$ predecessors of the events in the
deadlock pattern, and (ii) iteratively add $\leq_{\mathsf{TO}}$ and
$\mathsf{rf}$ predecessors of the current set of events. Additionally, we
identify and add the release events that must be included in the set. We
utilize _timestamps_ to ensure that the _entire_ fixpoint computation is
performed in linear time.

Thread-read-from timestamps. Given a set $\mathsf{Threads}$ of threads, a
timestamp is simply a mapping $T:\mathsf{Threads}\to\mathbb{N}$. Given
timestamps $T_{1},T_{2}$, we use the notations $T_{1}\sqsubseteq T_{2}$ and
$T_{1}\sqcup T_{2}$ for pointwise comparison and pointwise maximum,
respectively. For a set $U$ of timestamps, we write $\bigsqcup U$ to denote
the pointwise maximum over all elements of $U$. Let
$\leq^{\sigma}_{\mathsf{TRF}}$ be the reflexive transitive closure of the
relation
$(\leq^{\sigma}_{\mathsf{TO}}\cup\\{(\mathsf{rf}_{\sigma}(e),e)\,|\,\exists
x\in\mathsf{Vars}_{\sigma},\operatorname{op}(e)=\mathtt{r}(x)\\})$; observe
that $\leq^{\sigma}_{\mathsf{TRF}}$ is a partial order. We define the
timestamp $\mathsf{TS}_{\sigma}^{e}$ of an event $e$ in $\sigma$ to be a
$\mathsf{Threads}_{\sigma}$-indexed timestamp as follows:
$\mathsf{TS}_{\sigma}^{e}(t)=|\\{f\,|\,f\leq^{\sigma}_{\mathsf{TRF}}e\\}|$.
This ensures that for two events $e,e^{\prime}\in\mathsf{Events}_{\sigma}$,
$e\leq^{\sigma}_{\mathsf{TRF}}e^{\prime}$ iff
$\mathsf{TS}_{\sigma}^{e}\sqsubseteq\mathsf{TS}_{\sigma}^{e^{\prime}}$. For a
set $S\subseteq\mathsf{Events}_{\sigma}$, we overload the notation and say the
timestamp of $S$ is
$\mathsf{TS}_{\sigma}^{S}=\bigsqcup\\{\mathsf{TS}_{\sigma}^{e}\\}_{e\in S}$.
Given a trace $\sigma$ with $\mathcal{N}$ events and $\mathcal{T}$ threads we
can compute these timestamps for all the events in
$O(\mathcal{N}\cdot\mathcal{T})$ time, using a simple vector clock algorithm
(Mattern, 1989; Fidge, 1991).

Computing sync-preserving closures. Recall the basic template of the fixpoint
computation. In each iteration, we identify the set of release events that
must be included in the set, together with their
$\leq^{\sigma}_{\mathsf{TRF}}$-closure. In order to identify such events
efficiently, for every thread $t$ and lock $\ell$, we maintain a FIFO queue
$\mathsf{CSHist}_{t,\ell}$ (_critical section history_ of $t$ and $\ell$) to
store the sequence of events that acquire $\ell$ in thread $t$. In each
iteration, we traverse each list to determine the last acquire event that
belongs to the current set. For a given lock, we need to add the matching
release events of all thus identified events to the closure, except possibly
the matching release event of the latest acquire event (see Definition 4.4).
This computation is performed using timestamps, as shown in Algorithm 1.
Starting with a set $S$, the algorithm runs in time
$O(|S|\cdot\mathcal{T}+\mathcal{T}\cdot\mathcal{A})$, where $\mathcal{T}$ and
$\mathcal{A}$ are respectively the number of threads and acquire events in
$\sigma$.

Input: Trace $\sigma$, Timestamp $T_{0}$

1 let
$\\{\mathsf{CSHist}_{t,\ell}\\}_{\ell\in\mathsf{Locks}_{\sigma},t\in\mathsf{Threads}_{\sigma}}$
be the lock-acquisition histories in $\sigma$

2 $T\leftarrow T_{0}$

3 repeat

4 for  _$\ell\in\mathsf{Locks}$_ do

5 foreach  _$t\in\mathsf{Threads}$_ do

6 let $e_{t}$ be the last event in $\mathsf{CSHist}_{t,\ell}$ with
$\mathsf{TS}_{\sigma}^{e_{t}}\sqsubseteq T$

7 Remove all earlier events in $\mathsf{CSHist}_{t,\ell}$

8 let $e_{t*}$ be the last event in
$\\{e_{t}\\}_{t\in\mathsf{Threads}_{\sigma}}$ according to
$\leq^{\sigma}_{\mathsf{tr}}$

9 $T$ :=
$T\sqcup\bigsqcup\\{\mathsf{TS}_{\sigma}^{\mathsf{match}_{\sigma}(e_{t})}\,|\,e_{t}\neq
e_{t*}\\}$

10

11

12until  _$T$ does not change_

return $T$

Computing sync-preserving closure.

Algorithm 1 CompSPClosure:

Computing sync-preserving closure.

Input: Trace $\sigma$, ${D}^{\textsf{abs}}$ of length $k$

1 let $F_{0},\ldots,F_{k-1}$ be the sequences of acquires in
${D}^{\textsf{abs}}$

2 let $n_{0},\ldots,n_{k-1}$ be the lengths of $F_{0},\ldots,F_{k-1}$

3 foreach  _$j\in\\{0,\ldots,k-1\\}$_ do $i_{j}\leftarrow 1$

4 $T\leftarrow\lambda t,0$ while  _$\bigwedge\limits_{j=0}^{k-1}i_{j} <n_{j}$_
do

5 let $e_{0}=F_{0}[i_{0}],\ldots,e_{k-1}=F_{k-1}[i_{k-1}]$

6 $S\leftarrow\textsf{pred}_{\sigma}{\\{e_{0},\ldots,e_{k-1}\\}}$

7 $T\leftarrow$ CompSPClosure(_$\sigma,T\sqcup\mathsf{TS}_{\sigma}^{S}$_)

8 if  _$\forall j <k,\mathsf{TS}_{\sigma}^{e_{j}}\sqsubseteq T$_ then

9 report pattern $D=e_{0},\ldots,e_{k-1}$ and exit

10 foreach  _$j\in\\{0,\ldots,k-1\\}$_ do

11 $i_{j}=\min\\{l\leq
n_{j}\,|\,\mathsf{TS}_{\sigma}^{F_{j}[l]}\not\sqsubseteq T\\}$

12

Checking an abstract deadlock pattern.

Algorithm 2 CheckAbsDdlck:

Checking an abstract deadlock pattern.

Checking a deadlock pattern. After computing the timestamp $T$ of the closure
(output of Algorithm 1, starting with the set of events in the given deadlock
pattern), determining whether a given deadlock pattern
$D=e_{0},\ldots,e_{k-1}$ is a sync-preserving deadlock can be performed in
time $O(k\cdot\mathcal{T})$ — simply check if $\forall
i,\mathsf{TS}_{\sigma}(e_{i})\not\sqsubseteq T$. This gives an algorithm for
checking if a deadlock pattern of length $k$ is sync-preserving that runs in
time
$O(\mathcal{T}\cdot\mathcal{N}+k\cdot\mathcal{T}+\mathcal{T}\cdot\mathcal{A})=O(\mathcal{N}\cdot\mathcal{T})$.

###  4.4. Verifying Abstract Deadlock Patterns

Abstract acquires and abstract deadlock patterns. Given a thread $t$, a lock
$\ell$ and a set of locks $L\subseteq\mathsf{Locks}_{\sigma}\neq\varnothing$
with $\ell\not\in L$, we define the _abstract acquire_ $\eta=\langle
t,\ell,L,F\rangle$, where $F=[e_{1},\dots,e_{n}]$ is the sequence of all
events $e_{i}\in\mathsf{Events}_{\sigma}$ (in trace-order) such that for each
$i$, we have (i) $\operatorname{thread}(e_{i})=t$, (ii)
$\operatorname{op}(e_{i})=\mathtt{acq}(\ell)$, and (iii)
$\mathsf{HeldLks}_{\sigma}(e_{i})=L$. In words, the abstract acquire $\eta$
contains the sequence of all acquire events of a specific thread, that access
a specific lock and hold the same set of locks when executed, ordered as per
thread order. An _abstract deadlock pattern_ of size $k$ in a trace $\sigma$
is a sequence ${D}^{\textsf{abs}}=\eta_{0},\dots,\eta_{k-1}$ of abstract
acquires $\eta_{i}=\langle t_{i},\ell_{i},L_{i},F_{i}\rangle$ such that
$t_{0},\ldots,t_{k-1}$ are distinct threads, $\ell_{0},\ldots,\ell_{k-1}$ are
distinct locks, and
$L_{0},L_{1},\ldots,L_{k-1}\subseteq\mathsf{Locks}_{\sigma}$ are such that
$\ell_{i}\not\in L_{i}$, $\ell_{i}\in L_{(i+1)\%k}$ for every $i$, and
$L_{i}\cap L_{j}=\varnothing$ for every $i\neq j$. Thus, an abstract deadlock
pattern ${D}^{\textsf{abs}}$ succinctly encodes all concrete deadlock patterns
$F_{0}\times F_{1}\times\dots\times F_{k-1}$, called _instantiations_ of
${D}^{\textsf{abs}}$. We also write $D\in{D}^{\textsf{abs}}$ to denote that
$D\in F_{0}\times F_{1}\times\dots\times F_{k-1}$. We say that
${D}^{\textsf{abs}}$ contains a sync-preserving deadlock if there exists some
instantiation $D\in{D}^{\textsf{abs}}$ that is a sync-preserving deadlock. See
Fig. 3 for an example. Our next result is stated below, followed by its proof
idea.

###### Lemma 4.8.

Consider a trace $\sigma$ with $\mathcal{N}$ events and $\mathcal{T}$ threads,
and an abstract deadlock pattern ${D}^{\textsf{abs}}$ of $\sigma$. We can
determine if ${D}^{\textsf{abs}}$ contains a sync-preserving deadlock in
$O(\mathcal{T}\cdot\mathcal{N})$ time.

An abstract deadlock pattern of length $k\geq 2$ can have $\mathcal{N}^{k}$
instantiations, giving a naive enumerate-and-check algorithm running in time
$O(\mathcal{T}\cdot\mathcal{N}^{k+1})$, which is prohibitively large. Instead,
we exploit (i) the monotonicity properties of the sync-preserving closure
(Proposition 4.9) and (ii) instantiations of an abstract pattern (Corollary
4.10) that allow for an _incremental_ algorithm that iteratively checks
successive instantiations of a given abstract deadlock pattern, while spending
total $O(\mathcal{N}\cdot\mathcal{T})$ time. The first observation allows us
to re-use a prior computation when checking later deadlock patterns.

###### Proposition 4.9.

For a trace $\sigma$ and sets $S,S^{\prime}\subseteq\mathsf{Events}_{\sigma}$.
If for every event $e\in S$, there is an event $e^{\prime}\in S^{\prime}$ such
that $e\leq^{\sigma}_{\mathsf{TO}}e^{\prime}$, then
$\mathsf{SPClosure}_{\sigma}(S)\subseteq\mathsf{SPClosure}_{\sigma}(S^{\prime})$.

Consider $\sigma_{3}$ in Figure 3 and let
$S=\textsf{pred}_{\sigma_{3}}{(\\{e_{29},e_{16}\\})}$, and
$S^{\prime}=\textsf{pred}_{\sigma_{3}}{(\\{e_{29},e_{19}\\})}$. The sets
$S,S^{\prime}$ satisfy the conditions of Proposition 4.9, hence
$\mathsf{SPClosure}_{\sigma_{3}}(S)\subseteq\mathsf{SPClosure}_{\sigma_{3}}(S^{\prime})$,
as computed in Example 4.7. Next, we extend Proposition 4.9 to avoid redundant
computations when a sync-preserving deadlock is not found and later deadlock
patterns must be checked. Given two deadlock patterns
$D_{1}=e_{0},\ldots,e_{k-1}$ and $D_{2}=f_{0},\ldots,f_{k-1}$ of the same
length $k$, we say $D_{1}\prec D_{2}$ if they are instantiations of a common
abstract pattern ${D}^{\textsf{abs}}$ (i.e.,
$D_{1},D_{2}\in{D}^{\textsf{abs}}$) and for every $i<k$,
$e_{i}\leq^{\sigma}_{\mathsf{TO}}f_{i}$.

###### Corollary 4.10.

Let $\sigma$ be a trace and let $D_{1}=e_{0},\ldots,e_{k-1}$ and
$D_{2}=f_{0},\ldots f_{k-1}$ be deadlock patterns of size $k$ in $\sigma$ such
that $D_{1}\prec D_{2}$. Let $S_{1}=\\{e_{0},\ldots,e_{k-1}\\}$ and
$S_{2}=\\{f_{0},\ldots,f_{k-1}\\}$. If
$\mathsf{SPClosure}_{\sigma}(\textsf{pred}_{\sigma}(S_{1}))\cap
S_{2}\neq\varnothing$, then
$\mathsf{SPClosure}_{\sigma}(\textsf{pred}_{\sigma}(S_{2}))\cap
S_{2}\neq\varnothing$.

We now describe how Proposition 4.9 and Corollary 4.10 are used in our
algorithms, and illustrate them later in Example 4.12. Algorithm 2 checks if
an abstract deadlock pattern contains a sync-preserving deadlock. The
algorithm iterates over the sequences $F_{0},\ldots,F_{k-1}$ of acquires (one
for each abstract acquire) in trace order. For this, it maintains indices
$i_{0},\ldots,i_{k-1}$ that point to entries in $F_{0},\ldots,F_{k-1}$. At
each step, it determines whether the current deadlock pattern
$D=e_{0},\ldots,e_{k-1}$ constitutes a sync-preserving deadlock by computing
the sync-preserving closure of the thread-local predecessors of the events of
the deadlock pattern. The algorithm reports a deadlock if the sync-preserving
closure does not contain any of $e_{0},\ldots,e_{k-1}$. Otherwise, it looks
for the next eligible deadlock pattern, which it determines based on Corollary
4.10. In particular, it advances the pointer $i_{j}$ all the way until an
entry which is outside of the closure computed so far. Observe that the
timestamp $T$ of the closure computed in an iteration is being used in later
iterations; this is a consequence of Proposition 4.9. Furthermore, in the call
to the Algorithm 1 at Line 2, we ensure that the list of acquires
$\mathsf{CSHist}_{t,\ell}$, used in the function CompSPClosure is reused
across iterations, and not re-assigned to the original list of all acquire
events. The correctness of this optimization follows from Proposition 4.9. Let
us now calculate the running time of Algorithm 2. Each of the
$\mathsf{CSHist}_{t,\ell}$ in CompSPClosure is traversed at most once. Next,
each element of the sequences $F_{0},\ldots,F_{k-1}$ is also traversed at most
once. For each of these acquires, the algorithm spends $O(\mathcal{T})$ time
for vector clock updates. The total time required is thus
$O(\mathcal{N}\cdot\mathcal{T})$. This concludes the proof of Lemma 4.8.

###  4.5. The Algorithm SPDOffline

We now present the final ingredients of SPDOffline. We construct the _abstract
lock graph_ , enumerate cycles in it, check whether any cycle is an abstract
deadlock pattern, and if so, whether it contains sync-preserving deadlocks.

$t_{1},{\color[rgb]{0.24,0.24,0.24}\definecolor[named]{pgfstrokecolor}{rgb}{0.24,0.24,0.24}\pgfsys@color@gray@stroke{0.24}\pgfsys@color@gray@fill{0.24}\ell_{2}},\\{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\ell_{1}}\\},[e_{2}]$$t_{2},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\ell_{1}},\\{{\color[rgb]{0.24,0.24,0.24}\definecolor[named]{pgfstrokecolor}{rgb}{0.24,0.24,0.24}\pgfsys@color@gray@stroke{0.24}\pgfsys@color@gray@fill{0.24}\ell_{2}}\\},[e_{8}]$

$t_{2},{\color[rgb]{0.354,0.354,0.354}\definecolor[named]{pgfstrokecolor}{rgb}{0.354,0.354,0.354}\pgfsys@color@gray@stroke{0.354}\pgfsys@color@gray@fill{0.354}\ell_{3}},\\{{\color[rgb]{0.24,0.24,0.24}\definecolor[named]{pgfstrokecolor}{rgb}{0.24,0.24,0.24}\pgfsys@color@gray@stroke{0.24}\pgfsys@color@gray@fill{0.24}\ell_{2}}\\},[e_{4}]$$t_{3},{\color[rgb]{0.24,0.24,0.24}\definecolor[named]{pgfstrokecolor}{rgb}{0.24,0.24,0.24}\pgfsys@color@gray@stroke{0.24}\pgfsys@color@gray@fill{0.24}\ell_{2}},\\{{\color[rgb]{0.354,0.354,0.354}\definecolor[named]{pgfstrokecolor}{rgb}{0.354,0.354,0.354}\pgfsys@color@gray@stroke{0.354}\pgfsys@color@gray@fill{0.354}\ell_{3}}\\},[e_{18}]$

$t_{1},{\color[rgb]{0.24,0.24,0.24}\definecolor[named]{pgfstrokecolor}{rgb}{0.24,0.24,0.24}\pgfsys@color@gray@stroke{0.24}\pgfsys@color@gray@fill{0.24}\ell_{2}},\\{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\ell_{1}}\\}$,
$[e_{2},e_{4},e_{29}]$$t_{2},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\ell_{1}},\\{{\color[rgb]{.75,.5,.25}\definecolor[named]{pgfstrokecolor}{rgb}{.75,.5,.25}\ell_{4}}\\}$,
$[e_{23}]$$t_{3},{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\ell_{1}},\\{{\color[rgb]{0.24,0.24,0.24}\definecolor[named]{pgfstrokecolor}{rgb}{0.24,0.24,0.24}\pgfsys@color@gray@stroke{0.24}\pgfsys@color<EMAIL_ADDRESS>$[e_{16},e_{19}]$$t_{3},{\color[rgb]{0.354,0.354,0.354}\definecolor[named]{pgfstrokecolor}{rgb}{0.354,0.354,0.354}\pgfsys@color@gray@stroke{0.354}\pgfsys@color@gray@fill{0.354}\ell_{3}},\\{{\color[rgb]{0.24,0.24,0.24}\definecolor[named]{pgfstrokecolor}{rgb}{0.24,0.24,0.24}\pgfsys@color@gray@stroke{0.24}\pgfsys@color<EMAIL_ADDRESS>$[e_{13}]$

Figure 4.  Abstract lock graphs of the traces from Fig. 1(a) (left), Fig. 1(b)
(middle) and Fig. 3 (right).

Abstract lock graph. The abstract lock graph of $\sigma$ is a directed graph
$\mathsf{ALG}_{\sigma}=(V_{\sigma},E_{\sigma})$, where

  * •

$V_{\sigma}=\\{\langle t_{1},\ell_{1},L_{1},F_{1}\rangle,\dots,\langle
t_{k},\ell_{k},L_{k},F_{k}\rangle\\}$ is the set of abstract acquires of
$\sigma$, and

  * •

for every $\eta_{1}{=}\langle
t_{1},\ell_{1},L_{1},F_{1}\rangle,\eta_{2}{=}\langle
t_{2},\ell_{2},L_{2},F_{2}\rangle\in V_{\sigma}$, we have
$(\eta_{1},\eta_{2})\in E_{\sigma}$ iff $t_{1}\neq t_{2}$, $\ell_{1}\in
L_{2}$, and $L_{1}\cap L_{2}=\varnothing$.

A node $\langle t_{1},\ell_{1},L_{1},F_{1}\rangle$ signifies that there is an
event $\mathtt{acq}_{1}(\ell_{1})$ performed by thread $t_{1}$ while holding
the locks in $L_{1}$. The last component $F_{1}$ is a list which contains all
such events $\mathtt{acq}_{1}$ in order of appearance in $\sigma$. An edge
$(\eta_{1},\eta_{2})$ signifies that the lock $\ell_{1}$ acquired by each of
the events $\mathtt{acq}_{1}\in F_{1}$ was held by $t_{2}$ when it executed
each of $\mathtt{acq}_{2}\in F_{2}$ while not holding a common lock. The
abstract lock graph can be constructed incrementally as new events appear in
$\sigma$. For $\mathcal{N}$ events, $\mathcal{L}$ locks and nesting depth $d$,
the graph has $|V_{\sigma}|=O\big{(}\mathcal{T}\cdot\mathcal{L}^{d}\big{)}$
vertices, $|E_{\sigma}|=O(|V_{\sigma}|\cdot\mathcal{L}^{d-1})$ edges and can
be constructed in $O(\mathcal{N}\cdot d)$ time. See Fig. 4 for examples. In
the left graph, the cycle marks an abstract deadlock pattern and its single
concrete deadlock pattern ${D}^{\textsf{abs}}=\\{e_{2}\\}\times\\{e_{8}\\}$,
and similarly for the middle graph where
${D}^{\textsf{abs}}=\\{e_{4}\\}\times\\{e_{18}\\}$. In the right graph, there
is a unique cycle which marks an abstract deadlock pattern of $6$ concrete
deadlock patterns
${D}^{\textsf{abs}}=\\{e_{2},e_{4},e_{29}\\}\times\\{e_{16},e_{19}\\}$.

Input: A trace $\sigma$.

Output: All abstract deadlock patterns of $\sigma$ that contain a sync-
preserving deadlock.

1 Construct the abstract lock graph $\mathsf{ALG}_{\sigma}$

2 foreach  _cycle $C=\langle\eta_{0},\dots,\eta_{k-1}\rangle$ in $G$_ do

3 Let $\eta_{i}=\langle t_{i},\ell_{i},L_{i},F_{i}\rangle$

4 if  _$\forall i\neq j$ we have $t_{i}\neq t_{j}$ and $\ell_{i}\neq\ell_{j}$
and $L_{i}\cap L_{j}=\varnothing$ _ then // $C$ is an abstract deadlock
pattern

5 if  _$\textnormal{{CheckAbsDdlck}}(C)$_ then Report that $C$ contains a
sync-preserving deadlock

6

7

Algorithm 3 Algorithm SPDOffline.

Algorithm SPDOffline. It is straightforward to verify that every abstract
deadlock pattern of $\sigma$ appears as a (simple) cycle in
$\mathsf{ALG}_{\sigma}$. However, the opposite is not true. A cycle
$C=\eta_{0},\eta_{1},\ldots,\eta_{k-1}$ of $\mathsf{ALG}_{\sigma}$, where
$\eta_{i}=\langle t_{i},\ell_{i},L_{i},F_{i}\rangle$ defines an abstract
deadlock pattern if additionally every thread $t_{i}$ is distinct, all every
lock $\ell_{i}$ is distinct, and all sets $L_{i}$ are pairwise disjoint. This
gives us a simple recipe for enumerating all abstract deadlock patterns, by
using Johnson’s algorithm (Johnson, 1975) to enumerate every simple cycle $C$
in $\mathsf{ALG}_{\sigma}$, and check whether $C$ is an abstract deadlock
pattern. We thus arrived at our offline algorithm SPDOffline (Algorithm 3).
The running time depends linearly on the length of $\sigma$ and the number of
cycles in $\mathsf{ALG}_{\sigma}$.

###### Theorem 4.11.

Consider a trace $\sigma$ of $\mathcal{N}$ events, $\mathcal{T}$ threads and
$\textsf{Cyc}_{\sigma}$ cycles in $\mathsf{ALG}_{\sigma}$. The algorithm
SPDOffline reports all sync-preserving deadlocks of $\sigma$ in time
$O(\mathcal{N}\cdot\mathcal{T}\cdot\textsf{Cyc}_{\sigma})$.

Although, in principle, we can have exponentially many cycles in
$\mathsf{ALG}_{\sigma}$, because the nodes of $\mathsf{ALG}_{\sigma}$ are
_abstract_ acquire events (as opposed to _concrete_), we expect that the
number of cycles (and thus abstract deadlock patterns) in
$\mathsf{ALG}_{\sigma}$ remains small, even though the number of _concrete_
deadlock patterns can grow exponentially. Since SPDOffline spends linear time
per abstract deadlock pattern, we have an efficient procedure overall for
constant $\mathcal{T}$ and $\mathcal{L}$. We evaluate $\textsf{Cyc}_{\sigma}$
experimentally in Section 6, and confirm that it is very small compared to the
number of concrete deadlock patterns in $\sigma$. Nevertheless,
$\textsf{Cyc}_{\sigma}$ can become exponential when $\mathcal{T}$ and
$\mathcal{L}$ are large, making Algorithm 3 run in exponential time. Note that
this barrier is unavoidable in general, as proven in Theorem 3.1.

###### Example 0.

We illustrate how the lock graph is integrated inside SPDOffline. Consider the
trace $\sigma_{3}$ in Fig. 3. It contains $6$ concrete deadlock patterns
$D_{1}\ldots D_{6}$. A naive algorithm would enumerate each pattern explicitly
until it finds a deadlock. However, the tight interplay between the abstract
lock graph and sync-preservation enables a more efficient procedure.
SPDOffline starts by computing the sync-preserving closure of $D_{1}$,
$\mathsf{SPClosure}_{\sigma_{3}}(\textsf{pred}_{\sigma_{3}}(\\{e_{2},e_{16}\\}))=\\{e_{1},\ldots,e_{6},\,e_{8},\ldots,e_{15}\\}$.
As
$e_{2}\in\mathsf{SPClosure}_{\sigma_{3}}(\textsf{pred}_{\sigma_{3}}(\\{e_{2},e_{16}\\}))$,
we conclude that $D_{1}$ is not a sync-preserving deadlock. The algorithm
further deduces that the deadlock patterns $D_{2}$, $D_{3}$ and $D_{4}$ are
also not sync-preserving deadlocks, as follows. $D_{2}=\langle
e_{2},e_{19}\rangle$ shares a common event $e_{2}$ with $D_{1}$ but contains
the event $e_{19}$ instead of $e_{16}$, while
$e_{5}\in\mathsf{SPClosure}_{\sigma_{3}}(\textsf{pred}_{\sigma_{3}}(\\{e_{2},e_{16}\\}))$.
Since $e_{16}\leq^{\sigma_{3}}_{\mathsf{TO}}e_{19}$, and the sync-preserving
closure grows monotonically (Proposition 4.9), the sync-preserving closure of
$e_{2}$ and $e_{19}$ will also contain $e_{5}$ (and thus $e_{2}$). Therefore,
$D_{2}$ cannot be a sync-preserving deadlock. This reasoning is formalized in
Corollary 4.10, and also applies to $D_{3}$ and $D_{4}$. Next, the algorithm
proceeds with $D_{5}$. The above reasoning does not hold for $D_{5}$ as
$\mathsf{SPClosure}_{\sigma_{3}}(\textsf{pred}_{\sigma_{3}}(\\{e_{2},e_{16}\\}))\cap
S_{5}=\varnothing$ where $S_{5}=\\{e_{29},e_{16}\\}$. The algorithm then
computes the sync-preserving closure of $D_{5}$, reports a deadlock (Example
4.7) and stops analyzing this abstract deadlock pattern. In the end, we have
only explicitly enumerated the deadlock patterns $D_{1}$ and $D_{5}$.

###### Remark 1.

Although the concept of lock graphs exists in the literature (Havelund, 2000;
Bensalem and Havelund, 2005; Cai et al., 2020; Cai and Chan, 2014), our notion
of _abstract_ lock graphs is novel and tailored to sync-preserving deadlocks.
The closest concept to abstract lock graphs is that of equivalent cycles (Cai
and Chan, 2014). However, equivalent cycles unify all the concrete patterns of
a given abstract pattern and lead to unsound deadlock detection, which was
indeed their use.

##  5\. On-the-fly Deadlock Prediction

Although SPDOffline is efficient, both theoretically (Theorem 4.11) and in
practice (Table 1), it runs in two passes, akin to other predictive deadlock-
detection methods (Kalhauge and Palsberg, 2018; Cai et al., 2021). In a
runtime monitoring setting, it is desirable to operate in an _online_ fashion.
Recall that $\textnormal{{CheckAbsDdlck}}(\cdot)$ indeed operates online
(Section 4.4), while the offline nature of SPDOffline is tied to the offline
construction of the abstract lock graph $\mathsf{ALG}_{\sigma}$. To achieve
the golden standard of online, linear-time, sound deadlock prediction, we
focus on deadlocks of size $2$. This focus is barely restrictive as most
deadlocks in the wild have size $2$ (Lu et al., 2008). Further, deadlocks of
size $2$ enjoy the following computational benefits:  (a) cycles of length $2$
can be detected instantaneously without performing graph traversals, and  (b)
_every_ cycle of length $2$ is an abstract deadlock pattern.

Algorithm SPDOnline. The algorithm SPDOnline maintains all abstract acquires
of the form $\eta=\langle t,\ell_{1},\\{\ell_{2}\\},F\rangle$, i.e., we only
focus on one lock $\ell_{2}$ that is protecting each such acquire. When a new
acquire event $e=\langle t,\mathtt{acq}(\ell_{1})\rangle$ is encountered, the
algorithm iterates over all the locks
$\ell_{2}\in\mathsf{HeldLks}_{\sigma}(e)$ that are held in $e$, and append the
event $e$ to the sequence $F$ of the corresponding abstract acquire
$\eta=\langle t,\ell_{1},\\{\ell_{2}\\},F\rangle$; $F$ is maintained as FIFO
queue. Recall that we use timestamps on the acquire events in $F$ to determine
membership in our closure computation. Our online algorithm computes these
timestamps on-the-fly and stores them in these queues together with the
events. Then the algorithm calls $\textnormal{{CheckAbsDdlck}}(C)$ on the
abstract deadlock pattern $C$ formed between $\eta$ and $\eta^{\prime}=\langle
t^{\prime}\neq t,\ell_{2},\\{\ell_{1}\\},F^{\prime}\rangle$, in order to check
for sync-preserving deadlocks between the deadlock patterns in $F\times
F^{\prime}$. If $\textnormal{{CheckAbsDdlck}}(C)$ reports no deadlock, the
contents of $F^{\prime}$ are emptied as we are guaranteed that $F^{\prime}$
will not cause a sync-preserving deadlock with any further acquire of thread
$t$ on lock $\ell_{1}$. For a trace with $\mathcal{N}$ events, $\mathcal{T}$
threads and $\mathcal{L}$ locks. The algorithm calls CheckAbsDdlck for each of
the $O(\mathcal{T}^{2}\cdot\mathcal{L}^{2})$ abstract deadlock patterns of
size $2$, each call taking $O(\mathcal{N}\cdot\mathcal{T})$ time.

1

2function  _checkDeadlock(_$Lst$ , $I$, $\langle
t_{1},\ell_{1},t_{2},\ell_{2}\rangle$_)_

3 while
_$\textnormal{{not}}\,{Lst}\mathchoice{\mathbin{\vbox{\hbox{\scalebox{0.5}{$\displaystyle\bullet$}}}}}{\mathbin{\vbox{\hbox{\scalebox{0.5}{$\textstyle\bullet$}}}}}{\mathbin{\vbox{\hbox{\scalebox{0.5}{$\scriptstyle\bullet$}}}}}{\mathbin{\vbox{\hbox{\scalebox{0.5}{$\scriptscriptstyle\bullet$}}}}}{\textup{{isEmpty()}}}$_
do

4 ($C_{\textsf{pred}},C$) :=
${Lst}\mathchoice{\mathbin{\vbox{\hbox{\scalebox{0.5}{$\displaystyle\bullet$}}}}}{\mathbin{\vbox{\hbox{\scalebox{0.5}{$\textstyle\bullet$}}}}}{\mathbin{\vbox{\hbox{\scalebox{0.5}{$\scriptstyle\bullet$}}}}}{\mathbin{\vbox{\hbox{\scalebox{0.5}{$\scriptscriptstyle\bullet$}}}}}{\textup{{first()}}}$

5 $I$ := CompSPClosure(_$I\sqcup C_{\textsf{pred}}$ , $\langle
t_{1},\ell_{1},t_{2},\ell_{2}\rangle$_)

6 if  _$C\not\sqsubseteq I$_ then declare ‘Deadlock’ and break

7
${Lst}\mathchoice{\mathbin{\vbox{\hbox{\scalebox{0.5}{$\displaystyle\bullet$}}}}}{\mathbin{\vbox{\hbox{\scalebox{0.5}{$\textstyle\bullet$}}}}}{\mathbin{\vbox{\hbox{\scalebox{0.5}{$\scriptstyle\bullet$}}}}}{\mathbin{\vbox{\hbox{\scalebox{0.5}{$\scriptscriptstyle\bullet$}}}}}{\textup{{removeFirst()}}}$

8 return $I$

9

10handler  _write(_$t$ , $x$_)_

11 $\mathbb{LW}_{x}$ := $\mathbb{C}_{t}$

12 $\mathbb{C}_{t}$ := $\mathbb{C}_{t}[t\mapsto\mathbb{C}_{t}(t)+1]$

13

14handler  _release(_$t$ , $\ell$_)_

15 $\mathbb{C}_{t}$ := $\mathbb{C}_{t}[t\mapsto\mathbb{C}_{t}(t)+1]$

16 foreach
_$t_{1},t_{2}\in\mathsf{Threads},\ell_{1},\ell_{2}\in\mathsf{Locks}$_ do

17 ${{{\mathsf{CSHist}}_{t,\ell}^{\langle
t_{1},\ell_{1},t_{2},\ell_{2}\rangle}}\mathchoice{\mathbin{\vbox{\hbox{\scalebox{0.5}{$\displaystyle\bullet$}}}}}{\mathbin{\vbox{\hbox{\scalebox{0.5}{$\textstyle\bullet$}}}}}{\mathbin{\vbox{\hbox{\scalebox{0.5}{$\scriptstyle\bullet$}}}}}{\mathbin{\vbox{\hbox{\scalebox{0.5}{$\scriptscriptstyle\bullet$}}}}}{\textup{{last()}}}}\mathchoice{\mathbin{\vbox{\hbox{\scalebox{0.5}{$\displaystyle\bullet$}}}}}{\mathbin{\vbox{\hbox{\scalebox{0.5}{$\textstyle\bullet$}}}}}{\mathbin{\vbox{\hbox{\scalebox{0.5}{$\scriptstyle\bullet$}}}}}{\mathbin{\vbox{\hbox{\scalebox{0.5}{$\scriptscriptstyle\bullet$}}}}}{\textup{{updateRelease($\mathbb{C}_{t}$)}}}$

18

19

20handler  _acquire(_$t$ , $\ell$_)_

21 $C_{\textsf{pred}}$ := $\mathbb{C}_{t}$

22 $\mathbb{C}_{t}$ := $\mathbb{C}_{t}[t\mapsto\mathbb{C}_{t}(t)+1]$

23 ${g}_{\ell}$ := ${g}_{\ell}+1$

24 foreach
_$t_{1},t_{2}\in\mathsf{Threads},\ell_{1},\ell_{2}\in\mathsf{Locks}$_ do

25 ${{\mathsf{CSHist}}_{t,\ell}^{\langle
t_{1},\ell_{1},t_{2},\ell_{2}\rangle}}\mathchoice{\mathbin{\vbox{\hbox{\scalebox{0.5}{$\displaystyle\bullet$}}}}}{\mathbin{\vbox{\hbox{\scalebox{0.5}{$\textstyle\bullet$}}}}}{\mathbin{\vbox{\hbox{\scalebox{0.5}{$\scriptstyle\bullet$}}}}}{\mathbin{\vbox{\hbox{\scalebox{0.5}{$\scriptscriptstyle\bullet$}}}}}{\textup{{addLast($({g}_{\ell},\mathbb{C}_{t},\bot)$)}}}$

26 foreach  _$u\in\mathsf{Threads}$ , $\ell^{\prime}\in\mathsf{HeldLks}$_ do

27 ${{\mathsf{AcqHist}}_{t,\ell,\ell^{\prime}}^{\langle
u\rangle}}\mathchoice{\mathbin{\vbox{\hbox{\scalebox{0.5}{$\displaystyle\bullet$}}}}}{\mathbin{\vbox{\hbox{\scalebox{0.5}{$\textstyle\bullet$}}}}}{\mathbin{\vbox{\hbox{\scalebox{0.5}{$\scriptstyle\bullet$}}}}}{\mathbin{\vbox{\hbox{\scalebox{0.5}{$\scriptscriptstyle\bullet$}}}}}{\textup{{addLast(($C_{\textsf{pred}}$,
$\mathbb{C}_{t}$))}}}$

28 foreach  _$u\neq t\in\mathsf{Threads}$ ,
$\ell^{\prime}\in\mathsf{HeldLks}$_ do

29 $I$ := ${\mathbb{I}}^{\langle u,\ell^{\prime}t,\ell\rangle}\sqcup
C_{\textsf{pred}}$

30 ${\mathbb{I}}^{\langle u,\ell^{\prime}t,\ell\rangle}$ :=
checkDeadlock(_${\mathsf{AcqHist}}_{u,\ell^{\prime},\ell\,}^{\langle
t\rangle}$ , $I$, $\langle u,\ell^{\prime}t,\ell\rangle$_)

31

32

33handler  _read(_$t$ , $x$_)_

34 $\mathbb{C}_{t}$ := $\mathbb{C}_{t}\sqcup\mathbb{LW}_{x}$

35

Algorithm 4 SPDOnline.

SPDOnline is shown in detail in Algorithm 4. The pseudocode contains handlers
for processing the different events of $\sigma$ in a streaming fashion, as
well as a helper function for checking deadlocks. The main data structures of
the algorithm are (i) vector clocks $\mathbb{C}_{t}$, $\mathbb{LW}_{x}$, and
${\mathbb{I}}^{\langle t_{1},\ell_{1},t_{2},\ell_{2}\rangle}$, (ii) scalar
${g}_{\ell}$, and (iii) FIFO queues of vector clocks
${\mathsf{CSHist}}_{t,\ell}^{\langle t_{1},\ell_{1},t_{2},\ell_{2}\rangle}$
and ${\mathsf{AcqHist}}_{t,\ell_{1},\ell_{2}}^{\langle u\rangle}$, where
$t,t_{1},t_{2},u$ range over threads, $x$ ranges over variables, and
$\ell,\ell_{1},\ell_{2}$ range over locks. $\mathbb{C}_{t}$ stores the
timestamp $\mathsf{TS}_{\sigma}^{e}$ where $e$ is the last event in thread
$t$. $\mathbb{LW}_{x}$ keeps track of the $\mathsf{TS}_{\sigma}^{e}$ where $e$
is the last event such that $\operatorname{op}(e)=\mathtt{w}(x)$.
${\mathbb{I}}^{\langle t_{1},\ell_{1},t_{2},\ell_{2}\rangle}$ stores the
computed sync-preserving closures for every tuple $\langle
t_{1},\ell_{1},t_{2},\ell_{2}\rangle$. The scalar variable ${g}_{\ell}$ keeps
track of the index of the last acquire event on lock $\ell$. Similar to
Algorithm 1, the FIFO queue ${\mathsf{CSHist}}_{t,\ell}^{\langle
t_{1},\ell_{1},t_{2},\ell_{2}\rangle}$ is maintained to keep track of the
critical section history of thread $t$ and lock $\ell$. Lastly, for an acquire
event $e$, ${\mathsf{AcqHist}}_{t,\ell_{1},\ell_{2}}^{\langle u\rangle}$
maintains a queue of tuples of the form $\langle
C_{\textsf{pred}},\mathbb{C}_{t}\rangle$ where $C_{\textsf{pred}}$ and
$\mathbb{C}_{t}$ are the timestamps of $\textsf{pred}_{\sigma}(e)$ and $e$,
respectively These tuples are utilized when checking for deadlocks (Algorithm
4).

###### Theorem 5.1.

Consider a trace $\sigma$ of $\mathcal{N}$ events, $\mathcal{T}$ threads and
$\mathcal{L}$ locks. The online SPDOnline algorithm reports all sync-
preserving deadlocks of size $2$ of $\sigma$ in
$O(\mathcal{N}\cdot\mathcal{T}^{3}\cdot\mathcal{L}^{2})$ time.

##  6\. Experimental Evaluation

We first evaluated our algorithms in an offline setting (Section 6.1), where
we record execution traces and evaluate different approaches on the _same_
input. This eliminates biases due to non-deterministic thread scheduling.
Next, we consider an online setting (Section 6.2), where we instrument
programs and perform the analyses during runtime. We conducted all our
experiments on a standard laptop with
$1.8\text{\,}\mathrm{G}\mathrm{H}\mathrm{z}$ Intel Core i7 processor and
$16\text{\,}\mathrm{G}\mathrm{B}$ RAM.

###  6.1. Offline Experiments

Experimental setup. The goal of the first set of experiments is to evaluate
SPDOffline, and compare it against prior algorithms for dynamic deadlock
prediction. In order for our evaluation to be precise we evaluate all
algorithms on the _same_ execution trace. We implemented SPDOffline in Java
inside the RAPID analysis tool (Mathur, 2019), following closely the
pseudocode in Algorithm 3. RAPID takes as input execution traces, as defined
in Section 2. These also include fork, join, and lock-request events. We
compare SPDOffline with two state-of-the-art, theoretically-sound albeit
computationally more expensive, deadlock predictors, SeqCheck (Cai et al.,
2021) and Dirk (Kalhauge and Palsberg, 2018), both of which also work on
execution traces.

On the theoretical side, the complexity of SeqCheck is
$\widetilde{O}(\mathcal{N}^{4})$, as opposed to the
$\widetilde{O}(\mathcal{N})$ complexity of SPDOffline. Moreover, SeqCheck only
predicts deadlocks of size $2$, and though it could be extended to handle
deadlocks of any size, this would degrade performance further. SeqCheck may
miss sync-preserving deadlocks even of size $2$, but can detect deadlocks that
are not sync-preserving. Thus SeqCheck and SPDOffline are theoretically
incomparable in their detection capability. We refer to (arxiv) Appendix C for
examples. We noticed that SeqCheck fails on traces with non-well-nested locks
— we encountered one such case in our dataset. Dirk’s algorithm is
theoretically complete, i.e., it can find all predictable deadlocks in a
trace. In addition, it can find deadlocks beyond the predictable ones, by
reasoning about event values. However, Dirk relies on heavyweight SMT-solving
and employs windowing techniques to scale to large traces. Due to windowing,
it can miss deadlocks between events that are outside the given window. As
with previous works (Cai et al., 2021; Kalhauge and Palsberg, 2018), we set a
window size of $10$K for Dirk.

Our dataset consists of several benchmarks from standard benchmark suites —
IBM Contest suite (Farchi et al., 2003), Java Grande suite (Smith et al.,
2001), DaCapo (Blackburn et al., 2006), and SIR (Do et al., 2005) — and recent
literature (Kalhauge and Palsberg, 2018; Cai et al., 2021; Jula et al., 2008;
Joshi et al., 2009). Each benchmark was instrumented with RV-Predict (Rosu,
2018) or Wiretap (Kalhauge and Palsberg, 2018) and executed in order to log a
single execution trace.

Table 1.  Trace characteristics, abstract lock graph statistics and
performance comparison. Columns 2-6 show the number of events, threads,
variables, locks and total number of lock acquire and request events. Columns
7-9 show the number of cycles, abstract and concrete deadlock patterns in the
abstract lock graph. Columns 10 - 15 show the number of deadlocks reported and
the times (in seconds) taken. by Dirk, SeqCheck, and SPDOffline. Time out
(T.O) was set to $3$h. F stands for technical failure.

1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 | 10 | 11 | 12 | 13 | 14 | 15
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---
Benchmark | $\mathcal{N}$ | $\mathcal{T}$ | $\mathcal{V}$ | $\mathcal{L}$ | $\mathcal{A}/\mathcal{R}$ | A. Lock Graph | Dirk | SeqCheck | SPDOffline
—Cyc— | A. P. | C. P. | Dlk | Time | Dlk | Time | Dlk | Time
Deadlock | 39 | 3 | 4 | 3 | 8 | 1 | 1 | 1 | 1 | 0.02 | 0 | 0.09 | 0 | 0.16
NotADeadlock | 60 | 3 | 4 | 5 | 16 | 1 | 1 | 1 | 0 | 0.02 | 0 | 0.09 | 0 | 0.16
Picklock | 66 | 3 | 6 | 6 | 20 | 2 | 2 | 2 | 1 | 0.02 | 1 | 0.10 | 1 | 0.18
Bensalem | 68 | 4 | 5 | 5 | 22 | 2 | 2 | 2 | 1 | 0.02 | 1 | 0.12 | 1 | 0.16
Transfer | 72 | 3 | 11 | 4 | 12 | 1 | 1 | 1 | 1 | 0.02 | 0 | 0.09 | 0 | 0.15
Test-Dimmunix | 73 | 3 | 9 | 7 | 26 | 2 | 2 | 2 | 2 | 0.02 | 2 | 0.10 | 2 | 0.17
StringBuffer | 74 | 3 | 14 | 4 | 16 | 1 | 3 | 6 | 2 | 0.02 | 2 | 0.12 | 2 | 0.19
Test-Calfuzzer | 168 | 5 | 16 | 6 | 48 | 2 | 1 | 1 | 1 | 0.02 | 1 | 0.12 | 1 | 0.17
DiningPhil | 277 | 6 | 21 | 6 | 100 | 1 | 1 | 3K | 1 | 1.60 | 0 | 0.09 | 1 | 0.17
HashTable | 318 | 3 | 5 | 3 | 174 | 1 | 2 | 43 | 2 | 0.19 | 2 | 0.12 | 2 | 0.19
Account | 706 | 6 | 47 | 7 | 134 | 3 | 1 | 12 | 0 | 0.19 | 0 | 0.09 | 0 | 0.18
Log4j2 | 1K | 4 | 334 | 11 | 43 | 1 | 1 | 1 | 1 | 0.65 | 1 | 0.11 | 1 | 0.20
Dbcp1 | 2K | 3 | 768 | 5 | 56 | 2 | 2 | 3 | - | F | 2 | 0.11 | 2 | 0.19
Dbcp2 | 2K | 3 | 592 | 10 | 76 | 1 | 2 | 4 | - | F | 0 | 0.10 | 0 | 0.18
Derby2 | 3K | 3 | 1K | 4 | 16 | 1 | 1 | 1 | 1 | 0.23 | 1 | 0.10 | 1 | 0.17
RayTracer | 31K | 5 | 5K | 15 | 976 | 0 | 0 | 0 | - | F | 0 | 0.15 | 0 | 0.19
jigsaw | 143K | 21 | 8K | 2K | 67K | 172 | 12 | 70 | - | F | 2 | 0.36 | 1 | 1.55
elevator | 246K | 5 | 727 | 52 | 48K | 0 | 0 | 0 | 0 | 1.65 | 0 | 0.33 | 0 | 0.27
hedc | 410K | 7 | 109K | 8 | 32 | 0 | 0 | 0 | 0 | 2.09 | 0 | 0.50 | 0 | 0.24
JDBCMySQL-1 | 442K | 3 | 73K | 11 | 13K | 2 | 4 | 6 | 2 | 28.45 | 2 | 0.24 | 2 | 0.48
JDBCMySQL-2 | 442K | 3 | 73K | 11 | 13K | 4 | 4 | 9 | 1 | 3.37 | 1 | 0.22 | 1 | 0.33
JDBCMySQL-3 | 443K | 3 | 73K | 13 | 13K | 5 | 8 | 16 | 1 | 31.23 | 1 | 0.25 | 1 | 0.45
JDBCMySQL-4 | 443K | 3 | 73K | 14 | 13K | 5 | 10 | 18 | 2 | 5.51 | 2 | 0.28 | 2 | 0.49
cache4j | 775K | 2 | 46K | 20 | 35K | 0 | 0 | 0 | 0 | 5.86 | 0 | 0.46 | 0 | 0.39
ArrayList | 3M | 801 | 121K | 802 | 176K | 9 | 3 | 672 | 3 | 8.7K | 3 | 21.98 | 3 | 1.68
IdentityHashMap | 3M | 801 | 496K | 802 | 162K | 1 | 3 | 4 | 1 | 443.93 | 1 | 8.51 | 1 | 1.45
Stack | 3M | 801 | 118K | 2K | 405K | 9 | 3 | 481 | 1 | T.O | 3 | 25.34 | 3 | 2.94
Sor | 3M | 301 | 2K | 3 | 719K | 0 | 0 | 0 | 0 | 15.89 | 0 | 44.12 | 0 | 0.61
LinkedList | 3M | 801 | 290K | 802 | 176K | 9 | 3 | 10K | 3 | 4.7K | 3 | 48.02 | 3 | 2.06
HashMap | 3M | 801 | 555K | 802 | 169K | 1 | 3 | 10K | 3 | 4.4K | 2 | 504.36 | 2 | 1.65
WeakHashMap | 3M | 801 | 540K | 802 | 169K | 1 | 3 | 10K | - | T.O | 2 | 499.68 | 2 | 1.70
Swing | 4M | 8 | 31K | 739 | 2M | 0 | 0 | 0 | - | F | 0 | 0.72 | 0 | 0.88
Vector | 4M | 3 | 15 | 4 | 800K | 1 | 1 | 1B | - | T.O | 1 | 1.52 | 1 | 1.90
LinkedHashMap | 4M | 801 | 617K | 802 | 169K | 1 | 3 | 10K | 2 | 40.74 | 2 | 492.87 | 2 | 1.69
montecarlo | 8M | 3 | 850K | 3 | 26 | 0 | 0 | 0 | 0 | 2.6K | 0 | 1.81 | 0 | 0.79
TreeMap | 9M | 801 | 493K | 802 | 169K | 1 | 3 | 10K | 2 | 105.45 | 2 | 480.11 | 2 | 1.92
hsqldb | 20M | 46 | 945K | 403 | 419K | 0 | 0 | 0 | - | F | - | - | 0 | 2.38
sunflow | 21M | 16 | 2M | 12 | 1K | 0 | 0 | 0 | - | F | 0 | 8.35 | 0 | 1.62
jspider | 22M | 11 | 5M | 15 | 10K | 0 | 0 | 0 | - | F | 0 | 8.49 | 0 | 1.95
tradesoap | 42M | 236 | 3M | 6K | 245K | 2 | 1 | 4 | - | F | 0 | 108.16 | 0 | 7.06
tradebeans | 42M | 236 | 3M | 6K | 245K | 2 | 1 | 4 | - | F | 0 | 116.23 | 0 | 7.26
eclipse | 64M | 15 | 10M | 5K | 377K | 9 | 5 | 280 | - | F | 0 | 26.67 | 0 | 9.90
TestPerf | 80M | 50 | 599 | 9 | 197K | 0 | 0 | 0 | 0 | 795.04 | 0 | 47.56 | 0 | 4.30
Groovy2 | 120M | 13 | 13M | 10K | 69K | 0 | 0 | 0 | 0 | 1.7K | 0 | 38.06 | 0 | 8.92
Tsp | 200M | 6 | 24K | 3 | 882 | 0 | 0 | 0 | 0 | 7.6K | 0 | 72.62 | 0 | 12.70
lusearch | 203M | 7 | 3M | 98 | 273K | 0 | 0 | 0 | 0 | 1.3K | 0 | 75.88 | 0 | 14.44
biojava | 221M | 6 | 121K | 79 | 16K | 0 | 0 | 0 | - | F | 0 | 63.79 | 0 | 12.65
graphchi | 241M | 20 | 25M | 61 | 1K | 0 | 0 | 0 | - | F | 0 | 102.05 | 0 | 25.25
Totals | 1B | 7K | 70M | 37K | 8M | 256 | 93 | 1B | 35 | ¿18h | 40 | 2801 | 40 | 135

Evaluation. Table 1 presents our results. A bug identifies a unique tuple of
source code locations corresponding to events participating in the deadlock.
Trace lengths vary vastly from $39$ to about $241$M, while the number of
threads ranges from $3$ to about $800$, which are representative features of
real-world settings. Hsqldb contains critical sections that are not well
nested, and SeqCheck was not able to handle this benchmark; our algorithm does
not have such a restriction.

Abstract vs Concrete Patterns. Columns 7-9 present statistics on the abstract
lock graph $\mathsf{ALG}_{\sigma}$ of each trace $\sigma$. Many traces have a
large number of concrete deadlock patterns but much fewer abstract deadlock
patterns; a single abstract deadlock pattern can comprise up to an order of
$10^{4}$ more concrete patterns (Column $8$ v/s Column $9$). Unlike all prior
sound techniques, our algorithms analyze abstract deadlock patterns, instead
of concrete ones. We thus expect our algorithms to be much more scalable in
practice.

Deadlock-detection capability. In total, both SeqCheck and SPDOffline reported
40 deadlocks. SeqCheck misses a deadlock of size $5$ in DiningPhil, which is
detected by SPDOffline, and SPDOffline misses a deadlock in jigsaw which is
detected by SeqCheck. As SPDOffline is complete for sync-preserving deadlocks,
we conclude that there are no more such deadlocks in our dataset. Overall,
SPDOffline and SeqCheck miss only three deadlocks reported by Dirk. On closer
inspection, we found that these deadlocks are not witnessed by correct
reorderings, and require reasoning about event values. On the other hand, Dirk
struggles to analyze even moderately-sized benchmarks and times out in $3$ of
them. This results in Dirk failing to report 5 deadlocks after $9$ hours, all
of which are reported by SPDOffline in under a minute. Similar conclusions
were recently made in (Cai et al., 2021). Overall, our results strongly
indicate that the notion of sync-preservation characterizes most deadlocks
that other tools are able to predict.

Unsoundness of Dirk. In our evaluation, we discovered that the soundness
guarantee underlying Dirk (Kalhauge and Palsberg, 2018) is broken, resulting
in it reporting false positives. First, its constraint formulation (Kalhauge
and Palsberg, 2018) does not rule out deadlock patterns when acquire events in
the pattern hold common locks, in which case mutual exclusion disallows such a
pattern to be a real predictable deadlock. Second, Dirk also models
conditional statements, allowing it to reason about witnesses beyond correct
reorderings. While this relaxation allows Dirk to predict additional deadlocks
in Transfer, Deadlock and HashMap, its formalization is not precise and its
implementation is erroneous. We elaborate these aspects further in (arxiv).
Appendix D.

Running time. Our experimental results indicate that Dirk, backed by SMT
solving, is the least efficient technique in terms of running time — it takes
considerably longer or times out on large benchmark instances. SPDOffline
analyzed the entire set of traces $\sim\\!\\!\\!21\times$ faster than
SeqCheck. On the most demanding benchmarks, such as HashMap and TreeMap,
SPDOffline is more than $200\times$ faster than SeqCheck. Although SeqCheck
employs a polynomial-time algorithm for deadlock prediction, and thus
significantly faster than the SMT-based Dirk, the large polynomial complexity
in its running time hinders scalability on execution traces coming from
benchmarks that are more representative of realistic workloads. In contrast,
the linear time guarantees of SPDOffline are realized in practice, allowing it
to scale on even the most challenging inputs. More importantly, the improved
performance comes while preserving essentially the same precision.

False negatives. Our benchmark set contains $93$ abstract deadlock patterns,
$40$ of which are confirmed sync-preserving deadlocks. We inspected the
remaining $53$ abstract patterns to see if any of them are predictable
deadlocks missed by our sync-preserving criterion, independently of the
compared tools. $48$ of these $53$ patterns are in fact not predictable
deadlocks — for every such pattern $D$, the set $S_{D}$ of events in the
downward-closure of $\textsf{pred}(D)$ with respect to $\leq_{\mathsf{TO}}$
and $\mathsf{rf}$, already contains an event from $D$, disallowing any correct
reordering (sync-preserving or not) in which $D$ can be enabled. Of the
remaining, $4$ deadlock patterns obey the following scheme: there are two
acquire events $\mathtt{acq}_{1},\mathtt{acq}_{2}$ participating in the
deadlock pattern, each $\mathtt{acq}_{i}$ is preceded by a critical section on
a lock that appears in $\mathsf{HeldLks}(\mathtt{acq}_{3-i})$, again
disallowing a correct reordering that witnesses the pattern. Thus, _only one_
predictable deadlock is not sync-preserving in our whole dataset. This
analysis supports that the notion of sync-preservation is not overly
conservative in practice.

The above analysis concerns false negatives wrt. predictable deadlocks. Some
deadlocks are beyond the common notion of predictability we have adopted here,
as they can only be exposed by reasoning about event values and control-flow
dependencies, a problem that is $\mathsf{NP}$-hard even for 3 threads (Gibbons
and Korach, 1997). We noticed $3$ such deadlocks in our dataset, found by
Dirk, though, as mentioned above, Dirk’s reasoning for capturing such
deadlocks is unsound in practice.

###  6.2. Online Experiments

Experimental setup. The objective of our second set of experiments is to
evaluate the performance of our proposed algorithms in an _online_ setting.
For this, we implemented our SPDOnline algorithm inside the framework of
DeadlockFuzzer (Joshi et al., 2009) following closely the pseudocode in
Algorithm 4. This framework instruments a concurrent program so that it can
perform analysis on-the-fly while executing it. If a deadlock occurs during
execution, it is reported and the execution halts. However, if a deadlock is
predicted in an alternate interleaving, then this deadlock is reported and the
execution continues to search further deadlocks. We used the same dataset as
in Section 6.1, after discarding some benchmarks that could not be
instrumented by DeadlockFuzzer.

To the best of our knowledge, all prior deadlock prediction techniques work
offline. For this reason, we only compared our online tool with the randomized
scheduling technique of (Joshi et al., 2009) already implemented inside the
same DeadlockFuzzer framework. At a high level, this random scheduling
technique works as follows. Initially, it (i) executes the input program with
a random scheduler, (ii) constructs a _lock dependency relation_ , and (iii)
runs a cycle detection algorithm to discover deadlock patterns. For each
deadlock pattern thus found, it spawns new executions that attempt to realize
it as an actual deadlock. To increase the likelihood of hitting the deadlock,
DeadlockFuzzer biases the random scheduler by pausing threads at specific
locations.

The second, confirmation phase of (Joshi et al., 2009) acts as a best-effort
proxy for sound deadlock prediction. On the other hand, SPDOnline is already
sound and predictive, and thus does not require additional confirmation runs,
making it more efficient. Towards effective prediction, we also implemented a
simple bias to the scheduler. If a thread $t$ attempts to write on a shared
variable $x$ while holding a lock, then our procedure randomly decides to
pause this operation for a short duration. This effectively explores race
conditions in different orders. Overall, implementing SPDOnline inside
DeadlockFuzzer provided the added advantage of supplementing a powerful
prediction technique with a biased randomized scheduler. To our knowledge, our
work is the first to effectively combine these two orthogonal techniques. We
also remark that such a bias is of no benefit to DeadlockFuzzer itself since
it does not employ any predictive reasoning.

For this experiment, we run DeadlockFuzzer on each benchmark, and for each
deadlock pattern found in the initial execution, we let it spawn $3$ new
executions trying to realize the deadlock, as per standard
(https://github.com/ksen007/calfuzzer). We repeated this process $50$ times
and recorded the total time taken. Then, we allocated the same time for
SPDOnline to repeatedly execute the same program and perform deadlock
prediction. We measured all deadlocks found by each technique.

Table 2.  Performance comparison of SPDOnline (SPD) and DeadlockFuzzer (DF).
Columns 2-3 show the total number of bug reports. Columns 4-6 show the total
number of unique bugs found by each tool, and their union. Columns 7-12 show
the hit rate on each bug. Columns 13-16 show the runtime overhead of the
tools.

1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 | 10 | 11 | 12 | 13 | 14 | 15 | 16
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---
Benchmark |  Bug Hits |  Unique Bugs |  Bug 1 |  Bug 2 |  Bug 3 |  Runtime Overhead
SPD | DF | SPD | DF | All | SPD | DF | SPD | DF | SPD | DF | SPD-I | SPD | DF-I | DF
Deadlock | 50 | 50 | 1 | 1 | 1 | 50 | 50 | - | - | - | - |  2$\times$ |  3$\times$ |  2$\times$ |  4$\times$
Picklock | 227 | 97 | 2 | 1 | 2 | 226 | 97 | 1 | 0 | - | - |  2$\times$ |  2$\times$ |  2$\times$ |  5$\times$
Bensalem | 355 | 32 | 2 | 1 | 2 | 8 | 0 | 347 | 32 | - | - |  2$\times$ |  2$\times$ |  2$\times$ |  6$\times$
Transfer | 54 | 50 | 1 | 1 | 1 | 54 | 50 | - | - | - | - |  2$\times$ |  2$\times$ |  1$\times$ |  4$\times$
Test-Dimmunix | 702 | 0 | 2 | 0 | 2 | 351 | 0 | 351 | 0 | - | - |  2$\times$ |  2$\times$ |  2$\times$ |  4$\times$
StringBuffer | 153 | 131 | 2 | 2 | 2 | 128 | 118 | 25 | 13 | - | - | - | - | - | -
Test-Calfuzzer | 177 | 44 | 1 | 1 | 1 | 177 | 44 | - | - | - | - |  2$\times$ |  2$\times$ |  2$\times$ |  4$\times$
DiningPhil | 162 | 100 | 1 | 1 | 1 | 162 | 100 | - | - | - | - | - | - | - | -
HashTable | 169 | 120 | 2 | 2 | 2 | 82 | 21 | 87 | 99 | - | - | - | - | - | -
Account | 19 | 188 | 1 | 1 | 1 | 19 | 188 | - | - | - | - |  2$\times$ |  8$\times$ |  2$\times$ |  16$\times$
Log4j2 | 290 | 100 | 2 | 1 | 2 | 145 | 100 | 145 | 0 | - | - | - | - | - | -
Dbcp1 | 265 | 138 | 2 | 2 | 2 | 264 | 61 | 1 | 77 | - | - | - | - | - | -
Dbcp2 | 129 | 126 | 2 | 2 | 2 | 86 | 99 | 43 | 27 | - | - | - | - | - | -
RayTracer | 0 | 0 | 0 | 0 | 0 | - | - | - | - | - | - |  122$\times$ |  124$\times$ |  109$\times$ |  111$\times$
Tsp | 0 | 0 | 0 | 0 | 0 | - | - | - | - | - | - |  47$\times$ |  60$\times$ |  37$\times$ |  40$\times$
jigsaw | 1189 | 1 | 1 | 1 | 2 | 1189 | 0 | 0 | 1 | - | - | - | - | - | -
elevator | 0 | 0 | 0 | 0 | 0 | - | - | - | - | - | - |  2$\times$ |  2$\times$ |  2$\times$ |  2$\times$
JDBCMySQL-1 | 349 | 117 | 2 | 3 | 3 | 1 | 21 | 0 | 4 | 348 | 92 |  3$\times$ |  4$\times$ |  2$\times$ |  13$\times$
JDBCMySQL-2 | 559 | 73 | 1 | 1 | 1 | 559 | 73 | - | - | - | - |  2$\times$ |  4$\times$ |  2$\times$ |  18$\times$
JDBCMySQL-3 | 560 | 224 | 1 | 1 | 1 | 560 | 224 | - | - | - | - |  2$\times$ |  5$\times$ |  2$\times$ |  24$\times$
JDBCMySQL-4 | 1717 | 101 | 3 | 1 | 3 | 95 | 0 | 834 | 0 | 788 | 101 |  3$\times$ |  5$\times$ |  2$\times$ |  31$\times$
hedc | 0 | 0 | 0 | 0 | 0 | - | - | - | - | - | - |  2$\times$ |  2$\times$ |  1$\times$ |  2$\times$
cache4j | 0 | 0 | 0 | 0 | 0 | - | - | - | - | - | - |  2$\times$ |  2$\times$ |  2$\times$ |  2$\times$
lusearch | 0 | 0 | 0 | 0 | 0 | - | - | - | - | - | - |  16$\times$ |  17$\times$ |  13$\times$ |  16$\times$
ArrayList | 47 | 45 | 3 | 3 | 3 | 20 | 22 | 3 | 5 | 24 | 18 |  50$\times$ |  69$\times$ |  18$\times$ |  79$\times$
Stack | 44 | 27 | 3 | 3 | 3 | 18 | 13 | 8 | 4 | 18 | 10 |  69$\times$ |  91$\times$ |  64$\times$ |  86$\times$
IdentityHashMap | 68 | 62 | 2 | 2 | 2 | 13 | 47 | 55 | 15 | - | - |  4$\times$ |  8$\times$ |  3$\times$ |  10$\times$
LinkedList | 48 | 26 | 3 | 2 | 3 | 21 | 17 | 7 | 0 | 20 | 9 |  16$\times$ |  28$\times$ |  14$\times$ |  32$\times$
Swing | 0 | 0 | 0 | 0 | 0 | - | - | - | - | - | - |  5$\times$ |  6$\times$ |  4$\times$ |  6$\times$
Sor | 0 | 0 | 0 | 0 | 0 | - | - | - | - | - | - |  2$\times$ |  7$\times$ |  2$\times$ |  2$\times$
HashMap | 46 | 44 | 2 | 2 | 2 | 18 | 11 | 28 | 33 | - | - |  7$\times$ |  11$\times$ |  4$\times$ |  8$\times$
Vector | 126 | 50 | 1 | 1 | 1 | 126 | 50 | - | - | - | - |  2$\times$ |  2$\times$ |  2$\times$ |  3$\times$
LinkedHashMap | 57 | 43 | 2 | 2 | 2 | 22 | 10 | 35 | 33 | - | - |  10$\times$ |  10$\times$ |  4$\times$ |  8$\times$
WeakHashMap | 29 | 40 | 2 | 2 | 2 | 6 | 11 | 23 | 29 | - | - |  7$\times$ |  12$\times$ |  4$\times$ |  8$\times$
montecarlo | 0 | 0 | 0 | 0 | 0 | - | - | - | - | - | - |  16$\times$ |  100$\times$ |  13$\times$ |  126$\times$
TreeMap | 42 | 47 | 2 | 2 | 2 | 16 | 15 | 26 | 32 | - | - |  9$\times$ |  12$\times$ |  5$\times$ |  9$\times$
eclipse | 0 | 0 | 0 | 0 | 0 | - | - | - | - | - | - |  2$\times$ |  2$\times$ |  2$\times$ |  2$\times$
TestPerf | 0 | 0 | 0 | 0 | 0 | - | - | - | - | - | - |  2$\times$ |  2$\times$ |  2$\times$ |  2$\times$
Total | 7633 | 2076 | 49 | 42 | 51 | - | - | - | - | - | - | - | - | - | -

Evaluation. Table 2 presents our experimental results. Columns $2$-$3$ of the
table display the total number of bug hits, which is the total number of times
a bug was predicted by SPDOnline in the entire duration, or was confirmed in
any trial of DeadlockFuzzer. Columns $4$-$6$ display the unique bugs (i.e.,
unique tuples of source code locations leading to a deadlock) found by the
techniques. The employed techniques are able to find a maximum of $3$ unique
bugs for each benchmark in our benchmark set. Respectively, columns $7$-$12$
display the detailed information on the number of times a particular bug was
found by each technique. Runtime overheads are displayed in the columns
$13$-$16$, with $\mathsf{\tt-I}$ denoting the instrumentation phase only.

Deadlock-detection capability. DeadlockFuzzer had $2076$ bug reports in total,
and it found $42$ unique bugs. In contrast, SPDOnline flagged $7633$ bug
reports, corresponding to $49$ unique bugs. In more detail, DeadlockFuzzer
missed $9$ bugs reported by SPDOnline whereas SPDOnline missed $2$ bugs
reported by DeadlockFuzzer. Also, SPDOnline significantly outperformed
DeadlockFuzzer in total number of bugs hits. Our experiments again support
that the notion of sync-preservation captures most deadlocks that occur in
practice, to the extent that other state-of-the-art techniques can capture. A
further observation is that in the offline experiments, SPDOffline was not
able to find deadlocks in Transfer and Deadlock. However, the random
scheduling procedure allowed SPDOnline to navigate to executions from which
deadlocks can be predicted. This demonstrates the potential of combining
predictive dynamic techniques with controlled concurrency testing.

Runtime overhead. We have also measured the runtime overhead of both SPDOnline
and DeadlockFuzzer, both as incurred by instrumentation, as well as by the
deadlock analysis. The latter is the time taken by Algorithm 4 for the case of
SPDOnline, and the overhead introduced due to the new executions in the second
confirmation phase for the case of DeadlockFuzzer. Our results show that the
instrumentation overhead of SPDOnline is, in fact, comparable to that of
DeadlockFuzzer, though somewhat larger. This is expected, as SPDOnline needs
to also instrument memory access events, while DeadlockFuzzer only instruments
lock events, but at the same time surprising because the number of memory
access events is typically much larger than the number of lock events. On the
other hand, the analysis overhead is often larger for DeadlockFuzzer, even
though it reports fewer bugs. It was not possible to measure the runtime
overhead in certain benchmarks as either they were always deadlocking or the
computation was running indefinitely.

##  7\. Related Work

Dynamic techniques for detecting deadlock patterns, like the GoodLock
algorithm (Havelund, 2000) have been improved in performance (Cai et al.,
2020; Zhou et al., 2017) and precision (Bensalem and Havelund, 2005),
sometimes using re-executions to verify potential deadlocks (Samak and
Ramanathan, 2014b, a; Sorrentino, 2015; Joshi et al., 2009; Bensalem et al.,
2006). Predictive analyses directly infer concurrency bugs in alternate
executions (Şerbănută et al., 2013) and are typically _sound_ (no false
positives). This approach has been successfully applied for detecting bugs
such as data races (Said et al., 2011; Huang et al., 2014; Smaragdakis et al.,
2012; Kini et al., 2017; Pavlogiannis, 2019; Mathur et al., 2021; Roemer et
al., 2020), use-after-free vulnerabilities (Huang, 2018), and more recently
for deadlocks (Eslamimehr and Palsberg, 2014; Kalhauge and Palsberg, 2018; Cai
et al., 2021).

The notion of sync-preserving deadlocks has been inspired by a similar notion
pertaining to data races (Mathur et al., 2021). However, sync-preserving
deadlock prediction rests on some further novelties. First, unlike data races,
deadlocks can involve more than $2$ events. Generalizing sync-preserving
ideals of sets of events of arbitrary size, as well as establishing the
monotonicity properties (Proposition 4.9 and Corollary 4.10) for arbitrarily
many events is non-trivial. Second, our notions of abstract deadlock patterns
(Section 4.4) and abstract lock graphs (Section 4.5) are novel and carefully
crafted to leverage these monotonicity properties in the deadlock setting.
Indeed, the linear-time sync-preserving verification of each abstract deadlock
pattern is the cornerstone of our approach, for the first linear-time, sound
and precise deadlock predictor.

Although the basic principles of data-race and deadlock prediction are
similar, there are notable differences. First, identifying potential deadlocks
is theoretically intractable, whereas, potential races are identified easily.
Second, popular partial-order based techniques (Flanagan and Freund, 2009;
Kini et al., 2017) for data races are likely to require non-trivial
modifications for deadlocks, as they typically order critical sections, which
may hide a deadlock. Nevertheless, bridging prediction techniques between data
races and deadlocks is an interesting and relatively open direction.

Predicting deadlocks is an intractable problem, the complexity of which we
have characterized in this work. Prior works have also focused on the
complexity of predicting data races (Mathur et al., 2020; Kulkarni et al.,
2021) and atomicity violations (Farzan and Madhusudan, 2009).

##  8\. Conclusion

We have studied the complexity of deadlock prediction and introduced the new
tractable notion of sync-preserving deadlocks, along with sound, complete and
efficient algorithms for detecting them. Our experiments show that the
majority of deadlocks occurring in practice are indeed sync-preserving, and
our algorithm SPDOffline is the first deadlock predictor that achieves sound
and high coverage, while also spending only linear time to process its input.
Our online algorithm SPDOnline enhances the bug detection capability of
controlled concurrency testing techniques like (Joshi et al., 2009), at close
runtime overheads. Interesting future work includes incorporating static
checks (Rhodes et al., 2017) and exploring ways for deeper integration of
controlled concurrency testing with predictive techniques. Another step is to
extend the coverage of sync-preserving deadlocks while maintaining efficiency,
for example, by reasoning about program control flow.

###### Acknowledgements.

Andreas Pavlogiannis was partially supported by a research grant (VIL42117)
from VILLUM FONDEN. Umang Mathur was partially supported by the Simons
Institute for the Theory of Computing, and by a Singapore Ministry of
Education (MoE) Academic Research Fund (AcRF) Tier 1 grant. Mahesh Viswanathan
was partially supported by NSF SHF 1901069 and NSF CCF 2007428.

## Data and Software Availability Statement

The artifact developed for this work is available (Tunç et al., 2023), which
contains all source codes and experimental data necessary to reproduce our
evaluation in Section 6, excluding the results of SeqCheck.

## References

  * (1)
  * Agarwal et al. (2006) Rahul Agarwal, Liqiang Wang, and Scott D. Stoller. 2006\.  Detecting Potential Deadlocks with Static Analysis and Runtime Monitoring. In _Proceedings of the Parallel and Distributed Systems: Testing and Debugging (PADTAD) Track of the 2005 Haifa Verification Conference_ _(Lecture Notes in Computer Science, Vol. 3875)_. Springer-Verlag, 191–207.  https://doi.org/10.1007/11678779_14
  * Bensalem et al. (2006) Saddek Bensalem, Jean-Claude Fernandez, Klaus Havelund, and Laurent Mounier. 2006.  Confirmation of Deadlock Potentials Detected by Runtime Analysis. In _Proceedings of the 2006 Workshop on Parallel and Distributed Systems: Testing and Debugging_ (Portland, Maine, USA) _(PADTAD ’06)_. Association for Computing Machinery, New York, NY, USA, 41–50.  https://doi.org/10.1145/1147403.1147412
  * Bensalem and Havelund (2005) Saddek Bensalem and Klaus Havelund. 2005.  Dynamic Deadlock Analysis of Multi-Threaded Programs. In _Proceedings of the First Haifa International Conference on Hardware and Software Verification and Testing_ (Haifa, Israel) _(HVC’05)_. Springer-Verlag, Berlin, Heidelberg, 208–223.  https://doi.org/10.1007/11678779_15
  * Biswas et al. (2014) Swarnendu Biswas, Jipeng Huang, Aritra Sengupta, and Michael D. Bond. 2014.  DoubleChecker: Efficient Sound and Precise Atomicity Checking. In _Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation_ (Edinburgh, United Kingdom) _(PLDI ’14)_. ACM, New York, NY, USA, 28–39.  https://doi.org/10.1145/2594291.2594323
  * Blackburn et al. (2006) Stephen M. Blackburn, Robin Garner, Chris Hoffmann, Asjad M. Khang, Kathryn S. McKinley, Rotem Bentzur, Amer Diwan, Daniel Feinberg, Daniel Frampton, Samuel Z. Guyer, Martin Hirzel, Antony Hosking, Maria Jump, Han Lee, J. Eliot B. Moss, Aashish Phansalkar, Darko Stefanović, Thomas VanDrunen, Daniel von Dincklage, and Ben Wiedermann. 2006.  The DaCapo Benchmarks: Java Benchmarking Development and Analysis. In _Proceedings of the 21st Annual ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages, and Applications_ (Portland, Oregon, USA) _(OOPSLA ’06)_. Association for Computing Machinery, New York, NY, USA, 169–190.  https://doi.org/10.1145/1167473.1167488
  * Cai and Chan (2014) Yan Cai and W.K. Chan. 2014\.  Magiclock: Scalable Detection of Potential Deadlocks in Large-Scale Multithreaded Programs .  _IEEE Transactions on Software Engineering_ 40, 3 (2014), 266–281.  https://doi.org/10.1109/TSE.2014.2301725
  * Cai and Chan (2012) Yan Cai and W. K. Chan. 2012.  MagicFuzzer: Scalable Deadlock Detection for Large-Scale Applications. In _Proceedings of the 34th International Conference on Software Engineering_ (Zurich, Switzerland) _(ICSE ’12)_. IEEE Press, 606–616.  https://doi.org/10.1109/ICSE.2012.6227156
  * Cai et al. (2020) Yan Cai, Ruijie Meng, and Jens Palsberg. 2020.  Low-Overhead Deadlock Prediction. In _Proceedings of the ACM/IEEE 42nd International Conference on Software Engineering_ (Seoul, South Korea) _(ICSE ’20)_. Association for Computing Machinery, New York, NY, USA, 1298–1309.  https://doi.org/10.1145/3377811.3380367
  * Cai et al. (2021) Yan Cai, Hao Yun, Jinqiu Wang, Lei Qiao, and Jens Palsberg. 2021.  Sound and Efficient Concurrency Bug Prediction. In _Proceedings of the 29th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering_ (Athens, Greece) _(ESEC/FSE 2021)_. Association for Computing Machinery, New York, NY, USA, 255–267.  https://doi.org/10.1145/3468264.3468549
  * Chen et al. (2006) Jianer Chen, Xiuzhen Huang, Iyad A. Kanj, and Ge Xia. 2006\.  Strong computational lower bounds via parameterized complexity.  _J. Comput. System Sci._ 72, 8 (2006), 1346–1367.  https://doi.org/10.1016/j.jcss.2006.04.007
  * Do et al. (2005) Hyunsook Do, Sebastian Elbaum, and Gregg Rothermel. 2005\.  Supporting Controlled Experimentation with Testing Techniques: An Infrastructure and its Potential Impact.  _Empirical Software Engineering_ 10, 4 (2005), 405–435.  https://doi.org/10.1007/s10664-005-3861-2
  * Eslamimehr and Palsberg (2014) Mahdi Eslamimehr and Jens Palsberg. 2014.  Sherlock: Scalable Deadlock Detection for Concurrent Programs. In _Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering_ (Hong Kong, China) _(FSE 2014)_. Association for Computing Machinery, New York, NY, USA, 353–365.  https://doi.org/10.1145/2635868.2635918
  * Farchi et al. (2003) Eitan Farchi, Yarden Nir, and Shmuel Ur. 2003.  Concurrent Bug Patterns and How to Test Them. In _Proceedings of the 17th International Symposium on Parallel and Distributed Processing_ _(IPDPS ’03)_. IEEE Computer Society, Washington, DC, USA, 286.2.  https://doi.org/10.1109/IPDPS.2003.1213511
  * Farzan and Madhusudan (2009) Azadeh Farzan and Parthasarathy Madhusudan. 2009.  The Complexity of Predicting Atomicity Violations. In _Tools and Algorithms for the Construction and Analysis of Systems_ , Stefan Kowalewski and Anna Philippou (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 155–169.  https://doi.org/10.1007/978-3-642-00768-2_14
  * Fidge (1991) Colin Fidge. 1991\.  Logical Time in Distributed Computing Systems.  _Computer_ 24, 8 (1991), 28–33.  https://doi.org/10.1109/2.84874
  * Flanagan and Freund (2009) Cormac Flanagan and Stephen N. Freund. 2009.  FastTrack: Efficient and Precise Dynamic Race Detection. In _Proceedings of the 30th ACM SIGPLAN Conference on Programming Language Design and Implementation_ (Dublin, Ireland) _(PLDI ’09)_. ACM, New York, NY, USA, 121–133.  https://doi.org/10.1145/1542476.1542490