The final bugfix: using (logically) two separate mutexes for producers and consumers.
Instead of a single wait set for all threads, we separate waiting producers from waiting consumers.
With a single mutex/condition variable, notifyAll() wakes up ALL threads — including those that definitely cannot proceed. With separate conditions for "buffer not full" and "buffer not empty," we can be more precise.
This is exactly the kind of bug that TLA+ excels at finding: subtle concurrency issues that only manifest in specific interleavings.
Remove notifyAll and instead introduce two mutexes (one for Producers and one for Consumers). A Consumer will notify the subset of Producers waiting on the Producer mutex (vice versa for a Producer).
The spec does not have to introduce two mutexes. Instead, we can just pick the right thread type from the set of waiting threads. This fix completely solves the bug, but are we fully satisfied yet?