Self-Stabilization by Local Checking and Correction by George Varghese B.Tech, Electrical Engineering Indian Institute of Technology, Bombay (1981) M.S., Computer Studies North Carolina State University (1983) Submitted to the Department of Electrical Engineering and Computer Science in partial ful(cid:12)llment of the requirements for the degree of Doctor of Philosophy at the MASSACHUSETTS INSTITUTE OF TECHNOLOGY October 1992 (cid:13)c Massachusetts Institute of Technology 1992 :::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Signature of Author Department of Electrical Engineering and Computer Science October 20, 1992 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Certi(cid:12)ed by Baruch Awerbuch Associate Professor Thesis Supervisor ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Certi(cid:12)ed by Nancy A. Lynch Professor Thesis Co-supervisor :::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: Accepted by Campbell L. Searle Chairman, Departmental Committee on Graduate Students Self-Stabilization by Local Checking and Correction by George Varghese Submitted to the Department of Electrical Engineering and Computer Science on October 20, 1992, in partial ful(cid:12)llment of the requirements for the degree of Doctor of Philosophy Abstract A self-stabilizing protocol is one that begins to behave correctly in bounded time, no matter what state the protocol is started in. Self-stabilization abstracts the ability of a protocol to tolerate arbitrary faults that stop. We investigate the power and applicability of local checking and correction for the design of stabilizing network protocols. Alinksubsystemisapairofneighboringnodes andthetwolinksbetweenthem. Intuitively, a protocol P is locally checkable if whenever P is in a bad state, some link subsystem is also in a bad state. A protocol P is locally correctable if P can be corrected to a good state by locally correcting link subsystems. We present four general techniques for designing stabilizing protocols. We (cid:12)rst show that every locally checkable and correctable protocol can be stabilized in time proportional to the height of an underlying partial order. Second, we show that every locally checkable protocol on a tree can be stabilized in time proportional to the height of the tree. Third, we show that everylocallycheckable protocolcanbe stabilizedintimeproportionaltothenumberofnetwork nodes. The third result showsthat we can dispense with the need for local correctabilityor the need for the underlying topology to be a tree as long as we are willing to pay a higher price in stabilization time. Fourth, we show that any deterministic synchronous protocol (cid:25) can be converted to an asynchronous, stabilizing version of (cid:25). The fourth technique is useful because there are networktasksfor which asynchronous protocolexistsbut for which no asynchronous, locally checkable solution is known. Wealsopresenttwouseful heuristics. The(cid:12)rstheuristic,thatofremovingunexpected packet transitions, can often be used to transform a protocol into a locally checkable equivalent. A number ofexistingprotocolsworkin adynamic network model where linkscan failand recover. Thesecondheuristicstatesthatlocallycheckableprotocolsfordynamicnetworkscansometimes be made locally correctable. The basic idea is to use the link failure and recovery actions of the original protocol to locally correct link subsystems. Together our techniques cover a broad range of networking tasks. We use our general techniques to construct new or improved stabilizing solutions to many speci(cid:12)c for Mutual Exclusion, Network Resets, Spanning Trees, Topology Update, Min Cost Flows etc. Many of our solutions are practical and can be applied to real networks without appreciable loss in e(cid:14)ciency. For example, the messages required for local checking can easily be piggybacked on the "keep-alive" tra(cid:14)c sent between neighbors in real networks. Our techniques also help in succinctly understanding existing stabilizing protocols. We ii de(cid:12)ne a special case of local checking called one-way checking. We show that many existing protocolsimplicitlyuse one-way checking togetherwithtwoother methods thatwe callcounter (cid:13)ushing and timer (cid:13)ushing. In the past, papers on stabilizationhave avoided message passing models of communication because of the problems caused by unbounded storage Data links. In a stabilizing setting, such links can be initialized with an unbounded number of (cid:12)ctitious packets. Thus almost any non-trivialnetworktaskisimpossibleina stabilizingsettinginwhich thelinkshaveunbounded storageand thenodes arerestrictedtobe (cid:12)nite statemachines. Weavoidthisproblembyusing the standard asynchronous message passingmodel of a computer networkexcept thateach link is what we call a Unit Storage Data Link (UDL) that can store at most one packet. Our UDL model can be implemented over real physical channels. Our UDL model also generalizes easily to a Bounded Storage Data Link which can store a constant number of packets. We introduce a new de(cid:12)nition of stabilizationin terms of the external behavior of a system. The de(cid:12)nition allowsus to de(cid:12)ne that an automatonA stabilizesto another automatonB even though A and B have di(cid:11)erent state sets. The de(cid:12)nition also allows a clean statement of a useful Modularity Theorem. This theorem allows us to prove that a large system is stabilizing by proving that each of its pieces is stabilizing. Keywords: Self-Stabilization, Fault-Tolerance, Network Protocols, Distributed Algorithms, Local Checking and Correction. Thesis Supervisor: Baruch Awerbuch Title: Associate Professor Thesis Co-supervisor: Nancy A. Lynch Title: Professor iii Acknowledgments I have been fortunate to be helped by a huge number of talented people. Basically, I have had two sets of advisors { one set from DEC where I work, and another set from MIT. I thank Radia Perlman for being my advisor at DEC. I owe so much to her. My interest in the (cid:12)eld of self-stabilization began after watching Radia design two elegant and widely used stabilizing protocols. After Radia went back to MIT to complete her doctorate, she encouraged me to do the same. She plotted my course load, provided feedback, directed my application process, cajoled, consoled, and occasionally scolded. Recently, she was selected by Data Communications Magazine as one of twenty people who have changed the (cid:12)eld of networking. But to me she is something much better, a good and loyal friend. I thank Alan Kirby of DEC for being a wonderful manager and boss. By trusting and believing in me, he has helped me to do things that I did not think I was capable of. Besides being a (cid:12)ne manager, Alan also has a great deal of technical vision. All the projects he has assigned me to work on have provided seed ideas for this thesis. I thank Baruch Awerbuch of MIT who supervised my thesis together with Nancy Lynch. Baruch is a restless visionary who is constantly conquering new areas. This thesis began with Baruch’s conviction that the so called end-to-end problem had a stabilizing solution. That problem led us toinventlocalchecking and correction. Stilllater,Baruch wasconvinced that it was \easy" to construct an e(cid:14)cient and stabilizing reset protocol. It is typical of his approach that he began with problems that other people (especially me!) considered hard. I thank Nancy Lynch of MIT for being a superb thesis supervisor and advisor. Nancy had to struggle with initial drafts of this thesis that were truly terrible. Under her guidance, the formalismgraduallyemerged. Herideaofusingaspeci(cid:12)cationofstabilizationbasedonexternal behavior has been particularly fruitful. Working with her has been a true education, as I have begun to learn a little of what scholarship and rigor means. I thank Robert Gallager of MIT for his inspiration, and his patience in reading this thesis. Hisinsistenceonclarityhasshamedmeintorewritingpartsofthethesis. Iwillalwaysremember the kindness which he, a great and brilliant man, shows to his students. I thank Mark Tuttle of DEC Cambridge Research Lab for his painstaking reading of this thesis. Time and again, Mark spotted errors and helped clean up important de(cid:12)nitions. Even iv his most critical comments were leavened with humor and encouragement. If this thesis is reasonably free of errors, it is because of the hard work of Nancy and Mark. Mark also helped me to understand the big picture; the introduction and Chapter 10 have improved because of his e(cid:11)orts. I thank Boaz Patt who worked together with Baruch and myself on many of the ideas in this thesis. I thank Boaz especially for his hard work on an initialversion of the reset protocol, and for initiating the use of an external behavior speci(cid:12)cation for the reset protocol. I owe Boaz many things, including the succinct title of this thesis. I thank the DEC Graduate Engineering Program (GEEP) for their incredible generosity in allowing me to go to MIT on full salary for two years. I especially thank Shirley Stahl and TerrySarandreaofGEEPfortheirabilitytocutthroughadministrativeprocedures andtohelp me when I needed help. I also thank Joanne Talbot at MIT for her administrative support at MIT. This thesis is dedicated to my father, who would have loved to leaf through it if he were alive; and to my mother and sister, for their patience and love. Finally, I’d like to thank God and his son Jesus, from whom I believe all good gifts come { even this wonderful set of people that it has been such a joy to live and work with. v Contents 1 Introduction 9 : : : : : : : : : : : : : : : : : : : : : : : : : : : 1.1 A Door Closing Protocol 9 : : : : : : : : : : : : : : : : 1.2 Self-Stabilization using Domain Restriction 12 : : : : : : : : : : : : : : : : : : 1.3 Self-Stabilization in Computer Networks 15 : : : : : : : : : : : : : : : : : : : : : : : : 1.4 Criticisms of Self-Stabilization 18 : : : : : : : : : : : 1.4.1 Distinction between Program Code and State 18 : : : : : : : : : : : 1.4.2 Faults that Stop versus Faults that Continue 19 : : : : : : : : : : : : : : : : : : : : : : : 1.4.3 Permitting Initial Errors 19 : : : : : 1.4.4 Periodic Message Sending in the Self-stabilization Model 19 : : : : : : : : : : : : : : : : : : : : : : 1.5 Brief History of Self-Stabilization 20 : : : : : : : : : : : : : : : : : : : 1.5.1 Re(cid:12)nements of Dijkstra’s model 21 : : : : : : : : : : : : : : : : 1.5.2 Existing solutions for Speci(cid:12)c Tasks 21 : : : : : : : : : : : : : : : : : : : : : 1.5.3 Existing General Technique 22 : : : : : : : : : : : : : : : : 1.6 Local Checking and Correction: A Preview 22 1.6.1 Example of Checking and Correcting on a Single Link Subsystem 22 : : : : : : : : : : : : : 1.6.2 Extending the Idea to a General Network 25 : : : : : : : : : : : : 1.6.3 Examples of Local Checking and Correction 26 : : : : : : : : : : : : : : : : : : : : 1.6.4 Why Local Checking is Useful 28 : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 1.7 Thesis Organization 29 1 : : : : : : : : : : 1.7.1 Basic De(cid:12)nitions and Examples: Chapters 2 - 4 30 : : : : : : : : : : 1.7.2 Local Checking and Correction: Chapters 5 - 7 31 : : : : : : 1.7.3 Local Checking and Global Correction: Chapters 8 - 9 33 : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 1.8 Reading the Thesis 34 2 The I/O Automaton Model 35 : : : : : : : : : : : : : : : : : : : : : : : : : 2.1 The I/O Automaton Model 36 : : : : : : : : : : : : : : : 2.1.1 Why use the I/O Automaton Model? 36 : : : : : : 2.1.2 Four Important Features of the I/O Automaton Model 37 : : : : : : : 2.1.3 Specifying Correctness in the I/O Automaton Model 39 : : : : : : : : : : : : : : 2.2 Formal Summary of the I/O Automaton Model 42 : : : : : : : : : : : : : : : : : : : : : : : 2.2.1 Composition and Hiding 45 : : : : : : : : : : : : : : : : : : : : : : : : : : : : 2.2.2 Useful Notation 47 : : : : : : : : : : : : : : : : : 2.2.3 Modelling Asynchronous Protocols 47 3 Stabilization: De(cid:12)nitions and Properties 49 : : : : : : : : : : : : : : 3.1 De(cid:12)nitions of Stabilization based on Executions 49 : : : : : : : : : : 3.2 De(cid:12)nitions of Stabilization based on External Behavior 52 : : : : : : : : : : : : : : : : : 3.3 Discussion on the Stabilization De(cid:12)nitions 55 : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 3.4 Proof Technique 56 : : : : : : : : : : : 3.4.1 Proving that an Automaton Solves a Problem 57 : : 3.4.2 Proving that an Automaton Stabilizes to another Automaton 59 : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 3.5 Modularity Theorem 61 : : : : : : : : : : : : : : : 3.5.1 Discussion of the Modularity Theorem 65 : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 3.6 Summary 66 2 4 Local Checking and Correction in a Shared Memory Model 69 : : : : : : : : : : : : : : : : : : : : 4.1 Modelling Shared Memory Protocols 70 : : : : : : : : : : : : : : : : : : : : : : : : : 4.2 A Reset Protocol on a Tree 70 : : : : : : : : : : : : : : : 4.3 Tree Correction for Shared Memory Systems 76 : : : : : : : : : : : : : : : : 4.3.1 Weakening the Fairness Requirement 83 : : : : : : : : : : : : : : : : : : : : : 4.4 Rediscovering Dijkstra’s Protocols 84 : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 4.5 Summary 89 5 Local Checking and Correction for Network Protocols 90 : : : : : : : : : : : : : : : : : : : : : : : : 5.1 Modelling Network Protocols 91 : : : : : : : : : : : : : : : : : : : : 5.1.1 Modelling Network Topology 92 : : : : : : : : : : : : : : : : : : : : : : 5.1.2 Modelling Network Links 93 : : : : : : : : : : : : : : : : : : : : : : 5.1.3 Modelling Network Nodes 95 : : : : : : : : : : : : : : : : : : : : : : : : : : 5.1.4 Network Automata 97 : : : : : : : : : : : : : : : : 5.2 Implementing Our Model in Real Networks 98 : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 5.3 Locality 99 : : : : : : : : : : : : : : : 5.3.1 Link Subsystems and Local Predicates 100 : : : : : : : : : : : : : : : : : : : : : : : : : : 5.3.2 Local Checkability 101 : : : : : : : : : : : : : : : : : : : : : : : : : 5.3.3 Local Correctability 102 : : : : : : : : : : : : : : : : : : : : : : : : : : 5.4 Local Correction Theorem 104 : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 5.4.1 Overview 104 : : : : : : : : : : : : : : : : : : : 5.4.2 Precise Statement of the Result 105 : : : : : : : : : : : : : : : 5.4.3 Overview of the Transformation Code 106 : : : : : 5.4.4 Constructing Augmented Automata: Formal Description 109 : : : : : : : : : : : : : : : : 5.5 Intuitive Proof of Local Correction Theorem 114 : : : : : : : : : : : : : 5.5.1 Intuition Behind Counter Based Matching 114 : : : : : : : : : : : : : : : : : : 5.5.2 Intuition Behind Local Snapshots 116 3 : : : : : : : : : : : : : : : : : : : : 5.5.3 Intuition Behind Local Resets 117 : : : : : : : : : : : : 5.5.4 Intuition Behind Local Correction Theorem 118 : : : : : : : : : : : : : : : : 5.6 Formal Proof of Local Correction Theorem 119 : : : : : : : : : : : : : : : : : : : : : : 5.6.1 Overview of Formal Proof 119 : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 5.6.2 Phases 121 : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 5.6.3 Clean Phases 123 : : : : : : : : : : : : : 5.6.4 Quiet Links: Establishing Link Predicates 128 5.6.5 Projecting Behaviors of NjQ : : : : : : : : : : : : : : : : : : : : 131 5.6.6 Tying up the Proof : : : : : : : : : : : : : : : : : : : : : : : : : : 133 5.7 Implementing Local Checking in Real Networks : : : : : : : : : : : : : : 133 5.8 Summary : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 134 6 Stabilizing Mutual Exclusion and Tree Correction 136 6.1 Overview of Token Passing Protocol : : : : : : : : : : : : : : : : : : : : 137 6.2 Speci(cid:12)cation of Token Passing Protocol : : : : : : : : : : : : : : : : : : 138 6.3 Adding Local Checking and Correction : : : : : : : : : : : : : : : : : : : 139 6.4 Removing Unexpected Packet Transitions : : : : : : : : : : : : : : : : : 145 6.5 Tree Correction Theorem : : : : : : : : : : : : : : : : : : : : : : : : : : 148 6.6 Summary : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 149 7 Stabilizing Network Reset 152 7.1 Synchronization : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 153 7.1.1 Data Link Synchronization : : : : : : : : : : : : : : : : : : : : : 153 7.1.2 Network Synchronization : : : : : : : : : : : : : : : : : : : : : : 155 7.2 Existing Solutions : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 158 7.3 Specifying the Desired Behaviors of a Reset Protocol : : : : : : : : : : : 159 7.3.1 Interface to Reset Protocol : : : : : : : : : : : : : : : : : : : : : 159 4 7.3.2 Di(cid:14)culties in Specifying the Reset Problem : : : : : : : : : : : : 161 7.3.3 Formal Speci(cid:12)cation of Reset Problem : : : : : : : : : : : : : : : 162 7.3.4 Alternative Speci(cid:12)cations of Reset Problem : : : : : : : : : : : : 168 7.4 Overview of the solution : : : : : : : : : : : : : : : : : : : : : : : : : : : 169 7.4.1 Problems with a Simple Reset Protocol : : : : : : : : : : : : : : 170 7.4.2 The basic idea behind the Reset protocol : : : : : : : : : : : : : 172 7.4.3 Overview of the Code : : : : : : : : : : : : : : : : : : : : : : : : 173 7.4.4 Example : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 178 7.5 Reset Automaton : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 180 7.6 Reset Protocol is Locally Checkable and Correctable : : : : : : : : : : : 182 7.6.1 Overview of Predicates : : : : : : : : : : : : : : : : : : : : : : : : 182 7.6.2 Provingthat the Local Predicates of the Reset Protocol are Closed185 7.6.3 Reset Protocol is Locally Correctable : : : : : : : : : : : : : : : 187 7.7 The behaviors of a reset protocol after it stabilizes : : : : : : : : : : : : 190 7.7.1 Why the Termination Lemma Works : : : : : : : : : : : : : : : : 191 7.7.2 Why behaviors of the reset automaton are timely, consistent, and causal : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 193 7.8 Local Correctability and Dynamic Network Protocols : : : : : : : : : : : 201 7.9 Summary : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 203 8 Global Correction Theorem 205 8.1 Statement of Global Correction Theorem : : : : : : : : : : : : : : : : : 206 8.2 Proof of the Global Correction Theorem : : : : : : : : : : : : : : : : : : 208 + 8.2.1 Construction of N : : : : : : : : : : : : : : : : : : : : : : : : : 208 8.2.2 All reset triggers disappear in Linear Time : : : : : : : : : : : : 209 8.2.3 All Local Predicates Hold and All Signals Stop in Linear Time : 219 8.2.4 Proof of Global Correction Theorem is Modular : : : : : : : : : 220 5