生产者/消费者 Mesa vs Hoare 语义答案

【问题标题】：Producer/consumer Mesa vs Hoare semantics生产者/消费者 Mesa vs Hoare 语义
【发布时间】：2013-03-10 16:33:32
【问题描述】：

我遇到了两种不同的监视器实现。一种使用 while 循环的方法，该循环在每次进入睡眠前检查特定条件是否为真，并在从睡眠中醒来时再次检查。另一个只检查一次 if 条件是否为真，如果不是，则进入睡眠状态，但在唤醒时不再检查。我相信前者使用 Mesa 语义，后者使用 Hoare 语义。我相信维基百科实现生产者消费者问题（http://en.wikipedia.org/wiki/Producer-consumer_problem#Using_monitors）的方式是使用 Mesa 语义。我们将如何使用 Hoare 来实现这一点？

会是这样吗？

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;
    }
  }
}

【问题讨论】：

标签： c synchronization producer-consumer monitors

【解决方案1】：

我会这样做

monitor ProducerConsumer{
    int BUFFERSIZE ; 
    int itemCount ; // invariant 0 _< itemCount and itemCount _< BUFFERSIZE
    condition notFull; // signalled only if itemCount < BUFFERSIZE
    condition notEmpty; // signalled only if itemCount > 0

    init(n){
        // Assumption. init is called once, before any call to add or remove.
        // precondition n >_ 1
        BUFFERZISE = n ;
        itemCount = 0;
    }

    void add(Item item){
        if(itemCount == BUFFER_SIZE){
            wait(notFull)
        }
        putItemIntoBuffer(item);
        itemCount = itemCount + 1;
        if( ! empty( notEmpty) ) signal(notEmpty);
    }

    Item consume(){
        if(itemCount == 0){
            wait( notEmpty );
        }
        Item item = removeItemFromBuffer();
        itemCount = itemCount - 1;
        if( ! empty(notFull) ) signal(notFull);
        return item ;
    }
}

我假设，因为这是一个监视器，所以进入和离开监视器是隐式操作。

注意，在信号之后，线程不需要等待。如果该语言有 signalAndLeave 操作，则可以使用。例如，在 Java 中，使用我的 monitor 包，您可以使用 add 结束

if( ! notEmpty.isEmpty() ) notEmpty.signalAndLeave( ) ; else leave() ;

你可以结束remove

if( ! notFull.isEmpty() ) return notFull.signalAndLeave(item) else { leave() ; return item ; }

【讨论】：