Previous: , Up: Ports   [Contents][Index]

10.5.1.2 external

The external keyword specifies that communication over a requires port may experience a delay. This may for instance be caused by the switch between execution contexts as in inter-process communication or the use of threads. 

requires external itimer t;

During verification the delay on an external interface is experienced an additional interleaving of events that would otherwise not occur.

10.5.1.3 Race condition due to external delay

Component remote_timer_proxy illustrates how a delayed communication channel may cause a race condition leading to illegal behavior.

The implementation of component remote_timer_proxy is correct (no illegal behavior) for requires itimer rp but incorrect for requires external itimer rp due to race between pp.cancel and rp.timeout. 

extern double $double$;

interface itimer
{
  in void create (double seconds);
  in void cancel ();
  out void timeout ();
  behavior
  {
    bool is_armed = false;
    [!is_armed] on create: is_armed = true;
    on cancel: is_armed = false;
    [is_armed] on inevitable: {timeout; is_armed = false;}
  }
}

component remote_timer_proxy
{
  provides itimer pp;
  requires external itimer rp;
  behavior
  {
    bool is_armed = false;
    on pp.create (s):
      [!is_armed] {rp.create (s); is_armed = true;}
    on pp.cancel (): {rp.cancel (); is_armed = false;}
    on rp.timeout ():
      [is_armed] {pp.timeout (); is_armed = false;}
  }
}