* Flanagan et al. (2008) Cormac Flanagan, Stephen N. Freund, and Jaeheon Yi. 2008\.  Velodrome: A Sound and Complete Dynamic Atomicity Checker for Multithreaded Programs . In _Proceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and Implementation_ (Tucson, AZ, USA) _(PLDI ’08)_. ACM, New York, NY, USA, 293–303.  https://doi.org/10.1145/1375581.1375618
  * Genç et al. (2019) Kaan Genç, Jake Roemer, Yufan Xu, and Michael D. Bond. 2019.  Dependence-Aware, Unbounded Sound Predictive Race Detection.  _Proc. ACM Program. Lang._ 3, OOPSLA, Article 179 (2019), 30 pages.  https://doi.org/10.1145/3360605
  * Gibbons and Korach (1997) Phillip B. Gibbons and Ephraim Korach. 1997.  Testing Shared Memories.  _SIAM J. Comput._ 26, 4 (1997), 1208–1244.  https://doi.org/10.1137/S0097539794279614
  * Havelund (2000) Klaus Havelund. 2000\.  Using Runtime Analysis to Guide Model Checking of Java Programs. In _Proceedings of the 7th International SPIN Workshop on SPIN Model Checking and Software Verification_. Springer-Verlag, Berlin, Heidelberg, 245–264.  https://doi.org/10.1007/10722468_15
  * Huang (2018) Jeff Huang. 2018\.  UFO: Predictive Concurrency Use-after-Free Detection. In _Proceedings of the 40th International Conference on Software Engineering_ (Gothenburg, Sweden) _(ICSE ’18)_. Association for Computing Machinery, New York, NY, USA, 609–619.  https://doi.org/10.1145/3180155.3180225
  * Huang et al. (2014) Jeff Huang, Patrick O’Neil Meredith, and Grigore Rosu. 2014\.  Maximal Sound Predictive Race Detection with Control Flow Abstraction. In _Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation_ (Edinburgh, United Kingdom) _(PLDI ’14)_. ACM, New York, NY, USA, 337–348.  https://doi.org/10.1145/2594291.2594315
  * Johnson (1975) Donald B. Johnson. 1975\.  Finding All the Elementary Circuits of a Directed Graph.  _SIAM J. Comput._ 4, 1 (1975), 77–84.  https://doi.org/10.1137/0204007
  * Joshi et al. (2010) Pallavi Joshi, Mayur Naik, Koushik Sen, and David Gay. 2010\.  An Effective Dynamic Analysis for Detecting Generalized Deadlocks. In _Proceedings of the Eighteenth ACM SIGSOFT International Symposium on Foundations of Software Engineering_ (Santa Fe, New Mexico, USA) _(FSE ’10)_. Association for Computing Machinery, New York, NY, USA, 327–336.  https://doi.org/10.1145/1882291.1882339
  * Joshi et al. (2009) Pallavi Joshi, Chang-Seo Park, Koushik Sen, and Mayur Naik. 2009\.  A Randomized Dynamic Program Analysis Technique for Detecting Real Deadlocks . In _Proceedings of the 30th ACM SIGPLAN Conference on Programming Language Design and Implementation_ (Dublin, Ireland) _(PLDI ’09)_. Association for Computing Machinery, New York, NY, USA, 110–120.  https://doi.org/10.1145/1542476.1542489
  * Jula et al. (2008) Horatiu Jula, Daniel Tralamazza, Cristian Zamfir, and George Candea. 2008.  Deadlock Immunity: Enabling Systems to Defend against Deadlocks. In _Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation_ (San Diego, California) _(OSDI’08)_. USENIX Association, USA, 295–308.
  * Kalhauge and Palsberg (2018) Christian Gram Kalhauge and Jens Palsberg. 2018.  Sound Deadlock Prediction.  _Proc. ACM Program. Lang._ 2, OOPSLA, Article 146 (2018), 29 pages.  https://doi.org/10.1145/3276516
  * Kini et al. (2017) Dileep Kini, Umang Mathur, and Mahesh Viswanathan. 2017\.  Dynamic Race Prediction in Linear Time. In _Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation_ (Barcelona, Spain) _(PLDI 2017)_. ACM, New York, NY, USA, 157–170.  https://doi.org/10.1145/3062341.3062374
  * Kulkarni et al. (2021) Rucha Kulkarni, Umang Mathur, and Andreas Pavlogiannis. 2021\.  Dynamic Data-Race Detection Through the Fine-Grained Lens. In _32nd International Conference on Concurrency Theory (CONCUR 2021)_ _(Leibniz International Proceedings in Informatics (LIPIcs), Vol. 203)_ , Serge Haddad and Daniele Varacca (Eds.). Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 16:1–16:23.  https://doi.org/10.4230/LIPIcs.CONCUR.2021.16
  * Lamport (1978) Leslie Lamport. 1978\.  Time, Clocks, and the Ordering of Events in a Distributed System.  _Commun. ACM_ 21, 7 (1978), 558–565.  https://doi.org/10.1145/359545.359563
  * Liu et al. (2021) Bozhen Liu, Peiming Liu, Yanze Li, Chia-Che Tsai, Dilma Da Silva, and Jeff Huang. 2021\.  When Threads Meet Events: Efficient and Precise Static Race Detection with Origins . In _Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation_ (Virtual, Canada) _(PLDI 2021)_. Association for Computing Machinery, New York, NY, USA, 725–739.  https://doi.org/10.1145/3453483.3454073
  * Lu et al. (2008) Shan Lu, Soyeon Park, Eunsoo Seo, and Yuanyuan Zhou. 2008\.  Learning from Mistakes: A Comprehensive Study on Real World Concurrency Bug Characteristics. In _Proceedings of the 13th International Conference on Architectural Support for Programming Languages and Operating Systems_ (Seattle, WA, USA) _(ASPLOS XIII)_. Association for Computing Machinery, New York, NY, USA, 329–339.  https://doi.org/10.1145/1346281.1346323
  * Mathur (2019) Umang Mathur. 2019\.  RAPID.  https://github.com/umangm/rapid.  Accessed: 2022-10-14.
  * Mathur et al. (2020) Umang Mathur, Andreas Pavlogiannis, and Mahesh Viswanathan. 2020\.  The Complexity of Dynamic Data Race Prediction. In _Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science_ (Saarbrücken, Germany) _(LICS ’20)_. Association for Computing Machinery, New York, NY, USA, 713–727.  https://doi.org/10.1145/3373718.3394783
  * Mathur et al. (2021) Umang Mathur, Andreas Pavlogiannis, and Mahesh Viswanathan. 2021\.  Optimal Prediction of Synchronization-Preserving Races.  _Proc. ACM Program. Lang._ 5, POPL, Article 36 (2021), 29 pages.  https://doi.org/10.1145/3434317
  * Mathur and Viswanathan (2020) Umang Mathur and Mahesh Viswanathan. 2020.  Atomicity Checking in Linear Time Using Vector Clocks. In _Proceedings of the Twenty-Fifth International Conference on Architectural Support for Programming Languages and Operating Systems_ (Lausanne, Switzerland) _(ASPLOS ’20)_. Association for Computing Machinery, New York, NY, USA, 183–199.  https://doi.org/10.1145/3373376.3378475
  * Mattern (1989) Friedemann Mattern. 1989\.  Virtual Time and Global States of Distributed Systems.  In _Parallel and Distributed Algorithms: proceedings of the International Workshop on Parallel & Distributed Algorithms_, M. Cosnard et. al. (Ed.). Elsevier Science Publishers B. V., 215–226.
  * Musuvathi et al. (2008) Madanlal Musuvathi, Shaz Qadeer, Thomas Ball, Gerard Basler, Piramanayagam Arumuga Nainar, and Iulian Neamtiu. 2008.  Finding and Reproducing Heisenbugs in Concurrent Programs. In _Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation_ (San Diego, California) _(OSDI’08)_. USENIX Association, Berkeley, CA, USA, 267–280.
  * Naik et al. (2009) Mayur Naik, Chang-Seo Park, Koushik Sen, and David Gay. 2009\.  Effective Static Deadlock Detection. In _Proceedings of the 31st International Conference on Software Engineering_ _(ICSE ’09)_. IEEE Computer Society, USA, 386–396.  https://doi.org/10.1109/ICSE.2009.5070538
  * Ng and Yoshida (2016) Nicholas Ng and Nobuko Yoshida. 2016.  Static Deadlock Detection for Concurrent Go by Global Session Graph Synthesis . In _Proceedings of the 25th International Conference on Compiler Construction_ (Barcelona, Spain) _(CC 2016)_. Association for Computing Machinery, New York, NY, USA, 174–184.  https://doi.org/10.1145/2892208.2892232
  * Pavlogiannis (2019) Andreas Pavlogiannis. 2019\.  Fast, Sound, and Effectively Complete Dynamic Race Prediction.  _Proc. ACM Program. Lang._ 4, POPL, Article 17 (2019), 29 pages.  https://doi.org/10.1145/3371085
  * Pozniansky and Schuster (2003) Eli Pozniansky and Assaf Schuster. 2003.  Efficient On-the-Fly Data Race Detection in Multithreaded C++ Programs. In _Proceedings of the Ninth ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming_ (San Diego, California, USA) _(PPoPP ’03)_. Association for Computing Machinery, New York, NY, USA, 179–190.  https://doi.org/10.1145/781498.781529
  * Rhodes et al. (2017) Dustin Rhodes, Cormac Flanagan, and Stephen N. Freund. 2017\.  BigFoot: Static Check Placement for Dynamic Race Detection. In _Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation_ (Barcelona, Spain) _(PLDI 2017)_. Association for Computing Machinery, New York, NY, USA, 141–156.  https://doi.org/10.1145/3062341.3062350
  * Roemer et al. (2020) Jake Roemer, Kaan Genç, and Michael D. Bond. 2020\.  SmartTrack: Efficient Predictive Race Detection. In _Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation_ (London, UK) _(PLDI 2020)_. Association for Computing Machinery, New York, NY, USA, 747–762.  https://doi.org/10.1145/3385412.3385993
  * Rosu (2018) Grigore Rosu. 2018\.  _RV-Predict, Runtime Verification_.  Accessed: 2018-04-01.
  * Said et al. (2011) Mahmoud Said, Chao Wang, Zijiang Yang, and Karem Sakallah. 2011\.  Generating Data Race Witnesses by an SMT-Based Analysis. In _NASA Formal Methods_ , Mihaela Bobaru, Klaus Havelund, Gerard J. Holzmann, and Rajeev Joshi (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 313–327.  https://doi.org/10.1007/978-3-642-20398-5_23
  * Samak and Ramanathan (2014a) Malavika Samak and Murali Krishna Ramanathan. 2014a.  Multithreaded Test Synthesis for Deadlock Detection. In _Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages & Applications_ (Portland, Oregon, USA) _(OOPSLA ’14)_. Association for Computing Machinery, New York, NY, USA, 473–489.  https://doi.org/10.1145/2660193.2660238
  * Samak and Ramanathan (2014b) Malavika Samak and Murali Krishna Ramanathan. 2014b.  Trace Driven Dynamic Deadlock Detection and Reproduction. In _Proceedings of the 19th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming_ (Orlando, Florida, USA) _(PPoPP ’14)_. Association for Computing Machinery, New York, NY, USA, 29–42.  https://doi.org/10.1145/2555243.2555262
  * Savage et al. (1997) Stefan Savage, Michael Burrows, Greg Nelson, Patrick Sobalvarro, and Thomas Anderson. 1997\.  Eraser: A Dynamic Data Race Detector for Multithreaded Programs.  _ACM Trans. Comput. Syst._ 15, 4 (1997), 391–411.  https://doi.org/10.1145/265924.265927
  * Sen et al. (2005) Koushik Sen, Grigore Roşu, and Gul Agha. 2005\.  Detecting Errors in Multithreaded Programs by Generalized Predictive Analysis of Executions. In _Formal Methods for Open Object-Based Distributed Systems_ , Martin Steffen and Gianluigi Zavattaro (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 211–226.  https://doi.org/10.1007/11494881_14
  * Şerbănută et al. (2013) Traian Florin Şerbănută, Feng Chen, and Grigore Roşu. 2013\.  Maximal Causal Models for Sequentially Consistent Systems. In _Runtime Verification_ , Shaz Qadeer and Serdar Tasiran (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 136–150.  https://doi.org/10.1007/978-3-642-35632-2_16
  * Serebryany and Iskhodzhanov (2009) Konstantin Serebryany and Timur Iskhodzhanov. 2009.  ThreadSanitizer: Data Race Detection in Practice. In _Proceedings of the Workshop on Binary Instrumentation and Applications_ (New York, New York, USA) _(WBIA ’09)_. Association for Computing Machinery, New York, NY, USA, 62–71.  https://doi.org/10.1145/1791194.1791203
  * Smaragdakis et al. (2012) Yannis Smaragdakis, Jacob Evans, Caitlin Sadowski, Jaeheon Yi, and Cormac Flanagan. 2012.  Sound Predictive Race Detection in Polynomial Time. In _Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages_ (Philadelphia, PA, USA) _(POPL ’12)_. Association for Computing Machinery, New York, NY, USA, 387–400.  https://doi.org/10.1145/2103656.2103702
  * Smith et al. (2001) L. A. Smith, J. M. Bull, and J. Obdrzálek. 2001.  A Parallel Java Grande Benchmark Suite. In _Proceedings of the 2001 ACM/IEEE Conference on Supercomputing_ (Denver, Colorado) _(SC ’01)_. ACM, New York, NY, USA, 8–8.  https://doi.org/10.1145/582034.582042
  * Sorrentino (2015) Francesco Sorrentino. 2015\.  PickLock: A Deadlock Prediction Approach under Nested Locking. In _Proceedings of the 22nd International Symposium on Model Checking Software - Volume 9232_ (Stellenbosch, South Africa) _(SPIN 2015)_. Springer-Verlag, Berlin, Heidelberg, 179–199.  https://doi.org/10.1007/978-3-319-23404-5_13
  * Tu et al. (2019) Tengfei Tu, Xiaoyu Liu, Linhai Song, and Yiying Zhang. 2019\.  Understanding Real-World Concurrency Bugs in Go. In _Proceedings of the Twenty-Fourth International Conference on Architectural Support for Programming Languages and Operating Systems_ (Providence, RI, USA) _(ASPLOS ’19)_. Association for Computing Machinery, New York, NY, USA, 865–878.  https://doi.org/10.1145/3297858.3304069
  * Tunç et al. (2023) Hünkar Can Tunç, Umang Mathur, Andreas Pavlogiannis, and Mahesh Viswanathan. 2023.  _Sound Dynamic Deadlock Prediction in Linear Time_.  https://doi.org/10.5281/zenodo.7809600 Artifact.
  * Williams (2005) Ryan Williams. 2005\.  A new algorithm for optimal 2-constraint satisfaction and its implications.  _Theoretical Computer Science_ 348, 2 (2005), 357–365.  https://doi.org/10.1016/j.tcs.2005.09.023 Automata, Languages and Programming: Algorithms and Complexity (ICALP-A 2004).
  * Williams (2018) Virginia Vassilevska Williams. 2018\.  On some fine-grained questions in algorithms and complexity. In _Proceedings of the International Congress of Mathematicians: Rio de Janeiro 2018_. World Scientific, 3447–3487.  https://doi.org/10.1142/9789813272880_0188
  * Yin et al. (2011) Zuoning Yin, Ding Yuan, Yuanyuan Zhou, Shankar Pasupathy, and Lakshmi Bairavasundaram. 2011.  How Do Fixes Become Bugs?. In _Proceedings of the 19th ACM SIGSOFT Symposium and the 13th European Conference on Foundations of Software Engineering_ (Szeged, Hungary) _(ESEC/FSE ’11)_. Association for Computing Machinery, New York, NY, USA, 26–36.  https://doi.org/10.1145/2025113.2025121
  * Zhou et al. (2017) Jinpeng Zhou, Sam Silvestro, Hongyu Liu, Yan Cai, and Tongping Liu. 2017.  UNDEAD: Detecting and Preventing Deadlocks in Production Software. In _Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering_ (Urbana-Champaign, IL, USA) _(ASE ’17)_. IEEE Press, 729–740.  https://doi.org/10.1109/ASE.2017.8115684

##  Appendix A Proofs of Section 3

In this section we present rigorous proofs of our hardness results in Theorem
3.1, Theorem 3.2, and Theorem 3.3.

###  A.1. Proof of Theorem 3.1

Checking whether a trace of length $\mathcal{N}$ has a deadlock pattern of
size $k$ can be solved using a simple enumeration based algorithm in time
$O(\text{poly}(\mathcal{T})\cdot\mathcal{N}^{\mathcal{T}})$. In this section,
we show that this problem is, in fact, $\mathsf{W[1]}$-hard and thus is
unlikely to be FPT (fixed parameter tractable). In other words, an algorithm
with running time $O(f(\mathcal{T})\cdot\text{poly}(\mathcal{N}))$ is unlikely
to exist for this problem, for any computable function $f$.

See 3.1

###### Proof.

We show that there is a polynomial-time FPT-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$.

Construction. We assume that the vertices are indexed from $1$ through
$n=|V|$: $V=\\{v_{1},v_{2},\ldots,v_{n}\\}$. We also 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$.

Correctness. We now argue for the correctness of the construction. First,
consider the case when $G$ has an independent set $I=\\{v_{j_{1}},\ldots
v_{j_{c}}\\}$ of size $\geq c$. Let be $c$ distinct vertices from the
independent set. Let $e^{(i)}_{j}$ be the innermost acquire (on lock
$\ell_{(i+1)\%c}$) in the sub-trace $\sigma^{(i)}_{j}$. We show that the
sequence $D=\langle
e^{(1)}_{j_{1}},e^{(2)}_{j_{2}}\ldots,e^{(c)}_{j_{c}}\rangle$ is a deadlock
pattern. Observe that $\operatorname{thread}(e^{(i)}_{j_{i}})=t_{i}\neq
t_{i^{\prime}}=\operatorname{thread}(e^{(i^{\prime})}_{j_{i^{\prime}}})$ for
every $i\neq i^{\prime}$. Similarly, the locks acquired in $e^{(i)}_{j_{i}}$
and $e^{(i^{\prime})}_{j_{i^{\prime}}}$ are also distinct when $i\neq
i^{\prime}$. Finally, we want to show that
$\mathsf{HeldLks}_{\sigma}(e^{(i)}_{j_{i}})\cap\mathsf{HeldLks}_{\sigma}(e^{(i^{\prime})}_{j_{i^{\prime}}})=\varnothing$
for every $i\neq i^{\prime}$. Assume on the contrary that there is a lock
$\ell\in\mathsf{HeldLks}_{\sigma}(e^{(i)}_{j_{i}})\cap\mathsf{HeldLks}_{\sigma}(e^{(i^{\prime})}_{j_{i^{\prime}}})$.
Clearly, $\ell$ cannot be of the form $\ell_{m}$ for some $0\leq m<c$ as the
only such lock held at $e^{(i)}_{j_{i}}$ is $\ell_{i\%c}$ and the only such
lock held at $e^{(i^{\prime})}_{j_{i^{\prime}}}$ is $\ell_{i^{\prime}\%c}$
which are different. Thus, it must be of the form $\ell_{\\{u,v\\}}$ for some
$\\{u,v\\}\in E$. Since it is acquired in both sub-traces
$\sigma^{(i)}_{j_{i}}$ and $\sigma^{(i^{\prime})}_{j_{i^{\prime}}}$, we have
$\ell=\ell_{\\{v_{i},v_{i^{\prime}}\\}}$. This means that
$\\{v_{i},v_{i^{\prime}}\\}\in E$ contradicting that $I$ is an independent
set.

Now, consider the case when there is a deadlock pattern of size $c$:
$D=\langle e_{0},e_{1},\ldots,e_{c-1}\rangle$. Since there are exactly $c$
threads in $\sigma$, there must be one event in each thread. We first argue
that if there is one $e_{i}$ that acquires a lock of the form
$\ell_{\\{u,v\\}}$ then all events in the deadlock pattern do so. This follows
from a simple inductive argument — $e_{i+1}$ must acquire a lock held at
$e_{i}$ and thus must be of the form $\ell_{\\{u^{\prime},v^{\prime}\\}}$, and
so on. Next, all locks of the form $\ell_{\\{u,v\\}}$ are acquired in the
order consistent with the total order $<_{E}$. Hence, they cannot form a
cyclic dependency. Thus, the locks acquired at $e_{0},\ldots e_{c-1}$ are
$\ell_{0},\ldots,\ell_{c-1}$. Symmetry ensures that, you can assume, w.l.o.g
that $\operatorname{op}(e_{i})=\mathtt{acq}(\ell_{i\%c})$. Let $f(i)$ be the
index such that $e_{i}$ is in the subtrace $e^{(i)}_{f(i)}$. Then, we show
that the set $A=\\{v_{f(1)},v_{f(2)},\ldots,v_{f(c)}\\}$ is an independent set
of size $c$. Assume on the contrary that there are $i\neq i^{\prime}$ such
that $\\{v_{f(i)},v_{f(i^{\prime})}\\}\in E$. Then, our construction ensures
that the lock $\ell_{\\{}v_{f(i)},v_{f(i^{\prime})}\\}$ will be held at both
$e_{i}$ and $e_{i^{\prime}}$ contradicting that $D$ is a deadlock pattern.

Time complexity. The size of the trace is $O\big{(}c\cdot(2+\sum_{v\in
V}\mathsf{degree}(v))\big{)}$ $=O(c\cdot(|V|+|E|))$ and the time taken is also
the same. ∎

###  A.2. Proof of Theorem 3.2

See 3.2

###### 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},\ell,\ell^{\prime}$. $\sigma^{A}$ and $\sigma^{B}$,
intuitively 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})=(\ell,\ell^{\prime})$ if
$Z=A$, and $(m,m^{\prime})=(\ell^{\prime},\ell)$ otherwise.

  * •

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
inner most 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 inner most critical sections is inverted. Fig. 2(b) illustrates the
construction for an OV-instance with $n=2$ and $d=2$.

Correctness. We now argue for the correctness of the construction. First, if
$(A,B)$ is a positive $OV$ instance, then there are two indices
$\alpha,\beta\in\\{1,\ldots,n\\}$ such that $A_{\alpha}$ and $B_{\beta}$ are
orthogonal. Thus, for every $1\leq j\leq d$, we have $A_{\alpha}[j]=0$ or
$B_{\beta}[j]=0$ (possibly both). Based on the construction, this implies that
for every lock $\ell_{j}$ (with $1\leq j\leq d$), $\ell_{j}$ occurs in at most
one of the sub-traces $\sigma^{A}_{\alpha}$ and $\sigma^{B}_{\beta}$. This
gives a deadlock pattern $D=\langle e,e^{\prime}\rangle$, where $e$ is the
unique event in the sub-trace $\sigma^{A}_{\alpha}$ with
$\operatorname{op}(e)=\mathtt{acq}(\ell^{\prime})$ and $e^{\prime}$ is the
unique event in $\sigma^{B}_{\beta}$ with
$\operatorname{op}(e^{\prime})=\mathtt{acq}(\ell)$. This is because
$\ell\in\mathsf{HeldLks}_{\sigma}(e)$,
$\ell^{\prime}\in\mathsf{HeldLks}_{\sigma}(e^{\prime})$, and each lock
$\ell_{j}$ exists in at most one of $\mathsf{HeldLks}_{\sigma}(e)$ or
$\mathsf{HeldLks}_{\sigma}(e^{\prime})$ (and thus
$\mathsf{HeldLks}_{\sigma}(e)\cap\mathsf{HeldLks}_{\sigma}(e^{\prime})=\varnothing$).

Now, consider the case when there is a deadlock pattern $D=\langle
e,e^{\prime}\rangle$ in $\sigma$. W.l.o.g, we can assume that
$\operatorname{thread}(e)=t_{A}$ and
$\operatorname{thread}(e^{\prime})=t_{B}$. This means there is a $\alpha$ and
$\beta$ such that $e$ occurs in $\sigma^{A}_{\alpha}$ and $e^{\prime}$ occurs
in $\sigma^{B}_{\beta}$. Next, observe that $e$ and $e^{\prime}$ can only be
acquire events on locks $\\{\ell,\ell^{\prime}\\}$ and not on the locks
$\\{\ell_{1},\ldots,\ell_{d}\\}$. This is because the order of acquisition
amongst $\ell_{1},\ldots,\ell_{d}$ is always fixed and further, each of these
are never acquired inside of critical sections of $\ell$ or $\ell^{\prime}$.
By the choice of threads, $\operatorname{op}(e)=\mathtt{acq}(\ell^{\prime})$
and $\operatorname{op}(e^{\prime})=\mathtt{acq}(\ell)$. Since
$\mathsf{HeldLks}_{\sigma}(e)\cap\mathsf{HeldLks}_{\sigma}(e^{\prime})=\varnothing$,
for every $j$,
$\ell_{i}\not\in\mathsf{HeldLks}_{\sigma}(e)\cap\mathsf{HeldLks}_{\sigma}(e^{\prime})$.
This means that at most one of $A_{\alpha}[j]=1$ an $B_{\beta}[j]=1$ is true.
This means that the vectors $A_{\alpha}$ and $B_{\beta}$ are orthogonal.

Time complexity. The total size of the trace is $\mathcal{N}=O(n\cdot d)$ and
it has $\mathcal{L}=d+2=O(d)$ locks. The construction can be performed in time
$O(n\cdot d)$. Thus, if for some $\epsilon>0$, there is a
$O(\text{poly}(\mathcal{L})\cdot\mathcal{N}^{2-\epsilon})=O(\text{poly}(d)\cdot
n^{2-\epsilon})$ algorithm for the problem of detecting deadlock patterns of
length $2$, we would get a $O(\text{poly}(d)\cdot n^{2-\epsilon}+n\cdot
d)=O(\text{poly}(d)\cdot n^{2-\epsilon})$ time algorithm for OV, falsifying
the OV hypothesis. ∎

###  A.3. $\mathsf{W[1]}$-hardness for Deadlock Prediction

Finally, we prove that predicting deadlocks is a $\mathsf{W[1]}$-hard problem
parameterized by the number of threads $\mathcal{T}$.

See 3.3

###### Proof.

We establish a simple reduction from the problem of data-race prediction to
the problem of predicting deadlocks of size $2$. Given a trace $\sigma$ and a
deadlock pattern $D=\langle\mathtt{acq}_{1},\mathtt{acq}_{2}\rangle$ of size
$2$, we choose a fresh variable $x\not\in\mathsf{Vars}_{\sigma}$, and
construct two events
$\mathtt{w}_{1}=\langle\operatorname{thread}(\mathtt{acq}_{1}),\mathtt{w}(x)\rangle$
and
$\mathtt{w}_{2}=\langle\operatorname{thread}(\mathtt{acq}_{2}),\mathtt{w}(x)\rangle$,
where $x$. We construct a trace $\sigma^{\prime}$ by replacing
$\mathtt{acq}_{1}$ and $\mathtt{acq}_{2}$ in $\sigma$ with $\mathtt{w}_{1}$
and $\mathtt{w}_{2}$, respectively. It is straightforward to verify that any
correct $\rho$ reordering of $\sigma^{\prime}$ that witnesses
$(\mathtt{w}_{1},\mathtt{w}_{2})$ as a data race is also a correct reordering
of $\sigma$ that witnesses the deadlock $(\mathtt{acq}_{1},\mathtt{acq}_{2})$.
Since predicting data races is $\mathsf{W[1]}$-hard on $\mathcal{T}$(Mathur et
al., 2020), the desired result follows. ∎

##  Appendix B Proofs of Section 4

We first prove Lemma 4.5.

See 4.5

###### Proof.

Let $\rho$ be a sync-preserving correct reordering of $\sigma$ (and thus
$\mathsf{Events}_{\rho}\subseteq\mathsf{Events}_{\sigma}$) such that
$S\subseteq\mathsf{Events}_{\rho}$. Since, $\rho$ is a correct-reordering of
$\sigma$, for every event $e\in\mathsf{Events}_{\rho}$, we must have
$f\in\mathsf{Events}_{\rho}$ for every $f\leq^{\sigma}_{\mathsf{TO}}e$.
Likewise, for every read event $e\in\mathsf{Events}_{\rho}$, we must also have
$\mathsf{rf}_{\sigma}(e)\in\mathsf{Events}_{\rho}$, again because $\rho$ is a
correct reordering of $\sigma$. Finally, let $e\in\mathsf{Events}_{\rho}$ be
an acquire event (with $\operatorname{op}(e)=\mathtt{acq}(\ell)$), and let
$f\neq e$ be another acquire event (with
$\operatorname{op}(e)=\mathtt{acq}(\ell)$) with
$f\leq^{\sigma}_{\mathsf{tr}}e$. Since $\rho$ is a sync-preserving correct
reordering of $\rho$, we must also have
$\mathsf{match}_{\sigma}(f)\in\mathsf{Events}_{\rho}$. Thus, $\rho$ must
contain $\mathsf{SPClosure}_{\sigma}(S)$.

Let us now argue that we can construct a sync-preserving correct reordering
whose events are precisely $\mathsf{SPClosure}_{\sigma}(S)$. Consider the
sequence of events $\rho$ obtained by projecting $\sigma$ to
$\mathsf{SPClosure}_{\sigma}(S)$. We will argue that (a) $\rho$ is a well-
formed trace, (b) $\rho$ is a correct reordering of $\sigma$, and (c) $\rho$
preserves the order of critical section on the same lock as in $\sigma$. For
(a), we need to argue that critical sections on the same lock do not overlap
in $\rho$. This follows because if they did, then we have two acquire events
$e_{1}\neq e_{2}\in\mathsf{SPClosure}_{\sigma}(S)$ such that
$\operatorname{op}(e_{1})=\operatorname{op}(e_{2})=\mathtt{acq}(\ell)$ (for
some $\ell$), $e_{1}\leq^{\sigma}_{\mathsf{tr}}e_{2}$ (and thus $e_{1}$ also
appears before $e_{2}$ in $\rho$ by construction), but
$\mathsf{match}_{\sigma}(e_{1})$ either does not appear in $\rho$ or appears
later than $e_{2}$. In the first case, we arrive at a contradiction to the
definition of $\mathsf{SPClosure}_{\sigma}(S)$, and in the second case, we
arrive at a contradiction that $\rho$ is obtained without changing the
relative order of the residual events. Arguing (b) is straightforward:
$\mathsf{SPClosure}_{\sigma}(S)$ is closed under both
$\leq^{\sigma}_{\mathsf{TO}}$ as well as $\mathsf{rf}_{\sigma}$, and further
$\rho$ preserves the order of events as in $\sigma$. Likewise, (c) is easy to
argue because $\mathsf{Events}_{\rho}=\mathsf{SPClosure}_{\sigma}(S)$ are
closed under sync-preservation and the order of events in $\rho$ does not
change with respect to $\sigma$. ∎

Let us now turn our attention to Lemma 4.6.

See 4.6

###### Proof.

($\Rightarrow$). Assume $D$ is a sync-preserving deadlock of $\sigma$. Let
$\rho$ be the sync-preserving correct reordering of $\sigma$ that witnesses
$D$. Thus, each of $e_{0},\ldots,e_{k-1}$ are enabled in $\rho$. This means
that $\textsf{pred}_{\sigma}(S)\subseteq\mathsf{Events}_{\rho}$, and also
$S\cap\mathsf{Events}_{\rho}=\varnothing$. By Lemma 4.5, we have
$\mathsf{SPClosure}_{\sigma}(\textsf{pred}_{\sigma}(S))\subseteq\mathsf{Events}_{\rho}$,
giving us $\mathsf{SPClosure}_{\sigma}(\textsf{pred}_{\sigma}(S))\cap
S=\varnothing$.

($\Leftarrow$). Assume
$\mathsf{SPClosure}_{\sigma}(\textsf{pred}_{\sigma}(S))\cap S=\varnothing$.
From Lemma 4.5, there exists a sync-preserving correct reordering $\rho$ with
$\textsf{pred}_{\sigma}(S)\subseteq\mathsf{SPClosure}_{\sigma}(\textsf{pred}_{\sigma}(S))=\mathsf{Events}_{\rho}$.
Since $S\cap\mathsf{Events}_{\rho}=\varnothing$, the entire deadlock pattern
$D$ is also enabled in $\rho$. Thus, $D$ is a sync-preserving deadlock of
$\sigma$. ∎

The proof of the following proposition follows directly from the definition of
sync-preserving closure.

See 4.9

###### Proof.

Follows from the definition of $\mathsf{SPClosure}_{\sigma}(S)$. ∎

##  Appendix C Incomparability of SPDOffline and SeqCheck

In this section we provide two example traces and discuss the deadlocks found
and missed on them by SeqCheck and SPDOffline. Example C.1 discusses a trace
which contains a deadlock found by SPDOffline but missed by SeqCheck. Example
C.2 discusses a trace which contains a deadlock found by SeqCheck but missed
by SPDOffline. These examples showcase the incomparability of the techniques
SPDOffline and SeqCheck.

###### Example 0.

Fig. 5 displays a trace $\sigma$ in which SPDOffline reports a deadlock
whereas SeqCheck misses the deadlock. In this trace, there is a single
deadlock pattern $\langle e_{4},e_{14}\rangle$. This deadlock pattern can be
realized by the sync-preserving correct reordering
$\rho=e_{3},e_{12},e_{13},e_{8},e_{9}$. However, this deadlock is missed by
SeqCheck. The reason for this can be explained as follows. First, observe that
a correct reordering of $\sigma$ would need to include the event $e_{13}$ and
consequently $e_{9}=\mathsf{rf}_{\sigma}(e_{13})$. A strategy that SeqCheck
employs when it is producing correct reorderings is that it aims to close all
the critical sections that appear in the reordering. In order to fulfill this
constraint, SeqCheck closes the critical section on lock
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\ell_{1}}$
in thread $t_{1}$. This requires SeqCheck to execute the read event $e_{10}$
as well as the event $e_{7}=\mathsf{rf}_{\sigma}(e_{10})$. This in turn causes
SeqCheck to execute the events $e_{3}\ldots e_{6}$. Observe that the first
event that appears in the deadlock pattern, $e_{4}$, can no longer be
scheduled concurrently with $e_{14}$. Hence, SeqCheck is unable to report a
deadlock in this trace.

