3.3 Huang’s Algorithm
3.3.2 A Correctness Argument
Mutual Exclusion
In the algorithm, a process i has permission to enter C exactly if it obtains nil from L when executing T1 (i.e., pred = nil) or Spin(i) 6= (nil, nil). Since a process that obtains nil when executing T1 writes its identity, a non-nil value, to L in the same step, a nil in L permits at most one process to gain permission. Initially, L is set to nil and Spin(i) = (nil, nil) for each process i. Thus, at most one process may enter C initially.
To prove mutual exclusion, we focus on steps that may cause some process to gain permission, that is, on steps that may set L to nil or modify some process’s spin variable. Inspection of the algorithm clearly indicates that only steps E8, E10, and E12 need to be considered.
• Step E8 (tail := compare&swap(L, head, nil)) assigns the current value of L
to tail, and modifies L’s value to nil only if L = head. If the step indeed modifies L’s value, it is regarded as successful. A successful E8 allows at most one process to gain permission.
• Each of E10 and E12 modifies some process’s spin variable. Since the spin variables of any two processes are distinct, each of the two steps allows at most one process to gain permission.
According to the algorithm, a process that executes a successful E8 bypasses E10 since tail = head. Hence, a process in E executes exactly one of the following steps:
successful E8, E10, or E12. That is, a process in E passes its permission to at most one process.
Since at most one process may gain permission initially and each process having permission passes its permission to at most one process, the following lemma holds.
Lemma 3.1 Huang’s algorithm guarantees mutual exclusion.
Lockout-freedom
We now show that the algorithm is lockout-free. This also implies that the algorithm satisfies progress.
Before proving the lockout-freedom condition, we present several definitions that intend to organize all requests in an execution. First, a busy period is an execution fragment that starts with a step T1 that succeeds in acquiring nil from L, and ends with the following successful E8, which modifies L’s value to nil. Since L = nil initially, all occurrences of T1 (i.e., all requests) in an execution can be divided into busy period(s). In a busy period, each requesting process except the first one has the identity of its predecessor because each process makes a request by executing T1 on the same shared variable L.
Next, we try to divide all requests in a busy period into lists. A list in a busy period is a sequence of processes that execute T1 between the first T1, which obtains nil from L, and the following unsuccessful E8, or between an unsuccessful E8 and
the next unsuccessful one. Starting from the last process in a list, we can trace the whole list from the tail to the head through the value of pred of each process in the list. A process that executes E8 is called a controller. If a controller executes an unsuccessful E8, then it defines a new list and is also called the controller of the new list. Otherwise, if a controller executes a successful E8, then it ends the busy period.
Lemma 3.2 Huang’s algorithm guarantees lockout-freedom.
Proof. The argument for the exit region is simple. Since no loop occurs in the exit region, each process in E eventually enters R.
The lockout-freedom condition for the trying region is now considered. We argue that each requesting process in any busy period of an admissible execution eventually enters C.
In a busy period, the first T1 obtains nil from L and thus the first requesting process eventually enters C. When leaving C, the process identifies itself as a con-troller since pred = nil. After executing E4 to assign its current identity to head, it executes E8. When it executes E8, if L = head (i.e., no other request exists), it modifies L’s value to nil in the same step and ends the busy period. Otherwise, it defines the first list and is the controller of the list. We need to prove that each requesting process in the first list and all possible subsequent lists eventually enters C.
We show that each requesting process in the ith list, called list i, eventually enters C, and only the head of the list is selected as a new controller by induction on i.
Basis: i = 1. List 1 contains all processes that make requests between the first T1 in the busy period and the unsuccessful E8 executed by the controller of list 1.
Through the returned value of compare&swap in E8, the controller has the identity of the tail of the list. Lemma 3.1 implies that at most one process has permission at any system state. Thus, before the controller passes the permission to the tail, all requesting processes will be blocked at T3. The controller then executes E10 to
pass the permission to the tail by writing pair (head, tail) to the tail’s Spin variable, where head is the controller’s identity and tail is the tail’s identity. In list 1, each process except the head will not be selected as a new controller since pred 6= nil and pred 6= head, and will pass the permission to its predecessor by executing E12.
Thus, the permission will be conveyed along the whole list from the tail to the head so that each process in list 1 eventually enters C. When the head of list 1 leaves C, it identifies itself as a new controller since its pred is equal to the previous controller’s identity (i.e., pred = head).
Inductive step: Assume that each process in list i eventually enters C and only the head of the list is selected as a new controller. While the permission is conveyed along list i, all subsequent requesting processes, including those that are in list i and make requests again, will be blocked at T3.
According to the induction hypothesis, the head of list i identifies itself as a new controller after leaving C. The new controller executes E6 to assign the identity of the tail of list i to its head. Since a process always switches its identity in E15, if the process at the tail of list i makes a request, after having been given permission, it has a different identity. Thus, if L = head holds when the new controller executes E8, then no other request exists. The new controller modifies L’s value to nil in the same step and ends the busy period. Otherwise, it defines list i + 1 and is the controller of list i + 1. List i + 1 contains all requesting processes that make requests between the previous unsuccessful E8, which defines list i, and the unsuccessful E8 executed by the controller of list i + 1. The controller then passes the permission to the tail of list i + 1 by writing pair (head, tail) to the tail’s Spin variable, where head is the identity of the tail of list i and tail is the identity of the tail of list i + 1.
It remains to show that the permission will be conveyed along the whole list.
Although the process at the tail of list i may be a member of list i + 1, it has a different identity when it appears in list i + 1. Therefore, in list i + 1, only the head will identify itself as a new controller when checking whether its predecessor’s identity equals the identity of the tail of list i. The permission will be conveyed along the whole list so that each process in list i + 1 eventually enters C. 2
Bounded Bypass
In a busy period of an execution, since a list does not receive the permission until each process in the previous list has left C, the algorithm satisfies bounded bypass.
Lemma 3.3 Huang’s algorithm guarantees bounded bypass.
Chapter 4
Tight Bound on Space Complexity
In this chapter, two algorithms are proposed for systems under time and mem-ory constraints. Each of the algorithms utilizes constant two shared variables with fetch&store as well as read/write. The first algorithm satisfies the bounded bypass condition; the second is an improvement on the first that satisfies the FCFS condi-tion. To improve the fairness, the FCFS algorithm increases the number of values taken on by a shared variable from (n + 1)2 to 2(n + 1)3, where n is the number of all processes.
Additionally, a lower bound result shows that any bounded-bypass algorithm using the same set of primitives must utilize at least two shared variables. The proposed algorithms are therefore space-optimal. In other words, a tight bound of two on the number of shared variables is obtained.
The computational model adopted in this chapter is the shared memory model.
The formal description of the model appears in Chapter 2.
4.1 The 2-bounded-bypass Algorithm
This section presents a bounded-bypass mutual exclusion algorithm using two shared variables, as shown in Fig. 4.2. Figure 4.1 illustrates an example to help explain the working of the algorithm.
In summary, the algorithm links competing processes as circular lists by fetch&store
along with a shared variable. The permission to enter the critical region is trans-mitted along a list after its construction. While the permission is transtrans-mitted, subsequent requests constitute a new waiting list. The new list is closed when each process in the old list has left its critical region, at which time the new list re-ceives the permission. Likewise, after the new list is closed, subsequent requesting processes form another list and wait for the permission. Roughly speaking, permis-sion is conveyed along a list and then passed to the next waiting list. The algorithm thus satisfies the bounded bypass condition.
According to the construction of a list, a competing process has the identity of its predecessor rather than its successor. Consequently, the permission is conveyed from the tail of a list to the head, resulting in the failure to meet the FCFS condi-tion. The next section describes a modified algorithm that eliminates this drawback and achieves the FCFS condition by initiating an additional phase for every list to redirect the links in the list.