出版社：Centro Latinoamericano de Estudios en Informática
摘要：We study a class of distributed algorithms, generally known by the name of
diffusing computations, 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 parameterization 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 property and reusing the termination and safety
proofs of the underlying abstract algorithm.
