pith. sign in

arxiv: 2502.20070 · v3 · submitted 2025-02-27 · 💻 cs.PL

Partial Orders for Precise and Efficient Dynamic Deadlock Prediction

Bas van den Heuvel , Martin Sulzmann , Peter Thiemann This is my paper

Pith reviewed 2026-05-23 02:45 UTC · model grok-4.3

classification 💻 cs.PL
keywords deadlock predictionpartial ordersdynamic analysisconcurrent programslock acquisitionssoundnesscompletenessexecution traces
0
0 comments X

The pith

A new partial order on lock acquisitions from one trace predicts deadlocks without false positives.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

Standard dynamic deadlock detection from a single execution trace flags many cyclic lock patterns that can never occur under any scheduler. The paper defines the TRW partial order over lock acquisitions to filter those infeasible patterns: only unordered acquisitions that are not preceded by other deadlock patterns count as real deadlocks. It proves this TRW order is sound, meaning every reported deadlock is feasible. A slightly weakened variant is also complete, catching every possible deadlock. Both orders are computed directly from the trace in linear time and match on all deadlocks found across a large benchmark suite.

Core claim

Lock acquisitions must be unordered under the TRW partial order and must not be preceded by other deadlock patterns in order to identify true deadlocks. The TRW partial order is sound: it never reports a deadlock that cannot manifest. A weakened variant of TRW is complete: it misses no deadlocks. Both partial orders are derived from a single trace and run efficiently.

What carries the argument

The TRW partial order, which imposes ordering constraints on lock acquisitions observed in one execution trace to separate feasible from infeasible interleavings.

If this is right

  • Dynamic deadlock detectors can report only feasible deadlocks without requiring multiple traces or exhaustive search.
  • The same deadlocks are reported as prior methods, but with a soundness guarantee instead of possible false alarms.
  • The weakened TRW variant guarantees completeness while remaining efficient to compute from the trace.
  • Reporting the same deadlocks on benchmarks shows the partial-order filter preserves detection power in practice.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same trace-derived ordering technique might apply to predicting other schedule-dependent bugs such as atomicity violations.
  • Runtime monitors could use the TRW order on the fly to avoid schedules that would realize predicted deadlocks.
  • The method's reliance on a single trace leaves open whether certain classes of programs require multiple traces to expose all ordering constraints.

Load-bearing premise

A single execution trace contains enough ordering information to derive a partial order that correctly separates lock acquisitions that any scheduler can produce from those it cannot.

What would settle it

An execution trace from a program that contains a deadlock under some schedule, yet the TRW order on that trace reports no deadlock or reports one that never occurs.

Figures

Figures reproduced from arXiv: 2502.20070 by Bas van den Heuvel, Martin Sulzmann, Peter Thiemann.

