Message passing is a fundamental element in software development, ranging from concurrent and mobile computing to distributed services, but it suffers from communication errors such as deadlocks. Session types are a typing discipline for enforcing safe structured interactions between multiple participants. However, each typed interaction is restricted to having one fixed sender and one fixed receiver. In this paper, we extend session types with existential branching types, to handle a common interaction pattern with multiple senders and a single receiver in a synchronized setting, i.e. a receiver is available to receive messages from multiple senders, and which sender actually participates in the interaction cannot be determined till execution. We build the type system with existential branching types, which retain the important properties induced by standard session types: type safety, progress (i.e. deadlock-freedom), and fidelity. We further provide a novel communication type system to guarantee progress of dynamically interleaved multiparty sessions, by abandoning the strong restrictions of existing type systems. Finally, we encode Rust multi-thread primitives in the extended session types to show its expressivity, which can be considered as an attempt to check the deadlock-freedom of Rust multi-thread programs.

翻译：消息传递是软件开发中的基本要素，涵盖从并发与移动计算到分布式服务等各类场景，但易受死锁等通信错误的影响。会话类型是一种类型化规则体系，用于强制实现多参与者之间安全的结构化交互。然而，每个类型化交互都局限于一个固定发送者与一个固定接收者。本文通过引入存在分支类型扩展会话类型，以处理同步场景中多发送者与单接收者这一常见交互模式——即单个接收者可同时接收来自多个发送者的消息，而实际参与交互的发送者需在运行时才能确定。我们构建了包含存在分支类型的类型系统，该系统保留了标准会话类型的重要特性：类型安全性、进展性（即无死锁）及保真性。进一步地，我们提出一种新型通信类型系统，通过摒弃现有类型系统的严格限制，保证动态交织多方会话的进展性。最后，我们通过将Rust多线程原语编码至扩展会话类型中展示其表达能力，这可视作检测Rust多线程程序无死锁性的一种尝试。