프로듀서/소비자 Mesa vs Hoare 의미

Question

두 가지 다른 구현의 모니터가 있습니다. 잠을 자기 전에 매번 특정 조건이 true인지 여부를 확인하는 while 루프를 사용하고 잠에서 깨어 나면 다시 한 번 사용합니다. 다른 하나는 if 조건이 true인지 아닌지를 한 번 확인하고 깨지면 다시 확인하지 않습니다. 나는 전자가 Mesa 의미론을 사용하고 후자는 Hoare 의미론을 사용한다고 생각한다. Wikepedia가 생산자 소비자 문제 (http://en.wikipedia.org/wiki/Producer-consumer_problem#Using_monitors)를 구현하는 방식은 내가 믿는 메사 의미론을 사용하고 있습니다. 호아레를 사용하면 어떻게 될까요?

이렇게 될 수 있을까요? 이 입력하고 암시 적 작업을 모니터하는 떠나, 모니터이기 때문에

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 연산이 있으면이를 사용할 수 있습니다. 예를 들어, 자바, 내 monitor 패키지를 사용하여, 당신은

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

와 add을 끝낼 수 있었다 당신은

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

와 remove을 끝낼 수 있었다