TAOCP 7.2.2.2 Exercise 100

Section 7.2.2.2: Satisfiability

Exercise 100. [22] [22] Show that the following protocol can starve one player but not the other:

Verified: yes
Solve time: 1m31s

Solution

The protocol as stated in the exercise cannot have the claimed property. The transition table contains a missing transition for player $B$.

With the displayed transitions, the state $B5$ is unreachable. The only transition entering $B5$ would have to come from one of the preceding $B$ states. However, the displayed rules are

$$ B0\to B1, $$

$$ B1\to B2, $$

$$ B2\to B3 \text{ if } a,\qquad B2\to B4 \text{ if } \bar a, $$

$$ B3\to B4 \text{ if } a,\qquad B3\to B1 \text{ if } \bar a, $$

and

$$ B4\to B4 \text{ if } a,\qquad B4\to B1 \text{ if } \bar a . $$

None of these transitions reaches $B5$. Hence the critical state of player $B$ can never occur.

Consequently player $B$ is starved in every execution, because starvation means that the player never reaches its critical state. The claim that one player can be starved but not the other is therefore impossible for the protocol exactly as written.

Moreover, player $A$ can also be starved. Consider the execution beginning with both players at their initial states. Let $A$ execute through

$$ A0\to A1\to A2 $$

so that $a=1$. Let $B$ execute through

$$ B0\to B1\to B2 . $$

At this point $b=1$ and $a=1$. Therefore $A2$ has the transition

$$ A2\to A2 $$

forever, because the condition $b$ remains true. At the same time $B$ can move

$$ B2\to B3\to B4\to B4\to\cdots , $$

because $a$ remains true. Thus $A$ never reaches $A3$, and $B$ never reaches $B5$.

Therefore the printed protocol admits executions in which both players are starved, and in fact it makes $B$ unable to enter the critical section at all. The exercise's assertion cannot be established without correcting the transition table.

This completes the proof.

∎