Lesson 5: Increasing Concurrency

In the previous lesson, we modified ValveControllerImpl in an attempt to prevent it blocking its client while the valve is moving in order to comply with requirement R3. Our solution only partly meets this goal. To illustrate where our current solution fails, consider the following Coco snippet of a component implementation of a client using our ValveControllerImpl component:

    state Empty {
      client.startFillingTank() = {
        valve.open();
        setNextState(Filling);
      }
    }

    state Filling {
      client.isValveMoving() = !(valve.isOpen() || valve.isClosed())
    }

In state Filling, the client could be blocked when executing the transition for isValveMoving(), depending on whether or not the valve finished moving when isValveMoving() was called. This is because while the valve is moving, the ValveControllerImpl is in an execution state. If the client attempts a call on ValveControllerImpl while it is in an execution state, the client will become blocked until the ValveControllerImpl enters an event state.

The current implementation of the ValveControllerImpl therefore does not guarantee that isOpen() and isClosed() are always non-blocking, and so requirement R3 is not met.

In this lesson, we will build a solution in which the required non-blocking property of the valve controller is always preserved, and the client can always remain responsive.

We will be introducing the following new language features:

  • Nested states.
  • Component queues and handling incoming signals from required ports.
  • The built-in variable nextState.

Extending the Architecture

We could make the ValveHALBase component more complex to solve the asynchronies there. However, this goes against our objective of keeping ValveHALBase as a simple, handwritten component that makes the hardware/software interface accessible to the Coco components. Instead, we are going to define a new level of abstraction called the ValveDriverImpl with the goal of making a uniform interface defined by the ValveDriver port, which hides as many differences between different hardware valve types as possible.

The revised architecture is as follows:

ValveGroup valve : ValveControllerImpl driver : ValveDriverImpl client : ValveController client : ValveController client : ValveDriver hal : ValveHAL hal driver ValveHALBase Application client : ValveHAL valve ENC

In addition to the existing ValveControllerImpl component, we have now introduced the following two new components:

  1. ValveDriverImpl is a driver module which abstracts away valve-specific characteristics behind a common interface. The existence of this component, and its provided port are invisible to the client application.
  2. ValveGroup is an encapsulating component which consists of a ValveControllerImpl and a ValveDriverImpl, and implements ValveController as its provided port. It appears as a single opaque component to other components using it, which it interacts with via its provided port client.

We will abstract away from the details of whether or not the physical valve movement is synchronous or asynchronous, and the way in which the end of the valve movement is determined. This satisfies the requirement R4, and allows a single implementation of the ValveControllerImpl to work with more valve types, each of which potentially has its own, type-specific driver.

Step 1: Creating the ValveDriver Port

We start by creating a new module called ValveDriver as follows:

import unqualified ValveHAL

port ValveDriver {
  enum Status {
    case Unknown
    case Opened
    case Closed
    case Moving
    case Error
  }

  function setup(settings : ValveParameters) : Bool
  function open() : Nil
  function close() : Nil

  outgoing signal endOfMovement(result : Status)

  machine {
    // Initial position unknown
    var status : Status = .Unknown

    state Initial {
      setup(_) = nondet {
        ValidParameters:
        {
          setNextState(Ready);
          true
        },
        InvalidParameters: false,
      }
    }

    state Ready {
      open() = setNextState(Moving(.Opened))
      close() = setNextState(Moving(.Closed))
    }

    state Moving(target : Status) {
      spontaneous = {
        status = nondet {
          MoveSucceeded: target,
          MoveFailed: .Error,
        };
        endOfMovement(status);
        setNextState(Ready);
      }
    }
  }
}

We are not introducing any new Coco constructs in this port, so it should be clear to anyone who has worked through the previous lessons.

The complete Coco for this port is in Example_05B/src/ValveDriver.coco.

Step 2: Creating the ValveDriverImpl Component

