Gyroscope Rudder Problem


Description

Gyroscope produces position values which are placed in a single entry buffer. Rudder controller reads position values from the buffer and uses them to actuate the rudder.

Diagram

In a solution, we define two types threads; a gyroscope controller thread and rudder threads. A scenario (sequential behavior) of the gyroscope controller thread is (i.e., it repeats the following):

  • G1 reads a value from the gyroscope
  • G2 waits until the buffer becomes empty, writes a new value in the buffer.
A scenario for the rudder thread is (i.e., it repeats the following):
  • R1 waits until gyroscope value is in buffer, reads value from buffer.
  • R2 actuates rudder based on value.
Step G1 in the gyroscope controller's scenario constitutes synchronization region denoted R_G1. Step R1 in the rudder' scenario constitutes synchronization region, R_R1. If we focus on the buffer with value to be resources, R_G1 is the producer region and R_R1 is the consumer region. Therefore, Resource(R_G1,1,R_R1,1,0 ) must hold. If we focus on empty buffer to be resources, R_R1 is the producer region and R_G1 is the consumer region and Resource(R_R1,1,R_G1,1,1) must hold. Also gyroscope and rudder can not access the buffer at same time. We have exclusion(R_R1,R_G1).

gyroscope rudder 
	diagram

Synchronization Specification


Cluster: GyroRudder;
Regions: Gyroscope, Rudder;
Invariant: Resource(Rudder,1,Gyroscope,1,1) + Resource(Gyroscope,1,Rudder,1,0) +Exclusion(Gyroscope,Rudder);

Patterns Used

Exclusion and Resource

Global Invariant

Unbounded Global Invariant

(In_R1 <= Out_G1) and (In_G1 <= Out_R1 + 1) and ((In_G1 - Out_G1 ==0) or (In_R1 - Out_R1 == 0))

Bounded Global Invariant Counter Version

(R_pc1 <= 0 ) and (R_pc2 <=1) and (E1_0 == 0 or E1_1 == 0))

Core Functional Code

class GyroRudder$fine
{
    public static void main ( String argv [ ] )

    {
        new Gyroscope ( ) . start ( ) ;

        new Gyroscope ( ) . start ( ) ;

        new Rudder ( ) . start ( ) ;

        new Rudder ( ) . start ( ) ;

    }
}

final class Gyroscope extends Thread
{

    public void run ( )
    {
        while ( true )

        {
            /*** GyroRdder Gyroscope enter  ***/
            System . out . println ( "gyroscope putting:" ) ;

            System . out . println ( "gyroscope putting" ) ;

            /*** GyroRudder Gyroscope exit  ***/
        }
    }
}

final class Rudder extends Thread

{
    public void run ( )
    {
        while ( true )

        {
            /*** GyroRudder Rudder enter  ***/
            System . out . println ( "Rudder getting:" ) ;

            System . out . println ( "done getting" ) ;

            /*** GyroRudder Rudder exit  ***/

        }
    }
}

Unbounded Coarse-Grain Solution

CLUSTER: GyroRudder
STATE SPACE VARIABLES: Gyroscope_in, Rudder_out, Rudder_in, Gyroscope_out;
REGION: Gyroscope
ENTER: <AWAIT Gyroscope_in + 1 <= Rudder_out + 1 && Rudder_in == Rudder_out --> Gyroscope_in++;>
NOTIFY: ;
NOTIFYALL: ;
EXIT: <Gyroscope_out++;>
NOTIFY: Rudder_in;
NOTIFYALL: ;

REGION: Rudder
ENTER: <AWAIT Rudder_in + 1 <= Gyroscope_out && Gyroscope_in == Gyroscope_out --> Rudder_in++;>
NOTIFY: ;
NOTIFYALL: ;
EXIT: <Rudder_out++;>
NOTIFY: Gyroscope_in;
NOTIFYALL: ;

Bounded Counter Coarse-Grain Solution

CLUSTER: GyroRudder
STATE SPACE VARIABLES: R1_pc, R2_pc, E1_0, E1_1;
LOCAL VARIABLES: ;
REGION: Gyroscope
ENTER: <AWAIT R1_pc <= 0 && E1_1 == 0 --> R1_pc+=1;E1_0++;>
NOTIFY: ;
NOTIFYALL: ;
EXIT: <R2_pc-=1;E1_0--;>
NOTIFY: Rudder_in;
NOTIFYALL: ;

REGION: Rudder
ENTER: <AWAIT R2_pc <= -1 && E1_0 == 0 --> R2_pc+=1;E1_1++;>
NOTIFY: ;
NOTIFYALL: ;
EXIT: <R1_pc-=1;E1_1--;>
NOTIFY: Gyroscope_in;
NOTIFYALL: ;

