Notebook 26: Producer–Consumer Fairness Sandbox

Schedule the producer and consumer processes yourself, one asynchronous step at a time, and watch what an unfair run looks like before it ever becomes an infinite counterexample.

Producer–Consumer Fairness Sandbox

Chapter 7’s asynchronous producer–consumer example (ex:prod-cons) has a two-cell shared buffer. At each step, the scheduler runs at most one of the two processes; the other remains idle. This notebook lets you be the scheduler.

  • Producer fills the leftmost empty cell.
  • Consumer always empties cell 0; it keeps cell 1 only if cell 0 was non-empty just before running.

The property to watch is \(\mathbf{G}(\mathit{full} \to \mathbf{F}(\mathit{empty\_cell}))\): whenever the buffer is full, some cell is eventually freed. Without fairness, this is false—and you can build the exact schedule that breaks it.

Buffer

Schedule so far

What to try

  1. Fill the buffer, then click “Run Producer ×10”. The buffer is already full, so every extra producer step changes nothing—but the warning box still fires, because consumer.running stays enabled (the buffer has a non-empty cell) and is never taken. That is exactly the justice violation from the chapter’s fairness example: continued forever, this schedule refutes \(\mathbf{G}(\mathit{full} \to \mathbf{F}(\mathit{empty\_cell}))\).
  2. Alternate Producer/Consumer by hand. The buffer should never sit full for long, and the warning box should stay green.
  3. Notice what the badges track. “Producer enabled” and “consumer enabled” are exactly the formal Enabled predicate from the chapter’s fairness definitions (def:enabled)—a process being enabled is a fact about the current state, independent of whether the scheduler actually picks it.

[!TIP] Read the full chapter in the PDF

For the formal definitions of enabled/taken states, justice, and compassion that this sandbox visualizes, see Chapter 7, §“Fairness Constraints”.

Download the Full Lecture Notes (PDF)