CMSC 412 |
NOTE 7 |
Shankar: S99 |
But the resulting algorithm is still not easy to understand. So in this note we first look at a simplified version of the bakery algorithm, based a coarser grain of atomicity than is allowed by the mutual exclusion problem. Then we look at the original version.
When process i is thinking, num[i] equals zero. When process i becomes hungry, it sets num[i] to a value higher than the num of every other process; this operation is assumed to be atomic in this simplified algorithm. Then process i scans the other processes in order. For each process j, process i waits until num[j] is either zero or greater than num[i]. After going past every process, process i enters the critical section. Upon leaving the critical section, process i zeroes num[i].
The entry and exit codes for process i are:
entry(i) { i.1: num[i] := max( num[0], num[1], ... , num[N-1] ) + 1 ; // i.1 is atomic for p := 0 to N-1 do { // p is local to process i i.2: while num[p] != 0 and num[p] < num[i] do no-op ; } } exit(i) { i.3: num[i] := 0 ; }
Notation: For brevity, we introduce the following notation:
Suppose process i starts eating at t_{0}. Consider any other process j (need to show that j is not eating at t_{0}). At some time t_{1} (< t_{0}), i passed j. So num[j]=0 or num[j]>num[i] holds at t_{1}.
Case 1: Suppose num[j]=0 holds at t_{1} . Then j is thinking at t_{1} , i.e., control is at j.1. If j becomes hungry at some time t_{2}, it sets num[j] to a value higher than num[i]. So j cannot pass i during the interval (t_{2}, t_{1}).
Case 2: Suppose num[j] is not equal to 0 and num[j]>num[i] holds at t_{1} . Then it suffices to show that j has not yet passed i. Let j have chosen its num at time t_{2} . Because num[j] is higher than num[i], t_{2} must be in the interval (t_{1}, t_{0}). Thus at t_{2} , j has not passed i. Thus j has not passed i at t_{0} .
end of safety proof
Suppose i becomes hungry at time t_{1} . We need to show that it eventually eats. Because the max operation is atomic, no two processes with non-zero nums can have their nums equal. Thus all processes with non-zero nums are totally ordered by num.
We show that queue is FIFO. A process joins the queue when its num becomes non-zero. But because this can only happen via the max operation, the process would join at the tail of the queue. The process at the head of the queue has the smallest non-zero num. So it never gets stuck in the while loop test for any process. So it eventually eats.
end of progress proof
We now consider the original bakery algorithm, that is, without assuming the max operation to be atomic. We will show that it works assuming only read-write atomicity of boolean variables and integer variables ranging over 0..N. Because the max operation is no longer atomic, two processes may get non-zero nums with the same value.
The processes share two arrays:
boolean flag choosing[i] initially false ; integer num[i] initially 0
Variables choosing[i] and num[i] are writeable by process i only and readable by all other processes. num[i] is 0 when process i is thinking. (num[i],i), when num[i] is not equal to 0, is the timestamp of process i's request. choosing[i] is true while num[i] is being set to non-zero value.
When process i becomes hungry, it sets num[i] to one higher than all the nums of the other processes. Then for each process j, process i first busy waits until process j is not in the middle of choosing a num, then it busy waits until process j's num is either zero or greater (in timestamp order) than num[i]. After going past every process, process i enters the critical section.
Upon leaving the critical section, process i zeroes num[i].
The entry and exit codes for process i are:
entry(i) { i.1: choosing[i] := TRUE ; i.2: num[i] := max( num[0], num[1], ... , num[N-1] ) + 1 ; i.3: choosing[i] := FALSE ; for p := 0 to N-1 do { // p is local to process i i.4: while choosing[p] do skip ; i.5: while num[p] != 0 and (num[p],p)<(num[i],i) do skip ; } } exit(i) { i.6: num[i] := 0 ; }
Notation: For brevity, we introduce the following notation:
Suppose process i starts eating at time t_{0}. Consider any other process j. We need to show that process j is not eating at t_{0}.
Prior to entering the critical section, process i found choosing[j] to be false at some time t_{1}(<t_{0}), and passed j at some time t_{2} where t_{1}<t_{2}<t_{0}. At t_{1}, process j is either at j.1 or in j.4..6.
Case 1: Suppose at j.1 holds at t_{1}. Then num[j] = 0 at t_{1}. If num[j] changes during (t_{1}, t_{0}), it would become higher than (num[i],i) and process j would not get past process i.
Case 2: Suppose process j is in j.4..6 at t_{1}. Then we have two cases:
Case 2.2: Suppose (num[j],j)>(num[i],i) holds at t_{1}. We want to show that at time t_{1} process j has not gotten past process i. (This implies that process j does not get past process i before time t_{0}.)
Let t_{3} be the time when process j last executed j.3 prior to t_{1}. Let t_{4} be the time when process i last executed i.3 prior to t_{1}. t_{4}<t_{1} holds obviously. t_{3}<t_{1} holds because process j is in j.4..6 at t_{1}. There is no order between t_{3} and t_{4}, but t_{3} is after process i last executed i.1 (otherwise num[j] would be less than num[i]). Thus at t_{3}, process i is either choosing a num or has its num. Thus process j gets past j.4 with j.p=i only after t_{4}, Thus at max(t_{3},t_{4}), which is before t_{1}, process j has not gotten past process i. Thus process j would not get past process i before t_{1}.
In any case, process process j would not be eating.
Note that a proof by contradiction would probably be a bit shorter.
end of safety proof
Suppose process i becomes hungry at time t_{1} , i.e. executes i.1. We need to show that it eventually eats. The only places where process i can get stuck indefinitely are the while loops i.4 and i.5. So it suffices to show that this does not happen.
Rather than arguing at the level of the statements, it is instructive to take a more abstract view. With respect to a hungry process i, we can divide the processes into four groups:
A process j in group 1 with (num[i],i)<(num[j],j) holding will not eat before process i eats (because j will not get past process i). Thus the group 1 processes are queued in their timestamp order.
A process j in group 2 eventually joins group 1 (because the execution of j.2 cannot be blocked by other processes). It can join at any place in the ``timestamp queue'' of group 1, i.e., it does not have to join at the end.
A process j in group 3 may eventually join group 1, but it will only do so behind process i.
If process j is at the head of group 1's queue, then eventually either j will eat or another process (from group 2) will get ahead of it.
Let F_{1} be the number of processes in group 1 ahead of process i. Let F_{2} be the number of processes in group 2. Then F_{1}+F_{2} keeps decreasing, and so process i eventually eats.
A better metric is the lexicographically ordered two-tuple (F_{2}, F_{1}). If F_{2} is non-zero, then eventually either F_{2} decreases and F_{1} increases or F_{1} decreases. In either case the metric decreases, and it cannot go below (0,0).
end of progress proof