Last time we looked at the syntax and semantics of the π-calculus. Let’s get concrete for a moment and think of how we can write something with what we saw. What’s the simplest internet service you can imagine? I guess it’s echo, which just gives back whatever you send it. Let’s start simple: we’re going to receive something:
e(x).mumble
I’m using e for echo, and x for what we get. We’re starting with a fragment of a process, because e is not defined. Somewhere there has to be a (ν e) defining e. Let’s just assume our echo service is so popular that e is a well-known name.
Now we need to send x somewhere, but the only things we know about at this point are e and x! We actually need to receive two things—x, and where to send the reply:
e(x).f(r).r<x>.0
This receives x on channel e, then waits for r on channel f, and then just sends x on channel r.
The best part about having defined all of the reduction rules last time is that we can simulate the execution of our service. Let’s say we have a client who sends something to the echo service, and waits for a response:
(ν c).(ν n).e<n>.f<c>.c(m).0
Just read it left-to-right: there’s this thing c, another thing n; send n to e; send c to f; receive something on c and call it m; done. Let’s put this alongside our service, and step through the reduction rules to see how they interact. I’m dropping the (ν c).(ν n); they don’t really have an operational impact, they just say c and n exist. To begin, we have:
e<n>.f<c>.c(m).0 | e(x).f(r).r<x>.0
Then we apply the message send/receive rule, and we have:
f<c>.c(m).0 | (f(r).r<x>.0)[n/x]
We’ve dropped the send n on e and receive x on e; now we need to replace x with n as the rule states:
f<c>.c(m).0 | f(r).r<n>.0
Now there’s a send/receive on f:
c(m).0 | r<n>.0 [c/r]
And replacing c for r gives:
c(m).0 | c<n>.0
Now it looks as though n is set to be echoed back on c. Watch:
0 [n/m] | 0
As m doesn’t occur in 0 it seems as though the client just throws away what we echo back. From now on I’m going to do send/receive-and-substitute in one step. Let’s keep executing! Where were we?
0 | 0
We know 0 | Q = Q, so we’re left with:
0
And there’s nothing more we can do. We’ve exhausted all of the processes.
There are two major shortcomings to our echo web service. The first problem is: it only runs once! As the echo service executes it tears itself down and we’re left with 0. Let’s add a bang so it’s available forever:
!e(x).f(r).r<x>.0
Remember, !P means something like P | P | P | … With a bang out the front there’s an infinite number of copies of our echo service and it’s effectively available all the time, to any client.
Here’s the second major shortcoming: There’s nothing stopping clients getting their requests and replies all mixed up now! Let’s take two echo services and two clients:
e<n>.f<c>.c(m).0 | e<u>.f<k>.k(v).0 | e(x).f(r).r<x>.0 | e(x).f(r).r<x>.0
Let’s reduce! First, either send on e could match either receive on e, but that’s no problem, whichever you chose, the result is the same (because P | Q = Q | P):
f<c>.c(m).0 | f<k>.k(v).0 | f(r).r<n>.0 | f(r).r<u>.0
Now non-determinism will bite us! As before, either send (this time on f) could match either receive, but unlike before, these processes have remembered n and u. If we reduce one way, we get:
c(m).0 | k(v).0 | c<n>.0 | k<u>.0 (This is the one we intuitively expect.)
And if we reduce the other way, we get:
c(m).0 | k(v).0 | k<n>.0 | c<u>.0 (This swaps the responses!)
In this second case the process that sent n gets u, and the process that sent u gets n. Our echo service is broken! Until next time, can you think of a trick to mend it?
