Facilitating the Verification of Diffusing Computations and Their Applications

Abstract

We study a class of distributed algorithms, generally known by the name of diffusing computa- tions, that play an important role in all kinds distributed and/or database applications to perform tasks like termination detection, leader election, or propagation of information with feedback. We construct a highly parameterized abstract algorithm and shown that many existing algorithms and their applications can be obtained from this abstract algorithm by instantiating the parameters appropriately and/or refining some of its actions. Subsequently, we show that this use of param- eterization and re-usability of notation and proof leads to a reduction of the effort and cost of developing and verifying distributed diffusing computations. More specific, we show that proving the correctness of any application now boils down to verifying an application-specific safety prop- erty and reusing the termination and safety proofs of the underlying abstract algorithm.