The main features of pi-calculus that distinguish it from other process calculi with explicit input and output are transmission of channels and the treatment of replication. In pi-calculus, channel names are treated as data and may therefore may be transmitted on channels. This gives pi-calclus the partial flavor of a "calculus of mobile processes," as it is sometimes called. However, like most of the other systems we have considered, and unlike Obliq, for example, process distribution and migration are implicit in the model.
Replication is a technical device that serves in place of recursion. Specifically, a process that reads input may replicate itself before reading input. This leaves another "unexecuted" copy of the process available to accept additional input. The idea of treating duplication as an explicit operation appears to have been inspired by the development of linear logic, a logical system that treats "A and A" differently from "A", but has an operator that allows certain formulas to by replicated as needed.
Pict differs from pi-calculus in three main ways:
Some important ideas are:
Proc = Val?Abs input prefix Val?*Abs replicated input Val!Val output atom Proc|Proc parallel composition let Dec in Proc end declaration Abs = Pat > Proc abstraction Val = Id variable [Val, ..., Val] tuple record end empty record Val with Id=Val end record extension Pat = Id variable pattern [Pat, ..., Pat] tuple pattern record Id=Pat ... Id=Pat end record pattern _ wild card pattern Dec = new Id channel creation
A process reads input, writes output, is a parallel composition of processes or is a process with a locally declared channel. An example is
c?x > (x! | a!b)which, informally, reads a channel name from channel c, then in parallel writes the empty tuple to x and writes the value b on a.
Pattern matching is used to destructure an input value, such as a tuple. An example using pattern matching is
(c?[x,[y,z]] > e) | c![u,[[v,w],[w,v]] --> [u,[v,w],[w,v]/x,y,z] e
The difference between communication and replicated communication is that in replicated communication, the process receiving the communication is duplicated, with one copy accepting the input and the other copy remaining ready to accept another communication of the same form. For example:
c!v | (c?x > e) --> [v/x]e c!v | (c?x > e) --> [v/x]e | (c?x > e)
Process calculus, on the other hand, is generally presented as a synchronous system. We can see this using two processes, written in the notation used for Pict, but without the restriction on process output. Specifically, the following parallel composition has a deterministic evaluation order, up to further evaluation of P and Q:
(c!v > d!w > P) | (c?x > d?y > Q) --> (d!w > P) | (d?y > [v/x]Q) --> P | [w/y][v/x]QFor reasons argued in connection with Actors, etc. synchronous communication is not realistic for communication over most network -- it is "better" to use a more complex protocol using explicit send and acknowledgement messages, with programs given the opportunity to respond to failure of communication. Furthermore, it appears more reasonable to represent synchronous communication using asynchronous primitives than conversely.
In Pict, asynchrony is allowed as a consequence of limited form of process that can follow an output. (Let's watch to see how this works!) The closest we can come to expressing a process like c!x > P, which writes to a channel and continues, appears to be the following idiom:
let new ack in (c![x,ack] | ack?_ > P) endIntuitively, this process represents the asynchronous transmission of x on channel c, followed by computation of process P when the transmission is acknowledged. The acknowledgement is handled by passing a new channel to c, along with the data, and then waiting for a transmission along this channel before proceeding. We use this in the reference cell example below.
Exercise: Write a process that gives each customer at the grocery store counter a number. Other examples ??
A reference cell may be implemented as a process that read an initial value and a channel on which to send the resulting initialized cell. The new cell is represented by three channels, one containing the contents of the cell, the other two accepting set and get communication. The contents channel is kept as a "private" data structure (via scoping) of the cell "object"; the other two channels are returned as the cell "object".
CELL = ref?*[init, res] > let new contents, s, g in contents!init | res!record set=s, get=g end | (s?*[v, c] > contents?_ > contents!v | c!) | (g?*[r] > contents?x > contents!x | r!x) endWe can see how this works by evaluating this in parallel with a program that creates a cell, then sets and gets its contents. Note that set requires both a new value for the cell and a channel which receives an acknowldegement when the cell has been updated.
let new r, c in ref![3,r] | r?record set=s, get=g end > s![4,c] | c?_ > g!y endA simple pattern is used to enforce the intended order of reference cell operations. Specifically, the ref! action can be performed first since it is not waiting for any input. Each of the other processes, however, requires an input before it can proceed. Moreover, since r and c are new channels, the only way that set can be enabled is by first receiving a communication in response to ref! and, similarly, the only way that get can be enabled is by an acknowledgement from the set command.
Using the operational semantics, we can evaluate this program as follows, beginning with "scope extrusion" to move the CELL process inside the scope of the declaration of r.
CELL | let new r, c in ref![3,r] | r?record set=s, get=g end > s![4,c] | c?_ > g!y end == let new r, c in CELL | ref![3,r] | r?record set=s, get=g end > s![4,c] | c?_ > g!y end --> let new r, c in CELL | r?record set=s, get=g end > s![4,c] | c?_ > g!y | let new contents, s, g in contents!3 | r!record set=s, get=g end | (s?*[v, c] > contents?_ > contents!v | c!) | (g?*[r] > contents?x > contents!x | r!x) end end == let new r, c, contents, s, g in CELL | r?record set=s, get=g end > s![4,c] | c?_ > g!y \ | contents!3 > (* communication *) | r!record set=s, get=g end / | (s?*[v, c] > contents?_ > contents!v | c!) | (g?*[r] > contents?x > contents!x | r!x) end --> let new r, c, contents, s, g in CELL | s![4,c] | c?_ > g!y \ | contents!3> > (* communication *) | (s?*[v, c] > contents?_ > contents!v | c!) / | (g?*[r] > contents?x > contents!x | r!x) end --> let new r, c, contents, s, g in CELL | c?_ > g!y | contents!3 | contents?_ > contents!4 | c! | (s?*[v, c] > contents?_ > contents!v | c!) | (g?*[r] > contents?x > contents!x | r!x) end --> let new r, c, contents, s, g in CELL | g!y | contents!4 | (s?*[v, c] > contents?_ > contents!v | c!) | (g?*[r] > contents?x > contents!x | r!x) end --> let new r, c, contents, s, g in CELL | contents!4 | contents?x > contents!x | y!x | (s?*[v, c] > contents?_ > contents!v | c!) | (g?*[r] > contents?x > contents!x | r!x) end --> let new r, c, contents, s, g in CELL | y!4 | contents!4 | (s?*[v, c] > contents?_ > contents!v | c!) | (g?*[r] > contents?x > contents!x | r!x) endAt the end, the process is ready to send the updated cell value, 4, along channel y. Although we are done with the cell, the set and get "server processes" are still ready to continue receiving cell operations.
Exercise: what happens if we have several reads and writes waiting in parallel? What kind of nondeterminism is possible? For example:
CELL | let new r, c in ref![3,r] | r?record set=s, get=g end | s![4,c] | g!y | s![5,c] | g!y ) end
Value declarations and pattern matching
let val [x,y,z] = d in e endis sugar for
let new r run d![7,r] in r?[x,y,z] > e endThe derived forms for function definition and application are best understood by example.
let def f[x] = [2,x] in f end == let def f[x,r] > r![2,x] in f![3,r] end == let new f run f?*[x,r] > r![2,x] in f![3,r] end == let new f in f?*[x,r] > r![2,x] | f![3,r] end --> ... f?*[x,r] > r![2,x] | r![2,3]This assumes a continuation-like pespective, where the context is assumed to determine a channel that is "ready" to receive the value of an expression. (This is not explained as well as it might be in the documentation that I have...) As mentioned before, a common idiom is to order computation by explicit acknowledgements...
Reference cells, revisited:
def ref [init] = let new current run current!init in record set = abs [v,c] > current?_ > current!v | c! end get = abs [r] > current?x > current!x | r!x end end endWe can use this in a program by
val r = ref val v = r.get val _ = r.set val w = r.get
(a) Show how mutual recursion def c x > e and d y > f can be desugared into the core language, following the pattern illustrated for a single recursive declaration above. Illustrate the execution of a process with mutual recursion by example.
(b) Explain anonymouse abstraction abs Pat > Val for arbitrary pattern.
The nondeterministic choice (c?x > e) + (d?y > f) between two processes awaiting input may be written in Pict as
sync!( c => abs x > e end $ d => abs y > f end )Like the + analog, this expression can either read a value from c or from d, but once one begins, the other alternative is discarded.
The reason for not providing + as a primitive is efficiency of implementation. This looks like an interesting issue to look into.
def server  > sync!( c => abs x > ... (* handle request *) ... server! end $ d => abs y > ... (* handle request *) ... server! end )It seems natural to change state, Actor-style, by passing some parameter other than  at the end of each "service handler".
Reference cell objects in this style
def ref [init] = let new set, get def server x > sync!( set => abs [v,c] > c! | server!v end $ get => abs [r] > r!x | server!x end ) run server!init in record set=set, get=get end end
def newLock  = let new lock run lock?[r] > r!true | (lock?*[r] > r!false) in lock endThe identifiers sync, => and $ form part of an events library that provides selective communication in the style of CML. (Francois will talk about CML later in the course.)
def ($)[e1, e2] = abs lock > e1!lock | e2!lock end def sync e > e!(newLock ) def (=>) [c, receiver] = abs lock > c?v > if lock then receiver!v else c!v end end