1. Overview

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.

2. Simplified Bakery Algorithm

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:

• For processes i and j, ``i passes j'' means that i executes the while loop i.2 with i.p=j and the condition false (i.e., num[j]=0 or num[j]>num[i]).
• For a hungry processe i and any process j, ``i passed j'' means that in its current execution of the for loop, process i has already executed the while loop i.2 with i.p=j and the condition false (i.e., num[j]=0 or num[j]>num[i]).

Proof of Safety

Suppose process i starts eating at t₀. Consider any other process j (need to show that j is not eating at t₀). At some time t₁ (< t₀), i passed j. So num[j]=0 or num[j]>num[i] holds at t₁.

Case 1:  Suppose num[j]=0 holds at t₁ . Then j is thinking at t₁ , i.e., control is at j.1. If j becomes hungry at some time t₂, it sets num[j] to a value higher than num[i]. So j cannot pass i during the interval (t₂, t₁).

Case 2:  Suppose num[j] is not equal to 0 and num[j]>num[i] holds at t₁ . Then it suffices to show that j has not yet passed i. Let j have chosen its num at time t₂ . Because num[j] is higher than num[i], t₂ must be in the interval (t₁, t₀). Thus at t₂ , j has not passed i. Thus j has not passed i at t₀ .

end of safety proof

Proof of Progress

Suppose i becomes hungry at time t₁ . 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

2. Original Bakery Algorithm

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:

• For processes i and j, ``i passes j'' means that i executes the while loop i.5 with i.p=j and the condition false (i.e., num[j]=0 or (num[j],j)>(num[i],i)).
• For a hungry processe i and any process j, ``i passed j'' means that in its current execution of the for loop, process i has already executed the while loop i.5 with i.p=j and the condition false (i.e., num[j]=0 or (num[j],j)>(num[i],i)).
• Given a statement labeled S, ``at S'' means that control is at the start of S, ``in S'' means that control is inside S, ``after S'' means that control is immediately after S. Note that if S is atomic, then ``in S'' never holds.

Proof of Safety

Suppose process i starts eating at time t₀. Consider any other process j. We need to show that process j is not eating at t₀.

Prior to entering the critical section, process i found choosing[j] to be false at some time t₁(<t₀), and passed j at some time t₂ where t₁<t₂<t₀. At t₁, process j is either at j.1 or in j.4..6.

Case 1:  Suppose at j.1 holds at t₁. Then num[j] = 0 at t₁. If num[j] changes during (t₁, t₀), 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₁. Then we have two cases:

Case 2.1:  Suppose (num[j],j) < (num[i],i) holds at t₁. Then process i would not have gotten past process j until num[j] became zero, i.e., process j completes eating, at which point this case reduces to case 1.

Case 2.2:  Suppose (num[j],j)>(num[i],i) holds at t₁. We want to show that at time t₁ process j has not gotten past process i. (This implies that process j does not get past process i before time t₀.)

Let t₃ be the time when process j last executed j.3 prior to t₁. Let t₄ be the time when process i last executed i.3 prior to t₁. t₄<t₁ holds obviously. t₃<t₁ holds because process j is in j.4..6 at t₁. There is no order between t₃ and t₄, but t₃ is after process i last executed i.1 (otherwise num[j] would be less than num[i]). Thus at t₃, 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₄, Thus at max(t₃,t₄), which is before t₁, process j has not gotten past process i. Thus process j would not get past process i before t₁.

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

Proof of Progress

Suppose process i becomes hungry at time t₁ , 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 is in group 1 if in j.3..6 (i.e. num[j] is nonzero).
• a process j is in group 2 if in j.2 and started executing j.2 before process i finished executing i.2 (i.e. num[j] is zero but it may be assigned a value less than or equal to num[i]).
• a process j is in group 3 if either it is in j.1 or it is in j.2 and it started executing j.2 after process i finished executing i.2 (i.e. num[j] is zero and if it is changed it will be assigned a value greater than num[i]).

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₁ be the number of processes in group 1 ahead of process i. Let F₂ be the number of processes in group 2. Then F₁+F₂ keeps decreasing, and so process i eventually eats.

A better metric is the lexicographically ordered two-tuple (F₂, F₁). If F₂ is non-zero, then eventually either F₂ decreases and F₁ increases or F₁ decreases. In either case the metric decreases, and it cannot go below (0,0).

end of progress proof