Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Partial Orders for Precise and Efficient Dynamic Deadlock Prediction

Bas van den Heuvel, Martin Sulzmann, Peter Thiemann

TL;DR

This work tackles the challenge of false positives in dynamic deadlock prediction for concurrent programs by introducing partial-order inspired refinements to deadlock patterns. It presents a new TRW partial order that yields sound predictions and a weaker PWR variant that guarantees completeness, with an offline implementation and extensive benchmarks showing they report the same deadlocks as leading methods but with improved precision. The authors prove key properties, define concrete and abstract lock dependencies, and provide an efficient two-phase pipeline to compute partial orders and verify deadlock patterns. Empirically, TRW and PWR offer complementary guarantees, enabling practical, scalable deadlock prediction for real-world traces and paving the way for robust, sound-deadlock-prevention tooling.

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.

Partial Orders for Precise and Efficient Dynamic Deadlock Prediction

TL;DR

This work tackles the challenge of false positives in dynamic deadlock prediction for concurrent programs by introducing partial-order inspired refinements to deadlock patterns. It presents a new TRW partial order that yields sound predictions and a weaker PWR variant that guarantees completeness, with an offline implementation and extensive benchmarks showing they report the same deadlocks as leading methods but with improved precision. The authors prove key properties, define concrete and abstract lock dependencies, and provide an efficient two-phase pipeline to compute partial orders and verify deadlock patterns. Empirically, TRW and PWR offer complementary guarantees, enabling practical, scalable deadlock prediction for real-world traces and paving the way for robust, sound-deadlock-prevention tooling.

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.

Paper Structure

This paper contains 49 sections, 6 theorems, 16 equations, 12 figures, 4 tables.

Table of Contents

  1. Introduction
  2. Prior work.
  3. Our novel approach.
  4. A new partial order for sound and efficient deadlock prediction.
  5. Contributions and outline.
  6. Overview
  7. Lock Dependencies
  8. False Positives
  9. Partial-order Methods for Deadlock Prediction
  10. Happens-Before is too strict.
  11. Weak-Causally-Precedes is not strict enough.
  12. Total-Read-Write order and deadlock-pattern order for soundness.
  13. Comparison against the state of the art.
  14. Experimenting with other partial orders.
  15. Preliminaries
  16. ...and 34 more sections

Key Result

Theorem 1

If well-formed trace $T$ is TRW bounded and well nested, and DP $A$ in $T$ satisfies Conditions [DP-TRW/-Block], then $A$ is a predictable deadlock.

Figures (12)

  • Figure 1: Trace with lock dependencies.
  • Figure 2: False positive due to last-write dependency.
  • Figure 4: WCP false negative.
  • Figure 5: Trace where only the first deadlock pattern is feasible.
  • Figure 7: TRW false negative.
  • ...and 7 more figures

Theorems & Definitions (20)

  • Definition 1: Events and Traces
  • Definition 2: Well Formedness
  • Definition 3: Correctly Reordered Prefix
  • Definition 4: Critical Sections
  • Definition 5: Deadlock Patterns (DPs)
  • Definition 6: Predictable Deadlock
  • Definition 7: Total Read-Write Order (TRW)
  • Definition 8
  • Theorem 1: Soundness
  • Definition 9: Program-Write-Release Order (PWR)
  • ...and 10 more