#session #multiparty

bin+lib mpstthree

A library implementing Multiparty Session Types for 2 or more participants

15 releases

0.0.13 Sep 6, 2021
0.0.12 Sep 3, 2021
0.0.9 Jul 14, 2021
0.0.2 Sep 22, 2020
0.0.1 Mar 9, 2020

#24 in Concurrency

Download history 2/week @ 2021-06-25 3/week @ 2021-07-02 88/week @ 2021-07-09 31/week @ 2021-07-16 9/week @ 2021-07-23 33/week @ 2021-07-30 7/week @ 2021-08-06 17/week @ 2021-08-13 23/week @ 2021-08-27 36/week @ 2021-09-03 30/week @ 2021-09-10 17/week @ 2021-09-17 19/week @ 2021-10-01 25/week @ 2021-10-08

80 downloads per month

MIT/Apache

370KB
6.5K SLoC

Multiparty session types for Rust

Ubuntu Windows Mac Crate Minimum rustc version Documentation codecov

This library implements multiparty session types in Rust for at least two participants. It relies on sesh.

A short video presentation of the library can be found here: https://youtu.be/ej1FetN31HE.

Usage

Add this to your Cargo.toml:

[dependencies]
mpstthree = "0.0.13"

Example

Assume a simple protocol involving 3 participants, A, B and C. A sends a payload to B, then receives another payload from C. Upon receiving the payload from A, B sends a payload to C. This protocol can be written as A!B.A?C.B!C.0. To implement this example, first, get the right components from the library.

// Used for the functions that will process the protocol
use std::boxed::Box;
use std::error::Error;

// Used for creating the types
use mpstthree::binary::struct_trait::{end::End, recv::Recv, send::Send};
use mpstthree::meshedchannels::MeshedChannels;

// Used for creating the stack and the name of each role
use mpstthree::role::a::RoleA;
use mpstthree::role::b::RoleB;
use mpstthree::role::c::RoleC;
use mpstthree::role::end::RoleEnd;

// Used inside the functions which process the protocol for receiving one payload
use mpstthree::functionmpst::recv::recv_mpst_a_from_c;
use mpstthree::functionmpst::recv::recv_mpst_b_from_a;
use mpstthree::functionmpst::recv::recv_mpst_c_from_b;

// Used inside the functions which process the protocol for sending one payload
use mpstthree::functionmpst::send::send_mpst_a_to_b;
use mpstthree::functionmpst::send::send_mpst_b_to_c;
use mpstthree::functionmpst::send::send_mpst_c_to_a;

// Used inside the functions which process the protocol for closing the connexion
use mpstthree::functionmpst::close::close_mpst;

// Used for connecting all the roles, represented as MeshedChannels, together
use mpstthree::functionmpst::fork_mpst;

Then, you have to create the binary session types defining the interactions for each pair of participants. Note that each created type can be reused as many time as needed. For our example, we create several times the same binary session type for clarity, but we could use only two of those types for the whole protocol instead.

// Creating the binary sessions
// for A
type AtoB<N> = Send<N, End>;
type AtoC<N> = Recv<N, End>;

// for B
type BtoA<N> = Recv<N, End>;
type BtoC<N> = Send<N, End>;

// for C
type CtoA<N> = Send<N, End>;
type CtoB<N> = Recv<N, End>;

Add the stacks which give the correct order of the operations for each participant.

// Stacks
// for A
type StackA = RoleB<RoleC<RoleEnd>>;
// for B
type StackB = RoleA<RoleC<RoleEnd>>;
// for C
type StackC = RoleA<RoleB<RoleEnd>>;

You can now encapsulate those binary session types and stacks into MeshedChannels for each participant. We also add the names of the related roles.

// Creating the MP sessions
// for A
type EndpointA<N> = MeshedChannels<AtoB<N>, AtoC<N>, StackA, RoleA<RoleEnd>>;
// for B
type EndpointB<N> = MeshedChannels<BtoA<N>, BtoC<N>, StackB, RoleB<RoleEnd>>;
// for C
type EndpointC<N> = MeshedChannels<CtoA<N>, CtoB<N>, StackC, RoleC<RoleEnd>>;

To run the protocol, we need to detail the behaviour of the participants with functions that input the Endpoints defined above.

// Function to process Endpoint of A
fn simple_triple_endpoint_a(s: EndpointA<i32>) -> Result<(), Box<dyn Error>> {
    let s = send_mpst_a_to_b(1, s);
    let (x, s) = recv_mpst_a_from_c(s)?;

    close_mpst(s)
}

// Function to process Endpoint of B
fn simple_triple_endpoint_b(s: EndpointB<i32>) -> Result<(), Box<dyn Error>> {
    let (x, s) = recv_mpst_b_from_a(s)?;
    let s = send_mpst_b_to_c(2, s);

    close_mpst(s)
}

// Function to process Endpoint of C
fn simple_triple_endpoint_c(s: EndpointC<i32>) -> Result<(), Box<dyn Error>> {
    let s = send_mpst_c_to_a(3, s);
    let (x, s) = recv_mpst_c_from_b(s)?;

    close_mpst(s)
}

In the end, you have to link/fork the threads, related to the functions above, together with fork_mpst(). Do not forget to unwrap() the returned threads.

// Fork all endpoints
fn simple_triple_endpoints() {
    let (thread_a, thread_b, thread_c) = fork_mpst(
        endpoint_a,
        endpoint_b,
        endpoint_c,
    );

    thread_a.join().unwrap();
    thread_b.join().unwrap();
    thread_c.join().unwrap();
}

Getting started

These instructions will get you a copy of the project up and running on your local machine for development and testing purposes.

Prerequisites

You need to have Rust. You will get cargo installed.

Building

For building the library, run this code.

cargo build

Running

For running the library, run this code.

cargo run

Run test

For running the tests, run this code.

cargo test

Tests are divided into 8 folders:

  • unit contains unit tests for the library.
  • basics contains the protocol shown in Examples, alongside examples with the types and functions directly provided by the library.
  • basics_macros contains protocols with three or more participants using macros.
  • baking contains protocols written with methods instead of functions.
  • cancel contains protocols written with cancellation.
  • tcp contains protocols written to work with TCP transport.
  • http contains protocols written to work with HTTP transport.
  • scribble contains protocols generated with Scribble.
  • infinite_type contains protocols that fail because of overflow when evaluated.

Going further

With this library, one can write any protocol with at least two participants and using methods to shorten the writing and checking. You can check the tests and examples to have a larger overview of the different possibilities provided by this library.

Contributing

Please read CONTRIBUTING.md for details on our code of conduct, and the process for submitting pull requests to us.

Versioning

We use SemVer for versioning.

Authors

See also the list of contributors who participated in this project.

License

Licensed under either of Apache License, Version 2.0 or MIT license at your option.

Acknowledgment

This project is part of my current PhD under the supervision of Nobuko Yoshida, that I would like to thank. I was also helped by my colleagues from Imperial College London.

Dependencies

~1–3.5MB
~75K SLoC