A Multiparty Session Typing Discipline for Fault-tolerant Event-driven Distributed Programming

Correctly designing and implementing distributed systems software is notoriously difficult. Multiparty session types (MPSTs) is a typing discipline for concurrent processes that statically ensures properties such as freedom from message reception errors and deadlocks. The existing approaches in MPSTs cannot, however, be applied to a significant class of real-world distributed systems because they do not support practical specification and verification of protocols that handle and recover from partial failures.
This paper presents the first formulation of MPSTs for practical fault-tolerant distributed programming. We tackle the long-standing challenges faced by session types in this context: bringing structure to communication patterns involving asynchronous and concurrent partial failures, and integrating the range of features required to express fault-tolerant protocols in practice, that involve dynamic replacement of failed parties and retrying failed protocol segments in the presence of imperfect failure detection. Key to our approach is that we develop the first model of event-driven concurrency for multiparty sessions, to unify the session-typed handling of failures and regular I/O events. Moreover, the characteristics of our model allow us to prove a global progress property for well-typed processes engaged in multiple concurrent sessions, which does not hold in traditional MPST systems. To demonstrate its practicality, we implement our approach as a toolchain for Scala, and use it to specify and implement a session-typed version of the cluster manager (CM) system of the widely employed Apache Spark data analytics engine. Our session-typed CM integrates with the other vanilla Spark components to give a functioning Spark runtime; e.g., it can execute existing third-party Spark applications.

Presented at OOPSLA 2021, part of SPLASH 2021.
By Malte Viering, Raymond Hu, Patrick Eugster, Lukasz Ziarek