Document Type

Technical Report

Publication Date

1992

Filename

WUCS-92-10.pdf

Technical Report Number

WUCS-92-10

Abstract

We present a new proof methodology that uses dynamic process creation to capture the structure of recutsive distributed algorithms> Each recursive invocation of a distributed algorithm is modeled as a separate process, encouraging local reasoning about the individual recursive invocations and making explicit the communicatino that takes place among the concurrently executing invocations. Our methodology involves the construction of hierarchical correctness proofs in which the state of each individual call in a refined algorithm is mapped to the state of a corresponding call in a simpler or more abstract algorithm. Algorithm optimizations that result in the creation of fewer recursive calls are treated cleanly in the hierarchical proofs with the use of a hiding operator that makes explicit exactly which recursive calls of the abstract algorithms are optimized away in the refined algorithm. The proof methodology is presented and illustrated in the context of an extended example, the cloture voting Byzantine agreement algorithm of Berman, Garay and Perry. Dynamic process creation is used to capture the recursive structure of the cloture voting agorithm, and a complete hierarchical correctness proof for teh algorithm is given. The structure provided by dynamic process creation and the hierarchical correctness proof provides considerable insight into this rather complicated distributed algorithm.

Comments

Permanent URL: http://dx.doi.org/10.7936/K78P5XVW

Download

Share

COinS