Process Declarations in Pica

May 13 2007 Published by under Pi Calculus

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

No responses yet

  • Julia says:

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

  • Shouldn't that second declaration be
    proc B[] shows [a:X,b:Y] ??

  • Steve Massey says:

    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?

  • Mark C. Chu-Carroll says:

    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.

  • Xanthir, FCD says:

    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.

  • Daniel says:

    Is pica dead? 🙁

  • Mark C. Chu-Carroll says:

    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.

  • Mike says:

    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.

  • davide says:

    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.

Leave a Reply