Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Bas van den Heuvel, Jorge A. Pérez

TL;DR

This work presents Asynchronous Priority-based Classical Processes (APCP), a session-typed process framework that supports asynchronous communication, delegation, and recursion in cyclic process networks, and presents a new concurrent $\lambda$-calculus with asynchronous session types, dubbed LASTn.

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 $λ$-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.

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

TL;DR

This work presents Asynchronous Priority-based Classical Processes (APCP), a session-typed process framework that supports asynchronous communication, delegation, and recursion in cyclic process networks, and presents a new concurrent -calculus with asynchronous session types, dubbed LASTn.

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 -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.
Paper Structure (57 sections, 31 theorems, 267 equations, 22 figures, 1 table)

This paper contains 57 sections, 31 theorems, 267 equations, 22 figures, 1 table.

Table of Contents

  1. Introduction
  2. Deadlock Freedom
  3. Functional Calculi with Concurrency
  4. Contributions
  5. Organization
  6. Origin of the results
  7. Motivating Examples
  8. Milner's Cyclic Scheduler in APCP
  9. The Scheduler, Informally
  10. Syntax of APCP
  11. The Scheduler in APCP
  12. A Bookshop Scenario in LASTn
  13. APCP: Asynchronous Priority-based Classical Processes
  14. The Process Language
  15. A Convenient Notation
  16. ...and 42 more sections

Key Result

Theorem 3.16

Rules [typ-send$\ast$] and [typ-sel$\ast$] in f:APCP:typingRules (bottom) are derivable, and Rule [typ-lift] in f:APCP:typingRules (bottom) is admissible.

Figures (22)

  • Figure 1: Milner's cyclic sche-duler with 6 workers. Lines denote channels connecting processes on the indicated names.
  • Figure 2: Definition of APCP's process language.
  • Figure 3: Structural congruence for APCP: axioms.
  • Figure 4: The typing rules of APCP (top) and derivable rules (bottom).
  • Figure 5: Proof that Rules [typ-send$\ast$] and [typ-sel$\ast$] are derivable (cf. \ref{['t:APCP:derivable']}).
  • ...and 17 more figures

Theorems & Definitions (94)

  • Definition 3.1: APCP Syntax
  • Definition 3.3: Structural Congruence ($\equiv$) for APCP
  • Example 3.4
  • Definition 3.5: Session Types for APCP
  • Definition 3.6: Duality
  • Definition 3.7: Priorities
  • Example 3.8
  • Definition 3.9: Lift
  • Definition 3.10: Top Priority
  • Example 3.11
  • ...and 84 more