AF: Small: A Framework For Algorithmic Design of Self-Stabilizing Network Protocols

这项研究的重点是促进自稳定（SS）网络协议的设计，其中SS协议最终从任何有问题的配置恢复到合法配置（即，收敛）并且只要没有扰动就保持在合法配置中（即，关闭）。这是一个重要的问题，因为当今的复杂分布式系统（例如，因特网）频繁地达到非法配置，这是由于出现了扰乱协议而不造成永久性损害的瞬时故障（例如，存储器中的位翻转，错误的初始化）。大多数现有的方法是基于手动创建的初始设计和事后验证的手动设计。这项研究提出了一个基于“小规模综合和普遍化”哲学的范式转变。具体而言，研究人员研究（i）SS协议的小实例的自动生成，和（ii）合成的实例到较大的protocol.In，而不是设计和验证特定问题的SS协议，这项研究提供了一个可重用的资源库的合成方法添加收敛到不稳定的协议。此外，本研究提出了三种技术，即合成收敛阶梯，截断定理和结构归纳的综合协议的小实例的推广。为了进行评估，研究人员研究了真实的世界协议和经典分布式计算问题（例如，互斥和领导选举）。调查人员还确定了复杂性标准，并将其汇编成一个公共基准。

This research focuses on facilitating the design of Self-Stabilizing (SS) network protocols, where a SS protocol eventually recovers from any troubled configuration to a legitimate configuration (i.e., convergence) and stays in legitimate configurations as long as there are no perturbations (i.e., closure). This is an important problem as today's complex distributed systems (e.g., the Internet) frequently reach illegitimate configurations due to the occurrence of the transient faults that perturb the protocols without causing permanent damage (e.g., bit flips in memory, bad initialization). Most existing methods are based on the manual creation of an initial design and after-the-fact verification of the manual design. This research presents a paradigm shift based on a philosophy of 'synthesize in small scale and generalize'. Specifically, the investigators study (i) the automatic generation of small instances of SS protocol, and (ii) the generalization of the synthesized instances to larger protocols.Instead of designing and verifying problem-specific SS protocols, this research provides a reusable repository of synthesis methods for the addition of convergence to nonstabilizing protocols. Moreover, this research presents three techniques for the generalization of the small instances of the synthesized protocols, namely synthesized convergence stairs, cutoff theorems and structural induction. For evaluation, the investigators study the automated design of convergence for real world protocols and classic distributed computing problems (e.g., mutual exclusion and leader election) under different topologies and distinct fairness assumptions. The investigators also identify complexity criteria and compile them in a public benchmark.