Flex Protocol Examples

This document provides concrete examples demonstrating various features of Flex protocols. Each example focuses on a specific aspect of the protocol specification language.

A Simple Counter Service

A service generally refers to a software program that, for an indefinite amount of time, reacts to incoming messages by updating its internal state and/or responding with messages of its own.

Below, counterProtocol1 is a service that maintains a count state which is an integer. It can handle requests to increment the count, output the count, or quit running altogether.

struct Increment {}
struct GetValue {}
struct Quit {}

component CounterService;
component Client;

local protocol counterProtocol1 in CounterService {
  var count: int32 = 0;

  loop {
    listen
    | recv _: Increment from Client => set count = count + 1;
    | recv _: GetValue from Client => send count to Client;
    | recv _: Quit from Client => break;
    end
  }
}

Adding a Loop Invariant to the Counter Protocol

The counterProtocol1 that we defined earlier has a potential problem: if the value ever reaches the maximum integer value, then one more Increment would cause an overflow and make to value negative! Instead of overflowing, we would like the count to remain at the maximum integer value. Let's fix that by modifying the set statement:

local protocol counterProtocol2 in CounterService {
  var count: int32 = 0;

  loop {
    listen
    | recv _: Increment from Client =>
        set count = if count == 2147483647 then count else count + 1;
    | recv _: GetValue from Client => send count to Client;
    | recv _: Quit from Client => break;
    end
  }
}

Now we can use the model checker to prove that counterProtocol2 will never output a negative value. To do this, let's model a client protocol that sends an unspecified number of Increment and GetValue messages before sending a final Quit message and terminating. We attach assuming value >= 0 to the recv statement to indicate that we always want the received value to be nonnegative. The model checker will attempt to prove that this assumption is never violated.

local protocol clientProtocol in Client {
  loop {
    branch
    | true =>
        send any Increment to CounterService;
    | true =>
        send any GetValue to CounterService;
        recv any value: int32 assuming value >= 0 from CounterService;
    | true =>
        send any Quit to CounterService;
        break;
    end
  }
}

We also need a system containing our two protocols to pass to the model checker:

system counterSystem2 { counterProtocol2; clientProtocol; }

Unfortunately, even though the count will never overflow, the model checker can't prove it quite yet. The reason lies in the way the model checker handles looping. Software involving loops is typically tricky for verification tools to handle because loops can iterate a very large number of times (or sometimes even infinitely many times).

To avoid simulating a potentially infinite number of loop iterations, the model checker attempts to construct an inductive proof of some predicate P that is satisfied by the model. For a given P and a loop block in the model, the inductive proof that the model checker tries to build looks like this:

Base Case: P is true after zero loop iterations.
Inductive Case: If P is true after n iterations, then P is true after n+1 iterations.
Conclusion: P is true after any number of iterations.

The predicate P is called the loop invariant and can be provided by the invariant clause in a loop expression. In our example, using count >= 0 works as our loop invariant. This is coincidentally similar to the assuming value >= 0 clause that we want to verify, however this will not always be the case.

local protocol counterProtocol3 in CounterService {
  var count: int32 = 0;

  loop invariant (count >= 0) {
    listen
    | recv _: Increment from Client =>
        set count = if count == 2147483647 then count else count + 1;
    | recv _: GetValue from Client => send count to Client;
    | recv _: Quit from Client => break;
    end
  }
}

system counterSystem3 { counterProtocol3; clientProtocol; }

Now the model checker is able to prove that counterSystem3 is safe.

Examples of `send`

The most general version of a send statement is the send-let statement:

send let pos: Position
    where pos.x >= 0 && pos.y >= 0
    from Navigation to MissionControl;

The send-let statement above indicates that the Navigation component sends a message named pos to the MissionControl component. The message can be any value of type Position as long as it satisfies the condition pos.x >= 0 && pos.y >= 0. Additionally, the scope of pos extends past the send-let statement to the end of the current block and thus can be referenced by subsequent statements. The where clause can be omitted, in which case it is equivalent to writing where true. The from clause can also be omitted.

branch
| true =>
    // Send `pos`
    send let pos: Position
        where pos.x >= 0 && pos.y >= 0
        from Navigation to MissionControl;

    // Send the same position again
    send pos to MissionControl;

    // Error: `pos` is already in scope
    send let pos: Position
        where pos.x >= 0 && pos.y >= 0
        from Navigation to MissionControl;

