A Gentle Overview of Asynchronous Session-based Concurrency: Deadlock Freedom by Typing

TL;DR

This paper reviews recent advances in ensuring deadlock freedom in asynchronous session-based concurrency, highlighting typed process frameworks that guarantee safe communication in message-passing systems.

Contribution

It provides a gentle overview of three typed process frameworks that ensure deadlock freedom in asynchronous session-based concurrency models.

Findings

Three typed process frameworks for deadlock freedom

Application to a concurrent functional language with sessions

Clarification of asynchronous communication in session types

Abstract

While formal models of concurrency tend to focus on synchronous communication, asynchronous communication is relevant in practice. In this paper, we will discuss asynchronous communication in the context of session-based concurrency, the model of computation in which session types specify the structure of the two-party protocols implemented by the channels of a communicating process. We overview recent work on addressing the challenge of ensuring the deadlock-freedom property for message-passing processes that communicate asynchronously in cyclic process networks governed by session types. We offer a gradual presentation of three typed process frameworks and outline how they may be used to guarantee deadlock freedom for a concurrent functional language with sessions.