Modular Proof of Correctness for a Network Synchro nizer. 2nd Intcrnationai lvorkshop on Distribu:cd Algorithms

Abstract: In this paper we offer a formal, rigorous proof of the correctness of Awerbuch's algorithm for network synchronization. We specify both the algorithm and the correctness con-dition using the I/O automaton model, which has previously been used to describe and verify algorithms for concurrency control and resource allocation. We show that the model is also a powerful tool for reasoning about distributed graph algorithms. Our proof of correctness follows closely the intuitive arguments made by the designer of the algorithm by exploiting the model's natural support for such important design techniques as stepwise refinement and modularity. In particular, since the algorithm uses simpler algorithms for synchronization within and between 'clusters ' of nodes, our proof can import as lemmas the correctness of these simpler algorithms. 1 Overv iew 1.1 Verification methods and models As computer science has matured asa discipline, its activity has broadened from writing programs to include reasoning about those programs: proving their correctness and efficiency, and proving bounds on the performance of any program that accomplishes the same task. Recently distributed computing has begun to broaden in this way (albeit a decade or two later than the part of computer science concerned with sequential, uniproeessor algorithms). There are several reasons why particular care is necessary to prove the correctness of algorithms when the algorithm