Crate sesh[−][src]
Sesh 🥂
Sesh is an implementation of deadlock-free binary session types with failure in Rust.
What does that mean?
- The session types bit means that it uses Rust types to describe communication protocols, and ensure that they're implemented correctly.
- The binary bit means that for any protocol, there's two parties involved, no more, no less.
- The deadlock-free bit means, well, that if you write your session typed programs using Sesh, and you don't cheat by using other concurrency constructs, your can be sure your programs won't deadlock!
- The with failure bit means Sesh is aware that sometimes programs may fail, and that it takes failure into account. If one of the parties involved in a protocol crashes, like if the thread panics, the Sesh lets the other party know, to make sure it doesn't end up just waiting forever.
The author of this package is an academic, so she is contractually obliged to only come up with uninspiring examples. With that in mind, let's pretend you want a server that does addition. You send it two numbers, and it sends you a number back. There's two session types associated with that protocol. One for the client and one for the server. The type for the server, using Sesh, would be:
type AddServer = Recv<i64, Recv<i64, Send<i64, End>>>;
Session types are always dual. If the client sends a number, the server should be ready to receive a number, otherwise we'd be in trouble. We can get the session type for the client using duality. This just replaces all sends by receives, and vice versa:
type AddClient = <AddServer as Session>::Dual;
Once you've written down the protocol, the hard part is out of the way. Rust will make sure our server follows the protocol:
fn add_server(s: AddServer) -> Result<(), Box<dyn Error>> { let (i, s) = recv(s)?; // Receive the first number. let (j, s) = recv(s)?; // Receive the second number. let s = send(i + j, s); // Send the sum of both numbers. close(s) // Close the session. }
Macros
choose | Choose between many different sessions wrapped in an |
offer | Offer a choice between many different sessions wrapped in an |
Structs
End | End of communication. |
Recv | Receive |
Send | Send |
Traits
Session | Trait for session types. Provides duality. |
Functions
cancel | Cancels a session. Always succeeds. If the partner calls |
choose_left | Given a choice between sessions |
choose_right | Given a choice between sessions |
close | Closes a session. Synchronises with the partner, and fails if the partner has crashed. |
fork | Creates a child process, and a session with two dual endpoints of type |
offer_either | Offer a choice between two sessions |
recv | Receive a value of type |
select | Selects the first active session. Receives from the selected session. Returns the received value, the continuation of the selected session, and a copy of the input vector without the selected session. |
select_mut | Selects the first active session. Receives from the selected session, and removes the endpoint from the input vector. Returns the received value and the continuation of the selected session. |
send | Send a value of type |
Type Definitions
Choose | Choose between two sessions |
Offer | Offer a choice between two sessions |