Crate mpstthree

Source
Expand description

githubcrates-io![docs-rs]

[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:

  1. default: default features, for implementing the basic example above.
  2. 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. Contains macros_simple. 4. baking: feature for implementing protocols with any number of participants and using associated functions instead of functions. Contains macros_multiple. 5. transport_tcp: feature containing primitives for communicating with TCP. Requires openssl, pkg-config and libssl-dev installed on your machine.
  3. transport_udp: feature containing primitives for communicating with UDP. Requires openssl, pkg-config and libssl-dev installed on your machine. 7. transport_http: feature containing primitives for communicating with HTTP/HTTPS. Requires openssl, pkg-config and libssl-dev installed on your machine. 8. transport: feature containing transport_tcp, transport_udp and transport_http. 9. checking: feature for the top-down approach. Needs the KMC tool. 10. full: feature containing checking, baking and transport.

Modules§

attempt
This module contains the macro for attempting to run a block of code.
bakingbaking
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.
checkingchecking
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.
interleavedinterleaved
This module contains all the macros that are used for the interleaved sessions.
macros_multiplemacros_multiple
This module contains all the macros that are used for the parametrisation on the number of participants.
macros_simplemacros_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 into Rust 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_cancelmacros_multiple
Indefinitely loops to check all sessions if there is a Cancel signal and broadcast if it present. Will also close correctly if a Stop signal is received.
bundle_struct_fork_close_multimacros_multiple
Creates the structure MeshedChannels create_meshedchannels, the close_mpst and fork_mpst_multi.
bundle_struct_fork_close_multi_cancelmacros_multiple
Creates the structure MeshedChannels create_meshedchannels, the close_mpst_cancel and fork_mpst_multi functions to be used with more than 2 participants. It checks the send sides of the channels along the recv sides.
checker_concatchecking
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 the KMC tool and checking the properties of the provided protocol: it will return the minimal k according to this tool if it exists, and None if k is bigger than 50 or does not exist.
checker_concat_implchecking
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_allbaking_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_allmacros_multiple
Create a macro that simplifies the usage of choose_mpst_multi_to_all.
choose_mpst_multi_cancel_to_allmacros_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_allmacros_multiple
Choose among different sessions that are provided.
choose_mpst_to_allmacros_simple
Choose among two different sessions. Must be used with MeshedChannels.
choose_tcptransport or transport_tcp
Choose between many different sessions wrapped in an enum
choose_udptransport or transport_udp
Choose between many different sessions wrapped in an enum
close_mpstmacros_multiple
Create the close function to be used with more than 3 participants.
close_mpst_cancelmacros_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_cancelmacros_multiple
Create the close function to be used with more than 3 participants.
create_broadcast_rolemacros_simple
Create a new broadcast Role and its dual. A broadcast Role is used for sending a choice. Its dual is used for receving this choice.
create_broadcast_role_shortmacros_simple
Create a new broadcast Role and its dual. A broadcast Role 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_3macros_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_3macros_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_2macros_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_3macros_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_3macros_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_2macros_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_bothmacros_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_leftmacros_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_rightmacros_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_3macros_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_3macros_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_2macros_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_multimacros_multiple
Create the ChooseMpst type to be used with more than 3 participants.
create_fn_choose_mpst_cancel_multi_to_all_bundlemacros_multiple
Create choose fuunctions, to choose among different sessions that are provided.
create_fn_choose_mpst_multi_to_all_bundlemacros_multiple
Create choose fuunctions, to choose among different sessions that are provided.
create_meshedchannelsmacros_multiple
Creates a MeshedChannels for more than 3 participants.
create_multiple_broadcast_rolemacros_simple
Create multiple new broadcast Role and their respective dual. A broadcast Role is used for sending a choice. Its dual is used for receving this choice.
create_multiple_broadcast_role_shortmacros_simple
Create multiple new broadcast Role and their respective dual. A broadcast Role 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_namemacros_simple
Create multiple new Name.
create_multiple_normal_name_shortmacros_simple
Create multiple new Name. When a name X is given, the Names created are
create_multiple_normal_rolemacros_simple
Create multiple new Role and their respective dual.
create_multiple_normal_role_shortmacros_simple
Create multiple new Role and their respective dual. When a name X is given, the Roles created are
create_normal_namemacros_simple
Create a new Name.
create_normal_name_shortmacros_simple
Create a new Name. When a name X is given, the Names created are
create_normal_rolemacros_simple
Create a new Role and its dual.
create_normal_role_shortmacros_simple
Create a new Role and its dual. When a name X is given, the Roles created are
create_offer_mpst_session_1macros_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_2macros_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_multimacros_multiple
Creates an OfferMpst function to receive an offer on a given binary session type of a MeshedChannels.
create_offer_type_multimacros_multiple
Create the OfferMpst type to be used with more than 3 participants.
create_recv_mpst_sessionmacros_multiple
Creates a recv function to receive from a simple role on a given binary session type of a MeshedChannels.
create_recv_mpst_session_1macros_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_2macros_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_bundlemacros_multiple
Creates multiple recv functions to receive from a simple role on a given binary session type of a MeshedChannels.
create_send_check_cancelmacros_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_bundlemacros_multiple
Creates multiple send functions to send from a given binary session type of a MeshedChannels with more than 3 participants.
create_send_mpst_cancelmacros_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_bundlemacros_multiple
Creates multiple send functions to send from a given binary session type of a MeshedChannels with more than 3 participants.
create_send_mpst_sessionmacros_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_1macros_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_2macros_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_bundlemacros_multiple
Creates multiple send functions to send from a given binary session type of a MeshedChannels with more than 3 participants.
fork_mpst_multimacros_multiple
Creates the fork function to be used with more than 3 participants.
generatebaking
Create a new SessionMST structure, new roles and the baking environment. This macro creates the related fork_mpst function.
generate_atmpbaking_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 related fork_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_mpstmacros_multiple
Offer a choice and send the session to the broadcaster
offer_http_mpstmacros_multiple
Offer a choice between many different sessions wrapped in an enum. Used with http functions
offer_mpstmacros_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_tcptransport or transport_tcp
Offer a choice between many different sessions wrapped in an enum.
offer_udptransport or transport_udp
Offer a choice between many different sessions wrapped in an enum.
send_cancelmacros_multiple
Creates a function that will cancel a session and send a Cancel signal to the broadcasting role.