Going Beyond an Incident Report with TLA+

We propose an extension to the traditional incident workflow that incorporates modeling the behaviors involved via a specification language designed for use with concurrent and distributed systems. In many cases, this can lead to greater understanding of the factors that contributed to the incident, as well as providing a mechanism to explore the effectiveness of proposed strategies for preventing similar incidents from occurring in the future.

In Figure 1, we visualize how our contributions add to the existing state of the art. Considering an incident that has already been mitigated, the engineers who responded to the incident will already have collected a large amount of information regarding what happened and what was done. This is the “conventional outcome”, in which case all insight will be described using prose and diagrams. The problem with prose is that it can be hard to interpret after the fact, and it can hide subtle logical and factual inconsistencies. To make things more precise, once the facts are established, engineers should also produce a machine-analyzable model representing the systems involved and the configuration that lead to the incident scenario.

Thinking more broadly, if an incident report contains a machine-analyzable representation of what happened and why, its value increases significantly. Beyond recording the facts and the ideas of those involved, such a report can be used to predict future incidents and analyze potential after-effects of the incident’s mitigation. Many events observed in large-scale production environments may not be reproducible under test. Even using chaos engineering [1], only less-common behaviors can be explored with some probability, as opposed to exploring an exhaustive list of possible events. Tools do exist that help developers reason about unusual behaviors their code might exhibit [2, 4], but they have to stochastically sample a subset of possible implementation-level events rather than produce a comprehensive summary. As a result, a light-weight machine-analyzable representation of all of a system’s allowable behaviors is an important asset when reasoning about production incidents.

Note that while we use TLA+ (modeling language based on the Temporal Logic of Actions) [13] and TLC (model checker) [16], the principles we discuss apply to any reasoning tool with similar capabilities. For example, the Alloy [11], Promela [8], and P [5] modeling languages cover a related design space.

When representing an incident, the goal is not to model everything, or to represent what is modeled completely. Rather, the goal is to identify and represent the set of factors that contributed to the incident happening, such that the resulting model provides a useful abstraction over the problem domain. In this example, we focus on modeling Cosmos DB’s consistency guarantees and the interactions with the system which experienced the incident. It might be possible to broaden the inquiry, like addressing the many other reasons a system might end up in a state where workers are unable to read data for dequeued jobs, but generality is not always better. An over-general model can be harder to understand, and it may be harder to see that the model does not represent reality. This is similar to general-purpose strategies like a reprocessing mechanism that retries on failure. They can make a system more robust, but might also cause outages by unexpectedly interfering with system load [9]. With modeling, we think it is more reliable to start with specific concerns like the one we address here, and build up the insight needed to think about more general issues over time.

For our motivating incident, we chose to represent the situation as we summarized it in Figure 2. We modeled one work dispatcher, one worker, a message queue, and an instance of Cosmos DB. There is no need to model the system end-to-end, since the incident report already indicates which parts of the system would be interesting to model We don’t need to model what the work is, how the expected network communication happens, or any particular details of where the dispatcher gets its instructions. If the worker can gather the necessary metadata, then the issue has not occurred, and further events are not of interest. Similarly, all signs indicate that the message queue was working as designed: work was successfully enqueued at one end and then dequeued at the other. Without further evidence of it doing anything controversial, we chose to model it as simply as we could.

Cosmos DB, on the other hand, was the service whose behavior was directly involved in the problem outputs. That is not to say that it had a bug – it was in fact behaving as designed. This issue is an example of a cross-system interaction [15], and the underlying issue could be categorized similarly to a grey failure [10]. The fact that it was behaving in a way that was not fully explained meant that we needed to model its behavior in more detail, because an over-simplified representation of its expected behavior would simply not exhibit the issue. On the other hand, an overly detailed model would just complicate the incident model without increasing its usefulness.

With sufficient care, small ad-hoc abstractions can be used to summarize the relevant behaviors of target systems, which can be much easier to build than a complete model. That said, the ideal scenario is that the vendors of a given system would already provide a ready-to-use model of its expected behavior. A generic model authored by a system’s developer team could be better trusted to represent real system behaviors, reducing the need for ad-hoc modeling of a given system. Of course, the usefulness and trustworthiness of any model will always be relative; we are talking about a matter of practical utility and reducing manual effort. Optimistically, the growing use of formal methods in practical system development [3, 6, 12, 14] points toward this concept becoming more realistic over time.

By using a generic model of Cosmos DB’s behavior that we had previously built [7], and having sufficiently simplified our representation of all the other necessary components, it took us about 1 person day to recreate the interaction shown in Figure 2.

Listing 1 contains the majority of the model definitions needed to reproduce our motivating incident, with some boilerplate omitted for presentation. It is written using the imperative PlusCal syntax for TLA+, which can be more intuitive to read for those used to popular programming languages. To explore the model yourself, check it out from Github at https://github.com/ tlaplus/azure-cosmos-tla/tree/master/simple-model. All necessary data and configuration are provided; opening the folder with the TLA+ Visual Studio Code plugin (https://github.com/tlaplus/vscode-tlaplus) and selecting the TLA+: Check Model With TLC option is sufficient to view the counter-example we include in this article.

