Characterization and Derivation of Heard-Of Predicates for Asynchronous Message-Passing Models

Message-passing models of distributed computing vary along numerous dimensions: degree of synchrony, kind of faults, number of faults... One way to deal with this variety is by restricting communication to rounds. This is the setting of the Heard-Of model, which captures many models through predicates on the messages sent in a round and received on time, at this round or before on the receivers. Yet, it is not easy to define the predicate that best captures a given operational model. The question is even harder for the asynchronous case, as unbounded message delay means the implementation of rounds must depend on details of the model. This paper shows that characterising asynchronous models by heard-of predicates is indeed meaningful. This characterization relies on the introduction of delivered predicates, an intermediate abstraction between the informal operational model and the heard-Of predicates. Our approach splits the problem in two steps: first extract the delivered model capturing the informal model, and then characterize the heard-of predicates that can be generated by this delivered model. For the first part, we provide both examples of delivered predicates, and an approach to derive more. It uses the intuition that complex models are a combination of simpler models. We thus define operations like union, succession or repetition that make it easier to build complex delivered predicates from simple ones while retaining expressivity. For the second part, we formalize and study strategies for when to change round. Intuitively, the characterizing predicate of a model is the one generated by a strategy that waits for as much messages as possible, without blocking forever.