Skip to content

Detect partial deadlocks #3425

Open
Open
@RalfJung

Description

Currently we only report a deadlock when all threads stop running. Ideally we'd be able to detect partial deadlocks, where two threads are waiting on each other but other, unrelated threads can still make progress.

This will require tracking more information about why a thread is blocked. We can then build a graph of "thread X blocked on thread Y", and if there's a cycle in that graph we have a (partial) deadlock. It might require asking libraries to provide us with such information: e.g. for POSIX locks we know which thread is currently holding a lock, so we can add the edge in the graph; but for futex-based locks we don't know which thread a futex_wait is waiting for, so we can't know where that graph edge is supposed to point to.

Following this paper we should actually treat deadlocks and memory leaks together and then we can detect partial deadlocks and partial leaks, but it's not clear to me how to best apply that to Miri -- and the sheer number of memory allocations may make that infeasible.

Metadata

Assignees

No one assigned

    Labels

    A-concurrencyArea: affects our concurrency (multi-thread) supportC-enhancementCategory: a PR with an enhancement or an issue tracking an accepted enhancement

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions