Session 7   Processes

1  A 2-Process Algorithm

We begin with about the simplest multi-process algorithm I can think of.  It has a single variable x with initial value 0, and it adds 2 to that value by using two processes that each increment x by 1.  That algorithm is in module Session7, which you should now open in the Toolbox.

The algorithm begins like a uniprocess algorithm with its name, an opening {, and variable declarations:

--algorithm Add2 {
    variable x = 0 ; 

I have named the first process A and, for no good reason, I have given it the id 3.  It begins:

process (A = 3)

--algorithm Add2 {    
  variable x = 0 ;
  process (A = 3) {
    a: x := x + 1 
  }
  process (B = -7) {
    b: x := x + 1
  }
}

The algorithm satisfies the postcondition x = 2.  However, we can't simply check that it does with an assert statement because it's impossible to put a statement where it will be executed only after both processes have incremented x.  We have to express the postcondition as an invariant. 

The invariant must use the pc variable added by the translation.  For a multi-process algorithm, the value of pc is a function whose domain is the set of process ids.  If i is the id of a process, then pc[i] is the string that labels the next piece of code that the process will execute.  It equals "Done" if the process has terminated.  Therefore, TLC can check the postcondition by checking the invariance of:

(pc[3] = "Done") /\ (pc[-7] = "Done") => (x = 2)

We would also expect our tiny algorithm to terminate.  As with uniprocess algorithms, we have to add a fairness requirement to ensure that the algorithm actually takes steps.  Termination and fairness are discussed later.  For now, we just consider invariance properties.

Examine the algorithm's TLA+ translation.  Like the translation of a uniprocess algorithm, it begins with a VARIABLES declaration and a definition of the tuple vars of all variables.  It then defines ProcSet to be the set of all process ids.  As in the algorithm in Session 6, it defines formula Init that describes the initial values of the variables and a formula for each of the two labels a and b that describes the steps allowed by the corresponding algorithm statement.  We can ignore the rest of the translation, except to note that, like a uniprocess algorithm, it defines Spec to be the temporal logic formula that constitutes the complete mathematical description of the algorithm.

In formula Init, the initial value of pc is described with a function-valued expression of the form

[i \in D |-> exp]

Observe that process names and labels are used as identifiers in the translation.  Make sure that they are distinct from one another and from variable names and any identifiers declared or defined elsewhere in the module.  PlusCal allows some repeated use of the same identifier in an algorithm—for example, you can use the same label in different processes.  However, don't do that because the translator changes names to eliminate clashes, making the correspondence between the translation and the algorithm a little harder to see.

2  A Finer-Grained Algorithm

You could write a program in many languages in which a variable x initially equals 0 and two processes each increment x by 1.  Those processes would be called threads.  While the code would look quite different from the PlusCal code, it would have assignment statements that look very much like statements a and b in our algorithm.  However, they would be very different from the statements in the algorithm.  Each of the statements a and b increments x in a single step.  In the program, the statements incrementing x would each be executed as multiple steps.  In particular reading the value of x and writing its new value would occur in different steps.

We now consider an algorithm whose steps more closely resemble those of the program—an algorithm that increments x in two steps, the first reading its current value and the next writing its new value.  We obtain the algorithm by splitting an a step and a b step into two steps, the first step reading x and the second writing its new value.  A single step is sometimes called an atomic action, and splitting one step into multiple steps in this way is called refining the grain of atomicity. 

Splitting the incrementing of x into two steps requires remembering the value read in the first step, so that value must be put someplace.  Each process needs its own place to remember the value it read, and it's natural for a process to remember the value in a variable local to that process.  The initial values of these process-local variables are never used.  We can omit the specification of the initial value(s) from a variable declaration, in which case the translation provides a special initial value.  But it's better to provide an initial value, in part because it permits a simple type-correctness invariant.  Here is a suitable finer-grained algorithm:

--algorithm Add2FG {
  variable x = 0 ;
  process (A = 3) 
    variable ta = -1 ; 
    {  a1: ta := x ;
       a2: x := ta + 1 
    }  
  process (B = -7) 
     variable tb = -1 ;  
     { b1: tb := x ;
       b2: x := tb + 1 
     }
 }

3  Process Sets

Instead of writing our two algorithms with two separate processes, we can write them with a single process set containing two processes.  Here is how we rewrite the finer-grained algorithm.  The process set begins:

process (AB \in {3,-7})

process (AB \in {3,-7}) 
variable t = -1 ;
{ ab1: t := x ;
  ab2: x := t + 1
}

VARIABLES x, pc, ta, tb
vars == << x, pc, ta, tb >>
ProcSet == {3} \cup {-7}
Init == /\ x = 0
        /\ ta = -1
        /\ tb = -1
        /\ pc = [self \in ProcSet |-> CASE self = 3 -> "a1"
                                        [] self = -7 -> "b1"]
a1 == /\ pc[3] = "a1"
      /\ ta' = x
      /\ pc' = [pc EXCEPT ![3] = "a2"]
      /\ UNCHANGED << x, tb >>
a2 == ...
b1 == /\ pc[-7] = "b1"
      /\ tb' = x
      /\ pc' = [pc EXCEPT ![-7] = "b2"]
      /\ UNCHANGED << x, ta >>
b2 == ...

• The two process-local variables ta and tb have been replaced by the single array-valued variable t.  The values of ta and tb are now represented by the values of t[3] and t[-7], respectively.
• The formulas a1 and b1 have been replaced by the single formula ab1(self).  Substituting 3 for self, we get formula ab1(3) that describes the same steps as a1. Similarly, ab1(-7) describes the same steps as b1.
• In the same way, formulas a2 and b2 have been replaced by ab2(self).

A multiprocess algorithm can contain any number of individual processes and process sets.  However, there can be no name conflict between different processes and process sets, and the ids of different processes must be different.

4  Locks

Our fine-grained algorithms that takes two steps to add 1 to x models a real program, but it doesn't satisfy the postcondition that x equals 2.  The usual way to implement this postcondition with a real program that increments x by 1 in two different threads is to use a lock.  A lock is used to prevent two processes from stepping on each other's toes.  In this case, it would be used to prevent one process from incrementing x while the other process is also incrementing it.  In our process-set algorithm, this is achieved by having each process execute a Lock step before statement ab1 and an Unlock step after executing statement ab2.  A process executing between the Lock and Unlock steps is said to own the lock, and the lock is said to be free if no process owns it.

A lock is easy to represent with the PlusCal await statement.  For any formula F, the statement await F can be executed only when formula F equals TRUE. 

One way to describe a lock is with a variable called a semaphore.  The lock is free if the value of the variable is 1 and owned if the value is 0.  Here is our algorithm with a lock described with a semaphore variable sem:

--algorithm Add2FGSem {
   variable x = 0, sem = 1 ; 
   process (AB \in {3,-7}) 
    variable t = -1 ;
     { lock: await sem = 1 ;
             sem := 0 ;
        ab1: t := x ;
        ab2: x := t + 1;
     unlock: sem := 1 ;
     }
 }

Puzzle   Use TLC to find out what the algorithm does if you replace the Lock operation with:

lock: sem := sem - 1 ;
      await sem = 0 ;

   /\ sem = 1          /\ sem' = sem - 1
   /\ sem' = 0         /\ sem' = 0

\A i, j \in ProcSet : 
   (pc[i] \in {"ab1, ab2"}) /\ (pc[j] \in {"ab1, ab2"})  =>  (i = j)

\A i \in ProcSet : \A j \in ProcSet \ {i} :
    ~ ( (pc[i] \in {"ab1, ab2"}) /\ (pc[j] \in {"ab1, ab2"}) )

Locks are used in programs to make everything between a Lock step and the matching Unlock step act like a single step.  They are not needed for that purpose in PlusCal.  Any computation that you want to act like a single step can be written as a single PlusCal step.  Locks should be used in PlusCal only in an algorithm that is meant to model their use in a program's code.  If you have trouble describing a computation as a single step, it means that you don't know how to describe mathematically what is being computed.  Learning how requires learning how to use the full power of TLA+ when writing PlusCal expressions, which takes practice. 

5  The Grain of Atomicity

An algorithm is an abstract model of some code and/or hardware.  We want it to be as accurate as necessary and as simple as possible.  Simplicity means having a coarser grain of atomicity—that is, taking as few steps as possible, which means having as few labels as possible.  However, accuracy requires not having too coarse a grain of atomicity, which means not having too few labels.  For example, algorithm Add2 has too coarse a grain of atomicity to be a good model of the execution of a typical program in which two threads concurrently increment x by 1.  A better model is the finer-grained algorithm Add2FG.  It is better because it models executions in which a step of one process occurs between the two steps that describe the incrementing of x by another process.  That additional interleaving of the steps of the two process produces an outcome (a final value of x) not allowed by the coarser-grained algorithm. 

Now consider a still finer-grained algorithm Add2XFG in which incrementing t is split into an additional step:

process (AB \in {3,-7}) 
variable t = -1 ;
{ ab1a: t := x ;
  ab1b: t := t + 1 ;
   ab2: x := t 
}

In general, a step of a process that reads or modifies only process-local variables can be combined with the preceding or following step of that process.  Thus, we can combine step ab1b with step ab1a or step ab2, the latter producing algorithm Add2FG. More precisely, combining the step with its preceding or following step cannot make any difference in whether the algorithm satisfies a property that does not depend on the process-local variables mentioned in the step.  The situation is a little tricky for properties that depend on the variable pc, since even a step that mentions only process-local variables can change the value of pc.  However, it's easy to see that in our example, combining step ab1b with its preceding or following step cannot change whether its postcondition is satisfied by the algorithm, since pc appears in the postcondition only in expressions whose value depends on whether or not pc[i] equals "Done", for some processes i.