Deadlock in packet switching networks

TL;DR

This paper formalizes different types of deadlocks in packet switching networks, analyzes their relationships, and demonstrates an effective method for detecting deadlocks using symbolic model checking.

Contribution

It introduces formal definitions for global, local, and weak deadlocks and relates them, plus implements a deadlock detection tool with experimental validation.

Findings

Effective deadlock detection in packet switching networks

Formal relations between different deadlock notions

Successful identification of subtle deadlock scenarios

Abstract

A deadlock in a packet switching network is a state in which one or more messages have not yet reached their target, yet cannot progress any further. We formalize three different notions of deadlock in the context of packet switching networks, to which we refer as global, local and weak deadlock. We establish the precise relations between these notions, and prove they characterize different sets of deadlocks. Moreover, we implement checking of deadlock freedom of packet switching networks using the symbolic model checker nuXmv. We show experimentally that the implementation is effective at finding subtle deadlock situations in packet switching networks.