Sections

Due: Thursday, November 15 at 4:00pm
Submission cutoff: Sunday, November 18 at 4:00pm

The goal of this assignment is to deepen your understanding of session types by finding errors in a buggy session type implementation, and by adapting a network communication protocol into a session-typed implementation.

1. Find the bugs (30%)

In src/session_bug.rs, we have provided an implementation of a session types library akin to the version discussed in class. However, just because the theory is sound, that doesn’t mean our translation of theory to code is correct! The provided implementation has three bugs. Your goal is to identify each one and produce a counterexample. A counter example should generally have one of two forms:

  1. Here is something that should be a valid session type, but isn’t.
  2. Here is a program that should adhere to a given session type, but doesn’t.

For example, let’s say we omitted the Chan<Close> implementation (below) from the library:

impl Chan<Close> {
  pub fn close(self) {}
}

Then a valid counterexample would look like this:

/* Session-typed channel is missing an implementation for the Close type.
 * Therefore calling c.close() on a Chan<Close> will fail. */
fn bug() {
  type Server = Close;
  let (c, _): (Chan<Server>, _) = Chan::new();
  c.close();
}

error[E0599]: no method named `close` found for type `session_bug::Chan<session_bug::Close>` in the current scope
  --> src/counterex.rs:6:5
   |
6  |   c.close();
   |     ^^^^^
   |
  ::: src/session_bug.rs:39:1
   |
