What concurrency evidence establishes
What this concept is
Safety says prohibited states do not occur; liveness says desired progress eventually occurs under stated assumptions. Bounded queue size and no duplicate removal are safety properties. Waking a closed queue’s waiters supports shutdown progress, but the API does not guarantee fair lock acquisition.
Why it matters here
A passing stress run samples schedules and can miss a broken predicate or lost notification. Controlled synchronization makes a specific risky state reproducible. Neither a handful of controlled cases nor sequential model enumeration proves every interleaving correct.
Concrete example
Two split increments have six order-preserving read/write schedules. Four read the old value before either write and finish at 1; two serialize and finish at 2. The supplied model enumerates all six. Protecting only writes still permits the lost-update schedules; protecting the whole read-modify-write leaves two serialized orders.
Common confusion / misconception
This interleaving model is not a demonstration that C data races have predictable outcomes; C data races are undefined behavior. Python interpreter details also do not establish your program’s compound invariant. An observed timeout may indicate a missing wakeup or simply a heavily loaded test host; inspect the reached state.
How to use it
Keep three evidence layers: sequential histories against a simple model; controlled wait/close tests with Events; a small real-thread transfer run. Capture exceptions from workers and bound test joins. Explain the missing schedules and fairness assumptions instead of declaring the queue proven race-free.
Check yourself
Can a queue remain within capacity but fail to terminate consumers? Yes: close may omit notification. Can all 100 transfers succeed while a rare shutdown race remains? Yes. Which test specifically exercises blocked producers at close?
Mini drill or application
Remove close notification and predict the blocked waiters before running. Restore it, then replace one predicate loop with if and inject a synthetic wake. Preserve both counterexamples and distinguish what each failure says about safety or progress.
Read this only if stuck
Use OSTEP concurrency introduction to map instructions to interleavings, then explain the assumptions of your own bounded model.