title: Producer/consumer Mesa vs Hoare semantics
body: <p>I have come across two different implementations of monitors. One which uses a while loop that checks whether a particular condition is true each time before going to sleep and again when waking up from the sleep. The other just checks once whether the if condition is true and goes to sleep if it isn't but doesn't check again when woken up. I believe the former uses Mesa semantics and the latter uses Hoare semantics. The way Wikepedia implements the producer consumer problem (<a href="http://en.wikipedia.org/wiki/Producer-consumer_problem#Using_monitors" rel="nofollow">http://en.wikipedia.org/wiki/Producer-consumer_problem#Using_monitors</a>) is using Mesa semantics I believe. How would we accomplish this using Hoare?</p>
  
  <p>Would it be something like this?</p>
  
  <pre><code>monitor ProducerConsumer{
    int itemCount;
    int nextCount;
    condition full;
    condition empty;
    condition nextSem;
  
    init(n){
      itemCount = n;
    }
  
    void add(item){
      wait(mutex);
      if(itemCount == BUFFER_SIZE){
        cwait(full)
      }
      putItemIntoBuffer(item);
      itemCount = itemCount + 1;
      if(itemCount == 1){
        csignal(empty);
      }
  
      //To give priority to threads already in the monitor over
      //"normal" threads that want to enter the monitor for the 
      //first time.
      if(nextCount&gt;0){
        signal(nextSem);
      }else{
        signal(mutex);
      }
    }
  
    void consume(){
      wait(mutex);
      if(itemCount == 0){
        cwait(empty);
      }
      item = removeItemFromBuffer();
      itemCount = itemCount - 1;
      if(itemcount == BUFFER_SIZE - 1 ){
        csignal(full);
      }
  
      //To give priority to threads already in the monitor over
      //"normal" threads that want to enter the monitor for the 
      //first time.
      if(nextCount&gt;0){
        signal(nextSem);
      }else{
        signal(mutex);
      }
    }
  
    cwait(sem x){
      x.cnt = x.cnt + 1;
      if(nextCount &gt; 0)
        signal(nextSem);
      else
        signal(mutex);
      endif
      wait(x);
      x.cnt = x.cnt - 1;
    }
  
    csignal(sem x){
      if(x.cnt &gt; 1){
        nextCount = nextCount + 1;
        signal(x);
        wait(nextSem);
        nextCount = nextCount -1;
      }
    }
  }
  </code></pre>