STABILIZING COMMUNICATION PROTOCOLS

A communication protocol is stabilizing iff starting from any unsafe state (i.e., one that violates the intended invariant of the protocol), the protocol is guaranteed to converge to a safe state within a finite number of state transitions. Stabilization allows the processes in a protocol to reestablish coordination between one another, whenever coordination is lost due to some failure. In this paper, we identify some important characteristics of stabilizing protocols; we show in particular that a stabilizing protocol is nonterminating, has an infinite number of safe states, and has timeout actions. We also propose a formal method for proving protocol stabilization: in order to prove that a given protocol is stabilizing, it is sufficient (and necessary) to exhibit and verify what we call a "convergence stair" for the protocol. Finally, we discuss how to redesign a number of well-known protocols to make them stabilizing; these include the sliding-window protocol and the two-way handshake.