1 2-Process Algorithm

2 Finer-Grained Algorithm

3 Process Sets

4 Locks

5 The Grain of Atomicity

Prev:  Session 6

Next:  Session 8























Session 7   Processes

Leslie Lamport

Last modified on 6 December 2021

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 ; 
This is followed by two processes.  A process has a name and an identifier, which we call its id.  The name must be a legal TLA+ identifier; the id can be any value.  Different processes must have different names and unequal ids. 

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

process (A = 3)
This is followed by the process's code, which is enclosed in { } braces.  That code must begin with a label.  I gave the second process the sensible name B and the silly id -7.  Here is the complete algorithm

--algorithm Add2 {    
  variable x = 0 ;
  process (A = 3) {
    a: x := x + 1 
  process (B = -7) {
    b: x := x + 1
Quiz  Why couldn't I have given process B the id "B" instead of -7 Show the answer.

Answer   The ids of different processes must be unequal.  Since TLA+ doesn't specify whether or not a number equals a string, we don't know whether or not 3 and "B" are equal.

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)
Run the translator on the specification Session7, create a new model, and add the formula above to the Invariants section of the What to check? section of the model's Model Overview tab.  Running TLC should confirm that the algorithm satisfies its postcondition.

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]
explained in Session 6.  The expression exp uses the TLA+ CASE construct.  You should be able to deduce the meaning of the construct from this example.  The translation always uses self as the name of a bound variable that takes values in ProcSet. You should also be able to deduce the meaning of the expressions containing the EXCEPT construct in the definitions of a and b.

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 
If you've done any multi-threaded programming, you should realize that this algorithm doesn't satisfy the postcondition of the original algorithm.  It can terminate with x not equal to 2.  Run TLC on the model that checks the invariant asserting this postcondition and look at the error trace.  As you probably expected, it shows that each process read x before the other process changed its value, so they both set x to 1.  We'll see later how to fix the finer-grained algorithm so it satisfies the postcondition x = 2.  But first, more about processes.

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})
This declares two processes, one with id 3 and the other with id -7, just as before.  However, instead of naming each process separately, it gives the name AB to the process set containing the two processes.  The complete declaration of the process set is:

process (AB \in {3,-7}) 
variable t = -1 ;
{ ab1: t := x ;
  ab2: x := t + 1
Replace the two processes A and B in the fine-grained algorithm with this single process set AB and run the translator.  The translation of the two-process version began like this, where I've deleted some things:

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 == ...
Compare it with the translation of the new algorithm having a single process set.  Observe that it differs in the following ways.
  • 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).
In the definition of the formula Spec that describes the complete algorithm, self is a bound variable that is quantified over all the process ids.

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 ;
Replace the algorithm in specification Session7 by this version, and run TLC to check that the postcondition is now satisfied.

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

lock: sem := sem - 1 ;
      await sem = 0 ;
Explain why the algorithm does what it does.  Show the answer.

Answer   The modified algorithm behaves exactly like the original one.  A lock step consists of a complete execution from label lock to label ab1.  If sem equals 0, then subtracting 1 sets it equal to -1, so the await statement can't be executed and therefore the lock step can't be executed.  A lock step can be performed iff sem equals 1.  This change to the code does not change what the algorithm does.

From a programming perspective, one would say that the assignment to sem must be undone if sem was not equal to 1.  From an algorithmic perspective, the code simply says that nothing can be done if sem equals 0.  But the best way to understand what's happening is that the meaning of the algorithm is its TLA+ translation.  Comparing the definitions of lock(self) in the two versions of the algorithm, we find that they differ only in the following two lines — the lines on the left being from the original and the ones on the right from the modified version:

   /\ sem = 1          /\ sem' = sem - 1
   /\ sem' = 0         /\ sem' = 0
These two formulas are equivalent.  It's obvious that the first equals TRUE iff sem equals 1 and sem' equals 0.  You should convince yourself that the second formula also equals TRUE only in this case.  Since all the other formulas in the translation are identical, this means that the definitions of formula Spec for the two versions are equivalent, so the algorithms are equivalent. note

Whenever you are not sure what a PlusCal statement should do, you can find the answer in the TLA+ translation.

Exercise   Modify the algorithm by replacing {3,-7} with a set of N elements, for an arbitrary natural number N, so it satisfies the postcondition x = N.  Check that it satisfies this postcondition for a few values of N.  Also write and check an invariant asserting that two processes cannot be between their lock and unlock steps at the same time.  Show the answer.

Answer   TLC can find any errors in your algorithm by checking that it has no deadlock and that it satisfies the postcondition.  You should also check an invariant asserting there is at most one process between lock and unlock.  There are several ways to write that invariant; here are two:

\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 
This probably more accurately represents the actual execution of the program by a computer.  It allows the possibility of one process performing a step between the steps ab1a and ab1b of the other process—a possibility not allowed by algorithm Add2FG.  However, that additional possibility makes no difference to the possible results produced by the algorithm.  Any step that a process performs between steps ab1a and ab1b of the other process has the exact same effect as if that step were performed after the ab1b step.  This is because an ab1b step reads and modifies only the value of the process-local variable t, which cannot be read or modified by the other process.

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.