Process Declarations in Pica

Sorry for the slow pace of things around here lately; life interferes sometimes. I've mentioned my fathers illness before; things took a drastic change for the worse a week ago, which made things more than a little bit crazy. Of course, life wouldn't be life in things happened one at a time; so naturally, my asthma picked now to act up as well, so I've been coughing my lungs out. It's been a fun week, really.

Anyway, I've been wanting to look a bit more at Pica. I've been thinking about how a
named process definition looks, and what it does. The type part of a definition is
relatively straightforward: a process is defined by a set of externally visible channels; each channel is defined by a type. In a named definition, there are two types of channels to think about. One is a set of channels supplied to the process when it's created; the other is a set of channels created by the process, but which are 'exported': that is, made visible to other processes. The type of a process is a tuple of all of the channels which
the process exports the outside world.

Of course, there's always a hitch, right? Nothing is ever simple. One of the defining characteristics of the π-calculus is mobility: channels can be moved around. A process can send a channel to another process, and no longer retain any ability to use it; or it can receive a channel via a message from some other process, effectively adding an externally visible channel; and finally, it can create a new channel via "new", and then
send that channel via a message to another process, effectively adding a new externally visible channel.

For the purposes of declaring a process and its channels, we'll adopt the
following rules:

  1. A process type declares a set of fundamental channels for the process. Identifiers for a processes fundamental channels are treated as being immutable variables
    associated with a process instance.
  2. A process may have more channels associated with it than its fundamental
    channels - but those channels do not affect its static type.

The basic syntax of processes is the following pattern:

    proc Name[pchannels...] shows [echannels...] does
       process-body-stuff
    end

where:

  • pchannels is a set of fundamental channels associated
    with the process, and which are supplied to the process as parameters when a process
    instance is created; and
  • echannels is a set of fundamental channels associated with
    the process, and which are created by an implicit "new" when a process instance is
    created.

So, for example, let's bring back the old storage cell example from an earlier post.
We wrote that in π-calculus syntax as:

    NewCell[creator,initval]≡new(read,write).{Cell[read,write,initval]
                                              | !creator(read,write) }
    Cell[read,write,val]≡{!read(val).Cell[read,write,val]
                          + ?write(v).Cell[read,write,v]}

In Pica syntax, that would be:

    proc Cell[init:Val] shows [read:Val,write:Val] does
         !read(init).Cell[init]
      || ?write(v).Cell[v]
    end

It looks a lot simpler than the π-calculus version, but the differences are pretty much all syntactic sugar. One of the syntax tricks that I've used for the Pica version is creating a syntactic distinction between "invoking" a process definition, and instantiating a process. In the π-calculus version, we didn't have that distinction. The split between "NewCell" and "Cell" in the π-calculus version, and the existence of "read" and "write" as parameters of "Cell" are all artifacts of that - we needed to explicitly separate the process invocation that would create a new cell. For Pica, when we just refer to a process by name, we'll treat that as an in-place invocation of the named processes behavior in the current process. So recursively invoking "Cell" inside of "Cell" just continues "Cell", re-using its exported channels. So just invoking "Cell" won't create new copies of its fundamental exported channels. To really create a new process with new channels, you'd need to invoke it via "spawn Cell[v]".

Creating this distinction does, of course, introduce some trouble. Since new channels aren't created unless you do a spawn, what does the following mean?

    proc A[] shows [x:X,y:Y] does
          something.B[]
    end

    proc B[] shows [a:X,b:X] does
      something
    end

When "A" invokes the behavior of "B", what's the value of the "a" channel of B? Or the "b" channel of B? We need some more syntax to allow us to say how to assign name bindings
of fundamental channels when we invoke a processes behavior without spawning it. The easiest part of that is that we'll just say that if "A" invokes "B", and B has a fundamental channel which matches a fundamental channel of "A" in both name and type, the matches channels will be unified. For other channels, we'll steal some syntax from the reduction rules:

    proc A[] shows [x:X,y:Y] does
         something.B[][x/a,y/b]
    end

    proc B[] shows [a:X,b:X] does
      something
   end

So when we invoke a process as a behavior, if its channel names don't match, then we can add a second set of "[]"s which specify how to match the names.

One last thing for today. Suppose we have an instantiated process P, with visible channels [a:X,b:Y]. To reference process P's channel "a", you'd use the syntax "P::a".

