Bounded Buffer

var buffer : shared record
              pool: array [0..n-1] of item;
              count, in, out : integer;
             end;

in := 0; out := 0;

Producer:
region buffer when count < n do
   begin
      pool[in] := item; 
      in := (in + 1) mod n; count++;
   end;



Consumer:
region buffer when count > 0 do
   begin
      item := pool [out]; 
      out := (out + 1) mod n; count--;
   end

Readers and Writers (writer starvation)

Reader Entry

region mutex when nw = 0  do nr++;

Reader Exit

region mutex do nr--;

Writer Entry

region mutex when (nr=0 and nw=0) do nw++

Writer Exit

region mutex do nw--;

Reader-Writer (CORRECT)

Reader Entry             Writer Entry
region mutex do          region mutex do
   begin                   begin
    rwc++                   wwc++;
    await(wc=0 and          await(wc=0 & rc=0
      (turn=R or wwc=0))      &(turn=W or rwc=0))
    rwc--;                  wwc--;
    rc ++;                  wc++;
    if rwc=0 then          end;
        turn := W;
  end;

Reader Exit               Writer Exit
region mutex do            region mutex do
   rc--;                     begin
                               wc--;
                               turn := R;
                             end;

Dining Philosopher (No Deadlock, Yes Starvation)

Philosopher Pickup

region table 
   when chpstk[LEFT] and chpstk[RIGHT] do
   begin
     chpstk[LEFT] := false;
     chpstk[RIGHT] := false;
   end;


Philosopher Putdown

region table do
   begin
     chpstk[LEFT] := true;
     chpstk[RIGHT] := true;
   end;