Actor languages such as Erlang and Elixir are widely used for implementing scalable and reliable distributed applications, but the informally-specified nature of actor communication patterns leaves systems vulnerable to costly errors such as communication mismatches and deadlocks. Multiparty session types (MPSTs) rule out communication errors early in the development process, but until now, the many-sender, single-receiver nature of actor communication has made it difficult for actor languages to benefit from session types. This paper introduces Maty, the first actor language design supporting both static multiparty session typing and the full power of actors taking part in multiple sessions. Maty therefore combines the error prevention mechanism of session types with the scalability and fault tolerance of actor languages. Our main insight is to enforce session typing through a flow-sensitive effect system, combined with an event-driven programming style and first-class message handlers. Using MPSTs allows us to guarantee communication safety: a process will never send or receive an unexpected message, nor will a session get stuck because an actor is waiting for a message that will never be sent. We extend Maty to support Erlang-style supervision and cascading failure, and show that this preserves Maty's strong metatheory. We implement Maty in Scala using an API generation approach, and demonstrate the expressiveness of our model by implementing a representative sample of the widely-used Savina actor benchmark suite; an industry-supplied factory scenario; and a chat server.


翻译:诸如Erlang和Elixir等参与者语言被广泛用于实现可扩展且可靠的分布式应用,但参与者通信模式缺乏形式化规范的本质使得系统容易遭受通信失配和死锁等代价高昂的错误。多参与者会话类型(MPSTs)能在开发早期排除通信错误,然而迄今为止,参与者通信所具有的多发送者、单接收者特性使得参与者语言难以受益于会话类型。本文提出Maty——首个同时支持静态多参与者会话类型和参与者参与多重会话完整能力的参与者语言设计。Maty因此将会话类型的错误预防机制与参与者语言的可扩展性和容错性相结合。我们的核心洞见在于通过流敏感效应系统,结合事件驱动编程风格和一等消息处理器来强制执行会话类型。采用MPSTs使我们能够保证通信安全性:进程永远不会发送或接收意外消息,会话也不会因参与者等待永远不会发送的消息而陷入停滞。我们将Maty扩展至支持Erlang风格的监督和级联故障,并证明这保持了Maty强大的元理论。我们在Scala中使用API生成方法实现了Maty,并通过实现广泛使用的Savina参与者基准测试套件的代表性示例、工业提供的工厂场景以及聊天服务器,展示了我们模型的表达能力。

0
下载
关闭预览

相关内容

人们为了让计算机解决各种棘手的问题,使用编程语言 编写程序代码并通过计算机运算得到最终结果的过程。
综述:面向移动端大语言模型的隐私与安全
专知会员服务
19+阅读 · 2025年9月7日
【新书】大规模语言模型的隐私与安全,
专知会员服务
29+阅读 · 2024年12月4日
大型语言模型对齐技术综述:RLHF、RLAIF、PPO、DPO 等
专知会员服务
55+阅读 · 2024年7月24日
通信网络中大型语言模型的后门攻击的综述
专知会员服务
30+阅读 · 2023年9月5日
对话系统近期进展
专知
37+阅读 · 2019年3月23日
知识在检索式对话系统的应用
微信AI
32+阅读 · 2018年9月20日
最新人机对话系统简略综述
专知
26+阅读 · 2018年3月10日
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
4+阅读 · 2014年12月31日
VIP会员
最新内容
美国从乌克兰无人机战争中学习经验
专知会员服务
6+阅读 · 6月21日
ICML 2026 | 面向视觉语言模型的语义鲁棒性认证
专知会员服务
2+阅读 · 6月21日
学习数据的几何:形状空间分析数学综述
专知会员服务
9+阅读 · 6月17日
定向能反无人机系统最新发展动态
专知会员服务
11+阅读 · 6月17日
相关VIP内容
综述:面向移动端大语言模型的隐私与安全
专知会员服务
19+阅读 · 2025年9月7日
【新书】大规模语言模型的隐私与安全,
专知会员服务
29+阅读 · 2024年12月4日
大型语言模型对齐技术综述:RLHF、RLAIF、PPO、DPO 等
专知会员服务
55+阅读 · 2024年7月24日
通信网络中大型语言模型的后门攻击的综述
专知会员服务
30+阅读 · 2023年9月5日
相关基金
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
4+阅读 · 2014年12月31日
Top
微信扫码咨询专知VIP会员