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.
