The Buffered \pi-Calculus: A Model for Concurrent Languages

TL;DR

The paper introduces the buffered π-calculus, a variant of the π-calculus that models asynchronous communication with buffered channels, enabling practical and clear modeling of real-world concurrent languages like Go and Erlang.

Contribution

It presents the buffered π-calculus, demonstrating its full simulation in the polyadic π-calculus and its ability to encode real-world concurrent languages.

Findings

Buffered π-calculus can be fully simulated in the polyadic π-calculus.

It enables clear modeling of practical concurrent languages.

Core Go and Erlang are fully encoded in the buffered π-calculus.

Abstract

Message-passing based concurrent languages are widely used in developing large distributed and coordination systems. This paper presents the buffered $\pi$-calculus --- a variant of the $\pi$-calculus where channel names are classified into buffered and unbuffered: communication along buffered channels is asynchronous, and remains synchronous along unbuffered channels. We show that the buffered $\pi$-calculus can be fully simulated in the polyadic $\pi$-calculus with respect to strong bisimulation. In contrast to the $\pi$-calculus which is hard to use in practice, the new language enables easy and clear modeling of practical concurrent languages. We encode two real-world concurrent languages in the buffered $\pi$-calculus: the (core) Go language and the (Core) Erlang. Both encodings are fully abstract with respect to weak bisimulations.