Figure 1
Figure 1. Figure 1: Traces with potential deadlocks. [DP-Cycle] The acquired lock l2 of the first dependency is in the lockset {l2} of the second dependency, and the acquired lock l1 of the second dependency is in the lockset {l1} of the first dependency. [DP-Guard] The underlying locksets {l1} and {l2} are disjoint. Condition [DP-Guard] ensures that the deadlocked situation shown by the reordered pre￾fix [e1, e5] can be reac… view at source ↗
Figure 2
Figure 2. Figure 2: Partial orders for deadlock prediction. program trace. Ideally, this partial order captures the inter-event dependencies imposed be the trace and its semantics, making it possible to reason about correctly reordered traces without exploring all possible interleavings. This way, e.g., a partial order may order a read after its last write, or order the events within the same thread. Unordered events are then… view at source ↗
Figure 3
Figure 3. Figure 3: TRW versus SPDOffline versus PWR. Hence, the cyclic lock-dependency chain between D2 and D4 is not reachable, as it is blocked by the earlier cyclic lock-dependency chain between D1 and D3. To rule out such cases, we impose the following condition that imposes an order among deadlock patterns: [DP-Block] A deadlock pattern is not ordered after any other deadlock patterns. In Section 4, we show that conditi… view at source ↗
Figure 4
Figure 4. Figure 4: Example traces, with selected requests included (cf. Figu [PITH_FULL_IMAGE:figures/full_fig_p012_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Traces highlighting technical aspects of soundness and c [PITH_FULL_IMAGE:figures/full_fig_p015_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Standard versus abstract lock dependencies. [PITH_FULL_IMAGE:figures/full_fig_p018_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: Ordering conflicting write-write memory operations is critic [PITH_FULL_IMAGE:figures/full_fig_p036_7.png] view at source ↗
read the original abstract

Deadlocks are a major source of bugs in concurrent programs. They are hard to predict, because they may only occur under specific scheduling conditions. Dynamic analysis attempts to identify potential deadlocks by examining a single execution trace of the program. A standard approach involves monitoring sequences of lock acquisitions in each thread, with the goal of identifying deadlock patterns. A deadlock pattern is characterized by a cyclic chain of lock acquisitions, where each lock is held by one thread while being requested by the next. However, it is well known that not all deadlock patterns identified in this way correspond to true deadlocks, as they may be impossible to manifest under any schedule. We tackle this deficiency by proposing a new method based on partial orders to eliminate false positives: lock acquisitions must be unordered under a given partial order, and not preceded by other deadlock patterns. We prove soundness (no falsely predicted deadlocks) for the novel TRW partial order, and completeness (no deadlocks missed) for a slightly weakened variant of TRW. Both partial orders can be computed efficiently and report the same deadlocks for an extensive benchmark suite.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 3 minor

Summary. The paper introduces the TRW partial order (and a weakened variant) derived from a single execution trace to filter cyclic lock-acquisition patterns in dynamic deadlock prediction. It claims to prove that TRW is sound (no false-positive deadlocks reported) while the weakened variant is complete (no real deadlocks missed), that both orders are efficiently computable, and that they report identical deadlocks on an extensive benchmark suite.

Significance. If the stated soundness and completeness results hold, the work supplies a formal, parameter-free method that improves precision over standard dynamic deadlock detectors without sacrificing recall in the weakened case. The combination of proofs, efficient algorithms, and benchmark agreement would constitute a useful advance for concurrency analysis tools.

minor comments (3)
  1. [§4] The abstract states that soundness and completeness proofs exist; the main text should include a high-level proof sketch or key lemmas (e.g., in §4) so readers can assess the central claims without reading an appendix.
  2. [Evaluation] The claim that the two orders 'report the same deadlocks' on the benchmark suite should be supported by a table or figure showing per-benchmark counts rather than a single aggregate statement.
  3. [§3] Notation for the TRW relation (e.g., how 'unordered' and 'not preceded by other patterns' are combined) would benefit from a small worked example immediately after the definition.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive summary of our work and for recommending minor revision. No major comments were listed in the report, so we have no specific points to address point-by-point.

Circularity Check

0 steps flagged

No significant circularity identified

full rationale

The paper introduces a novel TRW partial order derived from execution traces, then states formal proofs of soundness (no false deadlocks) for TRW and completeness for a weakened variant. These proofs are presented as independent derivations from the order definitions and trace properties, with no reduction to fitted parameters, self-citations as load-bearing premises, or renaming of prior results. The central claims rest on explicit mathematical arguments and benchmark equivalence rather than any self-referential construction, satisfying the criteria for a self-contained derivation.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

The soundness and completeness claims rest on the definition of the TRW partial order and the assumption that it can be computed from trace data; no free parameters or invented physical entities are apparent from the abstract.

axioms (1)
  • domain assumption Lock acquisitions observed in a trace can be related by a partial order that reflects possible reorderings under different schedulers.
    This is the core modeling choice that allows the partial order to eliminate false positives.
invented entities (1)
  • TRW partial order no independent evidence
    purpose: To decide whether lock acquisitions in a candidate deadlock cycle are unordered.
    Newly introduced construct whose properties are proved in the paper.

pith-pipeline@v0.9.0 · 5721 in / 1163 out tokens · 29715 ms · 2026-05-23T02:45:20.146952+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

31 extracted references · 31 canonical work pages · 1 internal anchor

  1. [1]

    Adve and Kourosh Gharachorloo

    Sarita V. Adve and Kourosh Gharachorloo. Shared memory cons istency models: A tutorial. Computer, 29(12):66–76, December 1996. doi:10.1109/2.546611

    work page doi:10.1109/2.546611 1996

  2. [2]

    Agarwal, S

    R. Agarwal, S. Bensalem, E. Farchi, K. Havelund, Y. Nir-Buchbind er, S. D. Stoller, S. Ur, and L. Wang. Detection of deadlock potentials in multit hreaded programs. IBM Journal of Research and Development , 54(5):3:1–3:15, 2010. doi:10.1147/JRD.2010.2060276

    work page doi:10.1147/jrd.2010.2060276 2010

  3. [3]

    Predictive monitoring with stro ng trace pre- fixes

    Zhendong Ang and Umang Mathur. Predictive monitoring with stro ng trace pre- fixes. In Arie Gurfinkel and Vijay Ganesh, editors, Computer Aided Verification - 36th International Conference, CA V 2024, Montreal, QC, Ca nada, July 24-27, 2024, Proceedings, Part II , volume 14682 of Lecture Notes in Computer Science , pages 182–204. Springer, 2024. doi:10.1007/...

    work page doi:10.1007/978-3-031-65630-9 2024

  4. [4]

    Dynamic deadlock analysis of multi-threaded programs

    Saddek Bensalem and Klaus Havelund. Dynamic deadlock analysis of multi-threaded programs. In Proceedings of the First Haifa International Conference on Hardware and Software Verification and Testing , HVC’05, page 208–223, Haifa, Israel, 2005. Springer-Verlag. doi:10.1007/11678779_15

    work page doi:10.1007/11678779_15 2005

  5. [5]

    Yan Cai and W.K. Chan. Magiclock: Scalable detection of potential deadlocks in large-scale multithreaded programs. IEEE Transactions on Software Engineering , 40(3):266–281, 2014. doi:10.1109/TSE.2014.2301725

    work page doi:10.1109/tse.2014.2301725 2014

  6. [6]

    Sound and effi- cient concurrency bug prediction

    Yan Cai, Hao Yun, Jinqiu Wang, Lei Qiao, and Jens Palsberg. Sound and effi- cient concurrency bug prediction. In Diomidis Spinellis, Georgios Gous ios, Marsha Chechik, and Massimiliano Di Penta, editors, ESEC/FSE ’21: 29th ACM Joint European Software Engineering Conference and Symposium on the Foundations of 28 Software Engineering, Athens, Greece, August 2...

    work page 2021

  7. [7]

    doi:10.1145/3468264.3468549

    work page doi:10.1145/3468264.3468549

  8. [8]

    Cormac Flanagan and Stephen N. Freund. FastTrack: Efficient a nd precise dynamic race detection. Communications of the ACM , 53(11):93–101, 2010. doi:10.1145/1543135.1542490

    work page doi:10.1145/1543135.1542490 2010

  9. [9]

    Kaan Gen¸ c, Jake Roemer, Yufan Xu, and Michael D. Bond. Depe ndence-aware, un- bounded sound predictive race detection. Proc. ACM Program. Lang., 3(OOPSLA), October 2019. doi:10.1145/3360605

    work page doi:10.1145/3360605 2019

  10. [10]

    Jerry J. Harrow. Runtime checking of multithreaded applications with visual threads. In Klaus Havelund, John Penix, and Willem Visser, editors, SPIN Model Checking and Software Verification, 7th International SPIN Workshop , Stanford, CA, USA, August 30 - September 1, 2000, Proceedings , volume 1885 of Lecture Notes in Com- puter Science , pages 331–342. S...

    work page doi:10.1007/10722468_20 2000

  11. [11]

    Using runtime analysis to guide model checking of Java programs

    Klaus Havelund. Using runtime analysis to guide model checking of Java programs. In Proceedings of the 7th International SPIN Workshop on SPIN M odel Checking and Software Verification , page 245–264, Berlin, Heidelberg, 2000. Springer-Verlag

    work page 2000

  12. [12]

    Maximal sound predictive race detection with control flow abstraction

    Jeff Huang, Patrick O’Neil Meredith, and Grigore Ro¸ su. Maximal sound predictive race detection with control flow abstraction. In Michael F. P. O’Bo yle and Keshav Pingali, editors, PLDI ’14, pages 337–348, Edinburgh, United Kingdom, 2014. ACM. doi:10.1145/2594291.2594315

    work page doi:10.1145/2594291.2594315 2014

  13. [13]

    A r andomized dy- namic program analysis technique for detecting real deadlocks

    Pallavi Joshi, Chang-Seo Park, Koushik Sen, and Mayur Naik. A r andomized dy- namic program analysis technique for detecting real deadlocks. In Proceedings of the 30th ACM SIGPLAN Conference on Programming Language Design and Implemen- tation, PLDI ’09, page 110–120, Dublin, Ireland, 2009. Association for Co mputing Machinery. doi:10.1145/1542476.1542489

    work page doi:10.1145/1542476.1542489 2009

  14. [14]

    Sound deadlock pre diction

    Christian Gram Kalhauge and Jens Palsberg. Sound deadlock pre diction. Proc. ACM Program. Lang., 2(OOPSLA):146:1–146:29, October 2018. doi:10.1145/3276516

    work page doi:10.1145/3276516 2018

  15. [15]

    In: PLDI ’17

    Dileep Kini, Umang Mathur, and Mahesh Viswanathan. Dynamic rac e prediction in linear time. In Albert Cohen and Martin T. Vechev, editors, Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implemen- tation, PLDI 2017, Barcelona, Spain, June 18-23, 2017 , pages 157–170. ACM, 2017. doi:10.1145/3062341.3062374

    work page doi:10.1145/3062341.3062374 2017

  16. [16]

    Dynamic Race Prediction in Linear Time

    Dileep Kini, Umang Mathur, and Mahesh Viswanathan. Dynamic race prediction in linear time. CoRR, abs/1704.02432, 2017. URL: http://arxiv.org/abs/1704.02432, arXiv:1704.02432

    work page internal anchor Pith review Pith/arXiv arXiv 2017

  17. [17]

    Time, Clocks, and the Ordering of Events in a Distributed System

    Leslie Lamport. Time, clocks, and the ordering of events in a dist ributed system. Communications of the ACM , 21(7):558–565, 1978. doi:10.1145/359545.359563. 29

    work page doi:10.1145/359545.359563 1978

  18. [18]

    What happe ns-after the first race? enhancing the predictive power of happens-before ba sed dynamic race detection

    Umang Mathur, Dileep Kini, and Mahesh Viswanathan. What happe ns-after the first race? enhancing the predictive power of happens-before ba sed dynamic race detection. Proc. ACM Program. Lang. , 2(OOPSLA):145:1–145:29, October 2018. doi:10.1145/3276515

    work page doi:10.1145/3276515 2018

  19. [19]

    A tree clock data structure for causal orderings in concurrent ex- ecutions

    Umang Mathur, Andreas Pavlogiannis, H¨ unkar Can Tun¸ c, and Mahesh Viswanathan. A tree clock data structure for causal orderings in concurrent ex- ecutions. In Proceedings of the 27th ACM International Conference on Arc hitec- tural Support for Programming Languages and Operating Syst ems, ASPLOS ’22, page 710–725, Lausanne, Switzerland, 2022. Associatio...

    work page doi:10.1145/3503222.3507734 2022

  20. [20]

    Optimal predic- tion of synchronization-preserving races

    Umang Mathur, Andreas Pavlogiannis, and Mahesh Viswanathan . Optimal predic- tion of synchronization-preserving races. Proc. ACM Program. Lang., 5(POPL), jan

    work page

  21. [21]

    Jake Roemer, Kaan Gen¸ c, and Michael D. Bond. High-coverag e, unbounded sound predictive race detection. SIGPLAN Not. , 53(4):374–389, June 2018. doi:10.1145/3192366.3192385

    work page doi:10.1145/3192366.3192385 2018

  22. [22]

    Gen erating data race witnesses by an smt-based analysis

    Mahmoud Said, Chao Wang, Zijiang Yang, and Karem Sakallah. Gen erating data race witnesses by an smt-based analysis. In Proc. of NFM’11 , volume 6617 of LNCS, pages 313–327. Springer, 2011. doi:10.1007/978-3-642-20398-5_23

    work page doi:10.1007/978-3-642-20398-5_23 2011

  23. [23]

    Trace driven dy namic dead- lock detection and reproduction

    Malavika Samak and Murali Krishna Ramanathan. Trace driven dy namic dead- lock detection and reproduction. In Jos´ e E. Moreira and James R. Larus, editors, ACM SIGPLAN Symposium on Principles and Practice of Paralle l Programming, PPoPP ’14, Orlando, FL, USA, February 15-19, 2014 , pages 29–42. ACM, 2014. doi:10.1145/2555243.2555262

    work page doi:10.1145/2555243.2555262 2014

  24. [24]

    Sound predictive race detection in polynomial time

    Yannis Smaragdakis, Jacob Evans, Caitlin Sadowski, Jaeheon Yi, and Cormac Flana- gan. Sound predictive race detection in polynomial time. SIGPLAN Not., 47(1):387– 400, January 2012. doi:10.1145/2103656.2103702

    work page doi:10.1145/2103656.2103702 2012

  25. [25]

    Picklock: A deadlock prediction approa ch under nested lock- ing

    Francesco Sorrentino. Picklock: A deadlock prediction approa ch under nested lock- ing. In Proceedings of the 22nd International Symposium on Model Ch ecking Soft- ware - Volume 9232 , SPIN 2015, page 179–199, Stellenbosch, South Africa, 2015. Springer-Verlag. doi:10.1007/978-3-319-23404-5_13

    work page doi:10.1007/978-3-319-23404-5_13 2015

  26. [26]

    Efficient, near complete, and often sound hybrid dynamic data race prediction

    Martin Sulzmann and Kai Stadtm¨ uller. Efficient, near complete, and often sound hybrid dynamic data race prediction. In Stefan Marr, editor , MPLR ’20: 17th International Conference on Managed Programming Languages and Runtimes, Virtual Event, UK, November 4-6, 2020 , pages 30–51. ACM, 2020. doi:10.1145/3426182.3426185

    work page doi:10.1145/3426182.3426185 2020

  27. [27]

    Sound dynamic deadlock prediction in linear time

    H¨ unkar Can Tun¸ c, Umang Mathur, Andreas Pavlogiannis, and Mahesh Viswanathan. Sound dynamic deadlock prediction in linear time. Proc. ACM Pro- gram. Lang., 7(PLDI):1733–1758, 2023. doi:10.1145/3591291. 30

    work page doi:10.1145/3591291 2023

  28. [28]

    UNDEAD: Detecting and preventing deadlocks in production software

    Jinpeng Zhou, Sam Silvestro, Hongyu Liu, Yan Cai, and Tongping L iu. UNDEAD: Detecting and preventing deadlocks in production software. In Gr igore Rosu, Massi- miliano Di Penta, and Tien N. Nguyen, editors, Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineeri ng, ASE 2017, Urbana, IL, USA, October 30 - November 03, 20...

    work page 2017

  29. [29]

    31 A Proofs Lemma 1

    doi:10.1109/ASE.2017.8115684. 31 A Proofs Lemma 1. Given well-formed and well-nested trace T , <T DP is a strict partial order. Proof. Irreflexivity Take any DP A in T . Towards contradiction, suppose A < T DP A. Take any (a, q ) ∈ A. There exists ( a′, q ′) ∈ A such that q < T T r q′ and a ∈ AHT (q′). Since also a ∈ AHT (q), then thd( q) = thd( q′) = thd(...

    work page doi:10.1109/ase.2017.8115684 2017

  30. [30]

    = thd( q1) and thd( b2) = thd(b′

    work page

  31. [31]

    Number of concrete lock dependen- cies

    = thd( q2). Let q′ 1 and q′ 2 be the requests requesting b′ 2 and b′ 1, respectively, and let B = {(b1, q ′ 1), (b2, q ′ 2)}. Clearly, B is a cycle (satisfying Condition [DP-Cycle]) where b1 ∈ AHT (q1) and q′ 1 <T T r q1, and b2 ∈ AHT (q2) and q′ 2 <T T r q2. Hence, B < T DP A (Definition 8), reaching our desired contradiction that DP A satisfies Condition ...

    work page