A resource analysis of the pi-calculus

TL;DR

This paper introduces a resource-based semantic framework for the pi-calculus using separation logic, providing simple, fully abstract models for safety and liveness, and developing a logic for processes and resources.

Contribution

It presents a novel resource model distinguishing public and private ownership, refactors operational semantics, and develops simple, fully abstract denotational models for the pi-calculus.

Findings

Developed two fully abstract models for safety and liveness.

Established a connection with separation logic and Brookes's action trace model.

Created a logic of processes and resources based on the models.

Abstract

We give a new treatment of the pi-calculus based on the semantic theory of separation logic, continuing a research program begun by Hoare and O'Hearn. Using a novel resource model that distinguishes between public and private ownership, we refactor the operational semantics so that sending, receiving, and allocating are commands that influence owned resources. These ideas lead naturally to two denotational models: one for safety and one for liveness. Both models are fully abstract for the corresponding observables, but more importantly both are very simple. The close connections with the model theory of separation logic (in particular, with Brookes's action trace model) give rise to a logic of processes and resources.