Skip to Main content Skip to Navigation
Journal articles

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

Abstract : In distributed computing, multiple processes interact to solve a problem together. The main model of interaction is the message-passing model, where processes communicate by exchanging messages. Nevertheless, there are several models varying along important dimensions: degree of synchrony, kinds of faults, number of faults.. . This variety is compounded by the lack of a general formalism in which to abstract these models, for translating results from one to the other. One way to bring order to these models is to constrain them further, to communicate in 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, where the round is the one of the receiver). 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 into 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 examples of delivered predicates, and an approach to derive more. It uses the intuition that complex models are a composition of simpler models. We thus define operations like union, succession or repetition that make it easier to derive complex delivered predicates from simple ones while retaining expressivity. For the second part, we formalize and study strategies for when to change rounds. 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.
Complete list of metadata

https://hal.archives-ouvertes.fr/hal-03352272
Contributor : Philippe Queinnec Connect in order to contact the contributor
Submitted on : Thursday, September 23, 2021 - 9:39:54 AM
Last modification on : Tuesday, October 19, 2021 - 2:23:31 PM

File

article-published.pdf
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Citation

Adam Shimi, Aurélie Hurault, Philippe Quéinnec. Characterization and Derivation of Heard-Of Predicates for Asynchronous Message-Passing Models. Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2021, 17 (3), pp.26:1 - 26:43. ⟨10.46298/lmcs-17(3:26)2021⟩. ⟨hal-03352272⟩

Share

Metrics

Record views

61

Files downloads

35