Продюсер/потребитель Mesa vs Hoare semantics

Question

Я столкнулся с двумя различными реализациями мониторов. Тот, который использует цикл while, который проверяет, является ли конкретное условие истинным каждый раз перед сном и снова при пробуждении от сна. Другой только один раз проверяет, является ли условие if истинным и переходит в спящий режим, если это не так, но не проверяется снова при пробуждении. Я считаю, что первая использует семантику Меса, а вторая использует семантику Хоар. То, как Wikepedia реализует проблему потребительского потребления (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; 
    } 
    } 
} 

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