Proof Outlines

Since each labelled instruction in the trying and exit regions accesses at most one shared variable, it is set to correspond to a step of a process. That is, each labelled instruction in the algorithm is atomic. For each process i, pci is defined as the program counter of i; for instance, pci = T1 at a system state means that step T1 of process i is enabled. A private variable v of process i is denoted as vi. Finally, a process i in T, C or E is defined as a controller provided that predi = nil.

Mutual Exclusion

In the algorithm, whether a process in T can enter C depends on the value of Receiver. If Receiver = nil, then a controller waiting for nil in T is permitted to enter C, while if Receiver = i, 1 ≤ i ≤ n, then only process i is permitted to do so.

Inspection of the algorithm clearly indicates that only the process in E can modify Receiver’s value to nil or the identity of some other process using one of steps E4, E5, E7 or E8. (Although a controller in T modifies Receiver ’s value by executing T6, it sets Receiver to its identity, allowing no other process to enter C.) We show

that a nil can be taken as the permission for at most one process. Hence, a process in E allows at most one process to enter C. Additionally, since Receiver is set to nil initially, and a nil permits at most one process to enter C, at most one process can enter C from the starting state. Thus, the mutual exclusion condition is ensured.

The following lemma states that at most one controller is at T4, T5, or T6. In other words, at most one controller is waiting for nil at any reachable system state.

Once Receiver = nil, the controller enters C after step T6, which sets Receiver to its identity, a non-nil value. Thus, a nil in Receiver permits at most one process to enter C.

Lemma 4.1 At any reachable system state,

| { i ∈ P | predi = nil ∧ pci ∈ {T4, T5, T6}} | ≤ 1.

Proof. Since each process is in R at an initial system state, no process is in the set and thus the statement is true. We then argue that if a process enters the set at a systems state, no other process can enter the set until it leaves the set.

Consequently, starting from an initial state, at most one process is in the set at all reachable system states.

The steps that could cause processes to enter the set are considered. A process i can enter the set exactly if predi = nil after step T1, which simultaneously sets L := i. Before process i modifies L’s value to nil by executing step E2, no other process can obtain nil from L when executing step T1, and therefore no other process will enter the set. That is, no process can enter the set until i leaves the set. 2 . Since a process in E allows at most one process to enter C and at most one process can enter C from the starting state, the following theorem holds.

Theorem 4.2 The algorithm guarantees mutual exclusion.

Progress

We argue that the algorithm satisfies the lockout-freedom condition, that if no process stays in C indefinitely, any process in T eventually enters C ; and any

process in E eventually enters R. A lockout-free algorithm is intuitively also an algorithm satisfying the progress condition.

Theorem 4.3 The algorithm guarantees lockout-freedom.

Proof. The argument for the exit region is simply that 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 first show that each request is properly recorded in a list, and then argue that each list will receive the permission to enter C.

In the algorithm, each process i makes a request by performing f etch&store(L, i) (T1). A process that succeeds in acquiring nil from L starts a waiting list and becomes the controller of the list. Suppose a list controller gains permission to enter C at a later point. After passing through C, the controller closes the list by executing E2 which obtains the identity of the tail and modifies L’s value to nil, and then starts to convey the permission along the list from the tail. Before the controller closes the list, all processes that perform step T1 after the controller reads nil from L are well organized into the list, in which the controller has the identity of the tail and each other process in the list has the identity of its predecessor. Since L’s value is changed to nil, subsequent requests form a new list in the same way.

That is, in an execution fragment that starts with a system state at which L has the nil value and ends with a system state at which L’s value is changed to nil, all requesting processes form a list. Thus, each request is properly recorded in a list. Clearly, a closed list contains a finite number of waiting processes, since each process can occur in a list at most once.

To prove that each requesting process eventually enters C, it remains to be shown that each controller receives the permission. Since Receiver is initially set to nil, the first controller always gains the permission. The controller closes the list, and conveys the permission to the tail of the list, when it leaves C. Since a closed list contains a finite number of processes, if no process stays in C indefinitely, then each process in the list eventually gains the permission to enter C. When the process next

to the controller receives the permission, since its pred equals Head , it redirects the permission to the next controller by setting Receiver to nil after passing through C. (From Lemma 4.1, if one controller is waiting for nil, exactly one such controller exists.) Thus, each controller eventually receives the permission. 2

Bounded Bypass

A process i is said to be in the doorway if pci = T1, and it is said to be in the waiting part if pci ∈ {T2, . . . , T8}. As shown in the proof of Theorem 4.3, a process is recorded in a waiting list after passing through its doorway (i.e., after executing T1). Since a list does not receive the permission until each process in the previous list has left C, a process in a list may be bypassed by those processes in the same list and in the previous list. In addition, because a process can occur in a list at most once, a waiting process may be bypassed by any individual process at most twice. In other words, the algorithm satisfies 2-bounded bypass. The worst case, in which a process that has finished its doorway is bypassed twice by another process, may occur when a non-controller in a list quickly makes a request appending to the new list after receiving the permission. For example, in Fig. 4.1(f–h), process 7 is bypassed twice by process 4, which makes a request after receiving the permission.

Consequently, the following theorem holds.

Theorem 4.4 The algorithm guarantees 2-bounded bypass.