Bounded-buffer Producer-Consumer Problem

1. Problem statement

A buffer of size N is shared by several processes. We are given sequential code

add_item -- adds an item to the buffer.
remove_item -- removes an item from the buffer.

We want functions Append(item) and Remove(item) such that the following hold:

Mutually exclusive access to buffer: At any time at most one process should be executing add_item or remove_item.
No buffer overflow: A process executes add_item only when the buffer is not full (i.e., the process waits if the buffer is full).
No buffer underflow: A process executes remove_item only when the buffer is not empty.
No busy waiting.
No producer starvation: A process does not wait forever at Append() provided the buffer repeatedly becomes non-full.
No producer starvation: A process does not wait forever at Remove() provided the buffer repeatedly becomes non-empty.

Note that conditions 1, 2, 3, and 4 are safety requirements (what a process should not do) and conditions 5 and 6 are progress requirements (what a process should eventually do).

2. Solution using Semaphores

The natural approach to this problem is to introduce an integer variable that keeps track of the number of items in the buffer, and then make processes wait on a semaphore if the condition is not right. This approach leads to a cumbersome solution. A more elegant approach results if we really make use of the power of semaphores.

Semaphore nItem initially 0;  // number of items in the buffer
Semaphore nSpace initially 0;  // number of spaces in the buffer
Semaphore mutex initially 1;  // protects add_item and remove_item

Append( item ) {
  P( nSpace );
  P( mutex );
  add_item;
  V( mutex );
  V( nItem );
}

Remove( item ) {
  P( nItem );
  P( mutex );
  remove_item;
  V( mutex );
  V( nSpace );
}

NOTE:

Note that nItem does not always indicate the number of items in the buffer. In particular, when a process is just after the P(nItem) in Remove, nItem is actually one less than the number of items in the buffer. In general, M processes can be just after the P(nItem) in Remove, in which case nItem is equal to the number of items minus M.
A similar comment applies to nSpace.
So can you come up with a more accurate comment for nItem and nSpace.
Obtain a proof that the above algorithm solves the producer-consumer problem, i.e., each of its possible executions satisfies the requirements given in the problem statement.