Global progress for dynamically interleaved multiparty sessions
Global progress for dynamically interleaved multiparty sessions
复制标题
DOI：
10.1017/s0960129514000188
复制
发表时间：
2016-02-01
影响因子：
0.5
通讯作者：
Padovani, Luca
中科院分区：
文献类型：
--
作者：
Coppo, Mario;Dezani-Ciancaglini, Mariangiola;Padovani, Luca
多方会话在许多参与者之间形成结构化通信单元，这些参与者遵循作为全局类型指定的通信序列。当一个进程同时参与两个或多个会话时，不同的会话可以交错，并且可以在运行时发生干扰。先前关于多方会话类型的工作忽略了会话交错，通过假设不同会话之间的不干扰和禁止委托，只在单个会话中提供有限的进度属性。除了传统的组合通信类型系统外，本文还开发了一种新的静态交互类型系统，用于动态交错和干扰的多方会议的全局进度。交互类型系统推断通道的因果关系，确保进程不会在会话的中间阶段卡在委托的情况下。
A multiparty session forms a unit of structured communication among many participants which follow communication sequences specified as a global type. When a process is engaged in two or more sessions simultaneously, different sessions can be interleaved and can interfere at runtime. Previous work on multiparty session types has ignored session interleaving, providing a limited progress property ensured only within a single session, by assuming non-interference among different sessions and by forbidding delegation. This paper develops, besides a more traditional, compositional communication type system, a novel static interaction type system for global progress in dynamically interleaved and interfered multiparty sessions. The interaction type system infers causalities of channels making sure that processes do not get stuck at intermediate stages of sessions also in presence of delegation.