Crate session_types

session_types

This is an implementation of session types in Rust.

The channels in Rusts standard library are useful for a great many things, but they’re restricted to a single type. Session types allows one to use a single channel for transferring values of different types, depending on the context in which it is used. Specifically, a session typed channel always carry a protocol, which dictates how communication is to take place.

For example, imagine that two threads, A and B want to communicate with the following pattern:

1. A sends an integer to B.
2. B sends a boolean to A depending on the integer received.

With session types, this could be done by sharing a single channel. From A’s point of view, it would have the type int ! (bool ? eps) where t ! r is the protocol “send something of type t then proceed with protocol r”, the protocol t ? r is “receive something of type t then proceed with protocol r, and eps is a special marker indicating the end of a communication session.

Our session type library allows the user to create channels that adhere to a specified protocol. For example, a channel like the above would have the type Chan<(), Send<i64, Recv<bool, Eps>>>, and the full program could look like this:

extern crate session_types;
use session_types::*;

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

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() {
    connect(srv, cli);
}

Re-exports

pub use Branch::*;

Macros

chan_select

This macro plays the same role as the select! macro does for Receivers.

offer

This macro is convenient for server-like protocols of the form:

try_offer

Returns the channel unchanged on TryRecvError::Empty.

Structs

Chan

A session typed channel. P is the protocol and E is the environment, containing potential recursion targets

ChanSelect

Heterogeneous selection structure for channels

Choose

Active choice between P and Q

Eps

End of communication session (epsilon)

Offer

Passive choice (offer) between P and Q

Rec

Enter a recursive environment

Recv

Receive A, then P

S

Peano numbers: Increment

Send

Send A, then P

Var

Recurse. N indicates how many layers of the recursive environment we recurse out of.

Z

Peano numbers: Zero

Enums

Branch

Traits

HasDual

The HasDual trait defines the dual relationship between protocols.

Functions

connect

Connect two functions using a session typed channel.

hselect

Homogeneous select. We have a vector of channels, all obeying the same protocol (and in the exact same point of the protocol), wait for one of them to receive. Removes the receiving channel from the vector and returns both the channel and the new vector.

iselect

An alternative version of homogeneous select, returning the index of the Chan that is ready to receive.

session_channel

Returns two session channels