A Simple Example

Leslie Lamport

Last modified on 6 July 2018

TLA+ is not hard to learn. Amazon engineers report that:

"Engineers from entry level to principal have been able to learn TLA+ from scratch and get useful results in two to three weeks, in some cases in their personal time on weekends and evenings, without further help or training."

However, programmers and software engineers find TLA+ specs intimidating at first sight. I'm not going to risk scaring you now with a TLA+ spec. Instead, I'll present an example in PlusCal.

PlusCal looks like a simple toy programming language, except that an expression can be any TLA+ expression—meaning any mathematical formula—making it infinitely more expressive than any programming language. The algorithm is translated into a TLA+ specification that can be checked with the TLA+ tools. PlusCal is not as expressive as TLA+, but it is often more convenient to use than raw TLA+, especially for simple algorithms.

The example is Peterson's mutual exclusion algorithm. Here is the PlusCal code:

   --algorithm Peterson {
      variables flag = [i \in {0, 1} |-> FALSE],  turn = 0;
         \* Declares the global variables flag and turn and their initial values;
         \* flag is a 2-element array with initially flag[0] = flag[1] = FALSE.
      fair process (proc \in {0,1}) {
        \* Declares two processes with identifier self equal to 0 and 1.
        \* The keyword fair means that no process can stop forever if it can
        \* always take a step.
        a1: while (TRUE) {
             skip ;  \* the noncritical section
        a2:  flag[self] := TRUE ;
        a3:  turn := 1 - self ;   
        a4:  await (flag[1-self] = FALSE) \/ (turn = self); \* \/ is written || in C.
        cs:  skip ;  \* the critical section
        a5:  flag[self] := FALSE               }     }     }

To specify a concurrent algorithm, you must say what the atomic operations are. In PlusCal, the code from one label to the next is executed atomically.

The TLC model checker can verify that the algorithm satisfies two important properties: mutual exclusion, meaning that two processes are never executing their critical section at the same time; and starvation freedom, meaning that each process keeps executing its critical section. The TLA+ translation introduces an array variable pc whose value indicates where each process is in its algorithm. In particular, pc[i] = "cs" means that process i is in its critical section, so mutual exclusion means that pc[0] and pc[1] are never both equal to "cs" . This condition can be written as

   (pc[0] /= "cs") \/ (pc[1] /= "cs")

or more compactly as

{pc[0],pc[1]} /=
{"cs"}

. TLC can check that it is always true in any execution of the algorithm. Starvation freedom here means that each process executes its critical section infinitely often. This is expressed in temporal logic by the formula

  ∀ i ∈ {0,1} : ☐♢(pc[i] = "cs") typed as \A i \in {0,1} : []<>(pc[i] = "cs")

TLC can check that this property is satisfied by every execution of the algorithm.

In Peterson's algorithm, each read or write of a global variable should be in a separate atomic action. This is not true in the PlusCal code above because statement a4 reads both flag[1-self] and turn . This can be fixed by replacing statement a4 with

        a4: while (TRUE) {
              a4a: if (flag[1-self] = FALSE) {goto cs};
              a4b: if (turn = self) {goto cs}           } ;

TLC can verify that the resulting algorithm also satisfies mutual exclusion and starvation freedom.