###### Example 0.

Fig. 6 display a trace $\sigma$ in which SeqCheck reports one more deadlock
than SPDOffline. In this trace there are two deadlock patterns $\langle
e_{2},e_{6}\rangle$ and $\langle e_{2},e_{8}\rangle$. The first deadlock
pattern $\langle e_{2},e_{6}\rangle$ can be realized to a real deadlock by
both SeqCheck and SPDOffline. The second deadlock pattern $\langle
e_{2},e_{8}\rangle$ cannot be realized to a real deadlock by SPDOffline.
Whereas, SeqCheck is able to report this as a real deadlock. The reason why
SPDOffline misses the second deadlock can be explained as follows. The
computed sync-preserving closure for the second deadlock pattern is
$\mathsf{SPClosure}_{\sigma}(\textsf{pred}_{\sigma}(\\{e_{2},e_{8}\\}))=\\{e_{1},\ldots,e_{4},e_{5},\ldots,e_{7}\\}$.
Since the SPDOffline algorithm cannot reverse the order of critical sections
on a given lock, it always enforces to close the critical section on lock
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\ell_{1}}$
in thread $t_{2}$ after the one in $t_{1}$. This brings the event $e_{2}$ into
the sync-preserving closure of $\langle e_{2},e_{8}\rangle$ and disables
SPDOffline from realizing this deadlock pattern.