Our next step is to create a component to implement a virtual valve. It will behave asynchronously, and report error conditions, irrespective of whether or not the underlying hardware has these properties. We have designed this example to implement asynchronous movement on hardware that behaves synchronously, while modifying the ValveControllerImpl so that it remains responsive during the valve movement.

Our complete component for ValveDriverImpl is as follows:

import unqualified ValveDriver
import unqualified ValveHAL

@runtime(.MultiThreaded)
component ValveDriverImpl {
  val client : Provided<ValveDriver>
  val hal : Required<ValveHAL>

  machine {
    state Initial {
      client.setup(settings : ValveParameters) = if (hal.setParameters(settings)) {
        setNextState(Ready);
        return true;
      } else {
        return false;
      }
    }

    state Ready {
      client.open() = setNextState(Moving(.Open))
      client.close() = setNextState(Moving(.Close))
    }

    // Asynchronously execute the synchronous valve movement
    execution state Moving(target : ValveHAL.Moves) {
      hal.move(target);
      // Signal end of movement - this valve has no errors
      client.endOfMovement(match (target) {
        .Open => .Opened,
        .Close => .Closed,
      });
      // Ready for next move
      setNextState(Ready);
    }
  }
}

We have not used any new constructs in this component, so it should be clear to anyone who has worked through the previous lessons.

Similar to the previous implementation of the ValveControllerImpl, this component cannot respond to its client, the ValveControllerImpl, until the execution state has finished, and the state machine has changed to an event state. This means that for ValveControllerImpl to remain responsive to its client, it must not interact with ValveDriverImpl while the valve is moving.

The complete Coco for this component is in Example_05B/src/ValveDriver.coco.

Step 3: Modifying ValveControllerImpl to use ValveDriver

We now need to modify the ValveControllerImpl component to use the ValveDriverImpl component, instead of directly accessing the ValveHALBase. We will:

  1. Replace the current required port instance hal with a new instance of ValveDriver, called driver, and change all references of hal to driver throughout the state machine.
  2. Replace the execution state with an event state, which will handle the endOfMovement(…) signal from ValveDriver.

While making these changes, we will also take the opportunity to refactor ValveControllerImpl. The modified version looks like the following:

import unqualified ValveController
import unqualified ValveDriver
import unqualified ValveHAL

@runtime(.MultiThreaded)
component ValveControllerImpl {
  val client : Provided<ValveController>
  val driver : Required<ValveDriver>

  machine {
    client.isOpen() = false
    client.isClosed() = false

    state Initial {
      client.setup(settings : ValveParameters) = if (driver.setup(settings)) {
        setNextState(Ready.Unknown);
        return true;
      } else {
        return false;
      }
    }

    state Ready {
      client.open() = {
        driver.open();
        setNextState(Moving)
      }
      client.close() = {
        driver.close();
        setNextState(Moving)
      }

      // Valve position unknown until the first move request is received
      state Unknown {}

      state Opened {
        client.isOpen() = true
        client.open() = client.moveEnded(true)
      }

      state Closed {
        client.isClosed() = true
        client.close() = client.moveEnded(true)
      }
    }

    state Moving {
      driver.endOfMovement(result : ValveDriver.Status) = {
        setNextState(match (result) {
          .Opened => Ready.Opened,
          .Closed => Ready.Closed,
          _ => abort(),
        });
        client.moveEnded(true);
      }
    }
  }
}

In the refactored state machine, a new state called Ready is introduced to encapsulate all the stationary states that are able to receive open() and close() requests, namely Unknown, Opened, and Closed. These states are known as nested or child states of Ready, which in turn is referred to as their parent state. Ready has transition declarations for open() and close() at the top-level, which means that if either of them is called when the state machine is in one of the nested states with no matching transition enabled, then the corresponding top-level transition (i.e. in Ready) will be executed. For example, the nested state Unknown does not have any transitions, and therefore the corresponding transitions in the parent state Ready will be executed in the event that open() or close() is called.

Note