More like this

As a refresher for me, and to give some examples to help you guys understand it, I'm going to go through a couple of examples of interesting things you can build with π-calculus. We'll start with a simple way of building mutable storage. Before getting started, I'm going to be annoying and change…
As I did with my first attempt at explaining π-calculus, I think that before getting into any of the deep semantics, it's good to look at a few examples of things you can build with π-calculus. But before getting to the meat of the post, I'll give you the answer the puzzle I left in the last post…
Now that things are settling down a little bit, I wanted to get back to the stuff I was writing about π-calculus. But looking back at what I've already written, I think I did a terrible job of introducing it. So I'm going to start over, and try to be more clear. I'll start with a basic refresher…
Ok. So I'm still tweaking syntax, to try to find a way of writing π-calculus in a way that's easy for me to write in my editor, and for you to read in your browser. Here's the latest version: Sequential Composition: Process1.Process2. Send expressions: !channel(tuple).Process Receive…

Sorry to hear about your dad, and your asthma!

At least your wife didn't spend the morning of Mother's Day in the ER with one of her kids, right? (That didn't happen to me, but a friend of mine had to deal with that today. I was the kid that had to go to the ER on Mother's Day 29 years ago.)

Isn't making the echannels publicly visible rather than explicitly sending them back to the creator quite a fundamental change, in that it becomes harder to analyze where they are being used?

Are the pchannels also visible?

By Steve Massey (not verified) on 14 May 2007 #permalink

Steve:

Making the echannels visible is a fairly big change - but it's not quite as bad as it might seem.

When hacking π-calculus programs, it's easy to develop a sense that you've got a well-isolated component when, in fact, you don't. Channels leak all over the place in non-trivial π-calculus systems, and you have to design your system with the idea that most kinds of hygiene only exist if you're incredibly careful, and you put a lot of trust in your clients.

That second bit is the really tricky part. *If* you make your channel names available outside of your process at all, then you are relying on your clients to behave in a trustworthy way. But in any meaningful distributed system, you can't trust your clients. So making your channels available outside your process at all is introducing a degree of insecurity that your code needs to guard agaist. The idea that only sending the channels to your "creator" gives you additional security is a dangerous illusion.

But also - there's one other trick in there. The exported channels of a process P are only visible to other processes that have some way of specifying process P. In the syntax, we haven't gotten to process names yet - but process names are really just syntactic sugar for a special channel that uniquely identifies a process - and that channel is only available to the creator of the process unless it passes it elsewhere. So effectively, the echannels are just a shorthand which makes it easier for the creator of a process to get multiple channels from a process without
having to declare them as separate variables.

No, the pchannels are not externally visible.

Very cool. Pchannels fix what was, for me, the hardest part of doing π-calc programming. Having a set of consistent channels makes everything so much easier, and actually makes recursion seem possible (it was of course possible before, but more difficult with the framework you had to build).

Even just with this bit I'm suddenly turned on to pica.

By Xanthir, FCD (not verified) on 14 May 2007 #permalink

Is pica dead? :(

No, it's not dead - I've just been busy. The next stage for it is to start
some amount of implementation. I've been trying to find time to write a parser for it. When I manage to do that, I'll start on the next bit, which is figuring out
how to use expressions inside of a process body. I promise, there'll be more pica soon.

Just stumbled across this Pica stuff recently. Incidentally, not the first time that a search has lead me to wander around these here parts.

At any rate, I was surprised at some of the ground covered (Cell BE processor, Erlang etc.) The neatest thing that I've gotten out of this blog so far was the reference to PICT. Surprise #1 -- "Programming in the Pi Calculus" was written by Benjamin Pierce. Peeking at the typing rules in chapter 5, the style is very TAPL-ish (hopefully that will help in understanding it).

I also like their notation better than the notation in the Milner paper -- e.g.

- * seems more intuitive for replication than !,
- x!y seems more intuitive for "send y on x" than {overbar}x(y)
- y?w seems more intuitive for "receive on y, binding to w" than y(w)

Just reading chapter 1 of "Programming in the Pi Calculus", I'm starting to wonder about the possibility of a PICT(ish?) meta-language for Erlang. Maybe further reading will cure me of it.

Hi, what about yout pica lang project on google code? Your work so far was so good and I really need some stuff like pica.