39 | pub struct Chan<Sigma> {
   | ---------------------- method `close` not found for this

A counterexample should consist of a program along with a short comment describing the reason what the bug is, and why the program is a counterexample (as above). A valid counter example can either be a compile-time type error or a runtime assertion failure. For example, if a buggy channel implementation (somehow) always added 2 to every number sent, then a counter example would be:

fn bug() {
  type Server = Recv<i32, Close>;
  type Client = <Server as HasDual>::Dual;
  let (c1, c2): (Chan<Server>, Chan<Client>) = Chan::new();
  c2.send(0);
  let (c, n) = c1.recv();
  assert_eq!(n, 0); // assertion failed, 2 != 0
}

To test your bugs, you should uncomment the line // mod counterex in lib.rs. Once you have found all the bugs, move them into the written/assign7.tex Latex document. This section will be manually graded by the TAs, not via autograder.

2. Verified TCP (70%)

Next, your main challenge for this assignment is to implement a simplified, session-typed version of the TCP protocol. Before we dive into that, we first need to introduce one last session typing concept, which is the implementation of recursive session types.

Recursive session types

Recall from lecture that in their theoretical formulation, session types are allowed to be recursive. For example, here’s a protocol for an infinite echo server:

To implement this in Rust, we need to introduce a notion of recursion points and type variables, i.e. the and parts. Representing variables in our type system is a tricky problem, but we can simplify by avoiding names entirely and instead using de Bruijn indices. This is the same convention you saw with numbered label scopes in WebAssembly—the number 0 refers to the closest recursion point, 1 refers to the next up, and so on.

This reduces our problem to: how do we write numbers in Rust’s type system? And for that, we will use the Peano numerals, the same construction you saw on assignment 1 in the lambda calculus Church encoding. Specifically we have four new types:

pub struct Rec<S>(PhantomData<S>);
pub struct Z;
pub struct S<N>(PhantomData<N>);
pub struct Var<N>(PhantomData<N>);

Here, Rec<S> represents a recursion point . Z and S<N> are types representing Peano numerals, so S<S<S<Z>>> is the type corresponding to the number 3. Lastly, Var<N> represents a usage of a variable where N is a Peano number. For example, we can translate our echo server as:

type Server = Rec<Recv<String, Offer<Var<Z>, Close>>>;
type Client = <Server as HasDual>::Dual;

And we can implement this protocol:

fn server(c: Chan<(), Server>) {
  let mut c = c.rec_push();
  loop {
    c = {
      let (c, s) = c.recv();
      println!("{}", s);
      match c.offer() {
        Branch::Left(c) => c.rec_pop(),
        Branch::Right(c) => { c.close(); return; }
      }
    }
  }
}

fn client(c: Chan<(), Client>) {
  let mut c = c.rec_push();
  loop {
    c = {
      let c = c.send("echo!".to_string());
      c.left().rec_pop()
    }
  }
}

A few key differences from before. First, our Chan type now has two arguments: an environment Env and a session type S. The environment is similar to the proof context in that it represents a mapping from variables (numbers) to session types. At the start of our protocol, the environment is empty, represented by the unit type ().

Second, channels with outermost session type Rec and Var expose two methods: rec_push() and rec_pop(), respectively. rec_push() means “enter a recursive session”, and rec_pop() means “leave a recursive session”. Multiple rec_pop calls can return across multiple nested recursions. Effectively, rec_push puts the current session type onto the Env stack, and rec_pop removes it from the stack. To implement this, we add the following Chan implementations:

impl<Env, S> Chan<Env, Rec<S>> {
  pub fn rec_push(self) -> Chan<(S, Env), S> {
    unsafe { transmute(self) }
  }
}

impl<Env, S> Chan<(S, Env), Var<Z>> {
  pub fn rec_pop(self) -> Chan<(S, Env), S> {
    unsafe { transmute(self) }
  }
}

impl<Env, S, N> Chan<(S, Env), Var<S<N>>> {
  pub fn rec_pop(self) -> Chan<Env, Var<N>> {
    unsafe { transmute(self) }
  }
}

For another example, we have extended the ATM example from class to use recursive session types in src/atm.rs.

TCP

Now that you have the full power of session types at your fingertips, it’s time to talk networking. TCP, or the Transmission Control Protocol, is a communication protocol that defines a means to reliably transmit bytes over a network connection. We are going to define a protocol that looks loosely like TCP that you are going to implement using session types in Rust. The three core components of the protocol are the handshake, data transfer, and close. We are assuming unidirectional data transfer (from the client to the server).

  1. Handshake: a handshake is a sequence of three messages, a Syn, SynAck, and Ack. Specifically, we have the following types:

    struct Syn;
struct SynAck;
struct Ack;

    The server receives a Syn, responds with a SynAck, receives an Ack, then enters the data transfer phase.

  2. Data transfer: the payload is a series of buffers that the client will attempt to transfer to the server. The client sends each buffer in a Packet objects along with the buffer’s sequence number (which, for our purposes, is just its index in a list of packets the client wants to send). The server will receive some (but not necessarily all) of these packets (i.e. Vec<Packet>), and respond with the list of buffer sequence numbers received (i.e. Vec<usize>). Then the server will offer to enter the close phase if all the packets have been received, otherwise restart the data transfer process.

    type Buffer = Vec<u8>;

struct Packet {
  buf: Buffer,
  seqno: usize
}

    Note: the two types above are actually defined in session.rs to enable our noisy channel implementation, mentioned below.

  3. Close: once the client requests to close the connection, the server will send an Ack and then a Fin, receive a final Ack from the client, and then close the connection at the end of this sequence.

Here is an example of a possible session where the client wants to send three buffers. Curly braces are used to indicate an ordered sequence of values. Note that “Choose close” would normally be a “Fin” in TCP, but in your session type should be a Offer<..., TCPClose> branch (on the server), not a Recv<Fin, ...>.

Given this specification, your task is to implement the following:

type TCPHandshake = /* TODO */
type TCPRecv = /* TODO */
type TCPClose = /* TODO */
type TCPServer = TCPHandshake<TCPRecv<TCPClose>>;
type TCPClient = <TCPServer as HasDual>::Dual;

fn tcp_server(c: Chan<(), TCPServer>) -> Vec<Buffer>;
fn tcp_client(c: Chan<(), TCPClient>, packets: Vec<Buffer>);

First, uncomment the line // pub mod tcp in lib.rs.

Next, you should translate the English specification above into a session type TCPServer. We have helpfully suggested a possible decomposition of this type in src/tcp.rs.

Then, you should implement this session type in the tcp_server and tcp_client functions. tcp_server should return the list of received buffers in sorted order by sequence number.

Lastly, note that unlike a more robust TCP implementation, your protocol does not have to handle timeouts, SYN floods, or anything else. We are assuming the only point of failure is the packet transmission step, where packets can be dropped when sending from the client to the server.

Testing

We’ve given you two tests for your TCP implementation in lib.rs. One uses a standard implementation of Chan as in the session types lecture notes; one uses an implementation of Chan that drops packets with some probability, so that you can test your resend behavior. You can run these tests with cargo test (and cargo test -- --nocapture if you want to debug with print statements).

There should only be one correct implementation of the TCPServer and TCPClient types. When you upload your code to Gradescope, if you see a message in the autograder’s output that says your TCP type is wrong/uncompilable, then you should check your type implementation. If you see “Assignment graded”, that means your TCP type is correct (albeit with no guarantees on tests passing).

Submission

Copy your code and explanationfor each of the three bugs into assign7.tex, make the file, and upload the pdf to Gradescope. Please make sure your code is formatted so as to be readable, i.e. indented in a reasonable manner and not running off the page. To submit the rest of your code, run make_submission.sh and upload the resulting assign7.zip to Gradescope.