Contrasting Deadlock-Free Session Processes (Extended Version)

TL;DR

The paper analyzes deadlock-freedom (DF) in concurrent, message-passing systems through a comparative lens on three type systems: SP (a core session-pTyped pi-calculus), HCP (hypersequent-based CP), and Padovani’s P for asynchronous processes. It shows that hypersequents in HCP do not fundamentally expand the class of DF processes beyond what linear logic already yields and establishes precise relationships between HCP and P, including asynchronous variants, via SP as a baseline. Two technical techniques, commuting conversions and disentanglement, are key: they enable transforming HCP processes with delayed actions and self-synchronizations into DF-equivalent forms that align with CP and Padovani’s frameworks. The results hold for both synchronous and asynchronous communication and have practical implications for static analysis and the design of concurrent languages, clarifying essential mechanisms for statically avoiding deadlocks. Overall, the work deepens understanding of how different type-system perspectives relate to DF and demonstrates how asynchrony can be integrated without compromising deadlock guarantees.

Abstract

Deadlock freedom is a crucial property for message-passing programs. Over the years, several different type systems for concurrent processes that ensure deadlock freedom have been proposed; this diversity raises the question of how they compare. We address this question, considering two type systems not covered in prior work: Kokke etal's HCP, a type system based on a linear logic with hypersequents, and Padovani's priority-based type system for asynchronous processes, dubbed P. Their distinctive features make formal comparisons relevant and challenging. Our findings are two-fold: (1) the hypersequent setting does not drastically change the class of deadlock-free processes induced by linear logic, and (2) we relate the classes of deadlock-free processes induced by HCP and P. We prove that our results hold under both synchronous and asynchronous communication. Our results provide new insights into the essential mechanisms involved in statically avoiding deadlocks in concurrency.

Figures (13)

• Figure 1: Overview of main results (simplified version). $\mathbb{H}_{\mathsf{F}}$, $\mathbb{H}_{\mathsf{R}}$, $\mathbb{P}$, $\mathbb{C}$, and $\mu\mathbb{P}$ stand for classes of deadlock-free $\mathcal{\mathsf{SP}}\xspace$ processes. The red arrow represents optimizations (commuting conversions and disentanglement) that relate $\mathbb{H}_{\mathsf{F}}$ and $\mathbb{H}_{\mathsf{R}}$. The green lines denote the correspondence $\mathbb{C} = \mu\mathbb{P}$. The dotted line means that $P'$ and $P"$ are the representatives of $P$ in $\mathbb{H}_{\mathsf{R}}$ and $\mathbb{P}$, up to an encoding.
• Figure 2: $\mathcal{\mathsf{SP}}\xspace$: Reduction semantics (top) and structural congruence (bottom).
• Figure 3: $\mathcal{\mathsf{SP}}$: Typing Rules for Processes.
• Figure 4: $\mathsf{CP}\xspace$: Typing rules for processes.
• Figure 5: $\mathcal{\mathsf{HCP}}\xspace$: Typing rules for processes.

Theorems & Definitions (117)

• Definition 1: $\mathcal{\mathsf{SP}}\xspace$: Reduction
• Definition 2: $\mathcal{\mathsf{SP}}\xspace$: Session Types and Typing Environments
• Definition 3: $\mathcal{\mathsf{SP}}\xspace$: Duality
• Definition 4: $\mathcal{\mathsf{SP}}$: Typing Judgment and Typing Rules
• Theorem 5: $\mathcal{\mathsf{SP}}$: Preservation vasco_sess_typ
• Definition 6: $\mathcal{\mathsf{SP}}$: Well-formedness
• Theorem 7: Safety vasco_sess_typ
• Corollary 8: vasco_sess_typ
• Definition 9: $\mathcal{\mathsf{SP}}\xspace$: Deadlock Freedom
• Example 10: $\mathcal{\mathsf{SP}}$: A Typable but Deadlocked Process