Single Sleeping Barber Problem


Description

The shop has a barber, a barber chair, and a waiting room with several chairs. When a barber finishes cutting a customer's hair, the barber fetches another customer from the waiting room if there is a customer, or stands by the barber chair and daydreams if the waiting room is empty. A customer who needs a haircut enters the waiting room. If the waiting room is full, the customer comes back later. If the barber is busy but there is a waiting room chair available, the customer takes a seat. If the waiting room is empty and the barber is daydreaming, the customer sits in the barber chair and wakes the barber up.


Diagram

In a solution, we define two types threads: a barber thread and customer threads. Let integer variable numCustomers keep track of the number of customers in the waiting room. A scenario (sequential behavior) of the barber thread is (i.e., it repeats the following):

  • B1 {assertion: no customer is in the barber room} waits until a customer is in the waiting room;
  • B2 {assertion: met a customer} starts cutting the customer's hair;
  • B3 finishes the hair cut and informs the customer;
  • B4 waits until the customer leaves the barber room.
A scenario for the customer thread is (i.e., it repeats the following):
  • C1 checks if the waiting room is full (numCustomers == N), if so, leaves, else enters the waiting room (increment numCustomers by one);
  • C2 waits until the barber becomes free;
  • C3 {assertion: met the barber} leaves the waiting room (decrement numCustomers by one) and enters the barber room;
  • C4 waits until the barber finishes the hair cut ;
  • C5 {assertion: hair cut is done} leaves the barber room.
Steps B1, B3, and B4 in the barber's scenario constitute synchronization regions denoted R_B1, R_B3, and R_B4, respectively. Steps C2, C4, and C5 in the customers' scenario constitute synchronization regions, R_C2, R_C4, and R_C5, respectively. Three clusters are formed based on the reference relations: (R_B1, R_C2), (R_B3, R_C4), and (R_B4, R_C5). Cluster (R_B1, R_C2) forms barrier (R_1, R_2). Clusters (R_B3, R_C4) and (R_B4, R_C5) form Relay(R_B3, R_C4) and Relay(R_C5, R_B4).

It might be wondered why we do not combine steps B3 and B4 into one step, say B34, and steps C4 and C5 into another step, C45, to form a cluster with Barrier(R_B34, R_C45). This is because mutual exclusion is not guaranteed in regions in the Barrier synchronization. Therefore, there could be a situation in which a customer thread enters region R_C45 in the Barrier cluster (note that this releases the barber thread from region R_B34) and suddenly becomes slow. Suppose the barber thread immediately goes back to the beginning of the loop and meets the next customer thread in cluster (R_B1, R_C2). Then, the next customer thread may reach and immediately leave region R_C45 (which was already triggered by the barber thread in the previous iteration) before the first thread. One way to solve this problem is to use handshaking synchronization using two Relay clusters as shown in our solution. Another approach is to specify the cluster to be Bound(R_C45, 1) and Barrier(R_B34, R_C45).


Synchronization Specification


Cluster: B1C2;
Regions: B1, C2;
Invariant: Barrier(B1,C2);

Cluster: C1C3;
Regions: C1,C3;
Invariant: Bound(C1,1)+Bound(C3,1)+Exclusion(C1,C3);

Cluster: B3C4;
Regions: B3, C4;
Invariant: Relay(B3,C4);

Cluster: B4C5;
Regions: B4, C5;
Invariant: Relay(C5,B4);

Patterns Used

Exclusion, Bound, Barrier, and Relay.

Global Invariant

Unbounded Global Invariant

  • For cluster C1C3 which consists of regions C1 and C3:
    (In_C1 - Out_C1 <=1) and (In_C3 - Out_C3 <= 1) and ((In_C1 - Out_C1 ==0) or (In_C3 - Out_C3 == 0))
  • For cluster B1C2 which consists of regions B1 and C2:
    (Out_B1 <= In_C2) and (Out_C2 <= In_B1)
  • For cluster B3C4 which consists of regions B3 and C4:
    Out_C4 <= In_B3
  • For cluster B4C5 which consists of regions B4 and C5:
    Out_B4 <= In_C

