Session C example

Session C programming

Session C programming starts from designing a communication protocol between parallel/concurrent processes. A protocol describes the interaction between different roles (parallel/concurrent processes).

The toolchain is given as follows:

1. Design global protocol
2. Project global protocol into endpoint protocols for each of the roles
3. Write a program using each endpoint protocol as a communication specification
4. Type check program against protocol by a Session Type Checker to ensure implementation is correct

The end result of using this toolchain is a set of parallel/concurrent processes that is automatically guaranteed communication deadlock-free and all communication endpoints are matched.

Scribble Protocol

A global protocol, which describes the overall interaction of multiple roles is as follows:

// Global protocol
protocol Protocol(role Alice, role Bob, role Carol) {
  int from Alice to Bob;
  int from Bob to Carol;
  rec LOOP {
    int from Alice to Carol;
    int from Carol to Bob;
  }
  int to Carol;
}

An endpoint protocol, projected with respect to one of the roles (Alice) is given as follows. The projection algorithm is briefly described in this research paper.

protocol Protocol at Alice(role Bob, role Carol) {
  int to Bob;
  rec LOOP {
    int from Carol;
    LOOP;
  }
  int to Carol;
}

Session C source code

Session C source code is ordinary C source code, with message-passing based communication using special primitives from the Session C runtime library (libsess.h). Although most features of the C language can be used, some features, especially those involving control-flow of the program, such as switch-case statements or if-then-else statements must be used in a specific way. See this research paper for full details.

#include <libsess.h>
#include <stdlib.h>

int main()
{
  session *s;
  int ival;
  int sum = 0;

  // Begin and initialise a session
  join_session(&argc, &argv, &s, "Protocol_Endpoint.spr");

  // Get roles
  role Bob = s->get_role(s, "Bob");
  role Carol = s->get_role(s, "Carol");

  send_int(Bob, 42);

  while (i<3) {
    recv_int(Carol, &ival);
    sum += ival;
  }

  send_int(Carol, sum);

  // End a session and cleanup
  end_session(s);

  return EXIT_SUCCESS;
}

Type checking

Static type checking by the Session Type Checker (as a clang compiler plugin) is available to check that the source code is implemented as specified by the endpoint protocol. Simply run the below command to invoke the type checker.

clang -Xclang -load -Xclang $LLVM_ROOT/lib/libSessionTypeChecker.so -Xclang -add-plugin -Xclang sess-type-check $CFLAGS source_code.c $LDFLAGS