On the Monitorability of Session Types, in Theory and Practice (Extended Version)

TL;DR

This paper explores the theoretical foundations and practical implementation of session type monitoring in distributed systems, establishing new formal results and providing a Scala toolkit for runtime verification of communication protocols.

Contribution

It introduces a novel formal model for session-monitored processes and proves new results on monitorability, bridging static and runtime verification, and provides a practical Scala toolkit for monitor generation.

Findings

Formal model of session-monitored processes developed

Proved soundness and completeness of session type monitors

Scala toolkit successfully generates executable session monitors

Abstract

In concurrent and distributed systems, software components are expected to communicate according to predetermined protocols and APIs - and if a component does not observe them, the system's reliability is compromised. Furthermore, isolating and fixing protocol/API errors can be very difficult. Many methods have been proposed to check the correctness of communicating systems, ranging from compile-time to run-time verification; among such methods, session types have been applied for both static type-checking, and run-time monitoring. This work takes a fresh look at the run-time verification of communicating systems using session types, in theory and in practice. On the theoretical side, we develop a novel formal model of session-monitored processes; with it, we formulate and prove new results on the monitorability of session types, connecting their run-time and static verification - in terms of soundness (i.e., whether monitors only flag ill-typed processes) and completeness (i.e., whether all ill-typed processes can be flagged by a monitor). On the practical side, we show that our monitoring theory is indeed realisable: building upon our formal model, we develop a Scala toolkit for the automatic generation of session monitors. Our executable monitors can be used to instrument black-box processes written in any programming language; we assess the viability of our approach with a series of benchmarks.