Bounded Global Invariant Counter Version

  • For cluster C1C3 which consists of regions C1 and C3:
    (B1 <= 1) and (B2 <= 1) and ((E1_0 ==0) or (E1_1 == 0))
  • For cluster B1C2 which consists of regions B1 and C2:
    (Ba1_1 <= 0) and (Ba1_2 <= 0)
  • For cluster B3C4 which consists of regions B3 and C4:
    Re1 <= 0
  • For cluster B4C5 which consists of regions B4 and C5:
    Re2 <= 0

Core Functional Code

class Barber extends Thread {

    int times;
    Barber(int times) {
        this.times = times;

    }
    public void run() {
        while(times>0) {

            // R_B1
            /*** B1C2 B1 enter ***/
            System.out.println("Barber wait a customer");

            /*** B1C2 B1 exit ***/
            System.out.println("Barber has a customer");
            //R_B2

            System.out.println("Barber starts to cut the customer's hair");
            //R_B3
            /*** B3C4 B3 enter ***/

            System.out.println("Barber finished the hair cut");
            /*** B3C4 B3 exit ***/
            System.out.println("Barber informed the hair cut");

            //R_B4
            /*** B4C5 B4 enter ***/
            System.out.println("Barber wait the customer to leave");

            /*** B4C5 B4 exit ***/
            System.out.println("Barber: the customer to leave");
            times--;

        }
    }
}

class Customer extends Thread {

    private int id;
    Customer (int id) {

        this.id = id;
    }
    public void run() {

        //R_C1
        /*** C1C3 C1 enter ***/
        System.out.println("Customer "+id+"checks the waiting room");

        if(BarberShop.numCustomers == BarberShop.numChairs) {

            /*** C1C3 C1 exit ***/
            System.out.println("Customer "+id+"finds out the waiting room is full and leave");

            return;
        }
        else{
            /*** C1C3 C1 exit ***/
            BarberShop.numCustomers++;

            System.out.println("Customer "+id+" enters the waiting room");
            //R_C2

            /*** B1C2 C2 enter ***/
            System.out.println("Customer "+id+" wait the Barber become free");

            /*** B1C2 C2 exit ***/
            System.out.println("Customer "+id+" Barber is free");

            //R_C3
            /*** C1C3 C3 enter ***/
            BarberShop.numCustomers--;
            System.out.println("Customer "+id+" met the Barber");

            /*** C1C3 C3 exit ***/
            System.out.println("Customer "+id+" leaves the waiting room");

            //R_C4
            /*** B3C4 C4 enter ***/
            System.out.println("Customer "+id+" wait hair cut is done");

            /*** B3C4 C4 exit ***/
            System.out.println("Customer "+id+" hair cut is done");

            //R_C5
            /*** B4C5 C5 enter ***/
            System.out.println("Customer "+id+" starts to leave");

            /*** B4C5 C5 exit ***/
            System.out.println("Customer "+id+" leaved");

        }
    }
}

public class BarberShop {

    public static int numCustomers =0;
    public static int numChairs = 5;

    public static void main(String[] arg) {

        Barber barber = new Barber(3);
        Customer customer1 = new Customer(1);

        Customer customer2 = new Customer(2);
        Customer customer3 = new Customer(3);

        barber.start();
        customer1.start();
        customer2.start();

        customer3.start();
    }
}

Unbounded Coarse-Grain Solution

CLUSTER: B1C2
STATE SPACE VARIABLES: B1_in, B1_out, C2_in, C2_out;
REGION: B1
ENTER: <B1_in++;>
NOTIFY: C2_out;
NOTIFYALL: ;
EXIT: <AWAIT B1_out + 1 <= C2_in --> B1_out++;>
NOTIFY: ;
NOTIFYALL: ;

REGION: C2
ENTER: <C2_in++;>
NOTIFY: B1_out;
NOTIFYALL: ;
EXIT: <AWAIT C2_out + 1 <= B1_in --> C2_out++;>
NOTIFY: ;
NOTIFYALL: ;

