Munksgaard/session-types

Session Types for Rust

This is an implementation of session types for Rust.

Using this library, you can implement bi-directional process communication with compile-time assurance that neither party will violate the communication protocol.

Getting started

session-types is available on crates.io. It is recommended to look there for the newest released version, as well as links to the newest builds of the docs.

At the point of the last update of this README, the latest published version could be used like this:

Add the following dependency to your Cargo manifest...

[dependencies]
session_types = "0.3.1"

...and see the docs for how to use it.

Example

extern crate session_types;
use session_types::*;
use std::thread;

type Server = Recv<i64, Send<bool, Eps>>;
type Client = <Server as HasDual>::Dual;

fn srv(c: Chan<(), Server>) {
    let (c, n) = c.recv();
    if n % 2 == 0 {
        c.send(true).close()
    } else {
        c.send(false).close()
    }
}

fn cli(c: Chan<(), Client>) {
    let n = 42;
    let c = c.send(n);
    let (c, b) = c.recv();

    if b {
        println!("{} is even", n);
    } else {
        println!("{} is odd", n);
    }

    c.close();
}

fn main() {
    let (server_chan, client_chan) = session_channel();

    let srv_t = thread::spawn(move || srv(server_chan));
    let cli_t = thread::spawn(move || cli(client_chan));

    let _ = (srv_t.join(), cli_t.join());
}

We start by specifying a protocol. Protocols are constructed from the protocol types Send, Recv, Choose, Offer, Rec and Var (see Protocol types). In this case, our protocol is:

type Server = Recv<i64, Send<bool, Eps>>;

which reads:

• Receive a signed 64-bit integer
• Send a boolean
• Close the channel

The Client protocol is the dual, which is a well-defined concept in session types. Loosely, it means that every protocol step in one process has a matching step in the other. If one process wants to send a value, the other process must be ready to receive it. The dual of Server is:

type Client = Send<i64, Recv<bool, Eps>>;

With session-types, we do not have to construct the dual by hand, as we leverage the trait system to model this concept with the HasDual trait. This allows us to do:

type Client = <Server as HasDual>::Dual;

Why is it cool?

Session types are not a new concept. They are cool, because they allow for compile-time verification of process communication. In other words, we are able to check statically if two communicating processes adhere to their shared communication protocol.

But implementing session types requires a way to model that certain actions in the protocol have taken place. This is a complicated thing to do statically in most programming languages, but in Rust it is easy because of move semantics.

Using move semantics, we ensure that "taking a step" in the protocol (sending, receiving, etc) cannot be repeated.

Protocol types

Any session-typed communication protocol is constructed from some basic building blocks. This section goes through them pair-wise, showing an action and its dual.

A session-typed channel is defined as Chan<E, P> where E is an environment and P is a protocol. The environment E is always () for newly created channels (ie it is empty).

Eps

This is the final step of any terminating protocol. The simplest example is:

type Close = Eps;

Any channel whose type is Chan<E, Eps> implements the close() method that closes the connection. Eps is its own opposite, ie <Close as HasDual>::Dual = Eps

The simplest channels are of type Chan<(), Eps>. All you can do with such channels is to close the connection:

let (a, b) = session_channel::<Eps>();
a.close();
b.close();

Send and Recv

These are the most basic of actions: Transmitting and receiving values. The opposite of a Send with some type T is a Recv of type T.

type S = Send<String, Eps>;
type R = Recv<String, Eps>; // <S as HasDual>::Dual

A channel of type Chan<E, Send<T, P>> implements the method send(T) → Chan<E, P>.

A channel of type Chan<E, Recv<T, Q>> implements the method recv() → (T, Chan<E, Q>).

Choose and Offer

There is the option of making choices in the protocol, for one process to inform the other of a decision. The Choose and Offer constructs model such choices.

type C = Choose<Send<String, Eps>, Recv<String, Eps>>;
type O = Offer<Recv<String, Eps>, Send<String, Eps>>; // <C as Hasdual>::Dual

A channel of type Chan<E, Choose<P, Q>> implements two methods:

• sel1() → Chan<E, P>
• sel2() → Chan<E, Q>

that communicates the choice of protocols P and Q to the other process.

A channel of type Chan<E, Offer<P, Q>> implements offer() → Branch<Chan<E, P>, Chan<E, Q>>. Branch is an enum defined as:

enum Branch<L, R> {
    Left(L),
    Right(R),
}

A call to offer() should then be matched on to figure out which path the other process decided to take.

match c.offer() {
    Branch::Left(c) => …,
    Branch::Right(c) => …,
}

Rec, Var, S and Z

The type Rec implements the ability the recurse in the protocol, ie provides an iterator component. The type Rec<P> allows repeating the protocol P.

A channel of type Chan<E, Rec<P>> implements the method enter() → Chan<(P, E), P>. Calling enter() "stores" the protocol P in the channel environment.

The Var construct is then used to reference protocols stored in the environment. As the environment is essentially a stack, Var takes a counter that is modeled as a Peano number. Var<Z> points to the top of the stack.

A channel of type Chan<(P, E), Var<Z>> implements the method zero() → Chan<(P, E), P>, ie Var<Z> is replaced by P at the top of the stack.

type RS = Rec<Send<String, Var<Z>>>;
type RR = Rec<Recv<String, Var<Z>>>; // <RS as HasDual>::Dual

The following program indefinitely sends some string:

let c: Chan<(), Rec<Send<String, Var<Z>>> = …;
let mut c = c.enter();
loop {
    c = c.send("Hello!".to_string()).zero();
}

Protocols in the environment can also be popped from the stack with Var<S<N>>. This requires there to be at least one protocol in the stack.

A channel of type Chan<(P, E), Var<S<N>>> implements the method succ() -> Chan<E, Var<N>> that peels away the P from the environment and S in the counter.

Putting it all together

Using the constructions from above allows us put together more complex protocols. For example:

type Server = Rec<
                  Offer<
                      Eps,
                      Recv<String, Send<usize, Var<Z>>>
                  >
              >;

It reads:

• In a loop, either:
  • Close the connection
  • Or:
    1. Receive a String
    2. Send back a usize
    3. Go back to the beginning

An example implementation:

let c: Chan<(), Server> = …;
let mut c = c.enter();                  // c: Chan<(Offer<…>, ()), Offer<…>>
loop {
    c = match c.offer() {
        Branch::Left(c) => {            // c: Chan<(Offer<…>, ()), Eps>
            c.close();
            break
        },
        Branch::Right(c) => {           // c: Chan<(Offer<…>, ()), Recv<String, Send<usize, Var<Z>>>>
            let (c, str) = c.recv();    // c: Chan<(Offer<…>, ()), Send<usize, Var<Z>>>
            let c = c.send(str.len());  // c: Chan<(Offer<…>, ()), Var<Z>>
            c.zero()                    // c: Chan<(Offer<…>, ()), Offer<…>>
        }
    };
}

Additional reading and examples

For further information, check out Session Types for Rust and the examples directory.