Lattice-Structured Proof Technique Applied to a Minimum Spanning Tree Algorithm

摘要

Highly-optimized concurrent algorithms are often hard to prove correct because they have no natural decomposition into separately provable parts. This paper presents a proof technique for the modular verification of such non-modular algorithms. It generalizes existing verification techniques based on a totally-ordered hierarchy of refinements to allow a partially-ordered hierarchy-that is, a lattice of different views of the algorithm. The technique is applied to the well-known distributed minimum spanning tree algorithm of Gallager, Humblet and Spira, which was until recently lacked a rigorous proof. Keywords: Distributed algorithms, Verification, Modularity, Partially ordered refinements, Liveness proofs, Minimum spanning tree. (jhd)