paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Asynchronous Distributed Execution Of Fixpoint-Based Computational Fields

基于不动点的计算场的异步分布式执行
LMCS vol.Volume 13, Issue 12017匹配度 2/10 · 论文研究分布式聚合编程中基于不动点的形式语义与收敛性,虽涉及形式化和工程实现,但未涉及静态分析、LLM/Agent、浮点程序分析或贝叶斯程序分析,与用户核心研究方向关联很弱。引用 41 inbox
Alberto Lluch Lafuente, Michele Loreti, Ugo Montanari
dblp: 2026-09-10crossref: 2026-09-10arxiv: 2026-09-10

AI 速览

一句话:提出 SMuC 演算及分布式实现,证明公平异步与节点重初始化下不动点计算收敛。

论文面向动态分布式系统中的协调问题,关注空间分布、局部交互且可传播的计算场;这类计算场是聚合编程的关键,适用于物联网中节点低开销加入与离开的场景。作者用图状场表示空间拓扑,节点与边带属性,并提出 SMuC 演算,以类 μ 演算的模态公式描述如何组合邻居节点值来更新当前节点。不动点运算既可视为全局递归定义,也可看作局部异步收敛的传播过程。实现上,先将 SMuC 程序映射为范式纯迭代程序,再转换为分布式程序。关键结果证明在公平异步及节点重初始化下不动点计算收敛,前者允许节点以不同速度推进,后者提供对特定故障的鲁棒性。最后通过灾难恢复案例与原型模拟器评估恢复策略性能。

问题
如何为空间分布式、局部交互的计算场提供支持节点动态加入与离开的协调机制,并保证异步执行下不动点计算可靠收敛。
方法
提出 SMuC 演算,用类 μ 演算模态公式组合邻居值更新当前节点,并把程序先映射为范式纯迭代程序,再转换为分布式程序。
评估
通过灾难恢复案例在原型模拟器中评估恢复策略性能,并证明公平异步与节点重初始化下不动点计算具有收敛性和故障鲁棒性。
原文摘要(Abstract)

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

BibTeX
@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}
}