A Gentle Overview of Asynchronous Session-based Concurrency: Deadlock Freedom by Typing
Bas van den Heuvel, Jorge A. Pérez
TL;DR
The paper addresses deadlock freedom in asynchronous, session-based concurrency and presents a graduated framework: AP establishes a baseline asynchronous session calculus, ACP introduces a CP-like structure to guarantee deadlock freedom for tree-like topologies, and APCP adds priority-based typing to handle cyclic topologies. It then connects these foundations to LAST n by providing a translation from LAST n configurations to APCP-enabled AP processes, with operational soundness ensuring deadlock-freedom for closed programs when APCP typing holds. The work blends logic-based and priority-based approaches to yield a versatile verification toolkit for asynchronous session-typed systems, and it sketches implications for multiparty protocols and decentralized verification. Overall, the results offer a cohesive path from simple asynchronous sessions to deadlock-free cyclic networks, with practical impact for programming languages and distributed systems that rely on session-typed communication.
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.