Model Checking, Tla Plus, TLC, Java, Concurrency.
symmetric. Both methods are synchronized in order that their execution appear atomic to all threads. In particular, a thread cannot see intermediate states while the buffer is being modified by another thread. (This is also why the call to notify can take place before the buffer is actually