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.
Add this to your Cargo.toml
:
toml
[dependencies]
mpstthree = "0.0.6"
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.
```rust // 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::recvmpstafromc; use mpstthree::functionmpst::recv::recvmpstbfroma; use mpstthree::functionmpst::recv::recvmpstcfromb;
// Used inside the function which process the protocol for sending one payload use mpstthree::functionmpst::send::sendmpstatob; use mpstthree::functionmpst::send::sendmpstbtoc; use mpstthree::functionmpst::send::sendmpstctoa;
// 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.
```rust
/// Creating the binary sessions
type AtoB
type BtoA
type CtoA
Add the stacks, which give the correct order of the operations for each participant.
rust
/// 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.
rust
/// 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.
```rust
/// Function to process Endpoint of A
fn simpletripleendpointa(s: EndpointA
close_mpst(s)?;
Ok(())
}
/// Function to process Endpoint of B
fn simpletripleendpointb(s: EndpointB
close_mpst(s)?;
Ok(())
}
/// Function to process Endpoint of C
fn simpletripleendpointc(s: EndpointC
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.
```rust /// Fork all endpoints fn simpletripleendpoints() { let (threada, threadb, threadc) = forkmpst( endpointa, endpointb, endpoint_c, );
thread_a.join().unwrap();
thread_b.join().unwrap();
thread_c.join().unwrap();
} ```
These instructions will get you a copy of the project up and running on your local machine for development and testing purposes.
You need to have Rust. You should get cargo
installed.
For building the library, run this code.
sh
$ cargo build
For running the library, run this code.
sh
$ cargo run
For running the tests, run this code.
sh
$ cargo test
Tests are divided into 4 files:
This subsection explains the more complex and diverse features of the library.
This part details how to create new roles and how to use them.
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:
rust
create_normal_role!(RoleA, RoleADual);
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:
rust
create_send_mpst_session_1!(send_mpst_a_to_b, RoleB, RoleA);
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:
rust
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.
rust
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.
This part details how to create protocols with many multiple roles. Please have a look at the example longsimplefour.
Please read CONTRIBUTING.md for details on our code of conduct, and the process for submitting pull requests to us.
We use SemVer for versioning.
See also the list of contributors who participated in this project.
This project is licensed under the MIT License - see the LICENSE file for details.
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.