Bas van den Heuvel ; Jorge A. Pérez - Asynchronous Session-Based Concurrency: Deadlock-freedom in Cyclic Process Networks

lmcs:10128 - Logical Methods in Computer Science, November 13, 2024, Volume 20, Issue 4 - https://doi.org/10.46298/lmcs-20(4:6)2024
Asynchronous Session-Based Concurrency: Deadlock-freedom in Cyclic Process NetworksArticle

Authors: Bas van den Heuvel ; Jorge A. Pérez

    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.


    Volume: Volume 20, Issue 4
    Published on: November 13, 2024
    Accepted on: August 9, 2024
    Submitted on: October 7, 2022
    Keywords: Computer Science - Logic in Computer Science

    Classifications

    Mathematics Subject Classification 20201

    Consultation statistics

    This page has been seen 992 times.
    This article's PDF has been downloaded 433 times.