Multiple Sleeping Barbers Problem


Description

It is the same as single sleeping barber problem except that it has multiple barbers. When a barber becomes free, the barber fetches one customer from the waiting room.


Diagram

The only differences from the single barber solution are

  1. Change the synchronization of cluster(R_B1,R_C2) from Barrier synchronization to Group (Barrier) with Information Exchange;
  2. Change the synchronization of cluster (R_B3,R_C4) and (R_B4,R_C5) form anonymous Relay synchronization to specific synchronization.


Synchronization Specification


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

Cluster: B1C2R1;
Regions: B11, C21;
Invariant: Bound(B11,1) + Bound(C21,1);

Cluster: B1C2R2;
Regions: B12, C22;
Invariant: Barrier(B12,C22);

Cluster: B1C2R3;
Regions: B13, C23;
Invariant: Barrier(B13,C23);

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))
    Every Group with information exchange is divided into three clusters.
  • For cluster B1C2R1 which consists of regions B11 and C21:
    ( In_B11 - Out_B11 <= 1) and (In_C21 - Out_C21 <= 1)
  • For cluster B1C2R2 which consists of regions B12 and C22:
    (Out_B12 <= In_C22) and (Out_C22 <= In_B12)
  • For cluster B1C2R3 which consists of regions B13 and C23:
    (Out_B13 <= In_C23) and (Out_C23 <= In_B13)

  • 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 B1C2R1 which consists of regions B11 and C21:
    (B1 <= 1) and (B2 <= 1)
  • For cluster B1C2R2 which consists of regions B12 and C22:
    (Ba1_1 <= 0) and (Ba1_2 <= 0)
  • For cluster B1C2R3 which consists of regions B13 and C23:
    (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

This requires specific synchronization which is an extension of the tool.

Unbounded Coarse-Grain Solution

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: B1C2R1
STATE SPACE VARIABLES: B11_in, B11_out, C21_in, C21_out;
REGION: B11
ENTER: <AWAIT B11_in == B11_out --> B11_in++;>
NOTIFY: ;
NOTIFYALL: ;
EXIT: <B11_out++;>
NOTIFY: B11_in;
NOTIFYALL: ;

REGION: C21
ENTER: <AWAIT C21_in == C21_out --> C21_in++;>
NOTIFY: ;
NOTIFYALL: ;
EXIT: <C21_out++;>
NOTIFY: C21_in;
NOTIFYALL: ;

CLUSTER: B1C2R2
STATE SPACE VARIABLES: B12_in, B12_out, C22_in, C22_out;
REGION: B12
ENTER: <B12_in++;>
NOTIFY: C22_out;
NOTIFYALL: ;
EXIT: <AWAIT B12_out + 1 <= C22_in --> B12_out++;>
NOTIFY: ;
NOTIFYALL: ;

REGION: C22
ENTER: <C22_in++;>
NOTIFY: B12_out;
NOTIFYALL: ;
EXIT: <AWAIT C22_out + 1 <= B12_in --> C22_out++;>
NOTIFY: ;
NOTIFYALL: ;

CLUSTER: B1C2R3
STATE SPACE VARIABLES: B13_in, B13_out, C23_in, C23_out;
REGION: B13
ENTER: <B13_in++;>
NOTIFY: C23_out;
NOTIFYALL: ;
EXIT: <AWAIT B13_out + 1 <= C23_in --> B13_out++;>
NOTIFY: ;
NOTIFYALL: ;

REGION: C23
ENTER: <C23_in++;>
NOTIFY: B13_out;
NOTIFYALL: ;
EXIT: <AWAIT C23_out + 1 <= B13_in --> C23_out++;>
NOTIFY: ;
NOTIFYALL: ;

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: 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: B1C2R1
STATE SPACE VARIABLES: B3, B4;
LOCAL VARIABLES: ;
REGION: B11
ENTER: <AWAIT B3 == 0 --> B3++;>
NOTIFY: ;
NOTIFYALL: ;
EXIT: <B3--;>
NOTIFY: B11_in;
NOTIFYALL: ;

REGION: C21
ENTER: <AWAIT B4 == 0 --> B4++;>
NOTIFY: ;
NOTIFYALL: ;
EXIT: <B4--;>
NOTIFY: C21_in;
NOTIFYALL: ;

CLUSTER: B1C2R2
STATE SPACE VARIABLES: Ba1_1, Ba1_2;
LOCAL VARIABLES: ;
REGION: B12
ENTER: <Ba1_2--;>
NOTIFY: C22_out;
NOTIFYALL: ;
EXIT: <AWAIT Ba1_1 <= -1 --> Ba1_1++;>
NOTIFY: ;
NOTIFYALL: ;

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

CLUSTER: B1C2R3
STATE SPACE VARIABLES: Ba2_1, Ba2_2;
LOCAL VARIABLES: ;
REGION: B13
ENTER: <Ba2_2--;>
NOTIFY: C23_out;
NOTIFYALL: ;
EXIT: <AWAIT Ba2_1 <= -1 --> Ba2_1++;>
NOTIFY: ;
NOTIFYALL: ;

REGION: C23
ENTER: <Ba2_1--;>
NOTIFY: B13_out;
NOTIFYALL: ;
EXIT: <AWAIT Ba2_2 <= -1 --> Ba2_2++;>
NOTIFY: ;
NOTIFYALL: ;

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

To be added.