Fighting Livelock in the GNU i-Protocol:
A Case Study in Explicit-State Model Checking

Abstract

The i-protocol, an optimized sliding-window protocol for GNU uucp, first came to our attention in 1995 when we used the Concurrency Factory's local model checker to detect, locate, and correct a non-trivial livelock in version~1.04 of the protocol. Since then, we have conducted a systematic case study on the protocol using four verification tools, viz. Cospan, Murphi, Spin, and XMC, each of which supports some form of explicit-state model checking. Our results show that although the i-protocol is inherently complex---the size of its state space grows exponentially in the window size and it deploys several sophisticated optimizations aimed at minimizing control-message and retransmission overhead---it is nonetheless amenable to a number of general-purpose abstraction techniques whose application can significantly reduce the size of the protocol's state space.

Appendix