ABSTRACT
This chapter explains and specifies the Producer/Consumer problem. It discusses semaphores and shows the equivalence between two specifications. The chapter proves the correctness of the Dijkstra Producer/Consumer protocol. In general, the operations of producing an item and consuming it are of variable and unequal lengths. A policy of strict coordination in which the producer waits until the consumer is ready for the next item and then directly transfers it to the consumer may slow down the system to an unacceptable degree. A buffer is therefore useful here, using storage space to save time. A buffer consists of a finite array of buffer cells, each carrying an item. The producer loads these cells and the consumer unloads them. The simpler protocols use a single cell for buffering. More complex protocols employ an array of buffer cells, which has the advantage of allowing the producer and consumer to approach different buffer cells simultaneously.
