Correct Black-Box Monitors for Distributed Deadlock Detection: Formalisation and(…)
summary
Claims a distributed black-box monitoring algorithm that is sound and complete for detecting deadlocked services in RPC/gen_server-style systems, proved and mechanised in Coq. Monitors wrap each service, emit unique probe propagation control messages when a service becomes locked, and detect cycles (deadlocks) by returning probes without observed replies. The implementation DDMon attaches to Erlang/OTP, the authors measure message overhead (counting probes/messages) and report modest extra traffic with optimisations; proofs and artifact are available.
AI-written summary · about
chapters (8)
- 0:00Distributed deadlocks intro
- 1:51Existing deadlock detection limits
- 2:57Formalizing services and monitors
- 5:25Monitoring transparency needs
- 7:09Deadlock detection algorithm
- 8:58DDON implementation and eval
- 10:01Summary and future work
- 10:23Q&A
related talks
18mDDMon: a Monitoring Tool for Distributed Deadlock Detection
16mDynamic Partial Order Reduction for Checking Correctness Against Transaction Isolation(…)
30mZenMonitor: Scaling Distributed Monitoring
26mConcurrency: Unlocking a Solution
48mHow to build distributed concurrency primitives
01h 30mImplementing, verifying and debugging distributed event-based systems
39mTry Catch Blocks for your Distributed System
20mPerformal: Formal Verification of Latency Properties for Distributed Systems