$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{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}})$$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{w}(y)$$8$
$\mathtt{acq}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\ell_{1}})$$9$
$\mathtt{w}(x)$$10$ $\mathtt{r}(y)$$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{r}(x)$$14$ $\mathbf{\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}})}$$15$
$\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}})$$16$
$\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}})$

Figure 5.  A trace $\sigma$ with a sync-preserving deadlock, stalling $t_{2}$
on $e_{14}$ and $t_{3}$ on $e_{4}$.

$t_{1}$$t_{2}$$1$
$\mathtt{acq}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\ell_{1}})$$2$
$\mathbf{\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{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{rel}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\ell_{1}})$$5$
${\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}})}$$6$
$\mathbf{\mathtt{\bf
acq}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\ell_{1}})}$$7$
$\mathtt{rel}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\ell_{1}})$$8$
$\mathbf{\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}})$

Figure 6.  A trace $\sigma$ with a sync-preserving deadlock, stalling $t_{1}$
on $e_{2}$ and $t_{2}$ on $e_{6}$ and a predictable but not sync-preserving
deadlock stalling $t_{1}$ on $e_{2}$ and $t_{2}$ on $e_{8}$.

##  Appendix D Unsoundness Of Dirk

In this section we provide two example programs that showcase the unsoundness
of Dirk. Example D.2 discusses a program which is a modified version of the
Transfer benchmark. Dirk reports a false deadlock in this example due to that
it is aiming to relax the standard definition of correct reorderings and allow
a read event to read from a different write than in the original trace. Note
that this relaxation enables Dirk to predict deadlocks in the benchmarks
Transfer and Deadlock, which are missed by SPDOffline and SeqCheck. However,
this relaxation is not fully formalized and the implementation of it contains
errors. Example D.1 discusses a crafted program in which Dirk is reporting a
false deadlock due to missing that a common lock protects an otherwise
deadlock pattern.

