Recently we’ve been toying with writing a compiler for the π-calculus (here’s where it all started) and last time we modeled a trivial echo web service in π-calculus and found that we were leaking data if we got called by more than one client at a time. The echo service we had written so far:
!e(x).f(r).r<x>.0
The problem is that the service request channels e and f are well-known names. Let’s do something clever with those names:
!e(k).(ν f).k<f>.f(x).f(r).r<x>.0
Now we’ve added a third thing, k, which gets passed to echo before x or r. Not only that, we’re using a new f, and we’re receiving x and r along f now, one at a time. What’s going on here?
What we’re modeling is a private channel. When a client sends a message to e, e effectively says, psst—talk to me on f. Because we used a new f at that point, each client gets a unique f back, which only the client and the echo service know, and the client and service can use their private f to communicate in confidence. I’ve modified some clients to work with this new scheme:
e<c>.c(f).f<n>.f<d>.d(m).0 |
e<g>.g(f).f<i>.f<h>.h(j).0 |
e(k).(ν f).k<f>.f(x).f(r).r<x>.0 |
e(k).(ν f).k<f>.f(x).f(r).r<x>.0
The first two lines are the clients, and the second two are two echo servers. First, the clients initiate contact. As before, because there are two sends on e and two receives on e, either client could talk to either server, but the result is still the same anyway:
c(f).f<n>.f<d>.d(m).0 |
g(f).f<i>.f<h>.h(j).0 |
(ν f).c<f>.f(x).f(r).r<x>.0 |
(ν f).g<f>.f(x).f(r).r<x>.0
This is where ν f is critical. Do you see here, on each line, we really have four different fs. c(f) and g(f) are going to substitute f in the process they’re guarding for whatever they receive. c(f) guards the first line; g(f) the second—those fs are different. (Think of your favorite programming language—if you write two methods, each with a parameter called f, those parameters are different. They just happen to have the same name.) On the last two lines, we have ν f—make a new name f. Let’s make up a couple of new names in place of f:
c(f).f<n>.f<d>.d(m).0 |
g(f).f<i>.f<h>.h(j).0 |
c<a>.a(x).a(r).r<x>.0 |
g<b>.b(x).b(r).r<x>.0
I just used a and b. There’s an infinite supply of fresh names in π-calculus, even though we’re just using single letters here.
Now the servers communicate those new names back to their clients:
a<n>.a<d>.d(m).0 |
b<i>.b<h>.h(j).0 |
a(x).a(r).r<x>.0 |
b(x).b(r).r<x>.0
The right client gets the right channel name because they provided their own names to receive the channel on. And now you can see we have four processes, and two are linked by a channel a; and two are linked by a channel b; and there’s no concern about the echo service echoing the wrong thing:
a<d>.d(m).0 |
b<h>.h(j).0 |
a(r).r<n>.0 |
b(r).r<i>.0
Next step:
d(m).0 |
h(j).0 |
d<n>.0 |
h<i>.0
d gets n; h gets i. echo is handling multiple clients and not confusing them.
If you thought that was exhausting, it’s because we just reinvented a method call in π-calculus! Our ‘trick’ is to establish a private channel and then send the arguments (however many we like, but here there are just two—x and r) along the channel. Using a private channel avoids any confusion between multiple concurrent invocations of the same method. It’s not every day that we get to design the way we’re going to implement a method call! In this tiny calculus there’s the power and flexibility to do many different things. Some—like the method call—are traditional. But we also have the power to invent something completely new.
That’s enough of the formalism for now. Next time let’s turn it into a programming language!
