What Are Flex Protocols?

Flex protocols are formal descriptions of the behavior of software components that communicate with each other in a distributed system via synchronous message passing.

Protocols come in two flavors: global and local. Global protocols describe sequences of message exchanges between two or more components. Local protocols describe sequences of actions taken by a single component.

	Global Protocol	Local Protocol
# components involved	two or more	one
perspective	third-person	first-person
analogous to	entire sequence diagram	one sequence diagram lifeline

A system composed of a collection of local protocols can be analyzed with a model checker that detects potential deadlock or proves that deadlock between conforming components is impossible (given a perfectly functioning network).

Online Purchase Example Scenario

The details of Flex protocols are discussed in the Flex Protocols reference, but first we model an example interaction using Flex protocols to gain some high-level understanding. Our example involves customer, store, and warehouse components. During this interaction, the customer tries to purchase something by sending an Order to the store. The store checks with the warehouse to see if the item is in stock, and the warehouse responds appropriately. The store then concludes the interaction by sending a Confirmation or Denial back to the customer.

We capture the complete interaction by writing a Flex global protocol, provided below:

module examples.onlinePurchase

struct Order {}
struct InStockRequest {}
struct InStockResponse { isInStock: bit; }
struct Confirmation {}
struct Denial {}

component Customer;
component Store;
component Warehouse;

global protocol OnlinePurchaseProtocol {
  exch any Order from Customer to Store;
  exch any InStockRequest from Store to Warehouse;
  exch any InStockResponse into let r: InStockResponse from Warehouse to Store;
  choice in Store
  | r.isInStock =>
      exch any Confirmation from Store to Customer;
  | !r.isInStock =>
      exch any Denial from Store to Customer;
  end
}

For testing, implementation, or integration tasks, it is often more helpful to have the local protocols which focus on the behavior of each component individually. Since we have a global protocol, we can automatically generate the local protocols via an operation called projection. We can also write local protocols manually.

Here are the local protocols that describe the three components:

local protocol OnlinePurchaseProtocol__Customer in Customer {
  send any Order to Store;
  listen
  | recv _: Confirmation from Store =>
  | recv _: Denial from Store =>
  end
}

local protocol OnlinePurchaseProtocol__Store in Store {
  recv _: Order from Customer;
  send any InStockRequest to Warehouse;
  recv let r: InStockResponse from Warehouse;
  branch
  | r.isInStock =>
      send any Confirmation to Customer;
  | !r.isInStock =>
      send any Denial to Customer;
  end
}

local protocol OnlinePurchaseProtocol__Warehouse in Warehouse {
  recv _: InStockRequest from Store;
  send any InStockResponse to Store;
}

We can use the model checker to prove that a system composed of these three local protocols cannot deadlock by defining a system:

system OnlinePurchaseProtocolSystem {
  OnlinePurchaseProtocol__Customer;
  OnlinePurchaseProtocol__Store;
  OnlinePurchaseProtocol__Warehouse;
}

For the full syntax of every protocol statement form, see the Flex Protocols reference.