paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Multiparty Session Actors

多参与方会话 Actor
LMCS vol.Volume 13, Issue 12017匹配度 2/10 · 论文属于多参与方会话类型与 Actor 模型的运行时通信安全验证,虽涉及形式化方法与程序语言,但未涉及 LLM/Agentic 程序、静态分析、浮点程序分析或贝叶斯程序分析等用户核心方向。引用 10 inbox
Rumyana Neykova, Nobuko Yoshida
crossref: 2026-09-10

AI 速览

一句话:将多参与方会话类型引入 Actor 模型,通过角色与协议邮箱在 Python 中实现运行时通信安全验证。

Actor 程序缺乏合适的协议描述语言来协调通信,难以保证消息交互安全。本文研究多参与方会话类型(MPST)对 Actor 程序验证的适用性,通过引入 Actor 角色与协议邮箱等最小扩展,将会话集成进 Actor 模型;框架使用基于 MPST 的协议描述语言 Scribble,并支持 Actor 以类似实现多个接口的方式承担多个角色,实现单个 Actor 内的协作并发。作者在 Python 中设计并实现会话 Actor 库及其运行时验证机制,以保证参与实体的通信安全;通过 Actor 基准测试集中的 12 个例子评估适用性,基准结果显示运行时检查开销可忽略。

问题
Actor 编程中如何用合适的协议描述语言协调消息传递并验证通信安全,是 Actor 社区长期存在的问题。
方法
将多参与方会话类型协议引入 Actor 模型,增加 Actor 角色和协议邮箱,基于 Scribble 设计支持多角色的 Actor 编程模型,并在 Python 中实现带运行时验证的会话 Actor 库。
评估
在 12 个 Actor 基准例子中评估框架适用性,并通过基准测试表明运行时检查带来的开销可忽略。
原文摘要(Abstract)

Actor coordination armoured with a suitable protocol description language has been a pressing problem in the actors community. We study the applicability of multiparty session type (MPST) protocols for verification of actor programs. We incorporate sessions to actors by introducing minimum additions to the model such as the notion of actor roles and protocol mailboxes. The framework uses Scribble, which is a protocol description language based on multiparty session types. Our programming model supports actor-like syntax and runtime verification mechanism guaranteeing communication safety of the participating entities. An actor can implement multiple roles in a similar way as an object can implement multiple interfaces. Multiple roles allow for cooperative inter-concurrency in a single actor. We demonstrate our framework by designing and implementing a session actor library in Python and its runtime verification mechanism. Benchmark results demonstrate that the runtime checks induce negligible overhead. We evaluate the applicability of our verification framework to specify actor interactions by implementing twelve examples from an actor benchmark suit.

链接与引用

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

BibTeX
@article{paperbot194,
  title = {Multiparty Session Actors},
  author = {Rumyana Neykova and Nobuko Yoshida},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 13, Issue 1},
  year = {2017},
  doi = {10.23638/lmcs-13(1:17)2017}
}