CS 358. Concurrent Object-Oriented Programming
Spring 1996

Lectures 4-5. Process Equivalence, Interleaving and Partial Order Approaches

References:
G. Agha, ACTORS: A Model of Concurrent Computation in Distributed Systems, MIT Press, 1986.
P.C. Kanellakis and S.A. Smolka, CCS Expressions, finite state processes, and three problems of equivalence, Information and Computation 86, 43--68, 1990.
R. Milner, Semantics of Concurrent Processes, in J. van Leeuwen (ed.), Handbook of Theoretical Computer Science, Elsevier and MIT Press, 1990.
V.R. Pratt, Modeling Concurrency with Partial Orders, Int. J. of Parallel Programming, 15, 1, Feb 1986, pages 33-71.

Process equivalence, using execution trees

There are several forms of process equivalence that may be compared using execution trees. In addition, there are other approaches, such as the pomset model, that differ from these. There is an extensive literature on the subject and we will barely have time to scratch the surface.

Trace Equivalence

The simplest form of process equivalence is called trace equivalence. This is easier to express if we introduce some notation. Let us write P --t-->, for process P and sequence t of actions, if there is some P' with P --t--> P'. We say P is trace equivalent to Q if, for every sequence t of actions, we have P --t--> iff Q --t-->.

Another way of expressing trace equivalence, mathematically, is to define the trace interpretation of a process. The trace interpretation of process P is the set of all traces of P,

     Traces(P) = { t  |   P --t-->   }
Processes P and Q are trace equivalent if Traces(P) = Traces(Q).

Intuitively, trace equivalence compares processes according to what the can do. It does not take into account what they can, at some point, be in a position not do. For example, the processes

       a.b.Halt                       --a-->--b-->
       
                                     /--a-->--b-->
       a.Halt + a.b.Halt            /
                                    \
                                     \--a-->
are trace equivalent, because both can do a, both can do a followed by b, and neither can do anything else. In symbols,
              Traces(a.b.Halt) = { epsilon, a, ab }
     Traces(a.Halt + a.b.Halt) = { epsilon, a, ab }
However, these two processes might also be considered different because one may "refuse" to do b after doing a, while the other may not. More precisely, after doing a, the first process must be in a state where it is possible to do b, while the other may be in a state where it is not possible to do b. Informally, we might say that one may "deadlock" when run in the context
       C[ ]  =   ([ ] | a'.b'.Halt)\ab
while the other may not.

Trace Equivalence with Halt

A variant of trace equivalence may be used to distinguish between a.b.Halt and a.Halt + a.b.Halt. The idea is simply to mark the end of a maximal trace with some sort of symbol, indicating that the process cannot progress any farther. Using # to indicate that the process has halted, we have
              Traces#(a.b.Halt) = { epsilon, a, ab }
     Traces#(a.Halt + a.b.Halt) = { epsilon, a, a#, ab }
indicating that process a.Halt + a.b.Halt can do a and be in a state where it will no longer perform any additional actions.

This form of trace semantics can be extended to distinguish between different kinds of halting states. For example, we might identify a set of "deadlocked" process, and use different symbols at the end of traces to indicate whether a process has deadlocked or halted in a more desirable state.

A Normal Form, with trace equivalence
In an execution tree, there may be nondeterministic choices at any point in a path through the tree. However, each finite tree is trace equivalent to one with just a single finitely branching nondeterministic choice at the beginning. (The same holds for inifinite trees, but with possibly infinite branching.) This allows us to associate a set of linearly-ordered sequential behaviors with each process. For example, we have
          /--a-->----b-->--c-->                     / --a-->----b-->--c-->                          
         /                                         /             
         \        /--c-->        = trace =        /-----b-->----c-->                     
          \--b-->/                                \                        
                 \                                 \                     
                  \--d-->--e-->                     \ --b-->----d-->--e-->                              
This normal form will be useful in comparing the interleaving approach with partial order semantics of concurrent processes.
Silent actions in traces (?)
It seems possible to either consider silent actions as part of a trace, or leave them out. We might also want to consider a sequence of tau actions followed by a equivalent to one tau action followed by a or even to just a itself. There seem to be many possible variations and I don't know what experts would generally consider reasonable.

Bisimulation

Bisimulation is a way of comparing processes that requires equivalence between all corresponding future states, i.e., all processes that may be produced by performing a specific sequence of actions. This is best introduced by example.

