Expand description
[docs-rs]: https://img.shields.io/badge/docs.rs-66c2a5?style=for-the-badge&labelColor=555555&logoColor=white&logo=data:image/svg+xml;base64, PHN2ZyByb2xlPSJpbWciIHhtbG5zPSJodHRwOi8vd3d3LnczLm9yZy8yMDAwL3N2ZyIgdmlld0JveD0iMCAwIDUxMiA1MTIiPjxwYXRoIGZpbGw9IiNmNWY1ZjUiIGQ9Ik00ODguNiAyNTAuMkwzOTIgMjE0VjEwNS41YzAtMTUtOS4zLTI4LjQtMjMuNC0zMy43bC0xMDAtMzcuNWMtOC4xLTMuMS0xNy4xLTMuMS0yNS4zIDBsLTEwMCAzNy41Yy0xNC4xIDUuMy0yMy40IDE4LjctMjMuNCAzMy43VjIxNGwtOTYuNiAzNi4yQzkuMyAyNTUuNSAwIDI2OC45IDAgMjgzLjlWMzk0YzAgMTMuNiA3LjcgMjYuMSAxOS45IDMyLjJsMTAwIDUwYzEwLjEgNS4xIDIyLjEgNS4xIDMyLjIgMGwxMDMuOS01MiAxMDMuOSA1MmMxMC4xIDUuMSAyMi4xIDUuMSAzMi4yIDBsMTAwLTUwYzEyLjItNi4xIDE5LjktMTguNiAxOS45LTMyLjJWMjgzLjljMC0xNS05LjMtMjguNC0yMy40LTMzLjd6TTM1OCAyMTQuOGwtODUgMzEuOXYtNjguMmw4NS0zN3Y3My4zek0xNTQgMTA0LjFsMTAyLTM4LjIgMTAyIDM4LjJ2LjZsLTEwMiA0MS40LTEwMi00MS40di0uNnptODQgMjkxLjFsLTg1IDQyLjV2LTc5LjFsODUtMzguOHY3NS40em0wLTExMmwtMTAyIDQxLjQtMTAyLTQxLjR2LS42bDEwMi0zOC4yIDEwMiAzOC4ydi42em0yNDAgMTEybC04NSA0Mi41di03OS4xbDg1LTM4Ljh2NzUuNHptMC0xMTJsLTEwMiA0MS40LTEwMi00MS40di0uNmwxMDItMzguMiAxMDIgMzguMnYuNnoiPjwvcGF0aD48L3N2Zz4K
Mpstthree (also called MultiCrusty) is a library to write and check communication protocols based on Multiparty Session Types.
Currently this library is geared toward use with Scribble and New Scribble for full checking of protocols.
§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.
Here is the full working example, detailed afterwards:
// 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;
use mpstthree::name::a::NameA;
use mpstthree::name::b::NameB;
use mpstthree::name::c::NameC;
// 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::fork_mpst;
// 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>;
// Stacks
// for A
type StackA = RoleB<RoleC<RoleEnd>>;
// for B
type StackB = RoleA<RoleC<RoleEnd>>;
// for C
type StackC = RoleA<RoleB<RoleEnd>>;
// Creating the MP sessions
// for A
type EndpointA<N> = MeshedChannels<AtoB<N>, AtoC<N>, StackA, NameA>;
// for B
type EndpointB<N> = MeshedChannels<BtoA<N>, BtoC<N>, StackB, NameB>;
// for C
type EndpointC<N> = MeshedChannels<CtoA<N>, CtoB<N>, StackC, NameC>;
// Function to process Endpoint of A
fn 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 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 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)
}
// Fork all endpoints
fn main() {
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();
}
Here is the full description. First, you import the correct functions and types.
// 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::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, NameA>;
// for B
type EndpointB<N> = MeshedChannels<BtoA<N>, BtoC<N>, StackB, NameB>;
// for C
type EndpointC<N> = MeshedChannels<CtoA<N>, CtoB<N>, StackC, NameC>;
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 main() {
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();
}
The different features available are:
default
: default features, for implementing the basic example above.macros_simple
: feature for implementing protocols with three participants, whatever are their name. 3.macros_multiple
: feature for implementing protocols with any number of participants. Containsmacros_simple
. 4.baking
: feature for implementing protocols with any number of participants and using associated functions instead of functions. Containsmacros_multiple
. 5.transport_tcp
: feature containing primitives for communicating with TCP. Requiresopenssl
,pkg-config
andlibssl-dev
installed on your machine.transport_udp
: feature containing primitives for communicating with UDP. Requiresopenssl
,pkg-config
andlibssl-dev
installed on your machine. 7.transport_http
: feature containing primitives for communicating with HTTP/HTTPS. Requiresopenssl
,pkg-config
andlibssl-dev
installed on your machine. 8.transport
: feature containingtransport_tcp
,transport_udp
andtransport_http
. 9.checking
: feature for the top-down approach. Needs theKMC
tool. 10.full
: feature containingchecking
,baking
andtransport
.
Modules§
- attempt
- This module contains the macro for attempting to run a block of code.
- baking
baking
- This module contains the macros for creating the different structures and associated functions for any number of participants to simplify send/recv.
- baking_
atmp - This module contains the macros for creating the different structures and associated functions for any number of participants in timed protocols to simplify send/recv.
- binary
- The slightly modified binary session type library.
- binary_
atmp - The slightly modified binary session type library.
- checking
checking
- This module contains the macros and the functions for checking whether a protocol is well written or not, according to a bottom-up method.
- functionmpst
- This module contains all the functions that are used
for consuming
MeshedChannels
. - interleaved
interleaved
- This module contains all the macros that are used for the interleaved sessions.
- macros_
multiple macros_multiple
- This module contains all the macros that are used for the parametrisation on the number of participants.
- macros_
simple macros_simple
- This module contains all the macros that are used for the parametrisation on the name of the participants.
- meshedchannels
- The main structure used for representing a participant, also named a party, within a protocol.
- message
- This feature only includes a message structure. It is parameterised with a label and a payload.
- name
- The main trait used for representing the name of a participant.
- role
- The main trait used for representing an ordering of a participant.
- top_
down_ nuscr - This module allows to transform
nuscr
global protocols intoRust
files for mpstthree. - transport
- The module for interacting with different modes of transport such as HTTP or TCP
Macros§
- attempt
- Try to run the first block of code and,
upon error, run the second block of code.
Each step in the block of code must
return
Result<Ok(_), Err(e)>
. - broadcast_
cancel macros_multiple
- Indefinitely loops to check all sessions if there
is a
Cancel
signal and broadcast if it present. Will also close correctly if aStop
signal is received. - bundle_
struct_ fork_ close_ multi macros_multiple
- Creates the structure MeshedChannels
create_meshedchannels
, theclose_mpst
andfork_mpst_multi
. - bundle_
struct_ fork_ close_ multi_ cancel macros_multiple
- Creates the structure MeshedChannels
create_meshedchannels
, theclose_mpst_cancel
andfork_mpst_multi
functions to be used with more than 2 participants. It checks the send sides of the channels along the recv sides. - checker_
concat checking
- The macro that allows to create digraphs from each endpoint,
along with
enum
if needed. You can also provide the name of a file for running theKMC
tool and checking the properties of the provided protocol: it will return the minimalk
according to this tool if it exists, andNone
ifk
is bigger than 50 or does not exist. - checker_
concat_ impl checking
- This macro is available only if MultiCrusty is built with
the
"checking"
feature. - choose
- Choose between many different sessions wrapped in an
enum
- choose_
atmp - Choose between many different sessions wrapped in an
enum
- choose_
atmp_ mpst_ multi_ to_ all baking_atmp
- Choose among different sessions that are provided.
- choose_
mpst_ a_ to_ all - Choose, for A, among two different sessions
- choose_
mpst_ b_ to_ all - Choose, for B, among two different sessions
- choose_
mpst_ c_ to_ all - Choose, for C, among two different sessions
- choose_
mpst_ create_ multi_ to_ all macros_multiple
- Create a macro that simplifies the usage of
choose_mpst_multi_to_all
. - choose_
mpst_ multi_ cancel_ to_ all macros_multiple
- Choose among different sessions that are provided, may fail because of a canceled session. Need to exclude the first participant
- choose_
mpst_ multi_ to_ all macros_multiple
- Choose among different sessions that are provided.
- choose_
mpst_ to_ all macros_simple
- Choose among two different sessions.
Must be used with
MeshedChannels
. - choose_
tcp transport
ortransport_tcp
- Choose between many different sessions wrapped in an
enum
- choose_
udp transport
ortransport_udp
- Choose between many different sessions wrapped in an
enum
- close_
mpst macros_multiple
- Create the close function to be used with more than 3 participants.
- close_
mpst_ cancel macros_multiple
- Create the close function to be used with more than 3 participants. It is used for checking the send sides upon closing.
- close_
mpst_ check_ cancel macros_multiple
- Create the close function to be used with more than 3 participants.
- create_
broadcast_ role macros_simple
- Create a new broadcast
Role
and its dual. A broadcastRole
is used for sending a choice. Its dual is used for receving this choice. - create_
broadcast_ role_ short macros_simple
- Create a new broadcast
Role
and its dual. A broadcastRole
is used for sending a choice. Its dual is used for receving this choice. When a name X is given, the Roles created are - create_
choose_ both_ from_ 1_ to_ 2_ and_ 3 macros_simple
- Call both create_choose_right_from_1_to_2_and_3
and create_choose_left_from_1_to_2_and_3.
Must be used with
MeshedChannels
. - create_
choose_ both_ from_ 2_ to_ 1_ and_ 3 macros_simple
- Call both create_choose_right_from_2_to_1_and_3
and create_choose_left_from_2_to_1_and_3.
Must be used with
MeshedChannels
. - create_
choose_ both_ from_ 3_ to_ 1_ and_ 2 macros_simple
- Call both create_choose_right_from_3_to_1_and_2
and create_choose_left_from_3_to_1_and_2.
Must be used with
MeshedChannels
. - create_
choose_ left_ from_ 1_ to_ 2_ and_ 3 macros_simple
- Create the ChooseMpst function to send a Choose
left branch from the first role to the others. Must be
used with
MeshedChannels
. - create_
choose_ left_ from_ 2_ to_ 1_ and_ 3 macros_simple
- Create the ChooseMpst function to send a Choose
left branch from the second role to the others. Must be
used with
MeshedChannels
. - create_
choose_ left_ from_ 3_ to_ 1_ and_ 2 macros_simple
- Create the ChooseMpst function to send a Choose
left branch from the third role to the others. Must be
used with
MeshedChannels
. - create_
choose_ mpst_ session_ multi_ both macros_multiple
- Create the two ChooseMpst functions to send a Choose on each branch to be used with more than 3 participants. Only works when active role is the last one.
- create_
choose_ mpst_ session_ multi_ left macros_multiple
- Create the ChooseMpst function to send a Choose left branch to be used with more than 3 participants. Only works when active role is the last one.
- create_
choose_ mpst_ session_ multi_ right macros_multiple
- Create the ChooseMpst function to send a Choose right branch to be used with more than 3 participants. Only works when active role is the last one.
- create_
choose_ right_ from_ 1_ to_ 2_ and_ 3 macros_simple
- Create the ChooseMpst function to send a Choose
right branch from the first role to the others. Must be
used with
MeshedChannels
. - create_
choose_ right_ from_ 2_ to_ 1_ and_ 3 macros_simple
- Create the ChooseMpst function to send a Choose
right branch from the second role to the others. Must
be used with
MeshedChannels
. - create_
choose_ right_ from_ 3_ to_ 1_ and_ 2 macros_simple
- Create the ChooseMpst function to send a Choose
right branch from the third role to the others. Must be
used with
MeshedChannels
. - create_
choose_ type_ multi macros_multiple
- Create the ChooseMpst type to be used with more than 3 participants.
- create_
fn_ choose_ mpst_ cancel_ multi_ to_ all_ bundle macros_multiple
- Create choose fuunctions, to choose among different sessions that are provided.
- create_
fn_ choose_ mpst_ multi_ to_ all_ bundle macros_multiple
- Create choose fuunctions, to choose among different sessions that are provided.
- create_
meshedchannels macros_multiple
- Creates a MeshedChannels for more than 3 participants.
- create_
multiple_ broadcast_ role macros_simple
- Create multiple new broadcast
Role
and their respective dual. A broadcastRole
is used for sending a choice. Its dual is used for receving this choice. - create_
multiple_ broadcast_ role_ short macros_simple
- Create multiple new broadcast
Role
and their respective dual. A broadcastRole
is used for sending a choice. Its dual is used for receving this choice. When a name X is given, the Roles created are - create_
multiple_ normal_ name macros_simple
- Create multiple new
Name
. - create_
multiple_ normal_ name_ short macros_simple
- Create multiple new
Name
. When a name X is given, the Names created are - create_
multiple_ normal_ role macros_simple
- Create multiple new
Role
and their respective dual. - create_
multiple_ normal_ role_ short macros_simple
- Create multiple new
Role
and their respective dual. When a name X is given, the Roles created are - create_
normal_ name macros_simple
- Create a new
Name
. - create_
normal_ name_ short macros_simple
- Create a new
Name
. When a name X is given, the Names created are - create_
normal_ role macros_simple
- Create a new
Role
and its dual. - create_
normal_ role_ short macros_simple
- Create a new
Role
and its dual. When a name X is given, the Roles created are - create_
offer_ mpst_ session_ 1 macros_simple
- Create an offer function to recv on the first binary
session from any kind of role. Must be used with
MeshedChannels
. - create_
offer_ mpst_ session_ 2 macros_simple
- Create an offer function to recv on the second binary
session from any kind of role. Must be used with
MeshedChannels
. - create_
offer_ mpst_ session_ multi macros_multiple
- Creates an OfferMpst function to receive an offer on a given binary session type of a MeshedChannels.
- create_
offer_ type_ multi macros_multiple
- Create the OfferMpst type to be used with more than 3 participants.
- create_
recv_ mpst_ session macros_multiple
- Creates a recv function to receive from a simple role on a given binary session type of a MeshedChannels.
- create_
recv_ mpst_ session_ 1 macros_simple
- Create a recv function to recv on the first binary
session from any kind of role. Must be used with
MeshedChannels
. - create_
recv_ mpst_ session_ 2 macros_simple
- Create a recv function to recv on the second binary
session from any kind of role. Must be used with
MeshedChannels
. - create_
recv_ mpst_ session_ bundle macros_multiple
- Creates multiple recv functions to receive from a simple role on a given binary session type of a MeshedChannels.
- create_
send_ check_ cancel macros_multiple
- Creates a send function to send from a given binary session type of a MeshedChannels with more than 3 participants. Checks if the first binary session has a “cancel” signal and panic if yes. The send function will try to send and panic if not possible (canceled session).
- create_
send_ check_ cancel_ bundle macros_multiple
- Creates multiple send functions to send from a given binary session type of a MeshedChannels with more than 3 participants.
- create_
send_ mpst_ cancel macros_multiple
- Creates a send function to send from a given binary session type of a MeshedChannels with more than 3 participants. The send function will try to send and panic if not possible (canceled session).
- create_
send_ mpst_ cancel_ bundle macros_multiple
- Creates multiple send functions to send from a given binary session type of a MeshedChannels with more than 3 participants.
- create_
send_ mpst_ session macros_multiple
- Creates a send function to send from a given binary session type of a MeshedChannels with more than 3 participants.
- create_
send_ mpst_ session_ 1 macros_simple
- Create a send function to send on the first binary
session from any kind of role. Must be used with
MeshedChannels
. - create_
send_ mpst_ session_ 2 macros_simple
- Create a send function to send on the second binary
session from any kind of role. Must be used with
MeshedChannels
. - create_
send_ mpst_ session_ bundle macros_multiple
- Creates multiple send functions to send from a given binary session type of a MeshedChannels with more than 3 participants.
- fork_
mpst_ multi macros_multiple
- Creates the fork function to be used with more than 3 participants.
- generate
baking
- Create a new SessionMST structure, new roles and the baking environment.
This macro creates the related
fork_mpst
function. - generate_
atmp baking_atmp
- Create new SessionMST structures, new roles and the baking environment,
with
send
functions that can fail, for timed protocols. Also create the macros needed for choosing branches. Each macro is linked to a role X and are called as followed: choose_mpst_x_to_all!( s, # the current session enum_1::variant_1, # the first branch for the first passive role enum_2::variant_2, # the first branch for the second passive role … enum_n::variant_n, # the first branch for the n-th passive role ) This macro creates the relatedfork_mpst
function. - offer
- Offer a choice between many different sessions wrapped
in an
enum
- offer_
atmp - Offer a choice between many different sessions wrapped
in an
enum
- offer_
cancel_ mpst macros_multiple
- Offer a choice and send the session to the broadcaster
- offer_
http_ mpst macros_multiple
- Offer a choice between many different sessions wrapped in an
enum
. Used with http functions - offer_
mpst macros_multiple
- Offer a choice between many different sessions wrapped in an
enum
- offer_
mpst_ a_ to_ b - Offer a choice to A from B between many different
sessions wrapped in an
enum
- offer_
mpst_ a_ to_ c - Offer a choice to A from C between many different
sessions wrapped in an
enum
- offer_
mpst_ b_ to_ a - Offer a choice to B from A between many different
sessions wrapped in an
enum
- offer_
mpst_ b_ to_ c - Offer a choice to B from C between many different
sessions wrapped in an
enum
- offer_
mpst_ c_ to_ a - Offer a choice to C from A between many different
sessions wrapped in an
enum
- offer_
mpst_ c_ to_ b - Offer a choice to C from B between many different
sessions wrapped in an
enum
- offer_
tcp transport
ortransport_tcp
- Offer a choice between many different sessions wrapped
in an
enum
. - offer_
udp transport
ortransport_udp
- Offer a choice between many different sessions wrapped
in an
enum
. - send_
cancel macros_multiple
- Creates a function that will cancel a session and send a
Cancel
signal to the broadcasting role.