Workshop on Session Types using IOHK Typed Protocols Package

This material was prepared for a Monadic Party 2019 workshop on Session Types. It is based on the work of IOHK networking team with collaboration with Well-Typed and Predictable Network Solutions.

It consist of four parts:

Introduction to typed-protocols framework

Typed-protocols package is used at IOHK to develop protocols & network applications. The next release of Cardano crypto-currency is developed using it.

You will need to clone ouroboros-network repository. We will focus on the typed-protocols cabal project.

Example ping-pong protocol and protocol pipelining

The ping pong protocol. Instruction to run the ping pong demo are here.

Simple streaming protocol

A simple streaming protocol is presented in this package, under src/Network/Protocol/Stream. It contains client and server, a CBORG codec, and a demo application which streams a file from your file system over a Unix socket.

To run a demo server:

cabal new-run demo-stream -- server

To stream a single file

cabal new-run demo-stream -- client 10 ./some-file

Assignment

• Extend the streaming protocol to allow streaming of multiple files.
• Extend the demo to stream multiple files.
• Build a pipelined server, which can do protocol pipelining to hide latency.
• Add tests: checkout ping-pong tests suite, how to write property based tests for a protocol and its codec.

Build instructions

• The simplest way is to use cabal new-build (nix-style local build using cabal). You will need a recent cabal-2.4.0.0.

  To build the library:

  cabal new-build lib:monadic-party2019
  

  To build the demo:

  cabal new-build demo-stream