We start with a simple counter that can be incremented and
decremented. We use the syntax of the above paper.
Counter : monitor
begin
value : int;
procedure increment(result number : int)
begin
value := value + 1;
number := value;
end
procedure decrement(result number : int)
begin
value := value - 1;
number := value;
end
value := 0;
end
Next, we implement a resource that can be acquired and released.
Resource : monitor
begin
available : boolean;
free : condition;
procedure acquire()
begin
if (not available) free.wait;
available := false;
end
procedure release()
begin
available := true;
free.signal;
end
available := true;
end
Note this is a binary semaphore. A general semaphore can
be implemented as follows.
Semaphore : monitor
begin
value : int;
free : condition;
procedure P()
begin
if (value == 0) free.wait;
value := value - 1;
end
procedure V()
begin
value := value + 1;
free.signal;
end
value := 0;
end
Let us now implement a bounded buffer of size N.
BoundedBuffer : monitor
begin
buffer : int[];
count : int; // number of items in the buffer
next : int; // index within the array where to store the next item
empty : condition;
full : condition;
procedure put(value : int)
begin
if (count == N) full.wait;
buffer[next] := value;
next := (next + 1) mod N;
count := count + 1;
empty.signal;
end
procedure get(result value : int)
begin
if (count == 0) empty.wait;
value := buffer[(current - count) mod N];
count := count - 1;
full.signal;
end
count := 0;
next := 0;
end
Let us solve the readers-writers problem where
ReadersAndWriters : monitor
begin
readers : int; // number of processes that (want to) read
writing : boolean; // is a process writing?
procedure startRead()
begin
readers := readers + 1;
if (writing) read.wait;
read.signal;
end
procedure stopRead()
begin
readers := readers - 1;
if (readers == 0) write.signal;
end
procedure startWrite()
begin
if (readers > 0 || writing) write.wait;
writing := true;
end
procedure stopWrite()
begin
writing := false;
read.signal;
if (readers == 0) write.signal;
end
readers := 0;
writing := false;
end
Finally, we address the dining philosophers problem.
Table : monitor
begin
fork : boolean[];
philosopher : condition[];
procedure getForks(int i)
begin
while (!fork[i] || !fork[(i + 1) mod N]) philosopher[i].wait;
fork[i] := false;
fork[(i + 1) mod N] := false;
end
procedure putForks(int i)
begin
fork[i] := true;
fork[(i + 1) mod N] := true;
philosopher[(i - 1) mod N].signal;
philosopher[(i + 1) mod N].signal;
end
fork[i] := true for i = 0, ..., N-1
end