Abstract
Advanced type systems for the Pi-calculus have recently been proposed
to guarantee deadlock-freedom in the sense that certain communications
will eventually succeed unless the whole process diverges. Although
such guarantees are useful for reasoning about the behavior of
concurrent programs, there still remains the weakness that the success
of a communication is not completely guaranteed due to the possibility
of divergence. For example, although a server process that has
received a request message cannot discard the request, it is allowed
to infinitely delegate the request to other processes, causing a
livelock. In this paper, we present a type system which guarantees
that certain communications will eventually succeed under fair
scheduling, regardless of whether processes diverge. We also present a
variant of the type system which guarantees that a communication will
succeed within a given number of reduction steps.