Characterization and Derivation of Heard-Of Predicates for Asynchronous Message-Passing Models
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...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2021-09-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/6929/pdf |
| _version_ | 1797268521270378496 |
|---|---|
| author | Adam Shimi Aurélie Hurault Philippe Queinnec |
| author_facet | Adam Shimi Aurélie Hurault Philippe Queinnec |
| author_sort | Adam Shimi |
| collection | DOAJ |
| description | 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. One way to bring order is to
constrain these models 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. Yet, it is not easy to define the
predicate that 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 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 are 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
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. |
| first_indexed | 2024-04-25T01:33:48Z |
| format | Article |
| id | doaj.art-c7a6f4b33ebf4986b909b817c92a162e |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:33:48Z |
| publishDate | 2021-09-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-c7a6f4b33ebf4986b909b817c92a162e2024-03-08T10:35:15ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742021-09-01Volume 17, Issue 310.46298/lmcs-17(3:26)20216929Characterization and Derivation of Heard-Of Predicates for Asynchronous Message-Passing ModelsAdam ShimiAurélie HuraultPhilippe QueinnecIn 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. One way to bring order is to constrain these models 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. Yet, it is not easy to define the predicate that 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 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 are 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 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.https://lmcs.episciences.org/6929/pdfcomputer science - distributed, parallel, and cluster computing |
| spellingShingle | Adam Shimi Aurélie Hurault Philippe Queinnec Characterization and Derivation of Heard-Of Predicates for Asynchronous Message-Passing Models Logical Methods in Computer Science computer science - distributed, parallel, and cluster computing |
| title | Characterization and Derivation of Heard-Of Predicates for Asynchronous Message-Passing Models |
| title_full | Characterization and Derivation of Heard-Of Predicates for Asynchronous Message-Passing Models |
| title_fullStr | Characterization and Derivation of Heard-Of Predicates for Asynchronous Message-Passing Models |
| title_full_unstemmed | Characterization and Derivation of Heard-Of Predicates for Asynchronous Message-Passing Models |
| title_short | Characterization and Derivation of Heard-Of Predicates for Asynchronous Message-Passing Models |
| title_sort | characterization and derivation of heard of predicates for asynchronous message passing models |
| topic | computer science - distributed, parallel, and cluster computing |
| url | https://lmcs.episciences.org/6929/pdf |
| work_keys_str_mv | AT adamshimi characterizationandderivationofheardofpredicatesforasynchronousmessagepassingmodels AT aureliehurault characterizationandderivationofheardofpredicatesforasynchronousmessagepassingmodels AT philippequeinnec characterizationandderivationofheardofpredicatesforasynchronousmessagepassingmodels |