Correctness of the readers and writers algorithm

Proving monitors can be relatively succinct, because monitor invariants are only required to hold outside the monitor procedures themselves. Furthermore, the immediate resumption requirement allows us to infer that what was true before executing a Signal is true when a process blocked on that condition becomes unblocked.

Let R be the number of readers currently reading and W the number of writers currently writing. The proof of the following lemma is immediate from the structure of the program.

Lemma 7.1 The following formulas are invariant:

\[ R > 0 \] \[ W > 0 \] \[ R = readers \] \[ W = writers \]

We implicitly use these invariants to identify changes in the values of the program variables readers and writers with changes in the variables R and W that count processes. The safety of the algorithm is expressed using the variables R and W:

Theorem 7.2 The following formula is invariant: \[ ( R > 0 \rightarrow W=0 ) \land ( W \leq 1) \land ( W =1 \rightarrow R = 0)\]

In words, if a reader is reading then no writer is writing; at most one writer is writing; and if a writer is writing then no reader is reading.

Proof: Clearly, the formula is initially true. Because of the properties of the monitor, there are eight atomic statements: execution of the four monitor operations from start to completion, and execution of the four monitor operations that include signalC statements unblocking a waiting process.

Consider first executing a monitor operation from start to completion:

  • StartRead: This operation increments R and could falsify \( R > 0 \rightarrow W =0\), but the if statement ensures that the operation completes only if \(W = 0\) is true. The operation could falsify \(R = 0\) and hence \(W = 1 \rightarrow R = O\), but again the if statement ensures that the operation completes only if \(W = 1\) is false.

  • EndRead: This operation decrements R, possibly making \(R > 0\) false and \(R = O\) true, but these changes cannot falsify the invariant.

  • StartWrite: This operation increments W and could falsify \(W < 1\), but the if statement ensures that the operation completes only if \(W = 0\) is true. The operation could falsify \(W = 0\) and hence \(R > 0 \rightarrow W = 0\), but the if statement ensures that \(R > 0\) is false.

  • EndWrite: This operation decrements W,so \(W = 0\) and \(W < 1\) could both become true while \(W = 1\) becomes false; these changes cannot falsify the invariant.

Consider now the monitor operations that result in unblocking a process from the queue of a condition variable.

  • signal(OKtoRead) in StartRead: The execution of StartRead including signal(OKtoRead) can cause a reader r to become unblocked. But the if statement ensures that this happens only if \(W = 0\), and the IRR ensures that r continues its execution immediately so that \(W = 0\) remains true.

  • signal(OKtoRead) in EndWrite: By the inductive hypothesis, \(W < 1\), so \(W = 0\) when the reader resumes, preserving the truth of the invariant.

  • signal(OKtoWrite) in EndRead: The signal is executed only if \(R = 1\) upon starting the operation; upon completion \(R = 0\) becomes true, preserving the truth of the first and third subformulas. In addition, if \(R = 1\), by the inductive hypothesis we also have that \(W = 0\) was true. By the IRR for StartWrite of the unblocked writer, \(W = 1\) becomes true, preserving the truth of the second subformula.

  • signal(OKtoWrite) in EndWrite: By the inductive hypothesis \(W < 1\), the writer executing EndWrite must be the only writer that is writing so that \(W = 1\). By the IRR, the unblocked writer will complete StartWrite, preserving the truth of \(W = 1\) and hence \(W < 1\). The value of R is, of course, not affected, so the truth of the other subformulas is preserved.

The expressions not empty(OKtoWrite) in StartRead and empty(OKtoRead) in EndWrite were not used in the proof because they are not relevant to the safety of the algorithm.

We now prove that readers are not starved and leave the proof that writers are not starved as an exercise. It is important to note that freedom from starvation holds only for processes that start executing StartRead or StartWrite, because starvation is possible at the entrance to a monitor. Furthermore, both reading and writing are assumed to progress like critical sections, so starvation can occur only if a process is blocked indefinitely on a condition variable.

Let us start with a lemma relating the condition variables to the number of processes reading and writing:

Lemma 7.3 The following formulas are invariant:

\[\neg empty(OKtoRead) \rightarrow (W \neq 0) \lor \neg empty(OKtoWrite)\] \[\neg empty(OKtoWrite) \rightarrow (R \neq 0) \lor (W \neq 0).\]

Proof: Clearly, both formulas are true initially since condition variables are initialized as empty queues.

The antecedent of the first formula can only become true by executing StartRead, but the if statement ensures that the consequent is also true. Can the consequent of the formula become false while the antecedent is true? One way this can happen is by executing EndWrite for the last writer. By the assumption of the truth of the antecedent = empty(OKtoRead), signalC(OKtoRead) is executed. By the IRR, this leads to a cascade of signals that form part of the atomic monitor operation, and the final signal falsifies \(\neg\) empty(OKtoRead). Alternatively, EndRead could be executed for the last reader, causing signalC(OKtoWrite) to falsify a empty(OKtoWrite). But this causes \((W \neq 0)\) to become true, so the consequent remains true.

The truth of the second formula is preserved when executing StartWrite by the condition of the if statement. Can the consequent of the formula become false while the antecedent is true? Executing EndRead for the last reader falsifies \(R \neq 0\), but since - empty(OKtoWrite) by assumption, signalC(OKtoWrite) makes \(W \neq 0\) true. Executing EndWrite for the last (only) writer could falsify \(W \neq 0\), but one of the signalC statements will make either \(R \neq 0\) or \(W \neq 0\) true.

Theorem 7.4 Algorithm 7.4 is free from starvation of readers.

Proof: Ifa reader is starved is must be blocked indefinitely on OKtoRead. We will show that a signal(OKtoRead) statement must eventually be executed, unblocking the first reader on the queue. Since the condition queues are assumed to be FIFO, it follows by (numerical) induction on the position of a reader in the queue that it will eventually be unblocked and allowed to read.

To show

\[\neg empty(OKtoRead) \rightarrow \diamond signalC(OKtoRead)\]

assume to the contrary that

\[\neg empty(OKtoRead) \land \square \neg signalC(OKtoRead).\]

By the first invariant of Lemma 7.3, \((W \neq 0) \lor \neg empty(OKtoWrite)\). If ( W \neq 0), by progress of the writer, eventually EndWrite is executed; signalC(OKtoRead) will be executed since by assumption \(\neg\) empty(OKtoRead) is true (and it remains true until some signalC(OKtoRead) statement is executed), a contradiction.

If \(\neg\) empty(OKtoWrite) is true, by the second invariant of Lemma 7.3, \((R \neq 0) \lor (W \neq 0)\). We have just shown that \(W \neq 0\) leads to a contradiction, so consider the case that \(R \neq 0\). By progress of readers, if no new readers execute StartRead, all readers eventually execute EndReader, and the last one will execute signalC(OKtoWrite); since we assumed that > empty(OKtoWrite) is true, a writer will be unblocked making \(W \neq 0\) true, and reducing this case to the previous one. The assumption that no new readers successfully execute StartRead holds because = empty(OKtoWrite) will cause a new reader to be blocked on OKtoRead.