TAOCP 7.2.2.2 Exercise 102

The error in the previous solution is that it tries to simulate flickering reads by branching on the _value of the shared variable_ $v$.

taocpmathematicsalgorithmsvolume-4medium

Section 7.2.2.2: Satisfiability

Exercise 102. [22] [22] If Alice is setting a variable at the same time that Bob is trying to read it, we might want to consider a more stringent model under which he sees either 0 or 1, nondeterministically. (E.g., if he looks $k$ times before she moves to the next step, he might see $2^k$ possible sequences of bits.) Explain how to handle this model of "flickering" variables by modifying the clauses of exercise 87.

Verified: yes
Solve time: 2m17s

The error in the previous solution is that it tries to simulate flickering reads by branching on the value of the shared variable $v$. In the flickering model, the read result is not derived from $v$ at all, even nondeterministically. Each inspection produces an independent Boolean choice. The correct SAT encoding must therefore decouple reads from the state of $v$, not correlate them with it.

Correct solution

We start from the clauses of Exercise 87, where shared-memory operations are encoded in SAT under the standard model: a read of variable $v$ returns the current value of $v$, so read-literals are constrained to equal the value written by the last relevant write.

In the flickering model, this constraint is removed. A read during a write does not observe $v$; instead, each inspection yields an independent nondeterministic bit. Formally, every individual inspection is an unconstrained Boolean choice.

Step 1: Correct abstraction of a flickering read

For every read event $r$ of a variable $v$, and for every inspection of that read in the encoding of Exercise 87, introduce a fresh Boolean variable

$$ x_{r,i} $$

representing the value observed at the $i$-th inspection of that read event.

Key point: $x_{r,i}$ is not related to $v$ in any way. It is an independent Boolean degree of freedom.

Step 2: Clause transformation

Take every clause $C$ from Exercise 87. Each literal in such a clause is of one of two types:

  1. Write-derived literal (depends on memory state of $v$)
  2. Read-derived literal (depends on the value returned by a read event)

We modify clauses as follows:

  • If a literal refers to a write state of $v$, leave it unchanged.
  • If a literal corresponds to a read of $v$ (or any inspection of such a read), replace it by the corresponding fresh variable $x_{r,i}$.
  • If the literal is negated, replace it by $\neg x_{r,i}$.

Thus each clause $C$ becomes a clause $C'$ over the extended variable set.

Step 3: No additional constraints

No clauses are added to relate $x_{r,i}$ to $v$. In particular, there is no implication of the form $x_{r,i} \leftrightarrow v$, nor any probabilistic or nondeterministic coupling. Each $x_{r,i}$ is completely free.

This is essential: the flickering model explicitly allows the read result to disagree arbitrarily with the true value of $v$, even within the same write interval.

Step 4: Correctness argument

Any execution of the system in the flickering model corresponds to:

  • a choice of values for all shared variables $v$ at write events, and
  • an independent choice of a Boolean value for each inspection variable $x_{r,i}$.

Conversely, any satisfying assignment of the modified SAT clauses corresponds to a valid execution trace in this model, since:

  • write behavior is still constrained exactly as in Exercise 87,
  • read behavior imposes no constraints beyond the local clause structure,
  • and all nondeterministic observations are explicitly represented.

Thus satisfiability of the transformed clause set is equivalent to correctness of the original protocol under flickering semantics.

Why the previous approach fails

The rejected solution incorrectly replaced a flickering read literal $l$ by $v$ or $\neg v$, which implicitly assumes that even erroneous observations are still functions of the underlying memory value. This is incompatible with the model.

The correct model introduces new independent variables, rather than branching on the existing one. No enumeration over $2^k$ cases is required, because independence is represented syntactically by fresh variables.

This completes the corrected modification of the clauses of Exercise 87 under the flickering-variable model. ∎