Protocols

Ferrite uses the term protocol to refer to session types in Rust. All protocol in Ferrite implements the Protocol trait. The name of the protocols are defined based on the behavior of the provider. Most of the Ferrite protocols also contain continuation protocols, which describe the protocol that follows after the current protocol have been executed.

We have seen an example protocol in the previous section, SendValue<String, End>. This means that the type SendValue<String, End> implements the Protocol trait. This is so because End is a protocol representing termination, and the type SendValue<T, A> is a protocol if the continuation protocol A, which is End in this case, is a protocol. The type SendValue<String, End> describes a protocol which the provider sends a String value and then terminates with End. On the other end, this behavior is inversed, with the client receives the String value and then waits for the provider to terminate.

For a Rust type to be a Ferrite protocol. It has to follow certain conditions. For example, while we can define a Rust type like SendValue<String, i32>, it is not considered by Ferrite to be a protocol. This is because the continuation type i32 does not implement Protocol. Therefore SendValue<String, i32> also does not implement Protocol.

Some protocols also have additional constraints that need to be satisfied. For example, the protocol SendValue<T, A> also requires the Rust value to be send, T, to implement Send and 'static. This means that we can only send Rust values that can be safely transferred across threads, and do not contain other local lifetimes.

Using Ferrite, we can define complex protocols that have many layers of nested continuations. For example, the protocol SendValue<String, ReceiveValue<i32, SendValue<bool, End>>> describes a session type which the provider first sends a String value, then receives an i32 value, then sends a bool value, before finally terminating.

Overview of Linear Protocols in Ferrite

We will cover in detail each protocol in the upcoming chapters. Below shows a summary of protocols available in Ferrite:

ProtocolProvider Description
EndTermination
SendValue<T, A>Send a Rust value of type T, and continue as session type A
ReceiveValue<T, A>Receive a Rust value of type T, and continue as session type A
SendChannel<A, B>Send a channel of session type A, and continue as session type B
ReceiveChannel<A, B>Receive a channel of session type A, and continue as session type B
ExternalChoice<Choice>Provide the client with choices defined in Choice
InternalChoice<Choice>Offer a particular choice defined in Choice
Rec<F>Recursive session type, with F being a session type containing recursion markers such as Z.