Coco supports hierarchical state machines. This means that every event state, except for Terminated, can have nested states to any depth, forming a rooted tree of parent-child relationships with Main as the root. Event transitions for the same event can be declared in multiple states across the hierarchy.

When a component state machine receives an incoming function call or signal in a state S, it will execute the corresponding enabled event transition declared in S. If no such match exists, then the state machine will execute the corresponding match transition declared in the nearest ancestor of S. If no matching transitions exist in any of the ancestors of S up to and including Main, then it will execute the illegal handler for that incoming event. See Dispatching Events in a Component State Machine for further details.

Verifying your Changes (Example_05B)

The verification fails because the ValveControllerImpl is no longer well-formed and produces the following counterexample:

User User ValveControllerImpl ValveControllerImpl driver driver setup(_) setup(_) setup(_) setup(_) [nondet ] ValidParameters [nondet ] ValidParameters return true return true return true return true open() open() open() open() return nil return nil [spontaneous…tus.Error,} [spontaneous] status = nondet …r.Status.Error,} [nondet ] MoveSucceeded [nondet ] MoveSucceeded (queued): endO…tatus.Opened) (queued): endOfMovement(Status.Opened) Initial Initial Initial Initial Initial Ready Ready.Unknown Ready Ready.Unknown Ready.Unknown Ready.Unknown Moving(Status.Opened) Moving Moving(Status.Opened) Moving(Status.Opened) Moving(Status.Opened) Moving Queue full. Exception counterexample

Analysis

The counterexample shows the required port driver is sending a signal to ValveControllerImpl, but its queue is full. This is because we have not declared a queue for the ValveControllerImpl component yet, and therefore it cannot receive any of the signals sent to it by its required port.

Step 4: Adding a Queue to ValveControllerImpl

We need to extend the ValveControllerImpl component with a queue that is big enough to store all of the signals that can be sent by its required ports before they have to be processed. In this case, a queue length of size 1 suffices.

We add a queue by labelling the ValveControllerImpl component declaration with the following @queue attribute:

@queue(1)

The modified Coco for this component is in Example_05C/src/ValveControllerImpl.coco.

Verifying the Models (Example_05C)

During verification, Popili finds an error where ValveControllerImpl calls abort(), which is not allowed:

User User ValveControllerImpl ValveControllerImpl driver driver setup(_) setup(_) setup(_) setup(_) [nondet ] ValidParameters [nondet ] ValidParameters return true return true return true return true close() close() close() close() return nil return nil [spontaneous…tus.Error,} [spontaneous] status = nondet …r.Status.Error,} [nondet ] MoveFailed [nondet ] MoveFailed return nil return nil (queued): endOf…t(Status.Error) (queued): endOfMovement(Status.Error) (dequeued): en…(Status.Error) (dequeued): endOfMovement(Status.Error) Initial Initial Initial Initial Initial Ready Ready.Unknown Ready Ready.Unknown Ready.Unknown Ready.Unknown Moving(Status.Closed) Moving Moving(Status.Closed) Moving(Status.Closed) Moving(Status.Closed) Moving Moving Ready Moving A call to abort() was made. Exception counterexample

Analysis

This counterexample illustrates how the last event performed by ValveControllerImpl before the abort() call is to dequeue an endOfMovement(Status.Error) in state Moving. Examining the corresponding transition in Moving, we see:

      driver.endOfMovement(result : ValveDriver.Status) = {
        setNextState(match (result) {
          .Opened => Ready.Opened,
          .Closed => Ready.Closed,
          _ => abort(),
        });
        client.moveEnded(true);
      }

A match expression, matching on the result parameter in the endOfMovement(…) signal, is used to determine the next state based on the result of the movement. The type of result is Status, which is an enum with five values, but the match expression only provides logic for two of them, and an abort() for all the others.

Step 5: Adding Missing Match Cases to ValveControllerImpl

