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.
Download