Detect partial deadlocks #3425
Labels
A-concurrency
Area: affects our concurrency (multi-thread) support
C-enhancement
Category: a PR with an enhancement or an issue tracking an accepted enhancement
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.
The text was updated successfully, but these errors were encountered: