MAG$pi$: 失败易发通信的类型
摘要：多方会话类型（MPST）是一种用于通信为中心的系统的类型系统，可以保证通信的安全性、无死锁和协议的合规性。已经有一些研究对故障进行建模并引入了容错技术。然而，这些研究通常对底层网络做出假设，例如基于TCP的通信，其中消息得到了保证；或者采用集中式可靠节点和一种临时的可靠性概念；或者只解决一种故障，比如节点崩溃故障。在本文中，我们开发了MAG$pi$，一种多方、异步和广义的$pi$-演算。它是第一种同时适应以下几个方面的语言和类型系统：（i）最广泛范围的非拜占庭故障，包括消息丢失、延迟和重排序；节点崩溃故障和链路故障；以及网络分区；（ii）一种新颖且最普遍的可靠性概念，考虑到每个参与者在协议中的观点；（iii）从最低UDP-based网络编程到基于TCP的应用层的一系列网络假设。我们证明了主题约简和会话保真度；过程属性（无死锁、终止等）；故障处理的安全性和可靠性的遵守。
作者：Matthew Alan Le Brun and Ornela Dardha
论文ID：2301.10827
分类：Programming Languages
分类简称：cs.PL
提交时间：2023-01-27