// solution to monitor project
// burt rosenberg, oct 2010
// updated: oct 2011

// REMEMBER THIS IS PSEUDO-CODE!

semaphore lock_sema
semaphore wait_sema
integer wait_count

init:
	lock_sema unlocked (1)
	wait_sema locked (0)
	wait_count = 0 

enter: 
	assume: not holding lock_sema
	down on lock_sema

leave: 
	assume: holding lock_sema
	up on lock_sema

wait:
	assume: holding lock_sema
	// increment must be atomic
	wait_count++
	up on lock_sema
	// no critical race because wait_count 
	//    registers interest in waiting
	down on wait_sema
	// contend to reenter
	down on lock_sema
	
notify:
	assume: holding lock_sema
	// if and decrement must be atomic to be SMP safe
	if wait_count>0 
		wait_count--
		up on wait_sema
       	//*let waiting thread run
	//*up on lock_sema 
	//*down on lock_sema
	
notify_all:
	assume: holding lock_sema
	while wait_count>0
		wait_count--
		up on wait_sema
	//*up on lock_sema
	//*down on lock_sema
	
	

The wait_count++ and -- have to be done in a critical section 
to make the increment/decrement atomic.

Also, the check of the wait_count and the decrement have to be in 
the critical section to prevent two thread both finding wait_count positive
(but say equal to one) both doing the decrement (leaving wait_count negative).

I do place the wait_count++ under the lock so that there is not a race
between the decision to wait and the test by notify of wait_count of process
intending to wait

The lines marked //* were commented out to make this a Mesa style monitor