Hungry Birds Problem


Description

Given are N baby birds and one parent bird. The baby birds eat out of a common dish that initially contains F portions of food. Each baby repeatedly eats one portion of food at a time, sleeps for a while, and then comes back to eat. When the dish becomes empty, the baby bird who empties the dish awakens the parent bird, which finds F portions of food and puts them in the dish.

Diagram

We assume that the dish is divided into F slots, each of which holds one portion of food.

The scenario for the parent bird is:

  • P1 finds F portions of food
  • P2 waits until the dish becomes empty, and then {assertion: the dish is empty} places the F food portions in the dish.

The scenario for a baby bird is:

  • B1 sleeps for a while
  • B2 waits until the dish has at least one portion of food, and the {assertion: a food portion is in the dish} pick up a portion.
  • B3 eats the portion.

Steps P2 and B2 constitute synchronization regions, R_P2 and R_B2, forming cluster (R_P2,R_B2). The synchronization specification of the cluster is essentially a producers/consumers problem. If we focus on food portions to be resources, R_P2 is the producer region and R_B2 is the consumer region. Therefore, Resource(R_P2,F,R_B2,1,F) must hold. If we focus on empty slots in the dish to be resources, R_B2 is the producer region and R_P2 is the consumer region and Resource(R_B2,1,R_F2,F,0) must hold. Only one baby bird at a time may access the food and notify the parent bird of a empty dish. To realize this, we use a separate cluster with the Bound pattern.

hungry birds diagram

Synchronization Specification


Cluster: P2B2 ;
Regions: P2, B2;
Invariant: Resource(P2,5,B2,1,5) + Resource(B2,1,P2,5,0);

Cluster: CR;
Regions: R;
Invariant: Bound(R,1);

Patterns Used

Resource and Bound

Global Invariant

