Goal: resource schedulers -- group together procs that have to do with it

Monitor = local data + procedures called by resource acquirers/releasers

Monitor rules:
 - procedure bodies mutually exclusive among callers (at most one
   process can be active in the monitor at any given point in time)
 - monitor procedures cannot access non-local data; monitor-external
   procedures cannot access monitor-local data


Condition variable:
 - 2 operations: "wait" and "signal"
 - "signal" is followed immediately by resumption of a "wait"-ing process,
   with no intervening call from a third process
 - variable doesn't have a value; it's just an abstraction
 - unstated: cannot use pre-wait values after being signal-led
 - scheduled wait: specify priority, lowest priority woken up first


Implement semaphore w/ monitors
 - trivially

Implement monitor w/ semaphores

 - Outer synch: 1 mutex for entry/exit to/from monitor

 - Inner synch: 1 semaphore ("urgent") for mutual exclusion between
   waiting "about to be awoken" process and the signalling process --
   don't want to release mutex in order to prevent calls from
   occurring between signal and resumption; before exiting any
   procedure, check "urgent" before releasing mutex

 - Condition synch: 1 semaphore/condition ("condsem") to implement the
   condition variable

        wait:  condcount++
               if (urgentcount > 0) then V(urgent) else V(mutex)
               P(condsem)
               condcount--

      signal:  urgentcount++
               if (condcount > 0) then { V(condsem); P(urgent); }
               urgentcount--


Cool optimizations:
  - if signal is always last thing in a procedure, don't need 'urgent'
    and 'urgentcount'
  - if there are no recursive monitor calls, it's more efficient to
    put monitors in the kernel (non-interruptible mode)


Proof methods:

  I = invariant for monitor state
  B = resumption condition

  I       { wait   }  I && B
  I && B  { signal }  I


Examples:

  - bounded buffer
  - buffer allocation
  - disk head scheduler + elevator algorithm
  - readers and writers

Dynamic resource allocation: when resources are heavily loaded, fall
back to a more static regime.

Discuss p. 557: 1, 2, 5