The finer-grained forms of trace semantics using end-markers to identify termination states do not distinguish between different branching patterns within execution trees. For example, trace semantics will identify the following processes

                                           /--b-->
       a.(b.Halt + c.Halt)          --a-->/
                                          \
                                           \--c-->
                                           
       
                                     /--a-->--b-->
       a.b.Halt + a.c.Halt          /
                                    \
                                     \--a-->--c-->
It seems that reasonable people might disagree on whether these two processes are equivalent. Perhaps the simplest way to see the difference between them is to assign a specific interpretation to a, b, and c. Since the essential difference between the processes lies in when they "make a decision" of "commit themselves" on whether to do b or c, it helps to choose an example where we can imagine a human being carrying out these actions. For example, let us consider
     a  =   "I am going to the store"
     b  =   "I am going to buy some bubblegum"
     c  =   "I am going to buy some chocolate"
Then the two processes may be interpreted as
       a.(b.Halt + c.Halt)          I am going to go to the store.
                                       When I get there, I am willing to either
                                          buy some bubblegum, or
                                          buy some chocolate.
                                           
       
       a.b.Halt + a.c.Halt          I am willing to be convinced now to either
                                        go to the store and buy some bubblegum, or
                                        go to the store and buy some chocolate.
The distinction is relatively subtle. However, the difference shows up when we execute either in parallel with the processes a'.b'.Halt. The second process above could deadlock with a'.b'.Halt, but the first one will not.

Intuitively, Processes P and Q are bisimilar if, for all actions a,

if P --a--> P' then there is some Q with Q --a--> Q' and P',Q' bisimilar, and conversely,
if Q --a--> Q' then there is some P with P --a--> P' and P',Q' bisimilar.
We can give a slightly more precise definition using bisimulation relations. A relation ~ on processes is a bisimulation if, whenever P~Q the following two conditions are satisfied:
if P --a--> P' then there is some Q with Q --a--> Q' and P'~Q'
if Q --a--> Q' then there is some P with P --a--> P' and P'~Q'.
We say processes P and Q are bisimilar if there is some bisimulation ~ with P~Q. This is very similar to the relations used to represent expression equivalence on graph representations of symbolic expressions (see [Paterson and Wegman; Dwork, Kanellakis and Mitchell]) and the relations used to represent equivalence of deterministic finite automata (see [Aho, Sethi and Ullman; Hopcroft and Ullman]).

While the relationship to automata theory might suggest that there are efficient algorithms for deciding bisimilar, the automaton equivalence problem is only efficiently decidable for deterministic automata. The equivalence problem for nondeterministic automata, of the sort one usually obtains for processes, is pspace-complete. (The proof of pspace completeness uses a nondeterministic finite automaton to characterize the complement of the set of strings coding accepting computation sequences of pspace-bounding Turing machines.) See Kanellakis and Smolka for more information on connections between process equivalence and automata theory.

Examples:

  1. There is a bisimulation that relates the following two processes:
           a.b.Halt                                 ---a-->--b-->
           
                                                   /--a-->----b-->
           a.b.Halt + a.(b.Halt + b.Halt)         /
                                                  \        /--b-->
                                                   \--a-->/
                                                          \
                                                           \--b-->
    
    This relation may be drawn as a set of vertical line segments between these two horizontal trees. (Or we may draw trees vertically and represent the simulation by horizontal arcs.)
  2. There is no bisimulation between the following two processes:
                                                           /--b-->
           a.(b.Halt + c.Halt)                     ---a-->/
                                                          \
                                                           \--c-->
           
                                                   /--a-->----b-->
           a.b.Halt + a.(c.Halt + b.Halt)         /
                                                  \        /--c-->
                                                   \--a-->/
                                                          \
                                                           \--b-->
    
    We can attempt to construct a bisimulation by drawning a vertial line segment between the roots of these trees. This leads us to draw two vertical line segments between processes produced after doing one a action. But the line to the upper branch of the lower tree fails to satisfy the condition of bisimulation.
  3. With recursive processes, the test for bisimularity may be carried out on the finite dag presentation of the infinite execution tree. For deterministic processes, the test is like unification or finite automata equivalence. For nondeterministic processes, it seems that a nondeterministic version of the same algorithm works. However, I haven't been able to find anything like this in the literature yet (* check again *). The following two processes are bisimilar (if I haven't made a mistake):
                
                                                  |------c--------|
                                                  |               |  
                                                  V        /--b-->|
           mu P (a. (b.c.P + c.Halt))             \---a-->/
                                                          \
                                                           \--c-->
                                                           
    
                                                           |-------a------|
                                                           V              |
                                                           | /--b-->--c-->|  
                                                           |/     
                                                           /\
            a. (mu P (b.c.a.P + c.Halt) + c.Halt)  ---a-->/  \--c-->  
                                                          \
                                                           \--c-->
                                                          
    
    The second graph here has unlabelled arcs, corresponding to epsilon moves in finite automata. This can be regarded as a notational convenience (when writing cyclic graphs for infinite trees), or epsilon moves can be removed by expanding the graph (see elimination of epsilon moves in finite automata).