| true =>
    // Error: `pos` is not in scope here
    send pos to MissionControl;
end

// Error: `pos` is not in scope here
send pos to MissionControl;

Every send statement can be written as a send-let statement, though for convenience it is not recommended that you do so.

The send-any statement works the same as send-let except the bound identifier pos is only in scope in the where clause. This also means that including the where clause is required in send-any statements, otherwise binding the identifier would be pointless.

branch
| true =>
    // Send `pos`
    send any pos: Position
        where pos.x >= 0 && pos.y >= 0
        from Navigation to MissionControl;

    // Error: `pos` is not in scope here
    send pos to MissionControl;

    // Okay, because the previous `pos` is no longer in scope
    send any pos: Position
        where pos.x >= 0 && pos.y >= 0
        from Navigation to MissionControl;

| true =>
end

Sometimes we want to write a send-any statement without specifying any constraints on the sent message. We could write a send-any with a where true clause, but there is a shorter way to do this:

send any Position to MissionControl;

// equivalent to
send any pos: Position where true to MissionControl;

There is another shortcut when we want to send a message that is precisely equal to the result of evaluating an expression:

send oneMileNorthOf(somePos) to MissionControl;

// equivalent to
send any pos: Position where pos == oneMileNorthOf(somePos) to MissionControl;

Any expression will work, even complicated expressions like if-then-else:

send (if shouldGoNorth
      then oneMileNorthOf(somePos)
      else oneMileSouthOf(somePos))
    to MissionControl;

Examples of `recv`

The forms of recv statements are mostly analogous to the forms of send statements. The most general version of a recv statement is the recv-let statement:

recv let pos: Position
    assuming pos.x >= 0 && pos.y >= 0
    from Navigation to MissionControl;

The recv-let statement above indicates that the MissionControl component receives a message named pos from the Navigation component. The message can be any value of type Position as long as it satisfies the condition pos.x >= 0 && pos.y >= 0. Additionally, the scope of pos extends past the recv-let statement to the end of the current block and thus can be referenced by subsequent statements. The assuming clause can be omitted, in which case it is equivalent to writing assuming true. The to clause can also be omitted.

// Receive `pos`
recv let pos: Position
    assuming pos.x >= 0 && pos.y >= 0
    from Navigation to MissionControl;

// Receive the same position again
recv any pos1: Position assuming pos1 == pos from Navigation;

// Error: `pos` is already in scope
recv let pos: Position
    assuming pos.x >= 0 && pos.y >= 0
    from Navigation to MissionControl;

Most recv statements can be written as a recv-let statement. The only exception is recv-set statements which stores the incoming message in a previously declared var:

var pos: Position = Position{ x = 0; y = 0; }

// Receive a Position message and store it in `pos`.
recv pos from Navigation;

However, it might be nice to deprecate the recv-set statement in the future, so it's use is not encouraged. Its functionality is easily replicated by a recv-let and a set statement:

var pos: Position = Position { x = 0; y = 0; }

// Recommended instead of recv-set
recv let pos1: Position from Navigation;
set pos = pos1;

The recv-any statement works the same as recv-let except the bound identifier pos is only in scope in the assuming clause. This also means that including the assuming clause is required in recv-any statements, otherwise binding the identifier would be pointless.

// Receive `pos`
recv any pos: Position
    assuming pos.x >= 0 && pos.y >= 0
    from Navigation to MissionControl;

// Error: `pos` is not in scope here
recv any pos1: Position assuming pos1 == pos from Navigation;

// Okay, because the previous `pos` is no longer in scope
recv any pos: Position
    assuming pos.x >= 0 && pos.y >= 0
    from Navigation to MissionControl;

Sometimes we want to write a recv-any statement without specifying any constraints on the received message. We could write a recv-any with a assuming true clause, but there is a shorter way to do this:

recv _: Position from Navigation;

// equivalent to
recv any pos: Position assuming true from Navigation;

Synchronized Choice Example

This example focuses on motivating the synchronized choice global protocol construct.

In this interaction, the customer and store engage in some interaction. Then, optionally, the store could send a Confirmation message to the customer. First, let's try to model this behavior with a standard choice block and see what goes wrong:

struct Confirmation {}

component Customer;
component Store;