Unbounded Fine-Grain Solution

class SGCluster$GyroRudder {
// STATE SPACE VARIABLES: 
private static int Gyroscope_in , Rudder_out , Rudder_in , Gyroscope_out ;

// LOCAL VARIABLES: 

private static Object clusterCounterLock = new Object();


/**======================================================**
 **
 ** Generated lock and methods for await: Gyroscope$enter
 **
 **======================================================**/

private static Object condition$Gyroscope$enter = new Object();

public static void Gyroscope$enter(){
   synchronized (condition$Gyroscope$enter) {

      while ( !check$Gyroscope$enter())
         try {

            condition$Gyroscope$enter.wait();
         } catch (InterruptedException e){}

   }

}
private static boolean check$Gyroscope$enter() {

   synchronized (clusterCounterLock) {
      if (Gyroscope_in + 1 <= Rudder_out + 1 && Rudder_in == Rudder_out ) {

         Gyroscope_in ++ ; 
         return true;
      } else

         return false;
   }
}
/**======================================================**
 **
 ** Generated lock and methods for atomic: Gyroscope$exit
 **
 **======================================================**/

public static void Gyroscope$exit() {

   synchronized (clusterCounterLock) {
      Gyroscope_out ++ ; 
   }

   synchronized (condition$Rudder$enter) {
      condition$Rudder$enter.notify(); 
   }


}


/**======================================================**
 **
 ** Generated lock and methods for await: Rudder$enter
 **
 **======================================================**/

private static Object condition$Rudder$enter = new Object();

public static void Rudder$enter(){
   synchronized (condition$Rudder$enter) {

      while ( !check$Rudder$enter())
         try {

            condition$Rudder$enter.wait();
         } catch (InterruptedException e){}

   }

}
private static boolean check$Rudder$enter() {

   synchronized (clusterCounterLock) {
      if (Rudder_in + 1 <= Gyroscope_out && Gyroscope_in == Gyroscope_out ) {

         Rudder_in ++ ; 
         return true;
      } else

         return false;
   }
}
/**======================================================**
 **
 ** Generated lock and methods for atomic: Rudder$exit
 **
 **======================================================**/

public static void Rudder$exit() {

   synchronized (clusterCounterLock) {
      Rudder_out ++ ; 
   }

   synchronized (condition$Gyroscope$enter) {
      condition$Gyroscope$enter.notify(); 
   }


}

}

Bounded Fine-Grain Solution

class SGCluster$GyroRudder {
// STATE SPACE VARIABLES: 

private static int R1_pc , R2_pc , E1_0 , E1_1 ;

// LOCAL VARIABLES: 

private static Object clusterCounterLock = new Object();


/**======================================================**
 **
 ** Generated lock and methods for await: Gyroscope$enter
 **
 **======================================================**/

private static Object condition$Gyroscope$enter = new Object();

public static void Gyroscope$enter(){
   synchronized (condition$Gyroscope$enter) {

      while ( !check$Gyroscope$enter())
         try {

            condition$Gyroscope$enter.wait();
         } catch (InterruptedException e){}

   }

}
private static boolean check$Gyroscope$enter() {

   synchronized (clusterCounterLock) {
      if (R1_pc <= 0 && E1_1 == 0 ) {

         R1_pc += 1 ; E1_0 ++ ; 
         return true;

      } else
         return false;
   }
}
/**======================================================**
 **
 ** Generated lock and methods for atomic: Gyroscope$exit
 **
 **======================================================**/

public static void Gyroscope$exit() {
   synchronized (clusterCounterLock) {

      R2_pc -= 1 ; E1_0 -- ; 
   }

   synchronized (condition$Rudder$enter) {
      condition$Rudder$enter.notify(); 
   }


}


/**======================================================**
 **
 ** Generated lock and methods for await: Rudder$enter
 **
 **======================================================**/

private static Object condition$Rudder$enter = new Object();

public static void Rudder$enter(){
   synchronized (condition$Rudder$enter) {

      while ( !check$Rudder$enter())
         try {

            condition$Rudder$enter.wait();
         } catch (InterruptedException e){}

   }

}
private static boolean check$Rudder$enter() {

   synchronized (clusterCounterLock) {
      if (R2_pc <= -1 && E1_0 == 0 ) {

         R2_pc += 1 ; E1_1 ++ ; 
         return true;

      } else
         return false;
   }
}
/**======================================================**
 **
 ** Generated lock and methods for atomic: Rudder$exit
 **
 **======================================================**/

public static void Rudder$exit() {
   synchronized (clusterCounterLock) {

      R1_pc -= 1 ; E1_1 -- ; 
   }

   synchronized (condition$Gyroscope$enter) {
      condition$Gyroscope$enter.notify(); 
   }


}

}