Asynchronous Session-Based Concurrency: Deadlock-freedom in Cyclic Process Networks

TL;DR

This paper introduces a new session-typed process framework, APCP, and a concurrent lambda calculus, LASTn, both ensuring deadlock-freedom in asynchronous cyclic process networks through theoretical foundations and translations.

Contribution

It presents APCP, a session-typed framework supporting asynchronous communication in cyclic networks, and LASTn, a lambda calculus with deadlock-freedom guarantees transferred from APCP.

Findings

APCP supports deadlock-free asynchronous communication in cyclic networks.

LASTn can be translated into APCP, inheriting deadlock-freedom guarantees.

Meta-theoretical results confirm deadlock-freedom and operational correspondence.

Abstract

We tackle the challenge of ensuring the deadlock-freedom property for message-passing processes that communicate asynchronously in cyclic process networks. Our contributions are twofold. First, we present Asynchronous Priority-based Classical Processes (APCP), a session-typed process framework that supports asynchronous communication, delegation, and recursion in cyclic process networks. Building upon the Curry-Howard correspondences between linear logic and session types, we establish essential meta-theoretical results for APCP, most notably deadlock freedom. Second, we present a new concurrent $\lambda$-calculus with asynchronous session types, dubbed LASTn. We illustrate LASTn by example and establish its meta-theoretical results; in particular, we show how to soundly transfer the deadlock-freedom guarantee from APCP. To this end, we develop a translation of terms in LASTn into processes in APCP that satisfies a strong formulation of operational correspondence.