PI: Nobuko Yoshida, PhD Student: Nicolas Lagaillardie, Imperial College London, Co-I: Rumyana Neykova, Brunel University London

  • The first library, MultiCrusty, for multiparty programming in Rust.
  • MultiCrusty leverages Scribble toolchain and Rusts type system for deadlock detection.
  • Formalisation of our implementation and proof of correctness, including a type system for affine channels with deadlock-freedom guarantees. 
  • Performance evaluation shows MultiCrusty scales better than existing stats-of-the-art implementations.

The advantage of message-passing concurrency is well-understood: it allows cheap horizontal scalability at a time when technology providers have to adapt and scale their tools and applications to various devices and platforms. Multiparty session types (MPST) is a type-based discipline that ensures that concurrent and distributed systems are safe by design. It guarantees that message-passing processes following a predefined communication protocol, are free from communication errors and deadlocks. Rust is a particularly appealing language for the practical embedding of session types. Its affine type system allows for static typing of linear resources — an essential requirement for the safety of session type systems. Despite the interest in the Rust community for verification techniques handling multiple communicating processes, the existing Rust implementations are limited to binary (two-party) session types.

We have designed and implemented multiparty session types in Rust, visualised below.

Our design follows a state-of-the-art encoding of multiparty into binary session types. We generate local types in Rust, utilising the Scribble toolchain. Our library for MPST programming in Rust, MultiCrusty, is implemented as a thin wrapper over an existing binary session types library. Differently from other MPST implementations that check linear usage of channels at runtime, we rely on the Rust affine type system to type-check MPST programs.

Ours is the first formalisation of a multiparty session type system for affine processes. In addition, as we generate the local types from a readable global specification, errors caused by an affine (and not linear) usage of channels, a well-known limitation of the previous libraries, are easily avoided. Our library is available here.

PUBLICATIONS. [1] F. Zhou, F. Ferreira, R. Hu, R. Neykova, N. Yoshida. “Statically Verified Refinements for Multiparty Protocols.” OOPSLA’20. [2] N. Lagaillardie, R. Neykova, N. Yoshida. “Implementing Multiparty Session Types in Rust. “ Coordination’20.

RELATED GRANTS. Nobuko Yoshida, PI, EPSRC Standard Grant: “Session Types for Reliable Distributed Systems”, 10/2020-09/2024, £697,651; W Vanderbauwhede, PI (Nobuko Yoshida, Co-I) EPSRC Standard Grant: “AppControl: Enforcing Application Behaviour through Type-Based Constraints”, 09/2020-06/2024, £1.4M.

IMPACT. “One core challenge at Actyx is to give average programmers and automation engineers software tools for successfully digitising this world’s factories. Achieving this in a safe and modular way requires a behavioural typing discipline for static protocol verification such as the one Nicolas, Rumyana, and Nobuko develop and refine in close collaboration with us.”– Dr. Roland Kuhn, CTO & co-founder of Actyx AG –