Virtual Seminar: Multiparty Session Programming with Global Protocol Combinators
Speaker: Dr Rumyana Neykova
Abstract: Checking compatibility of concurrent programs, i.e. if two or more processes can communicate without errors, is a pressing problem in the verification community. State-of-the-art verification tools are limited to model-checkers and SMT solvers, which are foreign to many developers and too computationally expensive to use in practice.
In this talk, I will demonstrate a new approach to programming and verification of concurrent and distributed programs. The approach relies on a few compositional constructs, called global protocol combinator (GPC). I will show an encoding of a popular theory for communicating programs into GPC. Such encoding reveals that the problem of checking compatibility can be reduced to the standard problem of variant/record subtyping. This realisation allows type systems of existing general-purpose programming languages to be utilised for static detection of concurrency bugs, without the need for external model checkers. I will show an implementation of our encoding in native OCaml and will discuss its expressive power and performance. We have tested the approach by implementing and verifying a plethora of concurrency algorithms, as well as several popular communication protocols (DNS, OAuth, and SMPT).