This model has two explicit processes, the dispatcher and the worker, and one implicit one, the Cosmos DB service.

The two explicit processes are defined by process definitions, which each define a process that operates asynchronously to other processes by taking a sequence of atomic steps. Each atomic step is labeled, which shares a syntax with the low-level control flow construct of the same name. For example, dispatcherWriteTaskDataInit: is the first label of the dispatcher process. Sometimes, a step must wait for a condition to be true before being able to run. In that case, the await statement is used to ensure that the current step cannot execute until the relevant condition, such as serviceBus # <<>> (which reads “the service bus is not empty”), is true.

The Cosmos DB service is defined separately as a re-usable module, and its operations are referenced with the prefix CosmosDB!. WriteInit(key, value), WriteInitToken, and WriteCanSucceed(token) operate in combination, starting and completing a write operation to Cosmos DB. The first two operations begin a write and extract its identifier, WriteInitToken. The third is a predicate that is only satisfied if the write has succeeded (if the write fails, it will never be satisfied). SessionConsistencyRead(token, key) yields the set of values that may be read in the current system state given token and key. Depending on possible valid Cosmos DB internal states at any given time, the set may be empty or may contain multiple possible values. UpdateTokenFromRead(token, read) combines an existing session token with a chosen result of a read operation to produce a new, updated session token.

Note that the conspicuously absent service bus has been simplified to the extent that it is not represented as a process at all: its state is summarized by the global variable serviceBus, which is a plain TLA+ sequence. It starts as an empty sequence, which has the syntax <<>>. Sending to and receiving from the service bus is performed inline by the dispatcher and worker.

Overall, the model operates exactly as Figure 2 shows, albeit without any assumption that step (4) will fail. Instead, the worker reads from the database and records the outcome in the local state variables workerToken and workerValue. While these state variables are not functionally necessary, they can be used to examine the model’s behavior: we can write properties describing how their values should change over time, and we can model check whether these properties are universally true.

For our purposes, we want to assert that <>workerValue = "taskValue", or, “eventually workerValue will have the value "taskValue"”. That is, the worker will always read the intended value and not the “404” placeholder. If the property is always true, then the incident we are trying to model cannot happen. Replicating the incident, model-checking shows that the property does not hold for the system as modeled.

Listing 2 summarizes a counter-example scenario, edited for presentation but illustrative of the ASCII output when TLC finds a counter-example. The counter-example is a chronological series of events expressed as assignments to model state variables. Some of the variables are the same as in Listing 1, while others are defined separately. The Cosmos DB internals are summarized by readIndex, commitIndex, epoch, and log, which can completely represent any client-observable state Cosmos DB might reach. The pc variable stands for Program Counter, and is a proxy for control flow within the model. For the dispatcher and worker, it indicates which action each process should attempt next, corresponding directly to the labels Listing 1.

Paraphrased from the tool read-out, the counter-example reads as follows:

dispatcherWriteTaskDataInit Begin writing the key-value pair "taskKey", "taskValue". This adds the data to the database, but does not require any consensus-type actions.

Cosmos DB Some partial consensus action. A majority, but not all, Cosmos DB servers will have the new value. This is indicated by commitIndex advancing to point to index 1 of the log, while readIndex stays at 0.

dispatcherWriteTaskDataCommit The write process is considered complete. The dispatcher sends "taskKey" via the service bus.

workerBeginTask The worker receives "taskKey" via the service bus, and reads that key from Cosmos DB. It stores the value it read in workerValue, which is "NoValue".

The counter-example makes clear a logical problem with how the worker and dispatcher behave. Speaking intuitively, because Cosmos DB is operating in session consistency mode, if they do not share a session token then the clients are opting out of any consistency between reads and writes. It is entirely possible that the worker accesses a Cosmos DB server that has not yet received the value written by the dispatcher, and without a session token that server will just respond with the information it has on hand: "taskKey" does not refer to a value. With an up to date session token, the server would see evidence encoded into the token itself that its state is stale, and it would have to wait before responding.

To further demonstrate that the lack of forwarding session tokens caused the read failures, editing the dispatcher and worker as shown in Listing 3 to send a session token via the service bus changes the model checking outcome. If the two processes share a session token, then the model checker can no longer find any counter-examples to the property <>workerValue = "taskValue".

Looking at this explanation, it also becomes clear why the issue could not be found using conventional testing, nor could it easily be reproduced at the implementation level. The issue was of similar complexity to a grey failure [10], being rare and load-dependent, meaning that any implementation-level reproduction would have to reliably recreate those complex and difficult to control factors. That is why incident reports are usually prose and figures, because without an alternative strategy like modeling, it is simply impractical to do anything else. With the addition of high-level modeling however, creating a demo of this kind of rare issue becomes possible.