Journal of High Speed Networks

A self-stabilizing algorithm cannot detect by itself that stabilization has been reached. For overcoming this drawback Lin and Simon introduced the notion of an external observer, i.e., a set of processes, one being located at each node, whose role is to detect stabilization.

We propose here a less expensive approach, where there is a single observing process located at a unique node. This process is not allowed to detect false stabilization and it must eventually detect that stabilization is reached. Moreover it must not interfere with the observed self-stabilizing algorithm. Our result is that there exists such an observer for any problem on a distinguished network having a synchronous self-stabilizing solution. Note that our proof is constructive.

This paper reports the first self-stabilizing Border Gateway Protocol (BGP). BGP is the standard inter-domain routing protocol in the Internet. Self-stabilization is a technique to tolerate arbitrary transient faults.

The routing instability in the Internet can occur due to errors in configuring the routing data structures, the routing policies, transient physical and data link problems, software bugs, and memory corruption. This instability can increase the network latency, slow down the convergence of the routing data structures, and can also cause the partitioning of networks. Most of the previous studies concentrated on routing policies to achieve the convergence of BGP while the oscillations due to transient faults were ignored.

The purpose of self-stabilizing BGP is to solve the routing instability problem when this instability results from transient failures. The self-stabilizing BGP presented here provides a way to detect and automatically recover from this type of faults. Our protocol is combined with an existing protocol to make it resilient to policy conflicts as well.

The Hello protocol in OSPF allows each router in a network to check whether it can exchange messages with neighboring routers in its network. This check is carried out by making each router periodically send hello messages to every neighboring router in the network. Associated with the Hello protocol are two time periods: the hello period and the dead period. The hello period is the time period between sending two successive hello messages to the same neighbor. The dead period is the time period after which a router can declare a neighbor dead if during this period the router does not receive any hello messages from that neighbor. The original Hello protocol restricts the hello and dead periods to be fixed over time and to be identical in all routers. Simulation studies have shown that these restrictions contribute to network instabilities and even to network collapse. To improve network stability, we present a flexible Hello protocol where the hello and dead periods change over time and become consistent (rather than identical) in all routers. To ensure the fault-tolerance of our Hello protocol, the protocol is designed to be stabilizing. That is, when started from an arbitrary initial state, the protocol converges to a legitimate state, and remains in legitimate states throughout the remainder of its execution.

Distributed algorithms, self-stabilizing systems in particular, are often too delicate to be argued informally. Formal proofs are much more reliable, but unfortunately are often long and complicated. Some of the complication is inherent, but some is also the result of poor notation and formalism which is not abstract enough. Improving them would make formal proofs easier to write and to understand, which will also make them less error prone. In this spirit, this paper proposes an extension of the logic UNITY with a number of new operators to model self-stabilization and a formalization of a number of useful design strategies. They should enhance the formalism offered by UNITY with better abstraction to specify and reason about self-stabilization.

In this paper, we are interested in transformations of self-stabilizing algorithms from one model to another that preserve stabilization. We propose an easy technique for proving correctness of a natural class of transformations of self-stabilizing algorithms from any model to any other. We present a new transformation of self-stabilizing algorithms from a message passing model to a shared memory model with a finite number of registers of bounded size and processors of bounded memory and prove it correct using our technique. This transformation is not wait-free, but we prove that no such transformation can be wait-free. For our transformation, we use a new self-stabilizing token-passing algorithm for the shared memory model. This algorithm stabilizes in O(nlog ²n) rounds, which improves existing algorithms.