The Buffered Pi-Calculus: A Model for Concurrent Languages
Xiaojie Deng, Yu Zhang, Yuxin Deng and Farong Zhong
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.