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运动传感器与智能手表)的协议。