Monitor Examples


Mutual Exclusion

Mutual Exclusion provides exclusive access to a shared resource.


Synchronization

Synchronization provides a timing relationship among threads.

Bounded Buffer

Concurrent bounded-buffer blocks producers when buffer full, consumers when buffer empty, and handles multiple producers/consumers inserting/removing simultaneously.

#include <thread>										// condition
monitor Buffer {
	condition full, empty;
	int front, back, count;
	int elements[20];
};
void ?{}( Buffer & buffer ) with( buffer ) { front = back = count = 0; }
int query( Buffer & buffer ) { return buffer.count; }  // read-only, no mutual exclusion

void insert( Buffer & mutex buffer, int elem ) with( buffer ) {
	if ( count == 20 ) wait( empty );
	elements[back] = elem;
	back = ( back + 1 ) % 20;
	count += 1;
	signal( full );
}
int remove( Buffer & mutex buffer ) with( buffer ) {
	if ( count == 0 ) wait( full );
	int elem = elements[front];
	front = ( front + 1 ) % 20;
	count -= 1;
	signal( empty );
	return elem;
}

Dating Service

Girl/boy threads with matching compatibility codes exchange phone numbers.

#include <thread>                    // condition
enum { NoOfPairs = 20 };

monitor DatingService {
	condition Girls[NoOfPairs], Boys[NoOfPairs];
	unsigned int GirlPhoneNo, BoyPhoneNo;
};
unsigned int girl( DatingService & mutex ds, unsigned int PhoneNo, unsigned int ccode ) with( ds ) {
	if ( is_empty( Boys[ccode] ) ) {                    // no compatible boy ?
		wait( Girls[ccode] );                            // wait for boy
		GirlPhoneNo = PhoneNo;                            // make phone number available
	} else {
		GirlPhoneNo = PhoneNo;                            // make phone number available
		signal_block( Boys[ccode] );                    // restart boy to set phone number
	}
	return BoyPhoneNo;
}
unsigned int boy( DatingService & mutex ds, unsigned int PhoneNo, unsigned int ccode ) with( ds ) {
	if ( is_empty( Girls[ccode] ) ) {                    // no compatible girl ?
		wait( Boys[ccode] );                            // wait for girl
		BoyPhoneNo = PhoneNo;                            // make phone number available
	} else {
		BoyPhoneNo = PhoneNo;                            // make phone number available
		signal_block( Girls[ccode] );                    // restart girl to set phone number
	}
	return GirlPhoneNo;
}