###### Example 0.

Fig. 7 displays a program in which Dirk makes a false deadlock report. The
program spawns three threads T1, T2, and T3 and there exist three locks L1,
L2, and L3 which are used in these threads. In the program, T1 acquires the
lock L1 and then forks T2, and it holds the lock L1 until T2 is joined. Even
though the locks L2 and L3 are acquired in a cyclic manner in the threads T2
and T3, this program does not exhibit a deadlock due to the common lock L1.
Therefore, this program does not exhibit a deadlock. However, Dirk fails to
recognize the common lock L1 and reports a false deadlock. This observed
behavior is not an implementation error, but it is in alignment with the
underlying theory of Dirk (Kalhauge and Palsberg, 2018). In particular, Dirk
makes SMT queries to decide the existence of deadlocks, but its encoding
unsoundly neglects the condition that deadlocking events must have disjoint
lock sets.

###### Example 0.

Fig. 8 displays a program in which Dirk makes a false deadlock report. This
program is a modified version of the Transfer benchmark, which was used as a
running example to explain Dirk (Kalhauge and Palsberg, 2018). The example
contains the classes Transfer1, Transfer2, Store and UserObject. The Store
class contains two synchronized methods, transferTo and add. The transferTo
takes another Store object as argument and calls the add method by using this
object. Notice that if two different Store objects simultaneously call the
transferTo method by passing each other as the argument, then this can
potentially lead to a deadlock. Observe that in the given program there exists
such a scenario where transferTo is called with opposite Store objects in the
classes Transfer1 and Transfer2. However, in this case the program can never
actually deadlock. The reason is that the transferTo method in Transfer2 class
can only be executed if the UserObject.data can be cast to an integer value.
The UserObject.data is a volatile variable that is shared by the classes
Transfer1 and Transfer2. This variable is initialized to a string value and an
integer value is assigned to this variable only after the transferTo method
has been executed in Transfer1. Hence, this program does not exhibit a
deadlock. However, Dirk reports a deadlock in this program. The reason is that
Dirk unsoundly concludes that reading the value of UserObject.data at Line
$54$ does not affect the control flow of the program. Hence, in case the value
of UserObject.data object in Line $54$ is read from the write event on Line
$39$, Dirk ignores this dependency and concludes that Lines $38$ and $54$ can
execute concurrently and reports a false deadlock.