CLUSTER: C1C3
STATE SPACE VARIABLES: C1_in, C1_out, C3_in, C3_out;
REGION: C1
ENTER: <AWAIT C1_in == C1_out && C3_in == C3_out --> C1_in++;>
NOTIFY: ;
NOTIFYALL: ;
EXIT: <C1_out++;>
NOTIFY: C1_in;
NOTIFYALL: C3_in;

REGION: C3
ENTER: <AWAIT C3_in == C3_out && C1_in == C1_out --> C3_in++;>
NOTIFY: ;
NOTIFYALL: ;
EXIT: <C3_out++;>
NOTIFY: C3_in;
NOTIFYALL: C1_in;

CLUSTER: B3C4
STATE SPACE VARIABLES: B3_in, C4_out;
REGION: B3
ENTER: <B3_in++;>
NOTIFY: C4_out;
NOTIFYALL: ;
EXIT: <>
NOTIFY: ;
NOTIFYALL: ;

REGION: C4
ENTER: <>
NOTIFY: ;
NOTIFYALL: ;
EXIT: <AWAIT C4_out + 1 <= B3_in --> C4_out++;>
NOTIFY: ;
NOTIFYALL: ;

CLUSTER: B4C5
STATE SPACE VARIABLES: C5_in, B4_out;
REGION: B4
ENTER: <>
NOTIFY: ;
NOTIFYALL: ;
EXIT: <AWAIT B4_out + 1 <= C5_in --> B4_out++;>
NOTIFY: ;
NOTIFYALL: ;

REGION: C5
ENTER: <C5_in++;>
NOTIFY: B4_out;
NOTIFYALL: ;
EXIT: <>
NOTIFY: ;
NOTIFYALL: ;

Bounded Counter Coarse-Grain Solution

CLUSTER: B1C2
STATE SPACE VARIABLES: Ba1_1, Ba1_2;
LOCAL VARIABLES: ;
REGION: B1
ENTER: <Ba1_2--;>
NOTIFY: C2_out;
NOTIFYALL: ;
EXIT: <AWAIT Ba1_1 <= -1 --> Ba1_1++;>
NOTIFY: ;
NOTIFYALL: ;

REGION: C2
ENTER: <Ba1_1--;>
NOTIFY: B1_out;
NOTIFYALL: ;
EXIT: <AWAIT Ba1_2 <= -1 --> Ba1_2++;>
NOTIFY: ;
NOTIFYALL: ;

CLUSTER: C1C3
STATE SPACE VARIABLES: B1, B2, E1_0, E1_1; LOCAL VARIABLES: ;
REGION: C1
ENTER: <AWAIT B1 == 0 && E1_1 == 0 --> B1++;E1_0++;> NOTIFY: ;
NOTIFYALL: ;
EXIT: <B1--;E1_0--;>
NOTIFY: C1_in;
NOTIFYALL: C3_in;

REGION: C3
ENTER: <AWAIT B2 == 0 && E1_0 == 0 --> B2++;E1_1++;>
NOTIFY: ;
NOTIFYALL: ;
EXIT: <B2--;E1_1--;>
NOTIFY: C3_in;
NOTIFYALL: C1_in;

CLUSTER: B3C4
STATE SPACE VARIABLES: Re1;
LOCAL VARIABLES: ;
REGION: B3
ENTER: <Re1--;>
NOTIFY: C4_out;
NOTIFYALL: ;
EXIT: <>
NOTIFY: ;
NOTIFYALL: ;

REGION: C4
ENTER: <>
NOTIFY: ;
NOTIFYALL: ;
EXIT: <AWAIT Re1 <= -1 --> Re1++;>
NOTIFY: ;
NOTIFYALL: ;

CLUSTER: B4C5
STATE SPACE VARIABLES: Re2;
LOCAL VARIABLES: ;
REGION: B4
ENTER: <>
NOTIFY: ;
NOTIFYALL: ;
EXIT: <AWAIT Re2 <= -1 --> Re2++;>
NOTIFY: ;
NOTIFYALL: ;

REGION: C5
ENTER: <Re2--;>
NOTIFY: B4_out;
NOTIFYALL: ;
EXIT: <>
NOTIFY: ;
NOTIFYALL: ;

 

Unbounded and Bounded Fine-Grain Solutions