Appendix H. Peterson's Algorithm
In 1981, Gary L. Peterson came up with a beautiful solution to the mutual exclusion problem, now known as ``Peterson's Algorithm'' [37]. Figure 5.6 presents the algorithm. Why does it work? We will focus here on how one might go about proving mutual exclusion for an algorithm such as Peterson's. It turns out that doing so is not trivial. You have to understand a little bit about how the Harmony virtual machine (HVM) works. In Chapter 4 we talked about the concept of state: at any point in time the HVM is in a specific state. A state is comprised of the values of the shared variables as well as the values of the thread variables of each thread, including its program counter and the contents of its stack. Each time a thread executes a HVM machine instruction, the state changes (if only because the program counter of the thread changes). We call that a step. Steps in Harmony are atomic.
The HVM starts in an initial state in which there is only one thread ( __init__ ()) and its program counter is 0. A trace is a sequence of steps starting from the initial state, resulting in a sequence of states. When making a step, there are two sources of non-determinism in Harmony. One is when there is more than one thread that can make a step. The other is when a thread executes a choose operation and there is more than one choice. Because there is non-determinism, there are multiple possible traces. We call a state reachable if it is either the initial state or it can be reached from the initial state through a finite trace. A state is final when there are no threads left to make state changes.
It is often useful to classify states. Initial, final, and reachable, and unreachable are all examples of classes of states. Figure I.1 depicts a Venn diagram of various classes of states and a trace. One way to classify states is to define a predicate over states. All states in which x = 1, or all states where there are two or more threads executing, are examples of such predicates. For our purposes, it is useful to define a predicate that says that at most one thread is in the critical section. We shall call such states exclusive.
Figure I.1. Venn diagram classifying all states and a trace
An invariant of a program is a predicate that holds over all states that are reachable by that program. We want to show that exclusivity is an invariant because mutual exclusion means that all reachable states are exclusive. In other words, we want to show that the set of reachable states of executing the program is a subset of the set of states where there is at most one thread in the critical section.
One way to prove that a predicate is an invariant is through induction on the number of steps. First you prove that the predicate holds over the initial state. Then you prove that for every reachable state, and for every step from that reachable state, the predicate also holds over the resulting state. For this to work you would need a predicate that describes exactly which states are reachable. But we do not have such a predicate: We know how to define the set of reachable states inductively, but—given an arbitrary state—it is not easy to see whether it is reachable or not.
To solve this problem, we will use what is called an inductive invariant. An inductive invariant is a predicate over states that satisfies the following:
For any state in which
turn
turn
One candidate for such a predicate is exclusivity itself. After all, it certainly holds over the initial state. And as Harmony has already determined, exclusivity is an invariant: It holds over every reachable state. Unfortunately, exclusivity is not aninvariant. To see why, consider the following state: let thread 0 be at labeland thread 1 be at the start of thestatement. Also, in state= 1. Now let thread 1 make a step. Because= 1, thread 1 will stop waiting and also enter the critical section, entering a state that is not exclusive. So, exclusivity is an invariant (holds over every reachable state, as demonstrated by Harmony), but not an inductive invariant. It will turn out thatis not reachable.
We are looking for an inductive invariant that implies exclusivity. In other words, the set of states where the inductive invariant holds must be a subset of the set of states where there is at most one thread in the critical section.
Let us begin with considering the following important property: (i) = thread(i)@[10 17] ⇒ flags[i], that is, if thread i is executing in lines 10 through 17, then flags[i] is set. Although it does not, by itself, imply exclusivity, we can show that (i) is an inductive invariant (for both threads 0 and 1). To wit, it holds in the initial state, because in the initial state thread i does not even exist yet. Now we have to show that if (i) holds in some state, then (i) also holds in a next state. Since only thread i ever changes flags[i], we only need to consider steps by thread i. Since (i) holds, there are two cases to consider:
states in which flags [ i ] = true states in which ¬ thread ( i )@[10 17] (because false implies anything)
i
flags
i
i
flags
i
i
i
In each case, we need to show that if threadtakes a step, then) still holds. In the first case, there is only one step that threadcan take that would set] to false: the step from line 17 to line 18. But executing the line would also take the thread out of lines 1017, so) continues to hold. In the second case (threadis not executing in lines 1017), the only step that would cause threadto execute in lines 1017 would be the step in line 9. But in that case] would end up being true, so) continues to hold as well. So,) is an inductive invariant (for both threads 0 and 1).
While (i) does not imply mutual exclusion, it does imply the following useful invariant: thread(i)@cs ⇒ flags[i]: when thread i is at the critical section, flags[i] is set. This seems obvious from the code, but now you know how to prove it. We will use a similar technique to prove the exclusivity is invariant.
We need a stronger inductive invariant than (i) to prove mutual exclusion. What else do we know when thread i is in the critical section? Let (i) = ¬flags[1 - i] ∨ turn = i , that is, the condition on the await statement for thread i. In a sequential program, (i) would clearly hold if thread i is in the critical section: thread(i)@cs ⇒ (i). However, because thread 1 - i is executing concurrently, this property does not hold. You can use Harmony to verify this. Just place the following command in the critical section of the program:
assert (not flags[1 - self]) or (turn == self)
flags
turn
flags
C
i
thread
i
cs
i
∨
thread
-
i
i
-
i
When running Harmony, this assertion will fail. You can check the HTML output to see what happened. Suppose thread 0 is at the critical section,[0] = true,= 1, and thread 1 just finished the step in line 7, setting[1] to true. Then(0) is violated. But it suggests a new property:) =)@(1)@12. That is, if threadis at the critical section, then either) holds or thread 1is about to execute line 12.
(i) is an invariant for i = 0,1. Moreover, if (i) and (i) both hold for i = 0,1, then mutual exclusion holds. We can show this using proof by contradiction. Suppose mutual exclusion is violated and thus both threads are in the critical section. By it must be the case that both flags are true. By and the fact that neither thread is about to execute Line 12, we know that both C(0) and C(1) must hold. This then implies that turn = 0 ∧ turn = 1, providing the desired contradiction.
We claim that (i) is an inductive invariant. First, since neither thread in in the critical section in the initial state, it is clear that (i) holds in the initial state. Without loss of generality, suppose i = 0 (a benefit from the fact that the algorithm is symmetric for both threads). We still have to show that if we are in a state in which (0) holds, then any step will result in a state in which (0) still holds.
First consider the case that thread 0 is at label cs. If thread 0 were to take a step, then in the next state thread 0 would be no longer at that label and (0) would hold trivially over the next state. Therefore we only need to consider a step by thread 1. From we know that one of the following three cases must hold before thread 1 takes a step:
flags[1] = False; turn = 0; thread 1 is about to execute Line 12.
flags
flags
Let us consider each of these cases. We have to show that if thread 1 takes a step, then one of those cases must hold after the step. In the first case, if thread 1 takes a step, there are two possibilities: Either[1] will still be(in which case the first case continues to hold), or[1] will beand thread 1 will be about to execute Line 12 (in which case the third case will hold). We know that thread 1 never setsto 1, so if the second case holds before the step, it will also hold after the step. Finally, if thread 1 is about to execute Line 12 before the step, then after the stepwill equal 0, and therefore the second case will hold after the step.
Now consider the case where thread 0 is not in the critical section, and therefore (0) holds trivially because false implies anything. There are three cases to consider:
Thread 1 takes a step. But then thread 0 is still not in the critical section and Thread 0 takes a step but still is not in the critical section. Then again Thread 0 takes a step and ends up in the critical section. Because thread 0 entered the critical section, we know that flags}[1] = False or turn = 0 because of the await condition. And hence
We have now demonstrated mutual exclusion in Peterson's Algorithm in two different ways: one by letting Harmony explore all possible executions, the other using inductive invariants and proof by induction. The former is certainly easier, but it does not provide intuition for why the algorithm works. The second provides much more insight.
Even though they are not strictly necessary, we encourage you to include invariants in your Harmony code. They can provide important insights into why the code works.
A cool anecdote is the following. When the author of Harmony had to teach Peterson's Algorithm, he refreshed his memory by looking at the Wikipedia page. The page claimed that the following predicate is invariant: If thread i is in the critical section, then (i) (i.e., without the disjunct that thread 1 - i is about to execute Line 12. We already saw that this is not an invariant. (The author fixed the Wikipedia page with the help of Fred B. Schneider.)
This anecdote suggests the following. If you need to do a proof by induction of an algorithm, you have to come up with an inductive invariant. Before trying to prove the algorithm, you can check that the predicate is at least invariant by testing it using Harmony. Doing so could potentially avoid wasting your time on a proof that will not work because the predicate is not invariant, and therefore not an inductive invariant either. Moreover, analyzing the counterexample provided by Harmony may well suggest how to fix the predicate.
Exercises