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