This library implements multiparty session types in Rust for three participants. It relies on sesh. An other library is coming soon to extend to any number of participants.
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.2"
Here a way to create a simple protocol involving 3 participants, A, B and C. A sends a payoad to B, then receives an other 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 extern crate mpstthree;
use std::boxed::Box; use std::error::Error;
use mpstthree::binary::{End, Recv, Send}; use mpstthree::run_processes; use mpstthree::sessionmpst::SessionMpst;
use mpstthree::functionmpst::close::close_mpst;
use mpstthree::role::a::RoleA; use mpstthree::role::b::RoleB; use mpstthree::role::c::RoleC; use mpstthree::role::end::RoleEnd;
use mpstthree::functionmpst::recv::recvmpstatoc; use mpstthree::functionmpst::recv::recvmpstbtoa; use mpstthree::functionmpst::recv::recvmpstctob;
use mpstthree::functionmpst::send::sendmpstatob; use mpstthree::functionmpst::send::sendmpstbtoc; use mpstthree::functionmpst::send::sendmpstctoa; ```
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 the example, we create several times the same binary session type.
```rust
/// Creating the binary sessions
type AtoB
type BtoA
type CtoA
Add the queues, which give the correct order of the operations for each participants.
rust
/// Queues
type QueueA = RoleB<RoleC<RoleEnd>>;
type QueueB = RoleA<RoleC<RoleEnd>>;
type QueueC = RoleA<RoleB<RoleEnd>>;
You can now encapsulate those binary session types and queues into SessionMpst for each participant.
rust
/// Creating the MP sessions
type EndpointA<N> = SessionMpst<AtoB<N>, AtoC<N>, QueueA>;
type EndpointB<N> = SessionMpst<BtoA<N>, BtoC<N>, QueueB>;
type EndpointC<N> = SessionMpst<CtoA<N>, CtoB<N>, QueueC>;
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
/// Endpoint for A
fn simpletripleendpointa(s: EndpointA
close_mpst(s)?;
Ok(())
}
/// Endpoint for B
fn simpletripleendpointb(s: EndpointB
close_mpst(s)?;
Ok(())
}
/// Endpoint for 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 run_processes(). Do not forget to unwrap() the returned threads.
```rust /// Fork all endpoints fn simpletripleendpoints() { let (threada, threadb, threadc) = runprocesses( simpletripleendpointa, simpletripleendpointb, simpletripleendpoint_c, );
thread_a.unwrap();
thread_b.unwrap();
thread_c.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 in 4 files:
This subsection explains 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 own 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 role, the name of the nextfunction to go through the stack, the name of the dual of this role and the name of the next function for this dual. For instance, let's create the role RoleD. The expected code will be:
rust
create_normal_role!(RoleA, next_a, RoleD, next_d);
To create the role RoleD, you need the related next function, that can be named next_d, to go through a stack which head is RoleD, such as RoleD<RoleEnd>. The dual of RoleDis RoleDDualand the related next function, that can be named next_d_dual.
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 names of the role and the related nextfunction. 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, next_b, 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 names of the role and the related next function. 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,
recv_mpst_b_all_to_c,
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,
RoleCtoAll,
RoleADual,
RoleBDual,
next_c_to_all,
RoleC
);
To compare the traditional and the more complex methods, you can check the usecase and macro-choice files
For the multipke 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 methode and the more complex method.
This part details how to create create protocols many multiple roles. This is still a work in progress.
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.