Multiparty session types for Rust
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
:
[]
= "0.0.4"
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 Box;
use Error;
// Used for creating the types
use ;
use MeshedChannels;
// Used for connecting all the roles, represented as MeshedChannels, together
use fork_mpst;
// Used for create the stack and the name of each role
use RoleA;
use RoleB;
use RoleC;
use RoleEnd;
// Used inside the function which process the protocol for receiving one payload
use recv_mpst_a_from_c;
use recv_mpst_b_from_a;
use recv_mpst_c_from_b;
// Used inside the function which process the protocol for sending one payload
use send_mpst_a_to_b;
use send_mpst_b_to_c;
use send_mpst_c_to_a;
// Used inside the function which process the protocol for closing the connexion
use 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> = ;
type AtoC<N> = ;
type BtoA<N> = ;
type BtoC<N> = ;
type CtoA<N> = ;
type CtoB<N> = ;
Add the stacks, which give the correct order of the operations for each participant.
/// Stacks
type StackA = ;
type StackB = ;
type StackC = ;
You can now encapsulate those binary session types and stacks into MeshedChannels for each participant.
/// Creating the MP sessions
type EndpointA<N> = ;
type EndpointB<N> = ;
type EndpointC<N> = ;
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
/// Function to process Endpoint of B
/// Function to process Endpoint of C
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
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.
Running
For running the library, run this code.
Run test
For running the tests, run this code.
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!;
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!;
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!;
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!;
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
- Nicolas Lagaillardie - Initial work - NicolasLagaillardie
- Rumyana Neykova - Initial work - rumineykova
- Nobuko Yoshida - Initial work - NobukoYoshida
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.