The solution to this error is to amend the match statement by adding the missing cases as follows:

      driver.endOfMovement(result : ValveDriver.Status) = {
        setNextState(match (result) {
          .Open => Ready.Opened,
          .Closed => Ready.Closed,
          .Error => Ready.Unknown,
          .Unknown => Ready.Unknown,
          .Moving => abort(),
        });
        client.moveEnded(true);
      }

In the case of an error, we do not know the position of the valve. For completeness, we will also add the missing cases for .Unknown and .Moving.

The complete Coco for this component is in Example_05D/src/ValveControllerImpl.coco.

Verifying your Changes (Example_05D)

The verification fails because the ValveControllerImpl does not implement its provided port correctly:

client client User User ValveControllerImpl ValveControllerImpl driver driver setup(_) setup(_) setup(_) setup(_) [nondet ] ValidParameters [nondet ] ValidParameters setup(_) setup(_) [nondet ] ValidParameters [nondet ] ValidParameters return true return true return true return true return true return true open() open() open() open() [nondet 1] setN…ition.Opened)) [nondet 1] setNextState(Mov…osition.Opened)) open() open() return nil return nil [spontaneous…tus.Error,} [spontaneous] status = nondet …r.Status.Error,} [nondet ] MoveFailed [nondet ] MoveFailed (queued): endOf…t(Status.Error) (queued): endOfMovement(Status.Error) return nil return nil return nil return nil [spontaneous… = target;} [spontaneous] optional {position = target;} [nondet 0] position = target [nondet 0] position = target (dequeued): en…(Status.Error) (dequeued): endOfMovement(Status.Error) moveEnded(true) moveEnded(true) moveEnded(true) moveEnded(true) isOpen() isOpen() isOpen() isOpen() return false return false Initial Initial Initial Initial Initial Ready Initial Initial Ready Ready.Unknown Ready Ready Ready.Unknown Ready Ready.Unknown Moving(Position.Opened) Ready.Unknown Moving(Status.Open) Moving Moving(Status.Open) Moving(Status.Open) Moving(Status.Open) Moving Ready Moving(Position.Opened) Moving Moving(Position.Opened) Ready Ready.Unknown Ready Ready.Unknown Ready Ready.Unknown Ready.Unknown The last event performed by the component was not allowed by the provided port, which expected one of: return true Trace counterexample

Analysis

The counterexample shows the client calling open() on the ValveControllerImpl to close the valve, and in turn, ValveControllerImpl calls open() on its required port driver. driver sends an endOfMovement(.Error) signal to the ValveControllerImpl indicating that the move has failed, which in turn should send a moveEnded(false) signal to its client. Instead, it erroneously sends a moveEnded(true) specifying that the move completed without errors. As a result, the provided port, ValveController, expects ValveControllerImpl to be in state Opened when in fact, it is in state Unknown. Consequently, the isOpen() returns false when the provided port was expecting it to return true.

Note

When the verification finds an error, the shortest counterexample that results in the error is displayed. In this example, the same error can occur when the client calls open() or close(), and since their respective counterexamples are the same length, the one displayed may vary between releases.

Step 6: Modifying ValveControllerImpl

To resolve the error shown in the counterexample above, we will modify the Moving state in ValveControllerImpl to send the correct signals:

    state Moving {
      driver.endOfMovement(result : ValveDriver.Status) = {
        setNextState(match (result) {
          .Opened => Ready.Opened,
          .Closed => Ready.Closed,
          .Error => Ready.Unknown,
          .Unknown => Ready.Unknown,
          .Moving => abort(),
        });
        client.moveEnded(nextState != Ready.Unknown);
      }
    }

Note

The builtin variable nextState : State is an immutable copy of the parameter in the most recent call to one of the state transition functions. Its value can only be changed indirectly by calling one of these state transition functions, such as setNextState.

This nextState variable is used in the following statement:

        client.moveEnded(nextState != Ready.Unknown);

ValveControllerImpl sends the moveEnded() signal with an expression as its argument that refers to the value of nextState. If the value of nextState is Ready.Unknown, then this means that ValveControllerImpl has received one of the error conditions from the ValveDriverImpl, and sends the signal moveEnded(false). In all other cases, it sends the signal moveEnded(true).