⬇

1public class FalseDeadlock1 {

2 public static Object L1 = new Object();

3 public static Object L2 = new Object();

4 public static Object L3 = new Object();

5 public static long x, y;

6 public static final long ITERS = 10;

7

8 public static void main (String [] args) {

9 x = 0;

10 y = 0;

11 T1 t1 = new T1();

12 T3 t3 = new T3();

13 t1.start();

14 t3.start();

15 try{

16 t1.join();

17 }

18 catch(Exception ex) { }

19 try{

20 t3.join();

21 }

22 catch(Exception ex) { }

23 }

24

25 static class T1 extends Thread {

26 public void run () {

27 synchronized (L1) {

28 T2 t2 = new T2();

29 t2.start();

30 try{

31

32 t2.join();

33 }

34 catch(Exception ex){

35 }

36 }

37 }

38 }

39 static class T2 extends Thread {

40 public void run () {

41 synchronized (L2) {

42 synchronized (L3) {

43 for(int i = 0; i < ITERS; i++){

44 x = x + 1;

45 }

46 }

47 }

48 }

49 }

50 static class T3 extends Thread {

51 public void run () {

52 synchronized (L1) {

53 synchronized (L3) {

54 synchronized (L2) {

55 for(int i = 0; i < ITERS; i++){

56 y = y + 1;

57 }

58 }

59 }

60 }

61 }

62 }

63}

