一句话:提出 SMuC 演算及分布式实现,证明公平异步与节点重初始化下不动点计算收敛。
论文面向动态分布式系统中的协调问题,关注空间分布、局部交互且可传播的计算场;这类计算场是聚合编程的关键,适用于物联网中节点低开销加入与离开的场景。作者用图状场表示空间拓扑,节点与边带属性,并提出 SMuC 演算,以类 μ 演算的模态公式描述如何组合邻居节点值来更新当前节点。不动点运算既可视为全局递归定义,也可看作局部异步收敛的传播过程。实现上,先将 SMuC 程序映射为范式纯迭代程序,再转换为分布式程序。关键结果证明在公平异步及节点重初始化下不动点计算收敛,前者允许节点以不同速度推进,后者提供对特定故障的鲁棒性。最后通过灾难恢复案例与原型模拟器评估恢复策略性能。
Coordination is essential for dynamic distributed systems whose components exhibit interactive and autonomous behaviors. Spatially distributed, locally interacting, propagating computational fields are particularly appealing for allowing components to join and leave with little or no overhead. Computational fields are a key ingredient of aggregate programming, a promising software engineering methodology particularly relevant for the Internet of Things. In our approach, space topology is represented by a fixed graph-shaped field, namely a network with attributes on both nodes and arcs, where arcs represent interaction capabilities between nodes. We propose a SMuC calculus where mu-calculus- like modal formulas represent how the values stored in neighbor nodes should be combined to update the present node. Fixpoint operations can be understood globally as recursive definitions, or locally as asynchronous converging propagation processes. We present a distributed implementation of our calculus. The translation is first done mapping SMuC programs into normal form, purely iterative programs and then into distributed programs. Some key results are presented that show convergence of fixpoint computations under fair asynchrony and under reinitialization of nodes. The first result allows nodes to proceed at different speeds, while the second one provides robustness against certain kinds of failure. We illustrate our approach with a case study based on a disaster recovery scenario, implemented in a prototype simulator that we use to evaluate the performance of a recovery strategy.
DOI 原文 · arXiv · PDF(开放获取) · DBLP
@article{Lluch-LafuenteL16,
title = {Asynchronous Distributed Execution Of Fixpoint-Based Computational Fields},
author = {Alberto Lluch Lafuente and Michele Loreti and Ugo Montanari},
journal = {Logical Methods in Computer Science},
volume = {Volume 13, Issue 1},
year = {2017},
doi = {10.23638/lmcs-13(1:13)2017}
}