The complete Coco for this component is in Example_05E/src/ValveControllerImpl.coco.

Verifying your Changes (Example_05E)

The project now verifies correctly.

Step 7: Extending ValveControllerImpl to Preserve Signal Data

When the valve completes a movement, the ValveDriverImpl component sends an endOfMovement(…) signal that is declared with the following signature:

  outgoing signal endOfMovement(result : Status)

In contrast, when the ValveControllerImpl component sends a signal to its client to indicate the completion of the valve movement, it does so with a signal declared as follows:

  outgoing signal moveEnded(result : Bool)

This loses information that would probably be useful to its client. We will therefore change the moveEnded() signature to match the corresponding signal sent by ValveDriverImpl by:

  1. Modifying the ValveController port to change the signal signature.
  2. Modifying the ValveControllerImpl component to solve any static type errors caused by changing its provided port.
  3. Reverifying the project, and fixing any other issues resulting from the changes.

Modifying ValveController

We will take the following steps to modify ValveController:

  1. Import the declarations from ValveDriver.
  2. Modify the signature in the signal declaration.
  3. Adapt the transition handlers that send this signal to handle the new signature.
  4. Modify the transition that sends this signal in state Moving with the new arguments.
  5. Delete the enum Position.

Your modified ValveController port should look like the following:

import unqualified ValveDriver
import unqualified ValveHAL

port ValveController {
  function setup(settings : ValveParameters) : Bool
  function open() : Nil
  function close() : Nil
  function isOpen() : Bool
  function isClosed() : Bool

  outgoing signal moveEnded(result : ValveDriver.Status)

  machine {
    var position : ValveDriver.Status = .Unknown
    isOpen() = position == .Opened
    isClosed() = position == .Closed

    state Initial {
      setup(_) = nondet {
        InvalidParameters:
        {
          return false;
        },
        ValidParameters:
        {
          setNextState(Ready);
          return true;
        },
      }
    }

    state Ready {
      open() = nondet {
        {
          position = .Opened;
          moveEnded(position);
        },
        {
          setNextState(Moving(.Opened))
        },
      }
      close() = nondet {
        {
          position = .Closed;
          moveEnded(position);
        },
        {
          setNextState(Moving(.Closed))
        },
      }
    }

    state Moving(target : ValveDriver.Status) {
      entry() = {
        position = .Unknown;
      }

      spontaneous = {
        position = nondet {
          target,
          .Unknown,
          .Error,
        };
        setNextState(Ready);
      }

      exit() = {
        moveEnded(position);
      }
    }
  }
}

Let’s step through each change in turn.

The following line imports ValveDriver:

import unqualified ValveDriver

This brings the declaration of Status into scope. The following line is the amended signal declaration:

  outgoing signal moveEnded(result : ValveDriver.Status)

The following lines are changed to use the values of Status:

    var position : ValveDriver.Status = .Unknown
    isOpen() = position == .Opened
    isClosed() = position == .Closed

The following lines are also changed to use Status defined in ValveDriver:

      open() = nondet {
        {
          position = .Opened;
          moveEnded(position);
        },
        {
          setNextState(Moving(.Opened))
        },
      }
      close() = nondet {
        {
          position = .Closed;
          moveEnded(position);
        },
        {
          setNextState(Moving(.Closed))
        },
      }