global protocol syncChoiceExample {
  // Customer tells Store whether it wants the Confirmation message.
  exch let shouldConfirm: bit
      into let shouldConfirm1: bit
      from Customer to Store;

  // perform the transaction ...

  // WRONG!!!
  choice in Store
  | shouldConfirm1 =>
      exch any Confirmation from Store to Customer;
  | !shouldConfirm1 =>
      // do nothing
  end
}

At the end of the protocol, the customer must decide whether to wait for a Confirmation message or to terminate, but it is unclear how the customer is supposed to make this choice. Since the choice of branch happens in the store, the corresponding local syntax for choice in Store would be branch in the store component and listen in the customer component. However, the customer cannot listen for the "absence" of a message.

local protocol syncChoiceExample__Customer in Customer {
  send let shouldConfirm: bit to Store;
  
  // perform transaction ...

  // WRONG!!!
  listen
  | recv any Confirmation from Store =>
  | /* receive no message??? */ =>
      // do nothing
  end
}

We should be able to model this situation because by the end of the protocol, both components have enough information (shouldConfirm in the customer and shouldConfirm1 in the store) to choose the correct branch independently of each other. What we need is a version of the global choice block that corresponds to branch instead of listen in both the customer and store.

Enter the synchronized choice block. A synchronized choice is a choice with two or more "choosers" indicated by a comma-separated list after the choice in keywords:

global protocol syncChoiceExample {
  // Customer tells Store whether it wants the Confirmation message.
  exch let shouldConfirm: bit
      into let shouldConfirm1: bit
      from Customer to Store;

  // perform the transaction ...

  // shouldConfirm1 equals shouldConfirm, so both components know which branch to take.
  choice in Customer, Store
  where sc = in Customer {shouldConfirm}, in Store {shouldConfirm1}
  | sc =>
      exch any Confirmation from Store to Customer;
  | !sc =>
      // do nothing
  end
}

When multiple components independently choose a branch, it is critial that they all choose the same branch. This is facilitated by the where clause in the synchronized choice which asserts that all components are able to compute one or more values that are equal across all components. In this running example, the where clause asserts that shouldConfirm in Customer will always have the same value as shouldConfirm1 in Store. The newly introduced identifier sc refers to either of them depending on perspective.

Synchronized choice is considered unsafe and should be avoided whenever possible. This is because it is difficult in general to prove that all components participating in a synchronized choice will in fact choose the same branch in all cases.

Modeling State Machine Diagrams

State machine diagrams are a popular way of modeling software behavior. Technically speaking, any machine with a state that changes over time is a state machine. However, in systems engineering, a state machine usually refers to a graph-like diagram that depicts a set of disjoint states connected by transitions. Below is such a diagram depicting states of a hypothetical controller component on an aircraft:

Flex is able to express behavior in a way that cleanly maps to and from a state machine diagram. The behavior of each state can be modeled as a local protocol, and a state transition corresponds to the execution of a do tail statement:

component AircraftController;

local protocol initializing in AircraftController {
  // initialization work ...
  do tail standby;
}

local protocol standby in AircraftController {
  // wait for execution or finalize signal ...
  branch
  | true => do tail executing;
  | true => do tail finalizing;
  end
}

local protocol executing in AircraftController {
  // execution work ...
  // wait for standby or finalize signal ...
  branch
  | true => do tail standby;
  | true => do tail finalizing;
  end
}

local protocol finalizing in AircraftController {
  // finalization work ...
}

To run the model checker on a Flex specification that contains do or do tail statements, only the initial state should be included in the system:

system aircraftSystem { initializing; /* protocols for other components */ }

State machine diagrams are good at expressing high-level relationships between states of a protocol. However, they are usually very bad at including lower-level details. In the state machine diagram above, it is unspecified what exactly the aircraft controller should be doing while in each state. Low-level information is often defined separately from the high-level state diagrams with little to no connection defined between them.

Flex does not have this problem because both the high-level information of state transitions and the low-level information of computation are expressed in the same language. A do tail statement is just another protocol statement like send, var, or set. The only difference is that we have chosen to understand do tail as a state transition and the other statements as lower-level computation.

A Simple Counter Service​

Adding a Loop Invariant to the Counter Protocol​

Examples of send​

Examples of recv​

Synchronized Choice Example​

Modeling State Machine Diagrams​