Uniqueness Typing for Resource Management in Message-Passing Concurrency

TL;DR

This paper introduces a type system for message-passing concurrency that manages channel resources safely by combining uniqueness and affine typing, preventing runtime errors in resource-constrained environments.

Contribution

It extends the pi-calculus with resource management primitives and a novel type system to ensure safe reuse of channels in message-passing programs.

Findings

The type system effectively prevents ill-behaved programs with resource errors.

Channels can be safely reused for different types without runtime issues.

The approach enhances resource management in concurrent message-passing systems.

Abstract

We view channels as the main form of resources in a message-passing programming paradigm. These channels need to be carefully managed in settings where resources are scarce. To study this problem, we extend the pi-calculus with primitives for channel allocation and deallocation and allow channels to be reused to communicate values of different types. Inevitably, the added expressiveness increases the possibilities for runtime errors. We define a substructural type system which combines uniqueness typing and affine typing to reject these ill-behaved programs.