分布式Actor系统的可扩展终止检测
计算机科学中的逻辑
2020-07-24 v2
摘要
自动垃圾回收（GC）可防止某些类型的错误并降低编程开销。顺序程序的GC技术基于可达性分析。然而，从根集测试可达性不足以判定一个actor是否为垃圾，因为不可达的actor可能向可达的actor发送消息。相反，检查终止（有时也称为 quiescence）是充分的：如果一个actor当前未处理消息且未来不可能接收到消息，则它是终止的。此外，许多actor框架为所有actor提供文件I/O或外部存储的访问；在不检查actor内部代码的情况下，有必要检查该actor已终止，以确保其可在这些框架中被垃圾回收。先前的actor垃圾检测算法需要协调机制，例如因果消息传递或对actor变异的非本地监控。此类协调机制对并发产生不利影响，因此在分布式系统中代价高昂。我们提出一种低开销的引用列表技术（称为DRL），用于actor系统中的终止检测。DRL基于异步本地快照和actor间的消息传递。这实现了去中心化实现和瞬态网络分区容忍。本文给出了DRL的形式化描述，证明了所有被识别为垃圾的actor确实已终止（安全性），以及在特定合理假设下所有已终止的actor最终都将被识别（活性）。
引用
@article{arxiv.2007.10553,
title = {Scalable Termination Detection for Distributed Actor Systems},
author = {Dan Plyukhin and Gul Agha},
journal= {arXiv preprint arXiv:2007.10553},
year = {2020}
}
备注
23 pages, 7 figures. To appear in the proceedings of CONCUR 2020. Version 2: Fixed TeX error that omitted predicates in the third line of the Send rule: Actor $A$ must have active refobs $x$ and $y_1 \dots y_n$