⬇

33public class FalseDeadlock1 {

34 public static Object L1 = new Object();

35 public static Object L2 = new Object();

36 public static Object L3 = new Object();

37 public static long x, y;

38 public static final long ITERS = 10;

39

40 public static void main (String [] args) {

41 x = 0;

42 y = 0;

43 T1 t1 = new T1();

44 T3 t3 = new T3();

45 t1.start();

46 t3.start();

47 try{

48 t1.join();

49 }

50 catch(Exception ex) { }

51 try{

52 t3.join();

53 }

54 catch(Exception ex) { }

55 }

56

57 static class T1 extends Thread {

58 public void run () {

59 synchronized (L1) {

60 T2 t2 = new T2();

61 t2.start();

62 try{

63

64 t2.join();

65 }

Figure 7. FalseDeadlock1.java

⬇

1public class UserObject {

2 public volatile Object data;

3

4 public UserObject() {

5 this.data = "string1";

6 }

7}

8

9class Store {

10 private int var;

11

12 public Store(int var) {

13 this.var = var;

14 }

15

16 public synchronized void transferTo(int amount, Store other, int intVal) {

17 this.var -= amount;

18 other.add(amount);

19 }

20

21 public synchronized void add(int amount) {

22 this.var += amount;

23 }

24}

25

26public class Transfer1 implements Runnable {

27 private Store a;

28 private Store b;

29 private UserObject uObject;

30

31 public Transfer1(Store a, Store b, UserObject uObject) {

32 this.a = a;

33 this.b = b;

34 this.uObject = uObject;

35 }

36 public void run() {

37 uObject.data = "string2";

38 a.transferTo(1, b, 0);

39 uObject.data = 1;

40 }

41}

42public class Transfer2 implements Runnable {

43 private Store a, b;

44 private UserObject uObject;

45

46 public Transfer2(Store a, Store b, UserObject uObject) {

47 this.a = a;

48 this.b = b;

49 this.uObject = uObject;

50 }

51

52 public void run() {

53 try {

54 a.transferTo(1, b,(int) uObject.data);

55 } catch(Exception e) { }

56 }

57}

58

59public class FalseDeadlock2 {

60 public static void main(String[] args) {

61 Store a = new Store(1),

62 b = new Store(1);

63

64 UserObject uObject = new UserObject();

65 Transfer1 trans1 = new Transfer1(a, b, uObject);

66 Transfer2 trans2 = new Transfer2(b, a, uObject);

67

68 Thread[] threads = {

69 new Thread(trans1),

70 new Thread(trans2)

71 };

72

73 for (Thread t : threads) t.start();

74

75 for (Thread t : threads)

76 try { t.join(); }

77 catch (InterruptedException e) { };

78 }

79}

⬇

42public class UserObject {

43 public volatile Object data;

44

45 public UserObject() {

46 this.data = "string1";

47 }

48}

49

50class Store {

51 private int var;

52

53 public Store(int var) {

54 this.var = var;

55 }

56

57 public synchronized void transferTo(int amount, Store other, int intVal) {

58 this.var -= amount;

59 other.add(amount);

60 }

61

62 public synchronized void add(int amount) {

63 this.var += amount;

64 }

65}

66

67public class Transfer1 implements Runnable {

68 private Store a;

69 private Store b;

70 private UserObject uObject;

71

72 public Transfer1(Store a, Store b, UserObject uObject) {

73 this.a = a;

74 this.b = b;

75 this.uObject = uObject;

76 }

77 public void run() {

78 uObject.data = "string2";

79 a.transferTo(1, b, 0);

80 uObject.data = 1;

81 }

82}

Figure 8. FalseDeadlock2.java