spin failure model

spin_failure_model.pml

mtype = { FISH , RESCHEDULE , SCHEDULE , SCHEDULEREQ , SCHEDULEAUTH , ACK , NOWORK , SENDFAILED , PING } ; // message payload types
mtype = { ONNODE , INTRANSITION }; // spark.status types

typedef Node {
  chan inChan = [50] of {mtype, chan } ;
  bool hasSpark;
  bool waitingFish;
  bool waitingSchedAuth;
  bool dead;
};
#define SLAVES 3
Node slaves[SLAVES];
Node master;

typedef Location
{
  chan from = [50] of { mtype , chan } ;
  chan to = [50] of { mtype , chan } ;
}

typedef Spark
{
  mtype status;
  Location trail ;
};
Spark spark ;

chan dummy = [50] of { mtype , chan } ;
chan masterRequests  = [50] of { mtype , chan , chan } ;

inline send_schedule_to_random_alive_slave() {
  if
    :: !slaves[0].dead ->
       atomic {
         spark.trail.to = slaves[0].inChan;
         spark.status = INTRANSITION;
         spark.trail.from = master.inChan;
         master.hasSpark = false;
       }
       slaves[0].inChan ! SCHEDULE(master.inChan);
       
    :: !slaves[1].dead ->
       // atomicIORef.. (status and trail in the same IORef?)
       atomic {
         spark.trail.to = slaves[0].inChan;
         spark.status = INTRANSITION;
         spark.trail.from = master.inChan;
         master.hasSpark = false;
       }
       slaves[1].inChan ! SCHEDULE(master.inChan);
       spark.trail.to = slaves[1].inChan;
    :: !slaves[2].dead ->
       atomic {
         spark.trail.to = slaves[0].inChan;
         spark.status = INTRANSITION;
         spark.trail.from = master.inChan;
         master.hasSpark = false;
       }
       slaves[2].inChan ! SCHEDULE(master.inChan);
       spark.trail.to = slaves[2].inChan;
  fi ;
  
}

active proctype Master() priority 2 {
  // reflect this in the haskell
  d_step {
    spark.status = ONNODE ;
    spark.trail.to = master.inChan ;
  }
  
  // Run the supervising monitors . This re-distributes sparks when nodes die
  run MonitorNode(0);
  run MonitorNode(1);
  run MonitorNode(2);
  
  // Run the slaves, tell slave 1 to fail in the future
  run Slave(0, true);
  run Slave(1,false);
  run Slave(2, false);
  
  // Randomly send spark to one of three slaves
  send_schedule_to_random_alive_slave() ;
  
  /* Supervisor reacts to either ACK or SCHEDULENOTIFY */
  chan sendingNode;
  chan receivingNode;
  chan deadNode;
  do
    :: masterRequests ? SCHEDULEREQ(sendingNode, receivingNode) ->
       if
         :: spark.status == ONNODE ->
            spark.status = INTRANSITION;
            spark.trail.from = sendingNode ;
            spark.trail.to = receivingNode ;
            sendingNode ! SCHEDULEAUTH(receivingNode);
         :: else -> skip ;
       fi
       
    :: master.inChan ? ACK(receivingNode) ->
       spark.status = ONNODE;
       spark.trail.from = receivingNode ;
       spark.trail.to = receivingNode ;
       
    :: master.inChan ? RESCHEDULE(deadNode) -> // deadNode var not used
       // master.hasSpark = true ;
       send_schedule_to_random_alive_slave() ;
  od
}  // END OF MASTER

proctype Slave(int me; bool willFail) {
  
  slaves[me].dead = false;
  slaves[me].waitingFish = false;
  slaves[me].waitingSchedAuth = false;
  slaves[me].hasSpark = false;
  
  chan fishingNode , sender, authorizedReceiver;
  int failureCounter = 0 , timeToFailure = 20;
  
  /* Slaves receive either FISH , SCHEDULE or NOWORK */
  do
    :: (willFail == true) ->
       
       failureCounter++ ;
       if
         :: failureCounter > timeToFailure ->
            atomic { 
              slaves[me].dead = true;
              slaves[me].hasSpark = false;
            }
            // From now on, just reply to messages with SENDERROR
            goto ECHOFAILURE ;
         :: else -> skip ;
       fi
    :: (slaves[me].hasSpark == false && slaves[me].waitingFish == false) -> // Let's go fishing
       slaves[me].waitingFish = true;
       if
       :: (0 != me) && !slaves[0].dead -> slaves[0].inChan ! FISH(slaves[me].inChan) ;
       :: (1 != me) && !slaves[1].dead -> slaves[1].inChan ! FISH(slaves[me].inChan);
       :: (2 != me) && !slaves[2].dead -> slaves[2].inChan ! FISH(slaves[me].inChan);
       :: else -> printf("All nods exhausted for task re-distribution\n");
       fi ;
   :: slaves[me].inChan ? NOWORK(sender) -> slaves[me].waitingFish = false;      // can fish again
   :: slaves[me].inChan ? SENDFAILED(sender) -> slaves[me].waitingFish = false;  // can fish again
   :: slaves[me].inChan ? FISH(fishingNode) -> // React to FISH request
         if
         :: (slaves[me].hasSpark == true && ! slaves[me].waitingSchedAuth ) -> // We have the spark
               masterRequests ! SCHEDULEREQ(slaves[me].inChan, fishingNode);
               slaves[me].waitingSchedAuth = true;
         ::  else -> fishingNode ! NOWORK(slaves[me].inChan) ; // We don't have the spark
  fi 
  :: slaves[me].inChan ? SCHEDULEAUTH(authorizedReceiver) -> // React to FISH request
     slaves[me].waitingSchedAuth = false;
     slaves[me].hasSpark = false;
     slaves[me].waitingFish = false;
     authorizedReceiver ! SCHEDULE(slaves[me].inChan);
  :: slaves[me].inChan ? SCHEDULE(sender) -> // We're being sent the spark
          slaves[me].hasSpark = true;
          master.inChan ! ACK(slaves[me].inChan); // Send ACK To master
   od ;

ECHOFAILURE:// Mimics the error events from transport layer
  do
  :: slaves[me].inChan ? FISH(fishingNode)   -> fishingNode ! SENDFAILED(slaves[me].inChan) ;
  :: slaves[me].inChan ? NOWORK(fishingNode) -> fishingNode ! SENDFAILED(slaves[me].inChan) ;
  :: slaves[me].inChan ? NOWORK(fishingNode) -> fishingNode ! SENDFAILED(slaves[me].inChan) ;
  od ;

} // END OF SLAVE

proctype MonitorNode(int slaveID){
  
monitor:
  if
    :: (slaves[slaveID].dead == true) ->
       if
         :: spark.status == ONNODE ->
            if
              :: spark.trail.to == slaves[slaveID].inChan ->
                 printf("MASTER: re-distributing lost spark\n");
                 master.inChan ! RESCHEDULE(dummy);
                 goto terminate ;
              :: else -> skip ; // Failure not affecting spark
            fi
            
         :: spark.status == INTRANSITION ->
            if
              :: spark.trail.from == slaves[slaveID].inChan || spark.trail.to == slaves[slaveID].inChan ->
                 printf("MASTER: re-distributing lost spark\n");
                 master.inChan ! RESCHEDULE(dummy);
                 goto terminate ;
              :: else -> skip
            fi ;
       fi ;
    :: else -> goto monitor ;
  fi ;
  
terminate: skip
}