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