Partial Orders for Precise and Efficient Dynamic Deadlock Prediction

Fuente: arXiv
Enregistré dans:
Détails bibliographiques
Auteurs principaux: Heuvel, Bas van den, Sulzmann, Martin, Thiemann, Peter
Format: Preprint
Publié: 2025
Sujets:
Accès en ligne:
Tags: Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
_version_ 1866916001334951936
author Heuvel, Bas van den
Sulzmann, Martin
Thiemann, Peter
author_facet Heuvel, Bas van den
Sulzmann, Martin
Thiemann, Peter
contents 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.
format Preprint
id arxiv_https___arxiv_org_abs_2502_20070
institution arXiv
publishDate 2025
record_format arxiv
spellingShingle Partial Orders for Precise and Efficient Dynamic Deadlock Prediction
Heuvel, Bas van den
Sulzmann, Martin
Thiemann, Peter
Programming Languages
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.
title Partial Orders for Precise and Efficient Dynamic Deadlock Prediction
topic Programming Languages
url https://arxiv.org/abs/2502.20070