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.
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
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(); } } }