The parameter of state Moving is modified as follows:

    state Moving(target : ValveDriver.Status) {

Finally, the spontaneous transition handler is changed as follows:

        position = nondet {
          target,
          .Unknown,
          .Error,
        };

The complete Coco for this port is in Example_06A/src/ValveController.coco.

Modifying ValveControllerImpl

Your ValveControllerImpl component will now have type errors caused by the changes we have made to the signal declaration in its provided port ValveController.

To fix this, edit your component so that the state machine looks like the following:

  machine {
    client.isOpen() = false
    client.isClosed() = false

    state Initial {
      client.setup(settings : ValveParameters) = if (driver.setup(settings)) {
        setNextState(Ready.Unknown);
        return true;
      } else {
        return false;
      }
    }

    state Ready {
      client.open() = {
        driver.open();
        setNextState(Moving)
      }
      client.close() = {
        driver.close();
        setNextState(Moving)
      }

      // Valve position unknown until the first move request is received
      state Unknown {}

      state Opened {
        client.isOpen() = true
        client.open() = client.moveEnded(.Opened)
      }

      state Closed {
        client.isClosed() = true
        client.close() = client.moveEnded(.Closed)
      }
    }

    state Moving {
      driver.endOfMovement(result : ValveDriver.Status) = {
        setNextState(match (result) {
          .Opened => Ready.Opened,
          .Closed => Ready.Closed,
          .Error => Ready.Unknown,
          .Unknown => Ready.Unknown,
          .Moving => abort(),
        });
        client.moveEnded(result);
      }
    }
  }

The complete Coco for this component is in Example_06A/src/ValveControllerImpl.coco.

Step 8: Building an Encapsulating Component ValveGroup

As defined in the new architecture at the start of this lesson, some of the functionality of the ValveControllerImpl has been moved into a new component called ValveDriverImpl. The fact that we have divided the ValveControllerImpl into two components and how they are connected together at runtime, is private knowledge that should be hidden from the client. We should be free to refactor the ValveControllerImpl into as many components as we like in order to implement the specified behaviour, without having any impact on the client.

We will create a new encapsulating component called ValveGroup, which consists of an instance of ValveControllerImpl and an instance of ValveDriverImpl, and connects them together:

ValveGroup valve : ValveControllerImpl driver : ValveDriverImpl client : ValveController client : ValveController client : ValveDriver hal : ValveHAL hal driver ENC

Once we have done this, we will modify the TestValveGroup to instantiate the new ValveGroup component instead of ValveControllerImpl.

Creating ValveGroup

We start by declaring a new component called ValveGroup as follows:

import unqualified ValveController
import unqualified ValveControllerImpl
import unqualified ValveDriverImpl
import unqualified ValveHAL

@runtime(.MultiThreaded)
component ValveGroup {
  val client : Provided<ValveController>
  val hal : Required<ValveHAL>

  val valve : ValveControllerImpl
  val driver : ValveDriverImpl

  init() = {
    connect(client, valve.client);
    connect(valve.driver, driver.client);
    connect(driver.hal, hal);
  }
}

The following lines declare instances of its provided and required ports:

  val client : Provided<ValveController>
  val hal : Required<ValveHAL>

The following lines declare the instances valve and driver of the components ValveControllerImpl and ValveDriverImpl respectively:

  val valve : ValveControllerImpl
  val driver : ValveDriverImpl

The following constructor specifies how the component instances are connected together:

  init() = {
    connect(client, valve.client);
    connect(valve.driver, driver.client);
    connect(driver.hal, hal);
  }

Modifying TestValveGroup to use ValveGroup

Our next step is to make the following changes to TestValveGroup:

  1. Import the declaration from ValveGroup instead of ValveControllerImpl.
  2. Instantiate ValveGroup instead of ValveControllerImpl.

Our modified TestValveGroup is as follows:

import unqualified SimulatorImpl
import unqualified ValveController
import unqualified ValveGroup

@runtime(.MultiThreaded)
component TestValveGroup {
  val client : Provided<ValveController>

  val valve : ValveGroup
  val hal : SimulatorImpl

  init() = {
    connect(client, valve.client);
    connect(valve.hal, hal.client);
  }
}

The following architecture diagram is a graphical representation of our updated TestValveGroup:

TestValveGroup valve : ValveGroup hal : SimulatorImpl client : ValveController client : ValveController client : PValveHAL hal ENC ENC

Verifying your Changes (Example_06A)

Your project should now pass the verification without any errors.