The Buffered π-Calculus: A Model for Concurrent Languages

Abstract

Message-passing based concurrent languages are widely used in developing large distributed and coordination systems. This paper presents the buffered $π$-calculus --- a variant of the $π$-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 $π$-calculus can be fully simulated in the polyadic $π$-calculus with respect to strong bisimulation. In contrast to the $π$-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 $π$-calculus: the (core) Go language and the (Core) Erlang. Both encodings are fully abstract with respect to weak bisimulations.