LShift Ltd.

Pi Buffers

June 17th, 2006 matthias

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

Entry Filed under: Technology, Programming