PI: Nobuko Yoshida, University of Oxford. Co-I:  Martin Vassor, University of Oxford

  • Concurrent robotics control is difficult due to collision, deadlock and failure.
  • Type-based approaches have been successful to tackle those issues.
  • We propose a framework for multiparty session types (MPST) which can handle optimised message passing interactions between concurrent robotics and implement the framework in Rust.
  • Our approach uses features of Rust’s affine type system which can ensure the recovery from failures.

Concurrent and distributed robotics systems are ubiquitous and increase the difficulty to ensure correct control mechanisms. Specifically, it is notoriously complex to prevent and to fix bugs in robotics programming once noticed. To address those difficulties, we use Multiparty Session Types (MPST), which is a family of behavioural type systems for programming using message-passing concurrency.

To challenge this issue, we develop a general message passing framework to handle concurrent systems which is also resilient for failures and enables to automatically recover from them. We implement our framework in the tool-chain Rumpsteak, which is Rust framework that implements MPST. This framework integrates seamlessly with existing technologies (e.g. the Scribble language and the vScr tool), and makes the most of Rust, using extensively its type system and its async capabilities to achieve efficient and reliable implementations of protocols.

There are three different approaches of the tool chain as described in the figure below.

(1) *the top-down approach*, which generates state machines of individual participants from the specification of a global protocol;

(2) *the bottom-up approach*, which takes state machines of individual participants and ensures they are consistent with each other; and

(3) *the hybrid approach* which generates state machines from a specification — as in the top-down approach — and a set of optimised state machines, and ensures that the optimised state machines are consistent with the generated machines. Rumpsteak can accommodate all three approaches, although the top-down approach is most often used and the hybrid one is used to implement protocol optimisations enable efficient concurrent robotics programming.

Rumpsteak has been used and extended in order to implement state-of-the-art extensions of Multiparty Session Types. For instance asynchronous message reordering, which allows to increase the level of parallelism, integrated with the recovery from failures based on built-in affine types in Rust.

PUBLICATION. Zak Cutner, Nobuko Yoshida, and Martin Vassor. 2022. “Deadlock-free asynchronous message reordering in rust with multiparty session types.” PPoPP ’22

IMPACT. This VeTSS projects led to two grants (Digital Security by Design and Horizon EU):  Morello-HAT: Morello High-Level API and Tooling, EP/X015955/1 (£1.128 M), Glasgow, Essex and Oxford: 01 July 2022-31st Dec 2024 and TaRDIS: Trustworthy And Resilient Decentralised Intelligence For Edge Systems, Horizon EU (7M Euros).