Using Pi-Calculus Names as Locks

TL;DR

This paper presents a type system for the asynchronous pi-calculus that ensures safe lock usage and deallocation, guaranteeing deadlock-freedom and leak-freedom in concurrent programs.

Contribution

It introduces a novel type system that uses pi-calculus names as locks and guarantees deadlock- and leak-freedom, along with a behavioral equivalence framework.

Findings

Type system guarantees deadlock-freedom

Type system guarantees leak-freedom

Established sound behavioral equivalence

Abstract

Locks are a classic data structure for concurrent programming. We introduce a type system to ensure that names of the asynchronous pi-calculus are used as locks. Our calculus also features a construct to deallocate a lock once we know that it will never be acquired again. Typability guarantees two properties: deadlock-freedom, that is, no acquire operation on a lock waits forever; and leak-freedom, that is, all locks are eventually deallocated. We leverage the simplicity of our typing discipline to study the induced typed behavioural equivalence. After defining barbed equivalence, we introduce a sound labelled bisimulation, which makes it possible to establish equivalence between programs that manipulate and deallocate locks.