COSC6490A

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