TAOCP 7.2.2.2 Exercise 101

Section 7.2.2.2: Satisfiability

Exercise 101. ▶ [31] [31] Protocol (49) has the potential defect that Alice and Bob might both be trying to set the value of $l$ at the same time. Design a mutual-exclusion protocol in which each of them controls two binary signals, visible to the other. Hint: The method of the previous exercise can be enclosed in another protocol.

Verified: no
Solve time: 2m13s

Setup

The defect in protocol (49) is that both players may attempt to write the shared variable $l$ simultaneously. The purpose of the additional two binary signals is to implement a separate mutual-exclusion protocol for access to $l$. Let Alice control the bits $a$ and $a'$, and let Bob control the bits $b$ and $b'$.

The outer protocol protects the operation “set $l$”. Once a player has acquired the outer lock, that player executes the corresponding part of protocol (49), including the assignment to $l$, and then releases the outer lock. The inner protocol (49) is unchanged except that every occurrence of “set $l$” is replaced by “enter the outer lock, set $l$, leave the outer lock”.

The required construction is therefore a mutual-exclusion protocol for the four bits $a,a',b,b'$.

Solution

Alice's outer lock protocol is

$$ \begin{array}{ll} A0.&\text{Set }a\leftarrow1,\text{ go to }A1.\ A1.&\text{If }b=0\text{ go to }A4,\text{ else go to }A2.\ A2.&\text{Set }a'\leftarrow1,\text{ go to }A3.\ A3.&\text{If }b'=0\text{ go to }A1,\text{ else go to }A3.\ A4.&\text{Critical section for setting }l.\ A5.&\text{Set }a'\leftarrow0,\text{ go to }A6.\ A6.&\text{Set }a\leftarrow0,\text{ go to the remainder of protocol (49).} \end{array} $$

Bob's protocol is the symmetric version:

$$ \begin{array}{ll} B0.&\text{Set }b\leftarrow1,\text{ go to }B1.\ B1.&\text{If }a=0\text{ go to }B4,\text{ else go to }B2.\ B2.&\text{Set }b'\leftarrow1,\text{ go to }B3.\ B3.&\text{If }a'=0\text{ go to }B1,\text{ else go to }B3.\ B4.&\text{Critical section for setting }l.\ B5.&\text{Set }b'\leftarrow0,\text{ go to }B6.\ B6.&\text{Set }b\leftarrow0,\text{ go to the remainder of protocol (49).} \end{array} $$

The two extra bits $a'$ and $b'$ act as a handshake. A player that has raised its first bit and sees the other player's first bit raised cannot enter the protected region until the other player's handshake bit has been lowered.

Verification

Assume that Alice and Bob are both in their respective protected regions for setting $l$. Then Alice has reached $A4$, so she previously passed the test in $A1$ with $b=0$. Therefore Bob's bit $b$ was $0$ when Alice entered. Likewise, Bob reached $B4$ only after passing $B1$ with $a=0$. Therefore Alice's bit $a$ was $0$ when Bob entered.

Alice reaches $A4$ only after executing $a\leftarrow1$ in $A0$. Bob reaches $B4$ only after executing $b\leftarrow1$ in $B0$. Hence both $a$ and $b$ must be $1$ while both players are in their protected regions. This contradicts the two conditions $a=0$ and $b=0$ obtained above. Therefore both players cannot be in the protected region simultaneously.

The protocol also prevents a player from entering while the other player is between its first and second signals. Suppose Alice has $a=1$ and Bob has already raised $b'=1$. Alice cannot pass $A1$, because $b=1$. She raises $a'$ and waits at $A3$. Bob cannot pass $B1$ until Alice has lowered $a'$, because Bob sees $a'=1$. Therefore the player that has already completed the handshake cannot be overtaken by the other player.

When a player leaves the protected region, it first lowers its handshake bit and then its first bit. Thus the other player can eventually pass the corresponding waiting test. The construction therefore supplies mutual exclusion for the assignment to $l$, and the original protocol (49) can use $l$ without any simultaneous writes.

The original safety argument for protocol (49) now applies, because every access to $l$ occurs inside the protected region. The four binary signals are controlled as required: Alice writes only $a,a'$, and Bob writes only $b,b'$.

This completes the proof. ∎