Deadlock-free asynchronous message reordering in rust with multiparty session types
Deadlock-free asynchronous message reordering in rust with multiparty session types
复制标题
DOI：
10.1145/3503221.3508404
复制
发表时间：
2021-12
期刊：
影响因子：
--
通讯作者：
Zak Cutner;N. Yoshida;Martin Vassor
中科院分区：
文献类型：
--
作者：
Zak Cutner;N. Yoshida;Martin Vassor
Rust是一种专注于性能和可靠性的现代系统语言。为了补充Rust提供“无所畏惧的并发”的承诺，开发人员经常利用异步消息传递。不幸的是，以任意顺序发送和接收消息以最大化计算-通信重叠(消息传递应用程序中的一种流行优化)打开了一个由微妙的并发错误组成的潘多拉盒子。为了通过构造来保证死锁的自由，我们提出了一种新的基于多方会话类型的Rust框架。Rust中以前的会话类型实现要么构建在同步和阻塞通信之上，要么局限于两方交互。至关重要的是，为了提高效率，没有人支持消息的任意排序。Rumpsteak的目标是异步异步/等待代码。它的独特能力是允许开发人员任意排序发送/接收消息，同时保持死锁自由。为此，Rumpsteak结合了两个最新的高级会话类型理论：(1)k-多方兼容性(k-MC)，它全局地验证一组参与者的安全性；(2)异步多方会话子类型，它在单个参与者的上下文中局部验证优化。具体地说，我们提出了一种新颖的异步子分类算法，该算法既合理又可判定。我们首先评估了Rumpsteak与之前的三个Rust实现相比的性能和表现力。我们发现，Rumpsteak的效率大约提高了1.7-8.6倍，并且通过提供任意的消息排序，可以安全地表达更多的示例。其次，我们分析了新算法的复杂性，并将其与k-MC算法和二进制会话子分类算法进行了比较。我们发现它们比伦普牛排慢得多。
Rust is a modern systems language focused on performance and reliability. Complementing Rust's promise to provide "fearless concurrency", developers frequently exploit asynchronous message passing. Unfortunately, sending and receiving messages in an arbitrary order to maximise computation-communication overlap (a popular optimisation in message-passing applications) opens up a Pandora's box of subtle concurrency bugs. To guarantee deadlock-freedom by construction, we present Rumpsteak: a new Rust framework based on multiparty session types. Previous session type implementations in Rust are either built upon synchronous and blocking communication and/or are limited to two-party interactions. Crucially, none support the arbitrary ordering of messages for efficiency. Rumpsteak instead targets asynchronous async/await code. Its unique ability is allowing developers to arbitrarily order send/receive messages while preserving deadlock-freedom. For this, Rumpsteak incorporates two recent advanced session type theories: (1) k-multiparty compatibility (k-MC), which globally verifies the safety of a set of participants, and (2) asynchronous multiparty session subtyping, which locally verifies optimisations in the context of a single participant. Specifically, we propose a novel algorithm for asynchronous subtyping that is both sound and decidable. We first evaluate the performance and expressiveness of Rumpsteak against three previous Rust implementations. We discover that Rumpsteak is around 1.7--8.6x more efficient and can safely express many more examples by virtue of offering arbitrary ordering of messages. Secondly, we analyse the complexity of our new algorithm and benchmark it against k-MC and a binary session subtyping algorithm. We find they are exponentially slower than Rumpsteak's.