Sleeping Barber

• The barber sleeps in his chair when there are no customers. If a customer wakes him up, then he starts shaving him. Once he finishes, he proceeds with the next customer in the waiting room. If the waiting room is empty and no customer is remaining, the barber starts sleeping again in his chair.

• Each new customer enters the barber shop unshaved and, if the barber is sleeping, awakes him and sits in the barber chair to be shaved. Otherwise, if the barber is busy, the customer looks for a free chair in the sitting room taking his turn. If the sitting room is full, the customer simply leaves unattended.

We will introduce a slight variant in the problem and assume that any customer leaving the barbershop will take some arbitrary time and return at a given point (potentially) as many times as he likes.

Naive approach

The following file, barber0.pml, contains a first naive approach where someone has tried to program the behaviour described above in a completely straightforward manner. Several shared variables are used:

• The waiting room is a FIFO queue implemented as a circular buffer. To control the queue, two pointers are used: start points to the first element in the queue (if not empty) and end points to the first free position (if not full). A third variable, customers, keeps the number of elements in the queue. When the queue is empty, start==end and customers=0. When it is full, we also have start==end but customers==N.
  
• A variable sitting used to tell who is currently sitting at the barber chair. Each customer is numbered from 1 to C>=0 (the number of customers) and the BARBER is numbered with 0. The barber is sleeping when sitting==BARBER. There is no need to represent an empty chair.
• Finally, a boolean array shaved[i] reflects if person i has been shaved or not.
  

The file above starts with 4 customers and 2 seats in the waiting room. A simple execution of the code shows several anomalous situations and the execution normally ends up with an unexpected deadlock: remember that in this variant of the problem, the system should be running forever.

Exercise A: Force spin to obtain counterexamples of the following (safety) properties:

• The barber cannot be sleeping while there are customers waiting
• Any customer (take, for instance, 1) should never leave unattended while the barber is sleeping
  

To find short counterexamples, try reducing the number of seats and/or customers. In each case, explain the counterexample found and the cause of the wrong behaviour. Explain the reason for the deadlock too. Does it happen for any number N>=0 of seats in the waiting room?

Adapting the classical solution

The classical solution to the Sleeping Barber problem uses three semaphores:

1. A Boolean semaphore mutex used to protect the information about the waiting room (number of waiting customers, etc)
2. A Boolean semaphore ready used to point out that the barber is not busy
   
3. An integer semaphore counting the number of customers waiting, ready to be shaved

and a general variable freeseats that accounts for the number of free seats in the waiting room.

Exercise B: create a new version of the code above, barber1.pml, declaring the new Boolean semaphores and using the already existing variable customers as an integer semaphore. Adapt the classical solution of the Sleeping Barbers problem to the current implementation.

Exercise C: try again the previous properties in Exercise A, explaining their results. Additionally, try to check these properties:

• The barber can shave infinitely often
• If a customer enters the waiting room, he is eventually shaved
• A customer (say 1) can be shaved infinitely often. Try this query also with some values when C<N. Explain the difference.
  

Again, explain the answers and the counterexamples if those are found.