Upstream v13 calls this fix "(Logically) two mutexes": separate the waiting producers from the waiting consumers so each operation notifies the other kind of thread.
The abstract spec keeps one waitSet. NotifyOther(Consumers) selects a waiting consumer after a put, and NotifyOther(Producers) selects a waiting producer after a get. There is no need to represent two separate wait sets at this level.
With a single condition, notifyAll() wakes up all waiters, including those that cannot proceed. Separate conditions for "buffer not full" and "buffer not empty" let us signal only the relevant group.
The upstream title describes the logical separation of waiters, not a recommendation to protect shared buffer updates with unrelated locks. Its later Java implementation uses one ReentrantLock and two Condition objects; its C implementation likewise uses one mutex and two condition variables. Both producers and consumers must still synchronize access to the shared buffer.
notifyAll(), at the cost of unnecessary wakeups.This is exactly the kind of bug that TLA+ excels at finding: subtle concurrency issues that only manifest in specific interleavings.
TLC completes without a deadlock or invariant violation for the supplied model. Try different positive capacities and nonempty producer/consumer sets.
Are we fully satisfied? As upstream v14 points out, finite runs alone cannot prove the fix for arbitrary parameters. The upstream tutorial continues with TLAPS proofs and, later, starvation and fairness. Those topics are beyond this shortened walkthrough.