ABSTRACT
This chapter implements enqueue/dequeue operations with a protocol that uses registers rather than semaphores to control the buffer’s accesses. These registers carry unbounded numbers in the first solution, and only N + 1 numbers in the second solution, where N is the number of buffer cells. The protocols described here are quite standard and similar protocols can be found in any textbook on operating systems. The higher-level events are enumerated, and each of the items of this lemma can be proved by induction on the index of the event in this enumeration. To coordinate the producers, a semaphore is used, and to execute an enqueue operation any producer has to pass a operation.
