Correct Black-Box Monitors for Distributed Deadlock Detection - Formalisation and Implementation

Watch this 13-minute conference presentation from OOPSLA 2025 that introduces a groundbreaking approach to detecting deadlocks in distributed systems through black-box monitoring. Learn about a novel distributed monitoring algorithm that observes only incoming and outgoing messages between services to identify deadlocks without requiring access to internal service implementations. Discover how the researchers developed a formal model capturing popular RPC-based application styles like gen_servers in Erlang/OTP, and explore their mathematically proven sound and complete algorithm that eliminates both false positives and false negatives in deadlock detection. Examine the implementation of DDMon, a practical tool for monitoring Erlang/OTP applications, and review performance evaluation results. Understand how this research addresses the critical challenge of diagnosing deadlocks in complex microservice architectures where the core deadlock can be obscured by cascading effects throughout the system. Gain insights into the formal verification process, including mechanized proofs in Coq, and explore the complete artifact package that accompanies this peer-reviewed research. This presentation represents the first work to formalize, prove correctness, and implement distributed black-box monitors specifically for deadlock detection in concurrent and distributed systems.