A Lattice-structured Proof Technique Applied to a Minimum Spanning Tree Algorithm
Author(s)
Welch, Jennifer Lundelius; Lamport, Leslie; Lynch, Nancy A.![Thumbnail](/bitstream/handle/1721.1/149143/MIT-LCS-TM-361.pdf.jpg?sequence=3&isAllowed=y)
DownloadMIT-LCS-TM-361.pdf (62.36Mb)
Metadata
Show full item recordAbstract
Higly-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 has until recently lacked a rigorous proof.
Date issued
1988-06Series/Report no.
MIT-LCS-TM-361