Building Things in π-Calculus: Storage Cells

Mar 22 2007 Published by under Pi Calculus

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 the syntax a bit. Typeset π-calculus uses a channel name by itself for "receive message on channel", and the channel name with an overbar for "send message on channel". In yesterdays post, I used the unmarked channel name for receive, and added a "*" prefix for send. Playing with that, I find it very hard to read. So I'm going to start using a prefix for all uses of channel names: "?" for receive, and "!" for send.

First,we'll try to build a storage cell. A storage cell is a process that can store a value; and it provides channels that you can use to either receive a copy of its current value, or send it a new value.

Let's start with a very naive attempt at a cell.

Cell[val]= (νread,write)( !read(val).Cell[val]
+ ?write(v).Cell[v])

What that says is: "Cell" is a shorthand for a process expression which is parametric in a value, called "$val". Cell introduces its own read and write channels, and then either allows a client to read (which means cell writes to the channel that others might want to read from), followed by recursively invoking "Cell" on the same value; or it allows a client to update the value by writing a value to its "write" channel (in which case Cell reads from the channel and then recursively invokes cell with the new value.)

So this is a simple updatable storage cell. Almost.

What's wrong with it? A couple of things about the channel names:

  1. The (νread,write) creates two channels, local to the Cell process. That
    means that no one outside of the cell process can see them! They're initially scoped
    to Cell, and there's no method inside of Cell to send the channel name outside of its
    name-scope. So it's a storage cell, but no one can ever actually read it or write to it.
  2. The ν that creates the channel is inside of the part that is invoked
    recursively. So each time that "Cell" is invoked, it creates new channel names.

So, how can we fix that? Let's start by fixing the second problem, and make it always use the same names. We'll split it into two different definitions: one which creates a new cell (and allocates its channel names), and one which takes the channels that it should use or read and write.

NewCell[val]=(νread,write)Cell[read,write,val]
Cell[read,write,val]=  !read(val).Cell[read,write,val]
+ ?write(v).Cell[read,write,v])

Now we've got a cell which creates its channels once, and then just keeps reusing the same channels. That's a good start. Now, the remaining problem is that we don't have any way to tell a client what the names o the channels are. To fix that, we'll just add a parameter to NewCell, which is the name of a channel where we should send the names of the read and write channels.

NewCell[creator,initval]=(ν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])

So now, we're in good shape. We can create a storage cell. When we create it, it gets one set of channel names for reading and writing, and it sends those back to whoever created the cell, so that they'll be able to read from and write to it.

How would we use it? Let's just throw together a bit of code.

(ν me)( NewCell[me,0]
| ?me(r,w).!w(7).?r(x).!out(x) )

This creates a new cell; receives a message from the cell containing its read and write channels; then it sets the cell contents to 7; reads the cell contents into a variable "x",
and sends the contents it just read to an output channel.

No responses yet

  • Ørjan Johansen says:

    Are you sure using ! for sending is a good idea? The character ! is already used for repetition.
    Also, does the + operator actually wait until it knows which of the parts can be performed? Otherwise you may get deadlock with 50% probability each step.

  • I second the notion that ! is a poor choice for "send", unless you go and redefine the character that means "repeat".
    Personally, as the opposite of "?", it seems most natural to me to use "¿", but I understand that for most people (at least, on this side of the Atlantic) typing that character is difficult.
    Another possibility is to use <chan for read and >chan for write; however, if you do that your commentors will curse scienceblogs administration loudly for not upgrading their MT install to at least version 3.32. (write a comment with lots of < and > characters, preview it, then preview it again.)
    (Incidentally, failing to do that upgrade leaves SB open to a trivial type 1 XSS attack - if you have any influence to push them with, please do)
    Perhaps {read and }write? Maybe `read and 'write ? Or how about `read and ~write ?
    Also, you're going to need a more easily typeable symbol for ν. Now that you've removed * from being used to write, may I suggest using * in place of ν? So that your use case for new cell becomes:
    (* me)( NewCell[me,0]
    | `me(r,w).~w(7).`r(x).~out(x) )

  • Mark C. Chu-Carroll says:

    Yeah, you guys are right; using "!" is going to be far to confusing. I was thinking about mnemonics, not interactions. So "!", which means emphasis seemed good for "send!", and "?" which is asking for a response seemed good for receive. I'll think about how to make that better.
    For ν, when I get to the language, I'll probably just use "new". The point of using the ν character was a bit of a pun on Milner's part - it's allocating a "new" name, so use the greek letter "nu".

  • Steve says:

    What do 0 and 7 represent in this abstraction. Is there an implicit (... v-1 v0 v1 ...) at the top of every program, is there the oportunity to do really weird things like transmitting messages over numbers, as in "!0(7).?7(8)"

  • Torbjörn Larsson says:

    Now that you've removed * from being used to write, may I suggest using * in place of ν?

    Actually, I was going to suggest * for repetition, since ? and ! seems excellent mnemonics.
    But if we are considering Milner's theme, the greek "mu" could perhaps be better. It was derived from the hieoglyphic for water (//////), named after the Phoenicians "mem", and "appears in conjunction with alpha and omega to signify the "beginning, middle (meson) and end"" ( http://en.wikipedia.org/wiki/Mu_%28letter%29 ). This suggests plenty of repetitions to me, albeit not easily remembered.
    Btw, alpha and omega could be mnemonics for send and recieve too.

  • Xanthir, FCD says:

    If we're going for typeable constructs, I like ! for send and ? for receive. Very mnemonic.
    Just move * to represent repeats, as it's somewhat parallel to the Kleene star operation in regular expressions (spawn 0 or more copies of P).
    And yeah, definitely need a new symbol for opening a channel. That's not a typeable character. Perhaps ">"? That's even usable with current SB preview bugs!

  • Xanthir, FCD says:

    So, just to have some fun with this, a new hello world (using my suggested syntax, of course!). Purposely too complicated, just to make sure I'm doing it right.
    (> first, second)( NewCell(first,0) |
    NewCell(second,0) |
    ?first(r1,w1).!w1(Hello) |
    ?second(r2,w2).!w2(World) |
    ?r1(x).!out(x).?r2(x).!out(x))
    I've read up on pi calc a bit, but I'm still not 100% sure it'll actually run correctly. If things run concurrently like this, am I guaranteed that something won't try to run before it has a value? For example, I'm assuming that that ?r1(x) won't even try to run until ?first(r1,w1) has actually created the channel.

  • Xanthir, FCD says:

    Also! Mark, are you being consistent in your treatment of () and []? Or are they somewhat random right now?

  • Personally, I think ! is best reserved for send and something else used for recursion. I'm inclined to Hennessy's use as in rec.x(P|x). Here x is a recursive variable, which when invoked reproduces the whole term. Besides being unambiguous, it is nice for allowing you to be more explicit about when the recursive call happens - and I think it more clearly represents the idea that the recursion operator is producing identical processes in parallel.

Leave a Reply