mpstthree 0.0.8

A library implementing Multiparty Session Types for 2 or more participants
Documentation

Multiparty session types for Rust

Ubuntu Windows Mac Crate Minimum rustc version Documentation codecov License: MIT

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.6"

Example

Here a way to create a simple protocol involving 3 participants, A, B and C. A sends a payload to B, then receives another 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, Recv, Send};
use mpstthree::meshedchannels::MeshedChannels;

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

// Used for create 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 function 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 function 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 function which process the protocol for closing the connexion
use mpstthree::functionmpst::close::close_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. Here, for this 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
type AtoB<N> = Send<N, End>;
type AtoC<N> = Recv<N, End>;

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

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
type StackA = RoleB<RoleC<RoleEnd>>;
type StackB = RoleA<RoleC<RoleEnd>>;
type StackC = RoleA<RoleB<RoleEnd>>;

You can now encapsulate those binary session types and stacks into MeshedChannels for each participant.

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

To check to the protocol is correct, it is mandatory to detail the behaviour of the participants with functions which 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)?;

    Ok(())
}

/// 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)?;

    Ok(())
}

/// 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)?;

    Ok(())
}

In the end, you have to link 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 should 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 4 files:

  • simple is the basic global protocol shown in Examples.
  • choose checks that a protocol where a role B spreads a choice to the two other roles. For simplifying the test, role C is doing nothing. The protocol can be written as B→A:{B!A.0, B!A.0}.
  • usecase is implementing the protocol given in 1, where Client → C, Authenticator → A and Server → B.
  • usecase-recursive is implementing the protocol given in 2, where Client → C, Authenticator → A and Server → B.

Going further

This subsection explains the more complex and diverse features of the library.

Parametrisation on the name of the roles

This part details how to create new roles and how to use them.

Creation of new roles

Instead of being limited by roles RoleA, RoleB and RoleC, you can now create your roles. To achieve this, you need to use the macros create_normal_role and create_broadcast_role, respectively for binary types and broadcasted ones. Example of use can be found in the macro-basic. Those macros take, as parameters and in the order, the name of the rolea and the name of the dual of this role. For instance, let's create the role RoleD. The expected code will be:

create_normal_role!(RoleA, RoleADual);

Sending and receiving with those new roles

To send and receive with those new roles, it is mandatory to define new send and recv functions. This can easily be done with the macros create_send_mpst_session_1, create_send_mpst_session_2, create_recv_mpst_session_1 and create_recv_mpst_session_2. As you may notice, there is a difference made between session_1 and session_2. This is due to the current limitation of the library: this is for making the difference between the binary channels used during the communication. If A sends to B, it will send on the first channel, and by convention (alphanumerical order), it will be the first binary channel, hence create_send_mpst_session_1 will be used. If A send to C and B is among the participants, then create_send_mpst_session_2 will be used. The macros create_send_mpst_session_1, create_send_mpst_session_2, create_recv_mpst_session_1 and create_recv_mpst_session_2 expect the same inputs: the name of the new function created and the name of the involved roles. To create the send function from A to B, here is the expected line of code:

create_send_mpst_session_1!(send_mpst_a_to_b, RoleB, RoleA);

Making choice and offer with those new roles

To add a layer of features, one may expect to implement choice and offer. There are two different kind of branching: binary and multiple. The former refers to a branching with only two choices, whereas the latter refers to branching with as many choices as wanted. For the binary branching, the macros create_offer_mpst_session_1 and create_offer_mpst_session_2 for offer, and create_choose_left_from_X_to_Y_and_Z (where X, Y and Z are numbers linked to the roles) are used. The inputs are the name of the new offer( respectively choose) functions and the name of the involved roles. For instance, to create an offer function for role B to receive from role C, here is an example of code:

create_offer_mpst_session_2!(
    offer_mpst_session_b_to_c,
    RoleAlltoC,
    RoleB
);

On the opposite side, to create a choice from role C to the other roles, where C will choose the left choice, here is the expected code.

create_choose_left_from_3_to_1_and_2!(
    choose_left_mpst_session_c_to_all,
    RoleADual,
    RoleBDual,
    RoleCtoAll,
    RoleC
);

To compare the traditional and the more complex methods, you can check the usecase and macro-choice files

For the multiple branching, instead of creating new functions, the macro offer_mpst and choose_mpst_to_all can be used directly. The offer_mpst macro expects a session, the name of the recv function used and the branches for the matching. The choose_mpst_to_all macro expects the path to the different choices, the session and the send functions used for sending the choice. A comparison can be made between the files usecase-recursive and macro-recursive, which are respectively the traditional method and the more complex method.

Parametrisation on the number of roles

This part details how to create protocols with many multiple roles. Please have a look at the example long_simple_four.

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

This project is licensed under the MIT License - see the LICENSE file for details.

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.