Protocol Send/Recv Examples

This page catalogues the forms of send and recv statements and the synchronized choice construct. For the full protocol statement reference, see Flex Protocols Reference.

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 its 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.