We’re here to help you

Menu

Simplifying an 'external' Implementation Using 'blocking'

In this chapter, we will take a look at describing an asynchronous process as if it were synchronous. We will do this by use of the ‘blocking’ keyword. The asynchronous process we will be considering is the cancelling of RobustTimer. In case you hadn’t had a look at the snapshot containing Dezyne models and C++ source code already, it is available on Github.

Changing RobustTimer to provide a synchronous Timer interface

The goal is to make RobustTimer easier to use with respect to its provided port. We will still want the newer version of the ITimer interface to fully describe the behaviour of the ‘external’ requires port, but we want to translate this to a simplified version of ITimer. The original ITimer interface will suffice.

Exercise: Perform the following tasks:

  • rename the new ITimer interface to AsyncITimer

  • reinstate the “old” ITimer interface as ITimer

  • change the RobustTimer to requires ‘external’ AsyncITimer and provides ITimer


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

  behaviour {
    State state = State.Idle;

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

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

interface AsyncITimer {
  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: { cancelled; }
    }

    [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;
      }
    }
  }
}

component RobustTimer {
  provides ITimer iTimer;
  requires external AsyncITimer 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] { iTimer.cancelled(); }
    }

    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;
      }
    }
  }
}


These changes will break several parts of the application, but let’s focus on RobustTimer only for now. The cancellation process was quite nasty; a cancel event on its provided ITimer port started the process, at which point the provided ITimer port was unusable until the cancelled event from ext_iTimer came in. By separating the provides and requires interfaces, you are no longer forced to describe this period of unusability in the provides interface. From the provides port point of view, the cancellation process is synchronous again; all that remains is to make sure the RobustTimer component is verifiably correct with the new provides/requires ports.

The beginning of the cancellation process is the cancel event on the provided iTimer; the mark that denotes the end of the process is the cancelled event from the required ext_iTimer. ‘blocking’ allows you to postpone the return of an incoming event from a provides port until an event comes in from a different port; this sounds exactly like the scenario of the cancellation process.

In RobustTimer, there are two locations where the cancellation process is ended, both currently marked by the iTimer.cancelled() event left over from the previous iteration of RobustTimer. If we were to denote the iTimer.cancel() event as ‘blocking’, the ending of the transaction will be in the same locations as the current iTimer.cancelled() events:

component RobustTimer {
  provides ITimer iTimer;
  requires external AsyncITimer 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;
      }
    }

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

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

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

Note that the transaction endpoints are represented as port.reply() events. An important thing to keep in mind is that with ‘blocking’, you block the calling thread of the event until the blockage is lifted- which is done with the port.reply() event. The modified RobustTimer posted above is verifiably correct and will display the following behaviour:

On iTimer.cancel, the iTimer port is blocked. If the RobustTimer is Running, the cancel event will be sent to ext_iTimer and RobustTimer will transition to the Stopping state. In the Stopping state, the asynchronous ext_iTimer.cancelled event will release the blocked iTimer port. If RobustTimer was Idle upon receiving iTimer.cancel, the blocked iTimer port is immediately released.

This immediate release of the blocked iTimer port hints at a possible optimization; if a port is released instantly then it doesn’t really have to be blocked at all. By nesting the ‘blocking’ keyword deeper into the [guard]-on event scope you can avoid this unnecessary blockage:

component RobustTimer {
  provides ITimer iTimer;
  requires external AsyncITimer 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(): {
      blocking [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] {
        state = State.Idle;
        iTimer.reply();
      }
    }
  }
}

With the changes highlighted above, the ‘blocking’ keyword is nested deeper and affects fewer behaviour traces; the net behaviour is the same. Note that when on-event behaviour is not marked as blocking, a void port.reply() event is not allowed; hence, [state.Idle] now shows as no-op instead of port.reply(). The continuation is implicit when the on-event is not ‘blocking’.

From the perspective of the iTimer port, the cancellation process is now synchronous; a cancel event sent through the iTimer port will not return until the cancellation process has been completed. RobustTimer can still make use of the asynchronous specification of AsyncITimer to facilitate the cancellation handshake. Therefore, the asynchronous behaviour has successfully been made synchronous by using the ‘blocking’ keyword.

With the changes made to the provides interface of RobustTimer, you should also repair the Controller and AlarmSystem components. The Rearming state in the Controller can be removed as the cancellation process is synchronized. In AlarmSystem, some port types will have to be renamed to reflect the new interface names.

Exercise: Fix the models so they are free of errors again.


the final versions of the models in the AlarmSystem application can be found on Github.


Unlike in the ‘external’ tutorial, no native source code will have to be changed. All of the simplifications that were made are in Dezyne models and the native components and ports on the boundary of the System remain unchanged. The only requirement to be able to use ‘blocking’ is that your System is generated with a thread-safe-shell (and for now, only C++ is supported). The generation of a thread-safe-shell is included in the makefile, therefore the AlarmSystem application is fully functional again.

Now that we have implemented a simplification of the asynchronous ITimer interface, let’s consider some implications this will have for the runtime behaviour of the AlarmSystem application in the next chapter.

If you have questions that weren’t answered by this Guide,
let our support team help you out.

Enjoy this article? Don't forget to share.