Deadlock-free Context-free Session Types

TL;DR

The paper addresses deadlocks in statically verifiable, message-passing programs governed by context-free session types, extending CFSTs with a priority-based deadlock-freedom mechanism. It integrates polymorphism over priorities and non-regular recursion, enabling cycling networks like Milner's scheduler and tree-structured protocols while preserving type safety. The authors prove type preservation and deadlock-freedom, and demonstrate the approach via Milner's scheduler and tree-exchange examples, aided by an external priority oracle. It advances practical verification by aligning with the FreeST language and outlining paths to automation and compiler integration.

Abstract

We tackle the problem of statically ensuring that message-passing programs never run into deadlocks. We focus on concurrent functional programs governed by context-free session types, which can express rich tree-like structures not expressible in standard session types. We propose a new type system based on context-free session types: it enforces both protocol conformance and deadlock freedom, also for programs implementing cyclic communication topologies with recursion and polymorphism. We show how the priority-based approach to deadlock freedom can be extended to this expressive setting. We prove that well-typed concurrent programs respect their protocols and never deadlock.

Figures (14)

• Figure 1: Syntax of types.
• Figure 2: Syntax of priorities and priority variables.
• Figure 3: Polymorphic and priority typing contexts.
• Figure 4: Type formation.
• Figure 5: Type duality on session types.

Theorems & Definitions (16)

• Lemma 1: Strengthening
• Lemma 2
• Lemma 3: Agreement for process formation
• Lemma 4: Weakening
• Theorem 5
• Lemma 6
• Lemma 7: Value substitution
• Lemma 8: Type substitution
• Lemma 9: Priority substitution
• Lemma 10: Type Preservation: Expressions