Unbounded Global Invariant

  • For cluster R which consists of regions R:
    (In_R - Out_R <=1)
  • For cluster P2B2 which consists of regions P2 and B2:
    (In_B2 <= Out_P2*F+F) and (In_P2*F <= Out_B2)
  • Bounded Global Invariant Counter Version

  • For cluster R which consists of regions R:
    (B_R <=1)
  • For cluster P2B2 which consists of regions P2 and B2:
    (R_pc1 <= F) and (R_pc2 <= 0)

  • Core Functional Code

    class Birds
    
    {
        public static void main ( String argv [ ] )
    
        {
            new BabyBird ( ) . start ( ) ;
    
            new BabyBird ( ) . start ( ) ;
    
            new BabyBird ( ) . start ( ) ;
    
            new ParentBird ( ) . start ( ) ;
    
        }
    }
    
    final class BabyBird extends Thread
    
    {
        public void run ( )
        {
            while ( true )
    
            {
                /*** CR R enter ***/
                System . out . println ( "baby bird is ready to eat :" ) ;
    
                /*** P2B2 B2 enter ***/
                System . out . println ( "baby bird waits until the dish has at least one portion of food :" ) ;
    
                System . out . println ( "baby bird picks up food :" ) ;
    
                /*** P2B2 B2 exit ***/
                System . out . println ( "baby bird has done eating" ) ;
    
                /*** CR R exit ***/
            }
        }
    }
    
    final class ParentBird extends Thread
    
    {
        public void run ( )
        {
            while ( true )
    
            {
                /*** P2B2 P2 enter ***/
                System . out . println ( "parent bird waits until the dish becomes empty" ) ;
    
                System . out . println ( "parent bird places the F food portions in the dish" ) ;
    
                /*** P2B2 P2 exit ***/
            }
        }
    }
    

    Unbounded Coarse-Grain Solution

    CLUSTER: P2B2
    STATE SPACE VARIABLES: B2_in, P2_out, P2_in, B2_out;
    REGION: P2
    ENTER: <AWAIT P2_in * 5 + 5 <= B2_out --> P2_in++;>
    NOTIFY: ;
    NOTIFYALL: ;
    EXIT: <P2_out++;>
    NOTIFY: ;
    NOTIFYALL: B2_in;

    REGION: B2
    ENTER: <AWAIT B2_in + 1 <= P2_out * 5 + 5 --> B2_in++;>
    NOTIFY: ;
    NOTIFYALL: ;
    EXIT: <B2_out++;>
    NOTIFY: P2_in;
    NOTIFYALL: ;

    CLUSTER: CR
    STATE SPACE VARIABLES: R_in, R_out;
    REGION: R
    ENTER: <AWAIT R_in == R_out --> R_in++;>
    NOTIFY: ;
    NOTIFYALL: ;
    EXIT: <R_out++;>
    NOTIFY: R_in;
    NOTIFYALL: ;

    Bounded Counter Coarse-Grain Solution

    CLUSTER: P2B2
    STATE SPACE VARIABLES: R1_pc, R2_pc;
    LOCAL VARIABLES: ;
    REGION: P2
    ENTER: <AWAIT R2_pc <= -5 --> R2_pc+=5;>
    NOTIFY: ;
    NOTIFYALL: ;
    EXIT: <R1_pc-=5;>
    NOTIFY: ;
    NOTIFYALL: B2_in;

    REGION: B2
    ENTER: <AWAIT R1_pc <= 4 --> R1_pc+=1;>
    NOTIFY: ;
    NOTIFYALL: ;
    EXIT: <R2_pc-=1;>
    NOTIFY: P2_in;
    NOTIFYALL: ;

    CLUSTER: CR
    STATE SPACE VARIABLES: B1;
    LOCAL VARIABLES: ;
    REGION: R
    ENTER: <AWAIT B1 == 0 --> B1++;>
    NOTIFY: ;
    NOTIFYALL: ;
    EXIT: <B1--;>
    NOTIFY: R_in;
    NOTIFYALL: ;

    Unbounded Fine-Grain Solution

    class SGCluster$CR {
    // STATE SPACE VARIABLES: 
    private static int R_in , R_out ;
    
    // LOCAL VARIABLES: 
    
    private static Object clusterCounterLock = new Object();
    
    
    /**======================================================**
     **
     ** Generated lock and methods for await: R$enter
     **
     **======================================================**/
    
    private static Object condition$R$enter = new Object();
    
    public static void R$enter(){
       synchronized (condition$R$enter) {
    
          while ( !check$R$enter())
             try {
    
                condition$R$enter.wait();
             } catch (InterruptedException e){}
    
       }
    
    }
    private static boolean check$R$enter() {
    
       synchronized (clusterCounterLock) {
          if (R_in == R_out ) {
    
             R_in ++ ; 
             return true;
          } else
    
             return false;
       }
    }
    /**======================================================**
     **
     ** Generated lock and methods for atomic: R$exit
     **
     **======================================================**/
    
    public static void R$exit() {
    
       synchronized (clusterCounterLock) {
          R_out ++ ; 
       }
    
       synchronized (condition$R$enter) {
          condition$R$enter.notify(); 
       }
    
    
    }
    
    }
    
    
    class SGCluster$P2B2 {
    
    // STATE SPACE VARIABLES: 
    private static int B2_in , P2_out , P2_in , B2_out ;
    
    // LOCAL VARIABLES: 
    
    private static Object clusterCounterLock = new Object();
    
    
    /**======================================================**
     **
     ** Generated lock and methods for await: P2$enter
     **
     **======================================================**/
    
    private static Object condition$P2$enter = new Object();
    
    public static void P2$enter(){
       synchronized (condition$P2$enter) {
    
          while ( !check$P2$enter())
             try {
    
                condition$P2$enter.wait();
             } catch (InterruptedException e){}
    
       }
    
    }
    private static boolean check$P2$enter() {
    
       synchronized (clusterCounterLock) {
          if (P2_in * 5 + 5 <= B2_out ) {
    
             P2_in ++ ; 
             return true;
          } else
    
             return false;
       }
    }
    /**======================================================**
     **
     ** Generated lock and methods for atomic: P2$exit
     **
     **======================================================**/
    
    public static void P2$exit() {
    
       synchronized (clusterCounterLock) {
          P2_out ++ ; 
       }
    
       synchronized (condition$B2$enter) {
          condition$B2$enter.notifyAll(); 
       }
    
    
    }
    
    
    /**======================================================**
     **
     ** Generated lock and methods for await: B2$enter
     **
     **======================================================**/
    
    private static Object condition$B2$enter = new Object();
    
    public static void B2$enter(){
       synchronized (condition$B2$enter) {
    
          while ( !check$B2$enter())
             try {
    
                condition$B2$enter.wait();
             } catch (InterruptedException e){}
    
       }
    
    }
    private static boolean check$B2$enter() {
    
       synchronized (clusterCounterLock) {
          if (B2_in + 1 <= P2_out * 5 + 5 ) {
    
             B2_in ++ ; 
             return true;
          } else
    
             return false;
       }
    }
    /**======================================================**
     **
     ** Generated lock and methods for atomic: B2$exit
     **
     **======================================================**/
    
    public static void B2$exit() {
    
       synchronized (clusterCounterLock) {
          B2_out ++ ; 
       }
    
       synchronized (condition$P2$enter) {
          condition$P2$enter.notify(); 
       }
    
    
    }
    
    }
    
    

    Bounded Fine-Grain Solution

    class SGCluster$CR {
    
    // STATE SPACE VARIABLES: 
    private static int B1 ;
    // LOCAL VARIABLES: 
    
    private static Object clusterCounterLock = new Object();
    
    
    /**======================================================**
     **
     ** Generated lock and methods for await: R$enter
     **
     **======================================================**/
    
    private static Object condition$R$enter = new Object();
    
    public static void R$enter(){
       synchronized (condition$R$enter) {
    
          while ( !check$R$enter())
             try {
    
                condition$R$enter.wait();
             } catch (InterruptedException e){}
    
       }
    
    }
    private static boolean check$R$enter() {
    
       synchronized (clusterCounterLock) {
          if (B1 == 0 ) {
    
             B1 ++ ; 
             return true;
          } else
    
             return false;
       }
    }
    /**======================================================**
     **
     ** Generated lock and methods for atomic: R$exit
     **
     **======================================================**/
    
    public static void R$exit() {
    
       synchronized (clusterCounterLock) {
          B1 -- ; 
       }
    
       synchronized (condition$R$enter) {
          condition$R$enter.notify(); 
       }
    
    
    }
    
    }
    
    
    class SGCluster$P2B2 {
    
    // STATE SPACE VARIABLES: 
    private static int R1_pc , R2_pc ;
    // LOCAL VARIABLES: 
    
    private static Object clusterCounterLock = new Object();
    
    
    /**======================================================**
     **
     ** Generated lock and methods for await: P2$enter
     **
     **======================================================**/
    
    private static Object condition$P2$enter = new Object();
    
    public static void P2$enter(){
       synchronized (condition$P2$enter) {
    
          while ( !check$P2$enter())
             try {
    
                condition$P2$enter.wait();
             } catch (InterruptedException e){}
    
       }
    
    }
    private static boolean check$P2$enter() {
    
       synchronized (clusterCounterLock) {
          if (R2_pc <= -5 ) {
    
             R2_pc += 5 ; 
             return true;
          } else
    
             return false;
       }
    }
    /**======================================================**
     **
     ** Generated lock and methods for atomic: P2$exit
     **
     **======================================================**/
    
    public static void P2$exit() {
    
       synchronized (clusterCounterLock) {
          R1_pc -= 5 ; 
       }
    
       synchronized (condition$B2$enter) {
          condition$B2$enter.notifyAll(); 
       }
    
    
    }
    
    
    /**======================================================**
     **
     ** Generated lock and methods for await: B2$enter
     **
     **======================================================**/
    
    private static Object condition$B2$enter = new Object();
    
    public static void B2$enter(){
       synchronized (condition$B2$enter) {
    
          while ( !check$B2$enter())
             try {
    
                condition$B2$enter.wait();
             } catch (InterruptedException e){}
    
       }
    
    }
    private static boolean check$B2$enter() {
    
       synchronized (clusterCounterLock) {
          if (R1_pc <= 4 ) {
    
             R1_pc += 1 ; 
             return true;
          } else
    
             return false;
       }
    }
    /**======================================================**
     **
     ** Generated lock and methods for atomic: B2$exit
     **
     **======================================================**/
    
    public static void B2$exit() {
    
       synchronized (clusterCounterLock) {
          R2_pc -= 1 ; 
       }
    
       synchronized (condition$P2$enter) {
          condition$P2$enter.notify(); 
       }
    
    
    }
    
    }