一句话：证明可用 Heard-Of 谓词刻画异步消息传递模型，并给出经 delivered 谓词的两步推导框架与轮次切换策略。
分布式计算中的消息传递模型在同步、故障等方面差异大且缺乏统一形式化。Heard-Of 模型用轮次内发送与按时接收消息的谓词统一许多模型，但为给定操作模型定义相应谓词，尤其异步情形因消息延迟无界而困难。本文表明用 Heard-Of 谓词刻画异步模型有意义：引入 delivered 谓词作为中间抽象，先提取 delivered 模型，再刻画其生成的 Heard-Of 谓词。作者给出 delivered 谓词实例，并定义并集、接续与重复等组合操作，以从简单谓词推导复杂谓词并保持表达力。最后形式化并研究轮次切换策略，指出刻画谓词可由尽可能等待消息且不永久阻塞的策略生成。
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.
@article{paperbot1278,
title = {Characterization and Derivation of Heard-Of Predicates for Asynchronous Message-Passing Models},
author = {Adam Shimi and Aurélie Hurault and Philippe Queinnec},
journal = {Logical Methods in Computer Science},
volume = {Volume 17, Issue 3},
year = {2021},
doi = {10.46298/lmcs-17(3:26)2021}
}