paperbot · PL 论文追踪

全部论文 待读 收藏

P2 A Scalable Algorithm for Decentralized Actor Termination Detection

可扩展的去中心化 Actor 终止检测算法
LMCS vol.Volume 18, Issue 12022匹配度 2/10 · 该论文研究分布式 actor 系统中的去中心化终止检测与垃圾回收,属于运行时/分布式系统方向;与用户关注的静态分析、LLM/Agent 交叉、浮点程序分析、贝叶斯程序分析均无直接关联,仅在形式化安全/活性证明上与 PL 方法有微弱联系。引用 5 inbox
Dan Plyukhin, Gul Agha
crossref: 2026-09-10

AI 速览

一句话:提出 DRL:基于异步本地快照与消息传递的去中心化 actor 终止检测算法,支持垃圾回收并容忍网络分区。

在 actor 系统中,自动垃圾回收不能简单依赖根可达性:不可达 actor 仍可能向可达 actor 发送消息,因此需判定其已终止(不再处理消息且未来不能再收消息)。已有终止检测算法依赖因果消息投递或非本地变更监控等协调机制,损害并发性且分布式开销高。本文提出延迟引用列表(DRL):基于异步本地快照与 actor 间消息传递,实现去中心化终止检测,并能容忍瞬时网络分区。论文给出 DRL 的形式化描述,证明安全性(被识别为垃圾的 actor 确已终止)与活性(在合理假设下,所有已终止 actor 最终会被识别)。

问题
在 actor 框架中如何安全地判定 actor 已终止,以便进行垃圾回收;根可达性不足,已有算法需全局协调而损害并发。
方法
提出 DRL(延迟引用列表),利用异步本地快照和 actor 间消息传递进行去中心化终止检测,支持网络分区容忍。
评估
通过形式化描述与安全性/活性证明进行评估:识别为垃圾者确已终止,合理假设下终止者最终被识别。
原文摘要(Abstract)

Automatic garbage collection (GC) prevents certain kinds of bugs and reduces programming overhead. GC techniques for sequential programs are based on reachability analysis. However, testing reachability from a root set is inadequate for determining whether an actor is garbage: Observe that an unreachable actor may send a message to a reachable actor. Instead, it is sufficient to check termination (sometimes also called quiescence): an actor is terminated if it is not currently processing a message and cannot receive a message in the future. Moreover, many actor frameworks provide all actors with access to file I/O or external storage; without inspecting an actor's internal code, it is necessary to check that the actor has terminated to ensure that it may be garbage collected in these frameworks. Previous algorithms to detect actor garbage require coordination mechanisms such as causal message delivery or nonlocal monitoring of actors for mutation. Such coordination mechanisms adversely affect concurrency and are therefore expensive in distributed systems. We present a low-overhead deferred reference listing technique (called DRL) for termination detection in actor systems. DRL is based on asynchronous local snapshots and message-passing between actors. This enables a decentralized implementation and transient network partition tolerance. The paper provides a formal description of DRL, shows that all actors identified as garbage have indeed terminated (safety), and that all terminated actors--under certain reasonable assumptions--will eventually be identified (liveness).

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@article{paperbot1715,
  title = {A Scalable Algorithm for Decentralized Actor Termination Detection},
  author = {Dan Plyukhin and Gul Agha},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 18, Issue 1},
  year = {2022},
  doi = {10.46298/lmcs-18(1:39)2022}
}