Question: Assuming Hansen semantics for condition variables, our implementation of the blocking bounded queue in Figure does not guarantee freedom from starvation: if a continuous stream of threads makes insert() (or remove()) calls, it is possible for a waiting thread to wait forever. For example, a thread may call insert() and wait in the while(isFull()) loop; then, every time another thread calls remove() and signals on the itemRemoved condition variable, a different thread might call insert(), see that the queue is not full, and insert an item before the waiting thread resumes. Then, when the waiting thread resumes, it will retest the isFull() predicate, see that the queue is full, and wait(). Prove that under Hoare semantics and assuming that when a signal occurs, it is the longest-waiting thread that is resumed, our implementation of BBQ ensures freedom from starvation. That is, that if a thread waits in insert(), then it is guaranteed to proceed after a bounded number of remove() calls complete, and vice versa.
