Checking protocol conformance with OpenTelemetry and Multiparty Session Types

In this short article, we pilot our ongoing work of monitoring protocol conformance of a distributed system with OpenTelemetry and multiparty session types. Suggestions and feedback are very welcome, and will help us develop this research project further!

Background

What are Multiparty Session Types?

Multiparty session types (MPST for short) are a formal typing discipline for message passing processes. The typing discipline was originally proposed in a paper by Honda et al. (You can find a gentle introduction in this paper) Using a global type (protocol), we describe the communicating behaviour among all processes in a session (an execution run of the protocol). Processes have their respective local types, which describe their own communication behaviour with other processes in the protocol. Such local types can be obtained directly via projection from the global type. These local types can be used to type-check, implement or monitor the message passing processes, with static guarantees of freedom from communication type mismatches or deadlocks, in a correct-by-construction fashion.

What is OpenTelemetry?

OpenTelemetry is a framework for observability, designed for cloud software. The framework provides APIs and SDKs for telemetry data, including logs, metrics and traces, in a large variety of programming languages. Developers can use the API to instrument the web services to collect telemetry, the telemetry can be processed via the SDK provided. You can learn more via its official website at https://opentelemetry.io/.

A Simple Scenario

The objective of this project is to monitor whether a distributed system conforms to a prescribed protocol. We use multiparty session types (MPST) to describe a simple “Two Buyer” Protocol, and use OpenTelemetry APIs to collect traces from a Go implementation of the protocol. We show a simple MPST conformance monitor, as an OpenTelemetry processor, validating whether the implementation conforms to the protocol.

The “Two Buyer” Protocol

A canonical example of MPST is the “Two Buyer” Protocol. The protocol describes the interactions between two buyers (A, B) and a bookseller (S). The two buyers wish to buy a book together and divide the costs.

The progression of the protocol is as follows: Buyer A will ask the seller S for the price for a book of their interest, after which the seller S will provide a quote to both buyers. Buyer B will then propose to divide the cost with A. After receiving the proposal from B, A will inform the seller S whether they will buy the book.

Using Scribble to Describe the Protocol

The protocol can be easily described by the Scribble language, a language designed for modelling multiparty interactions:

global protocol TwoBuyer(role A, role B, role S) {
  query from A to S;  // Buyer A queries price of a book
  quote from S to A;  // Seller sends the quote to buyer A
  quote from S to B;  // Seller sends the quote to buyer B
  share from B to A;  // Buyer B proposes their share of the cost
  buy from A to S;    // Buyer A tells whether they will buy the book
}

In Scribble, the protocol is described as a series of labelled messages. Additionally, Scribble supports branching protocols (where a participant makes a choice) and recursive protocols, which are not demonstrated in this simple example.

Implementing the Protocol in Go

We implement the “Two Buyer” Protocol using a goroutine for each participant, and use Go channels to model the communication channels between pairs of participants. By doing this, we are using the processes to simulate a simplistic example of a distributed system. In particular, we use tracer APIs from OpenTelemetry to trace the communication actions, namely the sends and the receives of each participant process.

The following snippet shows how to use the tracing API to keep track of the messages from A to B. We use similar functions for receiving actions, and for interacting with the seller S.

Sending a message from process A to process B

Then, we can use those communication APIs to implement the endpoint process for buyer A.

Endpoint Process for Buyer A

We continue to implement the other endpoint processes in a similar way. As a result, when we run the processes in parallel, we get an output similar to this:

Two Buyer Protocol:
A: Sending query 86
S: Sending quote 172
B: Proposing share 90
Succeed!

Checking Conformance

Remember we used the OpenTelemetry tracing APIs to trace the communication between the participants. The trace information can then be analysed to check whether the execution conformed to a prescribed protocol.

We implemented an easy prototype MPST conformance checking processor using the OpenTelemetry SDKs. The processor analyses the traces from a protocol execution, and checks whether such a trace is permitted by the prescribed global type.

To begin with, we check whether each message sent has been received. For instance, if buyer A wants to buy the book anyway, ignoring the message from the other buyer, then the message from B is not received. Such an issue may cause an orphaned message, and will be detected by our monitor:

message labelled share sent from B is not received by A

After checking the reception of each message that are sent, we reconstruct the causal ordering of communication actions, and match the trace against a prescribed global type. Global types, according to their semantics (explained in this paper in detail), can be reduced by permitted communication actions. We use the causal ordering of the events to reduce the global type, and validate whether the terminal type (meaning no more communication occurs) is reached.

To explain with an example, if we also omit the message from B to A, there will be no orphaned messages, but the implementation does not strictly stick to the original protocol. Our monitor will report an error in such cases as well:

cannot consume message A_send_S:buy in the global type 
B --> A: {
  share: B -~> A share: A --> S: {
    buy: A -~> S buy: end
  }
}

The error message indicates that the current progression of the protocol requires a message to be sent from B to A with label “share”, therefore a message from A to S with label “buy” is not permitted in the current moment.

The monitor validates labels attached to messages follow the protocol. For instance, changing the label “buy” to “buy?” would lead to the following errors:

[
message label mismatch, sent from A to S, label buy? is sent, but buy is received; 
message labelled buy received by S without matching send, allegedly from A
]

Conclusion and Future Work

We demonstrate how to use multiparty session types and OpenTelemetry to validate protocol conformance. In the current prototype, we analyse the trace after a complete execution in a batch fashion, and we would like to adopt an on-the-fly approach of dynamic monitoring, as opposed to post-validating. In addition, we are developing a new semantic model for multiparty session types, to allow more protocols to be specified and monitored by our work, beyond the original MPST theory.

We look forward to hearing potential use cases and application scenarios, please contact us if you feel interested.

The code used in this post can be found at https://github.com/fangyi-zhou/mpst-tracing.