Static Deadlock Prevention in Dynamically Configured Communication Networks

We propose a technique to avoid deadlocks in a system of communicating processes. Our network model is very general. It supports dynamic process and channel creation and the ability to send channel endpoints over channels, thereby allowing arbitrary dynamically configured networks. Deadlocks happen in such networks if there is a cycle created by a set of channels, and processes along the cycle circularly wait for messages from each other. Our approach allows cycles of channels to be created, but avoids circular waiting by ensuring that for every cycle C, some process P breaks circular waits by selecting to communicate on both endpoints involved in the cycle C at P. We formalize this strategy as a calculus with a type system. Our type system keeps track of markers called obstructions where wait cycles are intended to be broken. Programmers annotate message types with design decisions on how obstructions are managed. Using these annotations, our type checker works modularly and independently on each process,without suffering any state space explosion. We prove the soundness of the analysis (namely deadlock freedom) on a simple but realistic language that captures the essence of such communication networks. We also describe how the technique can be applied to a substantial example.