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):
A scenario for the rudder 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.
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).
- R1 waits until gyroscope value is in buffer, reads value from buffer.
- R2 actuates rudder based on value.
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
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();
}
}
}