生產者/消費者梅薩vs霍爾語義

Question

我遇到了兩種不同的監視器實現。其中一種使用while循環來檢查特定條件在每次睡覺前是否爲真，以及從睡眠中醒來時是否爲真。另一個只檢查if條件是否爲真，如果不是，則在醒來時不再檢查。我相信前者使用Mesa語義，後者使用Hoare語義。 Wikepedia實現生產者消費者問題（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; 
    } 
    } 
} 

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