Session types using affinity and exception handling mechanisms have been developed to ensure the communication safety of protocols implemented in concurrent and distributed programming languages. Nevertheless, current affine session types are inadequate for specifying real-world asynchronous protocols, as they are usually imposed by time constraints which enable timeout exceptions to prevent indefinite blocking while awaiting valid messages. This paper proposes the first formal integration of affinity, time constraints, timeouts, and time-failure handling based on multiparty session types for supporting reliability in asynchronous distributed systems. With this theory, we statically guarantee that asynchronous timed communication is deadlock-free, communication safe, while being fearless -- never hindered by timeout errors or abrupt terminations. To implement our theory, we introduce a Rust toolchain designed to facilitate the implementation of safe affine timed protocols. Our toolchain leverages generic types and the time library to handle timed communications, integrated with optional types for affinity. We evaluate our approach by extending diverse examples from the literature to incorporate time and timeouts, demonstrating that our solution incurs negligible overhead compared with an untimed implementation. We also showcase the correctness by construction of our approach by implementing various real-world use cases, including a remote data protocol from the Internet of Remote Things domain, as well as protocols from real-time systems like Android motion sensors and smartwatches.
翻译:利用仿射性与异常处理机制的会话类型已被开发用于确保并发与分布式编程语言所实现协议的通信安全性。然而,当前的仿射会话类型不足以规范现实世界中的异步协议,因为这些协议通常受时间约束的制约——时间约束通过启用超时异常来防止在等待有效消息时发生无限期阻塞。本文首次提出了基于多参与方会话类型的仿射性、时间约束、超时及时间故障处理的正式集成方法,以支持异步分布式系统中的可靠性。基于该理论,我们静态保证了异步时序通信的无死锁性、通信安全性,同时实现无畏通信——永不因超时错误或突然终止而受阻。为实现该理论,我们引入了一套Rust工具链,旨在促进安全仿射时序协议的实现。该工具链利用泛型类型与时间库处理时序通信,并与用于仿射性的可选类型相集成。我们通过扩展现有文献中的多样化案例以纳入时间与超时机制来评估本方法,证明相较于非时序实现方案,我们的解决方案产生的开销可忽略不计。我们还通过实现多个现实应用场景来展示本方法“通过构造确保正确性”的特性,包括来自远程物联网领域的远程数据协议,以及来自实时系统(如Android运动传感器与智能手表)的各类协议。