DIGRESSION
Although we will not have time to discuss this in any detail, a useful way of restating the distinction between processes that "decide" at different stages in computation is through temporal logic. Temporal logic is an extension of ordinary propositional logic, with two operators
       <>  =  possibly
       []  =  necessarily
       a.(b.Halt + c.Halt)          ??? how does HM logic work here ???
                                           
       
       a.b.Halt + a.c.Halt          ???
END DIGRESSIONS
An interesting comparison with automata theory is that the determinization procedure for nondeterministic automata does not preserve bisimulation. In particular, we may regard
                                           /--b-->
       a.(b.Halt + c.Halt)          --a-->/
                                          \
                                           \--c-->
                                           
       
                                     /--a-->--b-->
       a.b.Halt + a.c.Halt          /
                                    \
                                     \--a-->--c-->
as nondeterministic finite automata. Although they are not bisimilar processes, the standard determinization procedure produces the same deterministic automaton from either of these. The reason is that the determinization procedure only preserves trace equivalence.

Brock-Ackerman Anomaly

Sequential programs may be characterized using input-output functions or, if nondeterministic, input-output relations. More specifically, an algorithm such as bubble sort or quick sort, has many properties. It requires some amount of time and space to transform an input array in arbitrary order into an output array in sorted order. However, for reasoning about program correctness, the exact time and space requirements are usually ignored. The input-output function, the mathematical function f: arrays --> arrays that maps any array to its sorted permutation gives us a useful abstraction of the algorithm. Most importantly, if we build a more complex program using a sorting procedure as part of the program, then the input-output behavior of the more complex program may be determined using only the input-output behavior of the sorting procedure. More detailed information, such as the order in which elements of the array are accessed, does not enter into the picture.

For a concurrent program that might occur inside a larger program or system, a simple function from inputs to outputs is not enough to determine the behavior of the full system. In other words, if we want to use a concurrent process as a "black box", simple input-output behavior is not enough to reason about the behavior of the black box inside a larger system. This is illustrated by an example known as the Brock-Ackerman anomaly. (History: Kahn-MacQueen nets, etc.)

The Brock-Ackerman anomaly is an example with three parts, two sequential processes, P_1 and P_2, and a system, S, that can interact with either one. If we look at the mapping from sequences of inputs to sequences of outputs, the two processes P_1 and P_2 are equivalent. However, they behave differently when placed in the system S. This shows that mappings from inputs to outputs are not enough to determine the compositional behavior of processes in concurrent systems. More detailed information involving the dependencies between elements of the input sequence and elements of the outpus sequence are required.

Sink  =   in x. Sink

D(nil)  = in x. D(x::x::nil)
D(x::l) = in y. D(y::y::x::l)   +  out x. D(l)


Q_1   =   in x. in y. out x. out y. Sink

Q_2   =   in x. out x. in y. out y. Sink


P_i   =  Q_i  |  D(nil) 

L     =  in x. out_1 x. out_2 b.L

Merge =  in_1 x. out x. Merge   +  in_2 x. out x. Merge 


                                                       ----------
P_i:    ----------------            S_i:          |    |        |
        |     |        |                          V    V        |
        |     V        |                         ---------      |
        |   -----      |                         | Merge |      |
        |   | D  |     |                         ---------      |
        |   ------     |                             |          |
        |     |        |                             V          |
        |     |        |                         ---------      |          
        |     V        |                         |  P_i  |      |
        |   -------    |                         ---------      |
        |   | Q_i |    |                             |          |
        |   -------    |                         ---------      |   
        |     |        |                         |   L   |-------
        |     V        |                         ---------   
        ----------------                             |
                                                     V
