Resource Usage Analysis for the Pi-Calculus

TL;DR

This paper introduces a novel type-based resource usage analysis for the pi-calculus, enabling static verification of resource access safety and correctness in concurrent programs.

Contribution

It extends behavioral type systems with resource access primitives and provides a sound inference algorithm, pioneering resource analysis for the pi-calculus.

Findings

Developed a type system guaranteeing safe resource access

Implemented a prototype resource usage analyzer

First resource analysis for an expressive concurrent language

Abstract

We propose a type-based resource usage analysis for the π-calculus extended with resource creation/access primitives. The goal of the resource usage analysis is to statically check that a program accesses resources such as files and memory in a valid manner. Our type system is an extension of previous behavioral type systems for the π-calculus, and can guarantee the safety property that no invalid access is performed, as well as the property that necessary accesses (such as the close operation for a file) are eventually performed unless the program diverges. A sound type inference algorithm for the type system is also developed to free the programmer from the burden of writing complex type annotations. Based on the algorithm, we have implemented a prototype resource usage analyzer for the π-calculus. To the authors' knowledge, ours is the first type-based resource usage analysis that deals with an expressive concurrent language like the pi-calculus.