Expand description
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:
A
sends an integer toB
.B
sends a boolean toA
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§
- This macro plays the same role as the
select!
macro does forReceiver
s. - This macro is convenient for server-like protocols of the form:
- Returns the channel unchanged on
TryRecvError::Empty
.
Structs§
- A session typed channel.
P
is the protocol andE
is the environment, containing potential recursion targets - Heterogeneous selection structure for channels
- Active choice between
P
andQ
- End of communication session (epsilon)
- Passive choice (offer) between
P
andQ
- Enter a recursive environment
- Receive
A
, thenP
- Peano numbers: Increment
- Send
A
, thenP
- Recurse. N indicates how many layers of the recursive environment we recurse out of.
- Peano numbers: Zero
Enums§
Traits§
- The HasDual trait defines the dual relationship between protocols.
Functions§
- Connect two functions using a session typed channel.
- 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.
- An alternative version of homogeneous select, returning the index of the Chan that is ready to receive.
- Returns two session channels