Search

A self-stabilizing program eventually resumes normal behavior even if execution begins in an abnormal initial state. In this paper, we explore the possibility of extending an arbitrary program into a self-stabilizing one. Our contributions are: (1) a formal definition of the concept of one program being a self-stabilizing extension of another; (2) a characterization of what properties may hold in such extensions; (3) a demonstration of the possibility of mechanically creating such extensions. The computational model used is that of an asynchronous distributed message-passing system whose communication topology is an arbitrary graph. We contrast the difficulties of self-stabilization in this model with those of the more common shared-memory models.

We present a formal proof method for distributed programs. The semantics used to justify the proof method explicitly identifies equivalence classes of execution sequences which are equivalent up to permuting commutative operations. Each equivalence class is called an interleaving set or a run. The proof rules allow concluding the correctness of certain classes of properties for all execution sequences, even though such properties are demonstrated directly only for a subset of the sequences. The subset used must include a representative sequence from each interleaving set, and the proof rules, when applicable, guarantee that this is the case. By choosing a subset with appropriate sequences, simpler intermediate assertions can be used than in previous formal approaches. The method employs proof lattices, and is expressed using the temporal logic ISTL.

The relations among various languages and models for distributed computation and various possible definitions of fairness are considered. Natural semantic criteria are presented which an acceptable notion of fairness should satisfy. These are then used to demonstrate differences among the basic models, the added power of the fairness notion, and the sensitivity of the fairness notion to irrelevant semantic interleavings of independent operations. These results are used to show that from the considerable variety of commonly used possibilities, only strong process fairness is appropriate for CSP if these criteria are adopted. We also show that under these criteria, none of the commonly used notions of fairness are fully acceptable for a model with an n-way synchronization mechanism. The notion of fairness most often mentioned for Ada is shown to be fully acceptable. For a model with nonblocking send operations, some variants of common fairness definitions are appraised, and two are shown to satisfy the suggested criteria.