Deadlock-free asynchronous message reordering in rust with multiparty session types
- 28 March 2022
- conference paper
- conference paper
- Published by Association for Computing Machinery (ACM)
Abstract
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.Keywords
Funding Information
- The Engineering and Physical Sciences Research Council (EPSRC) (EP/T006544/1, EP/K011715/1, EP/K034413/1, EP/L00058X/1, EP/N027833/1, EP/N028201/1, EP/T014709/1, EP/V000462/1)
This publication has 37 references indexed in Scilit:
- Session types for RustPublished by Association for Computing Machinery (ACM) ,2015
- Protocols by DefaultPublished by Springer Science and Business Media LLC ,2015
- The Scribble Protocol LanguageLecture Notes in Computer Science, 2014
- SPY: Local Verification of Global ProtocolsPublished by Springer Science and Business Media LLC ,2013
- Overlapping computation and communication of three-dimensional FDTD on a GPU clusterComputer Physics Communications, 2012
- Multiparty asynchronous session typesPublished by Association for Computing Machinery (ACM) ,2008
- Subtyping for session types in the pi calculusActa Informatica, 2005
- Language primitives and type discipline for structured communication-based programmingPublished by Springer Science and Business Media LLC ,1998
- An interaction-based language and its typing systemLecture Notes in Computer Science, 1994
- Depth-first iterative-deepening: An optimal admissible tree searchArtificial Intelligence, 1985