The input-output function for P_1 maps a --> aa, ab --> aabb, ab --> abab, ..., abc --> aabbcc, ... This is also the input output behavior of P_2. The only difference is in the way that Q_1 and Q_2 respond to their inputs. When P_1 is given input a, the duplicator D sends a twice to Q_1. However, Q_1 does not output a twice until both inputs are received. In contrast, Q_2 may send a out once when it recieves the first a and then again when it received the second a.

Systems S_1 and S_2 differ on a single input a. In system S_1, input a is sent on to P_1, where it is duplicated and then sent to Q_1, which passes both messages on to L. Process L then sends a twice on the output channel, along with some output back to merge. However, since Q_1 is now the process Sink, further inputs to P_1 have no effect. Therefore, S_1 maps the input token a to the output sequence aa.

In system S_2, a is sent on to P_2, where it is duplicated. However, since Q_2 can send its first output a out before receiving the second input, it is possible for the first a to be sent along to L, which then sends b back along the feedback communication path. It is possible for this to come next through the merge operator, then down to D to be passed on to Q_2 before the second a leaves D. Therefore, one possible behavior of S_2 is to map the single input token a to the output sequence ab.

Exercise: Rewrite this in CCS using, for example, an atomic action a for "send x on channel c" and a' for "receive x on channel c". If you need to have two possible values on a channel, you will need two possible atomic actions. For example, if in x. P could read a or b, you will need to replace in x. P by a.[a/x]P + b.[b/x]P, where [a/x]P is the result of substituting a for x in P.

Partial order vs. interleaving interpretations

When we use execution trees to study processes, we necessarily consider two processes with the same execution trees equivalent. However, there are some cases where this might not be the best view of process behavior. Some alternatives to execution trees, which describe linearly ordered sequences of events, are views that involve partially-ordered sets of events. One intuition for the partial order relation is time, and another is the ill-defined but still intuitively plausible notion of "causality."

To begin with a concrete example, let us try to see how the two processes

         a.Halt | b.Halt                    a.b.Halt  +  b.a.Halt
might be considered different. The first expression describes a concurrent system with two processes running in parallel. The two processes could be located anywhere in the world, or one on earth and one in space, for example. If physically separated, then an a action by one might have nothing to do with the b action by the other. One might occur before the other or, conceivably, they might in fact occur simultaneously. If we think of causality, then there may be no causal relationship at all. We might simply have a system where two unrelated events may occur independently.

In contrast, the expression a.b.Halt + b.a.Halt might describe a single process that could either do one sequence of actions or the other. There is a non-deterministic choice, but once the choice is made, we appear to have a single process that performs two events in order. We might even attribute causality, saying that if a.b.Halt occurs, then the a event causes the subsequent b event. There are lots of philosophical problems in defining causality in general. However, it is possible to get some insight using a crude but pragmatic approach. Specifically, let us say that action a causes action b, in process or system, if it is not possible to do b before a. With this view, the process a.b.Halt + b.a.Halt chooses between an execution where a causes b and one where b causes a, but does not allow independent execution.

A common way of accounting for the intuitive difference between a.Halt | b.Halt and a.b.Halt + b.a.Halt is to use partial orders of events. More specifically, in the execution tree interpretation, there are nondeterministic choices between sequential paths, with each tree trace equivalent to one with just a single nondeterministic choice at the beginning. Therefore, the execution tree model associates a set of linearly-ordered sequential behaviors with each processes. The partial order approach replaces each linearly ordered trace by a partially-ordered multiset (i.e., a set where an element may occur more than once) of actions. (* It isn't obvious how to incorporate the branching behavior that is considered important in bisimultion into the partial order model, but there might be some version of trees of partial orders (?) *)

Associating a set of partial orders with each process, we have

                                     /--a-->
       a.Halt | b.Halt              /
                                    \
                                     \--b-->
                                     
                                     
       a.b.Halt + b.a.Halt         { --a-->--b-->,   --b-->--a-->  }

In words, the first process has a single partially ordered trace, in which events a and b are unordered. The second process has two possible traces, one with a preceding b and one with the reverse order.

Some general advantages of partial orders are:

There are also some commonly held beliefs about the advantages of interleaving that are worth examining. Possible project: investigate partial order interpretation of CCS (the simple process calculus we have been looking at) and compare this to the interleaving interpretation. How would you define bisimultion with partial orders? Can you find two processes that are partial-order-bisimilar but not interleaving-bisimilar? How about the converse? (Hint: see van Glabbeek paper in LICS '95 conference proceedings)