Производитель/потребитель Меса против семантики Хоара

Я столкнулся с двумя разными реализациями мониторов. Тот, который использует цикл while, который проверяет, верно ли определенное условие каждый раз перед сном и снова при пробуждении ото сна. Другой просто проверяет один раз, истинно ли условие if, и переходит в спящий режим, если это не так, но не проверяет снова при пробуждении. Я считаю, что первый использует семантику Мезы, а второй использует семантику Хоара. Как Википедия реализует проблему производителя-потребителя (http://en.wikipedia.org/wiki/Producer-consumer_problem#Using_monitors) использует семантику Mesa. Как бы мы достигли этого, используя Хоара?

Было бы что-то вроде этого?

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>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>0){
      signal(nextSem);
    }else{
      signal(mutex);
    }
  }

  cwait(sem x){
    x.cnt = x.cnt + 1;
    if(nextCount > 0)
      signal(nextSem);
    else
      signal(mutex);
    endif
    wait(x);
    x.cnt = x.cnt - 1;
  }

  csignal(sem x){
    if(x.cnt > 1){
      nextCount = nextCount + 1;
      signal(x);
      wait(nextSem);
      nextCount = nextCount -1;
    }
  }
}