Monitor Invariant - Buffer

Monitor Invariant - Buffer

A monitor invariant is an assertion which is true whenever no thread is executing in the monitor. It is permitted to be false while a a thread is executing but must be true when the thread leaves the monitor by method return or wait().

A suitable monitor invariant for Buffer which satisfies the safety properties is:

Buffer Invariant: [0 count size]

The count = 0 initialisation establishes the invariant.

synchronized public void put(Object o) {

// [0 count size]

while (count==size) { wait() }

// [0 count < size]


// [0< count size]

notify(); // [0


Previous slide Next slide Back to the first slide View Graphic Version