Parameterized synthesis of self-stabilizing protocols in symmetric networks
Parameterized synthesis of self-stabilizing protocols in symmetric networks
复制标题
对称网络自稳定协议的参数化综合
DOI：
--
复制
发表时间：
2019
期刊：
影响因子：
0.6
通讯作者：
Borzoo Bonakdarpour
中科院分区：
文献类型：
--
作者：
Nahal Mirzaie;Fathiyeh Faghih;Swen Jacobs;Borzoo Bonakdarpour
分布式系统中的自稳定是一种在发生瞬时故障或初始化错误时保证收敛到一组合法状态而无需外部干预的技术。最近，有一个激增的努力，在设计技术的自动合成的自稳定算法，是正确的建设。然而，这些技术中的大多数都不是参数化的，这意味着它们只能为固定和预定数量的过程合成解决方案。在本文中，我们报告了一个突破性的参数化综合的自稳定算法的对称网络，包括环，线，网格和环面。首先，我们开发了一些截断点，保证（1）在合法状态下的闭包，以及（2）在合法状态之外的无死锁。我们还发展了一个充分条件的收敛自稳定系统。由于我们的一些截止值随着进程的局部状态空间的大小而增长，因此合成过程的可扩展性仍然是一个问题。我们解决这个问题，通过引入一种新的SMT为基础的技术，反例指导合成的自稳定算法在对称网络。我们已经完全实现了我们的技术，并成功地合成解决方案的最大匹配，三着色，和最大独立集的环和线拓扑结构的问题。
Self-stabilization in distributed systems is a technique to guarantee convergence to a set of legitimate states without external intervention when a transient fault or bad initialization occurs. Recently, there has been a surge of efforts in designing techniques for automated synthesis of self-stabilizing algorithms that are correct by construction. Most of these techniques, however, are not parameterized, meaning that they can only synthesize a solution for a fixed and predetermined number of processes. In this paper, we report a breakthrough in parameterized synthesis of self-stabilizing algorithms in symmetric networks, including ring, line, mesh, and torus. First, we develop cutoffs that guarantee (1) closure in legitimate states, and (2) deadlock-freedom outside the legitimate states. We also develop a sufficient condition for convergence in self-stabilizing systems. Since some of our cutoffs grow with the size of the local state space of processes, scalability of the synthesis procedure is still a problem. We address this problem by introducing a novel SMT-based technique for counterexample-guided synthesis of self-stabilizing algorithms in symmetric networks. We have fully implemented our technique and successfully synthesized solutions to maximal matching, three coloring, and maximal independent set problems for ring and line topologies.