Previous: , Up: How to use ‘external'?   [Contents]


4.2.4 ‘The’ solution: handshake protocol

The recommended option is to implement a handshake mechanism to ensure that the current session is closed. If you recall, the original problem we discovered was that it was possible to queue a timeout event while the timer was being cancelled. The description of the problem already hints at part of the solution: apparently there exists a state where the Timer is being cancelled. This state starts when the cancel event is sent and ends at some point in time.

When the being cancelled state has ended, this means that the Timer has fully stopped and as such, no timeout events can occur anymore. If you queue a notification that this condition is fulfilled, this notification can be used to denote the end of a Timer session.

As an exercise, extend the ITimer interface with a Stopping state that starts when a Running timer is cancelled. Within the Stopping state, in-events should be illegal and inevitably, an out-event cancelled should be sent.

Solution:

interface ITimer {
  extern long_integer $long$;
  enum State { Idle, Running, Stopping };
  in void start(long_integer milliseconds);
  in void cancel();
  out void timeout();
  out void cancelled();

  behaviour {
    State state = State.Idle;

    [state.Idle] {
      on start: state = State.Running;
      on cancel: { }
    }

    [state.Running] {
      on start: illegal;
      on cancel: state = State.Stopping;
      on inevitable: {
        state = State.Idle;
        timeout;
      }
    }

    [state.Stopping] {
      on start: illegal;
      on cancel: illegal;
      on inevitable: {
        state = State.Idle;
        cancelled;
      }
    }
  }
}

With the above interface modification, a handshake protocol can be supported where the end of a Timer session is marked with a cancelled event. You may find yourself wondering why this is so useful.

Here’s the trick: the event that marks the end of a session travels through the same communication channel as the timeout events. The interface prohibits sending timeouts during the Stopping state and the Stopping state transitions to the Idle state where again, no timeouts can be sent. Therefore, it is guaranteed that there will be no more timeout events from the previous session after the cancelled event has been placed into the queue.

So, the modified ITimer interface complies with the handshake we want to implement to solve the ‘external’ delay problem. What remains to be done is update the RobustTimer component behaviour to make use of the newly added handshake.

The behaviour we want to add to the RobustTimer is the addition of the Stopping state. When a cancel event is sent to its provided ITimer port, this is propagated to the ‘external’ ITimer port and the RobustTimer transitions to the Stopping state. Until the ‘external’ ITimer port has replied with a cancelled event, any timeouts coming through the port while Stopping should be silently discarded. When the cancelled event is handled, the RobustTimer transitions back to the Idle state and the cancelled event is propagated to the provided ITimer.

As an exercise, add the changes listed above to the behaviour of the RobustTimer component.

Solution:

component RobustTimer {
  provides ITimer iTimer;
  requires external ITimer ext_iTimer;

  behaviour {
    enum State { Idle, Running, Stopping };
    State state = State.Idle;

    on iTimer.start(ms): {
      [state.Idle] {
        ext_iTimer.start(ms);
        state = State.Running;
      }
    }

    on iTimer.cancel(): {
      [state.Running] {
        ext_iTimer.cancel();
        state = State.Stopping;
      }
      [state.Idle] { }
    }

    on ext_iTimer.timeout(): {
      [state.Running] {
        iTimer.timeout();
        state = State.Idle;
      }
      [state.Stopping] { /* discard */ }
    }

    on ext_iTimer.cancelled(): {
      [state.Stopping] {
        iTimer.cancelled();
        state = State.Idle;
      }
    }
  }
}

If you verify the behaviour in the above solution, you will still encounter one last verification error. While we were focussing on making sure possibly delayed timeouts are properly handled, we didn’t implement the handshake we designed for that purpose in the scenario where an Idle Timer receives a cancel event. Luckily, the fix for this is a pretty simple one:

interface ITimer {
  // variable and event declarations
  behaviour {
    [state.Idle] {
      on start: state = State.Running;
      on cancel: { cancelled; }
    }
    // rest of the behaviour specification
component RobustTimer {
  provides ITimer iTimer;
  requires external ITimer ext_iTimer;

  behaviour {
    // variable declarations
    on iTimer.cancel(): {
      [state.Running] {
        ext_iTimer.cancel();
        state = State.Stopping;
      }
      [state.Idle] { iTimer.cancelled(); }
    }
    // rest of the component implementation

With these additions in place, the RobustTimer component will pass verification and you have successfully implemented a protocol that is robust against possibly delayed asynchronous events from a foreign component. By doing this in a Dezyne component, any other component that is connected to the ITimer port provided by RobustTimer can use it as if it were not ‘external’. Only the RobustTimer component is responsible for handling the ‘external’ behaviour.

In the next and final section, we will have a look at what needs to be updated in the rest of the Alarm System and afterwards we will take a step back and summarise what we’ve discovered throughout this tutorial.


Previous: , Up: How to use ‘external'?   [Contents]