Register to build your agenda.

Protocol pipelining in Typed-Protocols


Marcin Szamotulski
IOHK, Software Engineering Lead

I did a PhD degree in pure mathematics (abstract algebra).  After a few years of experience in various programming languages (python, JavaScript, C) I happily settled with Haskell. Currently, I am a software engineering lead at IOHK working on a distributed real-time system (the Cardano cryptocurrency).

Pipelining is a latency hiding technique commonly used in various systems including network applications or processor architecture. I will present a new approach to protocol pipelining in our typed-protocols package. Typed-protocols is an implementation of binary session types in terms of an initial deep encoding. For performance reasons we provide pipelining, which however depends on concurrency and though an elegant solution it restricts the way some application has to be written. I will present how to design pipelining in a typed correct way without these limitations, at an expense of advanced type level programming. The talk will be illustrated by two simple ping-pong protocols. I will also present a proof that client and server applications, whether using pipelining or not, build with the framework are always dual to each other (hence communicate without deadlocks), and if they terminate they terminate at a common terminal state.