טכניון מכון טכנולוגי לישראל
הטכניון מכון טכנולוגי לישראל - בית הספר ללימודי מוסמכים  
M.Sc Thesis
M.Sc StudentShimony Benny
SubjectA New Correctness Proof of Gallager, Humblet and Spira's
Minimum Spanning Tree Protocol
DepartmentDepartment of Electrical Engineering
Supervisor Professor Yoram Moses


Abstract

A new correctness proof of the celebrated distributed Minimum Spanning Tree protocol of Gallager, Humblet and Spira (GHS) is presented. The protocol is fundamental and is considered by many to have opened a new era in the theory of network algorithms. While the protocol itself is very elegant and the arguments for why the protocol should be correct are fairly convincing, a rigorous correctness proof of the GHS protocol turns out to be a considerable challenge. The proof presented in this thesis uses an invariant assertion approach, supported by a new decomposition of the algorithm into abstraction levels. In particular, the new intermediate-level abstraction, we call by as the rainbow-construction, refines an abstraction, typically used to describe GHS, by the assignment of colors to nodes. The construction mimics essential aspects of the search process in the GHS algorithm, while completely abstracting details of communication and local variables of processes. Thus, in the protocol level analysis, rather than using a full refinement proof, an augmented version of the GHS algorithm is defined, in which auxiliary rainbow steps are inserted at specific points in the protocol. The state of the rainbow construction computation (also called - painted forest), is appended to protocol configuration as an auxiliary data structure that is used as a “legend” or “road map” to fix the global context of protocol configurations. The proof presented demonstrates that a refinement decomposition can be a powerful tool for analysis, that can be carried over to other problems with a rich dynamic structure.