5.12 Blocking in system context

Blocking has a direct effect on a single event, but it also influences the rest of the system behavior. To investigate the effects of the blocking keyword in system context, we will describe two examples. In the first example we concentrate our attention on the event interleaving at the provides ports. The second example focusses on the interleaving of events that originate from the requires ports.

The indirect effect of the use of the blocking keyword is referred to as collateral blocking. Blocking an event means making the caller wait by withholding its return until some state has been reached which is indicated by another event. To achieve this, the other processes outside the component that is applying the blocking keyword must be able to make progress. Furthermore the component must be exposed to this progress to be able to resolve the blocking situation by returning to its caller.

Let us recapitulate blocking with a small example component that will be used by each of the examples in this section.

import iblock.dzn;
import iworld.dzn;

component block
{
  provides blocking iblock b;
  requires iworld w;
  behavior
  {
    blocking on b.block():
    {
      w.hello();
      //execution waits here for b.reply()
      //to occur as a result of w.world()
    }

    on w.world(): b.reply();
  }
}

Here we see component block that withholds its return on port b until it has received event r.world. Remember that a significant amount of time may pass between r.hello and r.world. During this time the rest system that contains our block component could make progress, without the component becoming aware. If we add more system context to our block component we can see how collateral blocking manifests itself. We will add component collateral as a client to block.

import ihelloworld.dzn;
import iworld.dzn;
import iblock.dzn;

component collateral
{
  provides blocking ihelloworld h;
  requires blocking iblock b;
  requires iworld w;

  behavior
  {
    bool idle = true;
    [idle] on h.hello(): {w.hello(); b.block(); idle = false;}
    [!idle] on w.world(): {h.world(); idle = true;}
  }
}

Besides being a client to component block this component is also a client to another regular non-blocking component. The event sequence trace below shows the first of the two possible scenarios implemented by the collateral component.

In this first scenario nothing is out of the ordinary, but now take a look at the second event sequence trace below.

Here we can see that during the time between b.block and b.return the world event on port w is allowed to occur. This is the result of the fact that although the collateral component is blocked on its call to b.block, it will find w.world in its queue before returning to its caller. And as a result, forwarding w.world as h.world will occur before returning to its caller, which differs from the previous scenario. Verification of component collateral will check for both scenarios and ensure that the component behavior complies with all of the inteface behavior or otherwise report the non-compliant scenario. Verification relies on the blocking annotation on port b in order to infer the collateral blocking scenario and check for it.

• Collateral blocking and multiple provides.

5.12.1 Collateral blocking and multiple provides.

We can now revisit the blocking multiple provides example. Instead of making the multiplexing component responsible for the synchronization, we can also add a level of indirection by splitting up blocking_multiple_provides into a separate component that takes care of synchronizing the asynchronous behavior and a separate multiple provides component. The latter can be expressed as component mux below:

import ihello.dzn;
import iblock.dzn;

component mux
{
  provides blocking ihello left;
  provides blocking ihello right;

  requires blocking iblock b;

  behavior
  {
    on left.hello(): b.block();
    on right.hello(): b.block();
  }
}

This component, notwithstanding the blocking annotations on its ports, behaves exactly like component multiple_provides. However, when we bring its clients into scope we get the system model below.

import mux.dzn;
import proxy.dzn;

component collateral_multiple_provides
{
  provides blocking ihello left;
  provides blocking ihello right;

  requires blocking iblock block;

  system
  {
    proxy l;
    proxy r;
    mux m;

    left <=> l.h;
    l.r <=> m.left;
    right <=> r.h;
    r.r <=> m.right;

    m.b <=> block;
  }
}

In its event sequence trace we can see another impact of collateral blocking.

Although the behavior across the mux component is non-overlapping the behavior of the client components is interleaved.

Note: In Dezyne blocking is implemented by means of coroutines. Therefore the interleaving of event sequences is a form of cooperative multi-tasking. As a result its behavior is deterministic as opposed to non-deterministic as in multi-threaded interleaving.