CS 358. Concurrent Object-Oriented Programming
Spring 1996

Lectures 14-15. Pict: Concurrent objects based on pi-calculus

References:
B. Pierce and D.N. Turner, Concurrent objects in a process calculus, in T. Ito and A. Yonezawa (eds.), Proc. Theory and Practice of Parallel Programming (TPPP), Sendai, Japan (Nov.{} 1994), Springer-Verlag Lecture Notes in Computer Science 907, 1994, pages 187--215. (Available from Pierce's web site.)

Main Concepts

Pict is a language with concurrent objects that is based on pi-calculus. Pi-calculus is a form of process calculus, as considered in earlier lectures. with explicit input and output instead of the "propositional" system with only atomic actions. Although Pict is based on pi-calculus, there are some important differences, some restrictions, and a lot of syntactic sugar designed to make it easier to write larger programs.

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:

Extensions: many derived forms are provided to make programming more feasible. In addition to simple sugar providing multiple declarations, function definitions and the like, there is a notion of object arising from the natural grouping of related channels and (implicitly) the processes they communicate with.
Restrictions: some features of pi-calculus are restricted, such as the Pict convention that replication only occurs at process input.
Communication: while pi-calculus is generally formulated using synchronous communication, Pict is based on asynchronous communication. More precisely, the form of Pict process output is restricted so that the formal semantics are consistent with an asynchronous interpretation of communication. There is (apparently?) no way to express a computation that halts on output, waiting until the precise moment that another process reads input. However, synchronous communication may be simulated by waiting until an explicit acknowledgement is received.

Some important ideas are:

Represent object as record of functions/channels
Represent record as single channel that selects operation ...
Use channels (with "pending output") to maintain shared state; this ensures mutual exclusion
Asynchrony leads to explicit acknowldegement of completetion. This can be used in conjunction with a continuation-like style to order computations, represent functions as processes that return a result to the "continuation channel", and so on.

Core language

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)

Synchronous and Asynchronous Communication

An important difference between Pict and pi-calculus is that Pict is based on asynchronous communication while pi-calculus uses synchrounous communication. This is achieved using a syntactic restriction. Specifically, output only occurs in processes of the form Val!Val which output a value and then terminate. Since such a process cannot do any further actions based on the completion of its transmission, an asynchronous implentation of communication may be faithful to operational semantics of Pict. (Is this proved somewhere? Try Kohei Honda paper on asynchronous pi-calculus ?)

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]Q

For 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) end

Intuitively, 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 ??

Operational semantics

(see paper)

Example: Reference cells

A simple example process is a "reference cell," as in ML. A reference cell is initialized when created. Thereafter, it supports set and get operations, the first changing the value in the cell and the second reading the stored value.

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

We 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 
    end

A 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)
     end

At 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

Syntactic Extensions to the Core Language

Conditional expressions for processes: if b then P else Q
Special syntax for integers, strings, etc.
Channel priniti that prints integers on the standard output stream
Compound declarations, such as
let d_1 d_2 in e for let d_1 in let d_2 in e
let run e in f for e | f
Recursive definitions: def d x > e for new d run d?x >e
Anonymous abstractions: abs [x,y,z] > e for let def t [x,y,z] > e in t
Function definition and application:
[p_1, ..., p_n] = v for [p_1, ..., p_n, r] = r!v
f[a_1, ..., a_n] for new r ... run r![a_1, ..., a_n, r] ... r? ... (See example below.)
Infix operators: a+b for (+)[a,b]
Declaration val p = v (see below)
Sequencing e;f for let val _ = e in f end

Examples:
Value declarations and pattern matching

let val [x,y,z] = d[7]  in e end

is sugar for

let 
   new r
   run d![7,r]
in
   r?[x,y,z] > e
end

The derived forms for function definition and application are best understood by example.

let def f[x] = [2,x] in f[3] 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
    end

We can use this in a program by

    val r = ref[0]
    val v = r.get[]
    val _ = r.set[5]
    val w = r.get[]

Exercise:
(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.

Choice

While process calculi like CCS have a nondeterministic choice operator, +, this is not included in the Pict core language. However, we can define choice in Pict using ... Let's see how this is used, before we go into how choice is definable as a "library module" (= derived form?).

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.

Objects using choice

A reasonable idiom for servers is a recursive definition that "restarts" the process when each response is complete. This looks more object-like, in fact a bit like Actors.

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

Implementing Choice

Basic abstraction is "lock":

   def newLock [] = let
     new lock
     run lock?[r] > r!true | (lock?*[r] > r!false)
   in 
     lock
   end

The 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

CS 358. Concurrent Object-Oriented Programming Spring 1996