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

Abstract

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jun 01, 1988
Accession Number
ADA198312

Entities

People

  • Jennifer L. Welch
  • Leslie Lamport
  • Nancy Lynch

Organizations

  • Massachusetts Institute of Technology

Tags

Communities of Interest

  • Materials and Manufacturing Processes

DTIC Thesaurus Topics

  • Abstracts
  • Algorithms
  • Automata
  • Classification
  • Computer Programming
  • Computer Science
  • Computers
  • Decomposition
  • Hierarchies
  • Information Processing
  • Language
  • Massachusetts
  • Programming Languages
  • Security
  • Simulations
  • Theoretical Computer Science
  • Verification

Fields of Study

  • Computer science

Readers

  • Applied Combinatorial Optimization and Logic Circuit Design.
  • Mathematical Modeling and Probability Theory.
  • Parallel and Distributed Computing.