Pi Buffers

By: on June 17, 2006

I was recently asked to code up a bi-directional unbounded buffer in the pi-calculus, i.e. a process parameterised by two names x,y that buffers all values received on x and y, and outputs them on y and x respectively. Here is what I came up with, in the syntax of MWB:

agent Cell(c,v,n)    = 'c<v>.'c<n>.0
agent Waiting(x,c,n) = x(v).(^ m)(Cell(n,v,m) | Waiting(x,c,m))
                     + c(w).c(c).Ready(x,c,n,w)
agent Ready(x,c,n,w) = x(v).(^ m)(Cell(n,v,m) | Ready(x,c,m,w))
                     + 'x<w>.Waiting(x,c,n)
agent Buffer(x,y)    = (^ n,m)(Waiting(x,n,m) | Waiting(y,m,n))

Stepping through a few possible traces of the Buffer process in MWB produces the expected result. The main complication in the implementation is the need to prevent the ends of the buffer from consuming their own outputs. This means they cannot be implemented as a parallel composition of an input and output process; we have to use a choice instead.

It should be the case that Buffer(x,y) is weakly bisimilar to (^ z)(Buffer(x,z) | Buffer(z,y)). Unfortunately MWB goes into a spin when trying to prove this, probably because the Buffer process has infinitely many states (since it is an unbounded buffer).


Leave a Reply

Your email address will not be published.

You may use these HTML tags and attributes: <a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <s> <strike> <strong>