异步消息传递模型中"Heard-Of"谓词的表征和推导
摘要：在分布式计算中，多个进程相互交互以共同解决问题。主要的交互模型是消息传递模型，其中进程通过交换消息进行通信。然而，存在着多个在重要维度上变化的模型：同步程度、故障类型、故障数量等。这种多样性又加剧了缺乏一个通用形式来抽象这些模型的问题。一种带来秩序的方式是将这些模型约束为以轮次进行通信。这就是所谓的“Heard-Of”模型的设置，通过对轮次发送和及时接收的消息进行谓词判断，捕捉了许多模型。然而，对于捕捉给定操作模型的谓词定义并不容易。对于异步情况来说，问题变得更加困难，因为无界消息延迟意味着轮次的实现必须依赖模型的细节。本文展示了使用“Heard-Of”谓词对异步模型进行表征的意义。这种表征依赖于“已接收”谓词，它是非正式操作模型和“Heard-Of”谓词之间的中间抽象。我们的方法将问题分为两个步骤：首先提取捕捉非正式模型的“已接收”模型，然后表征由该“已接收”模型生成的“Heard-Of”谓词。对于第一部分，我们提供了“已接收”谓词的示例，并提供了更多导出的方法。它利用了复杂模型是简单模型的组合的直觉。我们定义了像联合、后继或重复等操作，使得从简单谓词派生复杂的“已接收”谓词更加容易，并且保持表达能力。对于第二部分，我们形式化并研究了何时改变轮次的策略。直观上，一个模型的特征化谓词是由等待尽可能多的消息但又不会永远阻塞的策略生成的谓词。
作者：Adam Shimi, Aur''elie Hurault, Philippe Queinnec
论文ID：2011.12879
分类：Distributed, Parallel, and Cluster Computing
分类简称：cs.DC
提交时间：2023-06-22