We make two assumptions:
- A signaler must exit immediately after signaling on a condition variable by executing a return statement.
- Signaled thread has priority inside the monitor over any thread waiting to enter the monitor through a service method call (barging is not possible)
These two assumptions make sure that the condition variable whose becoming true caused our signaler to signal does not have an opportunity to change after the signaler signals but before the signaled thread can enter the thread.
These two assumptions mean that we can use Hoare semantics (yes, a somewhat unfortunate name). Remember that our assumptions are purely a mind exercise and NOT valid in Java. From the same OSTEP book in section D.3, we have:
They were well-known systems researchers, and they soon found that Hoare semantics, while more amenable to proofs, were hard to realize in a real system (there are a lot of reasons for this, perhaps too many to go through here).
