I started playing around with TLA+ and its more programmer friendly variant PlusCal about a year ago. At that time the amount of documentation that was understandable to people like me who do not enjoy reading white papers full of mathematical notation was slim to none. (Today you can buy Hillel Wayne’s excellent book Practical TLA+) So I started reading other people’s code (errr…specs) and began piecing together some idea of how things were done.

TLA+ is a tool to model and verify concurrent systems, finding bugs in them before you have written any code by testing every possible combination of inputs. You might say “well how is that different from fuzzing inputs in more conventional functional tests?” and the answer is because TLA+ also simulates the kind of timing issues commonplace with distributive or concurrent systems. As microservices continue to dominate conversations about modern architecture, the question of what happens when a service sends a request that never arrives or arrives before something else has finished or gets repeated become more and more relevant. TLA+ allows you to test for these scenarios.

Beyond that it’s a radically different way of thinking about computer programs. It’s not a programming language so one has to abandon certain mental crutches and really think about how we represent what we mean. You can write an excellent model and then write code that doesn’t actually do things the way the model is describing. So you have to think about how your favorite frameworks and libraries actually do what they do.

I’m a huge fan of anything that might bring unvocalized assumptions up to the surface where people can explore them. It’s hugely difficult to build a complex system of services if two teams are not in sync about their assumptions.

The best way to think of TLA+ is like drawing a blueprint for software you’re going to build. I’ve seen people use it to test algorithms, but I’ve also seen people use it to model user flows throughout an application.

However the Toolbox is Awful

When you’re ready to test your models in TLA+ virtually every resource will direct you to the TLA+ Toolbox. The toolbox is a java application that looks a bit like it’s supposed to be an IDE and allows you to translate PlusCal into TLA+, configure models, test them and explore errors. Its UX is awful, simply awful. How you open a TLA file in the toolbox is not intuitive, things will often fail without any errors (or rather the toolbox will do what you’ve told it to do, which is nothing because you needed to click some buttons you didn’t click first). It’s literally exhibit A for why software developers should respect the skills of designers on their teams.

On top of that I find it a little clunky. I generally don’t work with full scale IDEs if I can avoid it. I prefer the stripped down elegance of TextMate, Sublime or Atom. Sometimes this means I miss out on valuable features, but I’m a person who currently has over thirty tabs open in Chrome, three projects open in TextMate and at least one WiP up in Scrivener…. I like to use my computer’s memory, okay? This is a light day.

At some point while I was noising around other people’s TLA+ specs to try to understand the language I realized that there seemed to be command line versions of the key tools from the toolbox. Rather than open up the toolkit I could compile PlusCal and test my models from my terminal and even more exciting … from other scripts.

Wait… there’s a command line version?

Yup! If you’ve downloaded the TLA+ toolbox, you already have the command line tools installed on your computer. To configure them there’s a helpful set of shell scripts you can download here.

One of the first things I did with this knowledge was build a little proof of concept python application that parsed other python programs and tried to write models in PlusCal based on what they were going to do. I wanted to learn more about bytecode and AST and this seemed like a fun way to do it. It was partially successful in that I could write a few simple programs that became working models, but eventually I hit a wall trying to learn two new things at the same time.

But the potential of command line interfaces is still the same. If model checking can be executed via command line, then it can be executed by other programs. You can update your models and test them automatically the same way you might do with other forms of testing in continuous integration.

pcal: Translating PlusCal to TLA+

Once you have installed and configured the command line toolbox, you can start translating PlusCal comments in your specs to TLA+ using the pcal command.

Note that pcal will assume the extension .tla so you can leave it off if you want. For the sake of clarity I will include it.

The basic command is:

pcal myspec.tla

Unlike command line tools you might be used to pcal is very particular about order of arguments. The name of the file you want to translate should always be last, any flags should come before it.

-version does something that might be unexpected. Rather than telling you the version of pcal you have installed, it lets you pick which version of PlusCal the translator will assume it’s translating (this currently goes up to 1.8)

If you want to see the AST for your PlusCal you can use the -writeAST flag to forego the rest of the translation just to output the AST.

This is super useful tool but not without its bugs. For example, I understand that-spec and -spec2 are supposed to let you choose between version 1 and 2 of TLA+, but I’ve never been able to get them to work.

Defining Models with Configuration files

If you’re used to the Toolbox interface, you’re probably wondering how you can configure your invariants and other test cases. The answer is the .cfg file automatically generated for you by the pcal command.

Normally it will look like this:

SPECIFICATION Spec
\* Add statements after this line.

But there are a variety of parameters you can set before checking your models. The most useful of these areINVARIANT and PROPERTY which specify which invariants and which temporal properties to test respectively.

Here’s a full list of all the possible configuration settings

INVARIANT
INVARIANTS
PROPERTY
PROPERTIES
CONSTANT
CONSTANTS
CONSTRAINT
CONSTRAINTS
ACTION_CONSTRAINT
ACTION_CONSTRAINTS
INIT
NEXT
VIEW
SYMMETRY
TYPE
TYPE_CONSTRAINT

I have not been able to figure out what the difference between the singular form of the parameter (eg CONSTANT) and the plural form of the parameter (eg CONSTANTS) is. Both can take multiple values if separated by a space. It might be that there’s some backwards compatibility issue involved here but…. ¯\_(ツ)_/¯

Make sure you add your custom configuration below the line. If you put them above that comment line, pcal will overwrite them every time you translate.

tlc: Checking the Models

Now it’s time to run the model checker! Like pcal the .tla extension is optional. The basic command looks like this:

tlc myspec.tla

And this will produce the following output:

TLC2 Version 2.10 of 28 September 2017
Running breadth-first search Model-Checking with 1 worker on 4 cores with 910MB heap and 64MB offheap memory (Mac OS X x.x.x x86_64, Oracle Corporation x.x.x_x x86_64).
Parsing file myspec.tla
Parsing file /var/folders/sx/tb9t1_890xd0hs9y0xb1k5fr0000gn/T/Integers.tla
Parsing file /var/folders/sx/tb9t1_890xd0hs9y0xb1k5fr0000gn/T/Naturals.tla
Semantic processing of module Naturals
Semantic processing of module Integers
Semantic processing of module myspec
Starting... (2019-01-17 23:06:59)
Implied-temporal checking--satisfiability problem has 1 branches.
Computing initial states...
Finished computing initial states: 25 distinct states generated.
Progress(5) at 2019-01-17 23:07:00: 332 states generated, 222 distinct states found, 0 states left on queue.
Checking temporal properties for the complete state space with 222 total distinct states at (2019-01-17 23:07:00)

This tells you what modules were imported and how many states the model has. If you’re curious the actual spec we’re running here is the wire transfer example in Hillel Wayne’s book. That particular spec has a temporal property that we know will be violated by the algorithm. This is what that looks like:

Error: Temporal properties were violated.

Error: The following behavior constitutes a counter-example:

State 1: <Initial predicate>
/\ people = {"alice", "bob"}
/\ sender = <<"alice", "alice">>
/\ receiver = <<"bob", "bob">>
/\ acc = [alice |-> 5, bob |-> 5]
/\ amount = <<1, 1>>
/\ pc = <<"CheckAndWithdraw", "CheckAndWithdraw">>

State 2: <Action line 55, col 27 to line 61, col 77 of module wire>
/\ people = {"alice", "bob"}
/\ sender = <<"alice", "alice">>
/\ receiver = <<"bob", "bob">>
/\ acc = [alice |-> 4, bob |-> 5]
/\ amount = <<1, 1>>
/\ pc = <<"CheckAndWithdraw", "Deposit">>

State 3: <Action line 55, col 27 to line 61, col 77 of module wire>
/\ people = {"alice", "bob"}
/\ sender = <<"alice", "alice">>
/\ receiver = <<"bob", "bob">>
/\ acc = [alice |-> 3, bob |-> 5]
/\ amount = <<1, 1>>
/\ pc = <<"Deposit", "Deposit">>

State 4: <Action line 63, col 18 to line 66, col 68 of module wire>
/\ people = {"alice", "bob"}
/\ sender = <<"alice", "alice">>
/\ receiver = <<"bob", "bob">>
/\ acc = [alice |-> 3, bob |-> 6]
/\ amount = <<1, 1>>
/\ pc = <<"Done", "Deposit">>

State 5: Stuttering
Finished checking temporal properties in 00s at 2019-01-17 23:07:00
332 states generated, 222 distinct states found, 0 states left on queue.
Finished in 01s at (2019-01-17 23:07:00)

If you are already familiar with the Toolbox, this looks pretty much like the output you’d see before, expect without the highlighting.

By default tlc stops at the first invariant error. If you’d like it to continue, you use the flag -continue. In general tlc's options are split into two types: MODE-SWITCHES and GENERAL-SWITCHES. Mode switches change how the models are run, from switching from breadth-first to depth-first, to picking a seed number for randomization. General switches allow you to specify different configuration files, how much detail is printed to stdout.

I hope this is enough to get you started. I will update this post from time to time as I figure out more about how the tools work. Happy Model Checking!

Introduction to TLA+ Model Checking in the Command Line was originally published in Software Safety on Medium, where people are continuing the conversation by highlighting and responding to this story.

TLA+is traditionally used to model the algorithms that power distributed systems. However, most engineering teams do not build their own message queues, they install and configure multiple solutions developed by other people. The biggest threat to these teams is how all those solutions interact together at scale.

Typically, engineering teams search for those threats by doing live failure tests. Either running extensive performance tests on a special testing environment, or actually sabotaging their own infrastructure to trigger a response ala Chaos Monkey. These are great practices, but somewhat resource intensive. And because they are resource intensive, organizations tend to put them off.

Modeling and its Discontents

There’s a popular saying a statistics: All models are wrong, but some are useful.

I’ve been played around with TLA+ for a while and was curious if it could be used to model the interactions between systems well enough to catch the kinds of complex failures that happen when distributed systems are chained together. I wasn’t sure it was possible to reach a“math proof” level of accuracy between the model and the real life system it was built to reflect but I was eager to try.

That being said, the purpose of this type of modeling is not to build perfect systems, but to help your team define and clarify assumptions. This kind of modeling forces the team to ask themselves exactly how the various products and services they are using interact and it can help find places where we actually don’t know what the expected behavior is, which is useful in minimizing complex failure but will not totally eliminate it.

The hard thing about modeling is figuring out when to simplify and when to specify. The whole point is to uncover details that in retrospect seem obvious but were otherwise not top of mind. But if one tries to capture every detail in the model it will likely be too complex to run.

Example One: The Naive Cluster

Let’s start off with a basic situation. We have three VMs. Each of them has a finite amount of resources, we can think of this as memory, CPU, or I/O but to be frank we don’t need that level of specificity. The important thing is that once the resources are exhausted on any single VM it is no longer healthy.

We start off with something like this:

------------------- MODULE provisioning_naive -------------------
EXTENDS TLC, Integers, Sequences

VMs == {"Server1","Server2","Server3"}

(*--algorithm provisioning
variables
 Cluster = [v \in VMs |-> 4],

define
 ServersHealthy == \A vm \in VMs: Cluster[vm] <= 9
end define;

end algorithm *)
==================================================================

In this model we’re going to use 0–10 to represent resource use percentage. We could use 0–100, but that would increase the amount of states TLA+ has to check rather dramatically without really providing any additional value. The way TLA+ works is that it runs all possible sets of input looking for places where requirements that you have defined (assertions, invariants, temporal properties) are violated. It is unlikely that for this model an input of 57% will produce an error that an input of 55% didn’t already catch, so we take the opportunity to simplify and use 0–10.

We then define an invariant called ServersHealthy in which we tell TLA+ that every server in our cluster should be below 90% resource use. We initialize our servers at 40% resource use to start. Why 40%? Here’s a great example of how model checking can lead to interesting conversations about what we really know with any given architecture. We know that when we spin up a new server it is using some memory and some CPU… that number is not 0%, but it’s also not 100%. What number in between is the most accurate? How would we figure that out? Should we be tracking this over time?

Anyway, let’s say we did all that and we decide on an initial state of 40% utilization. This is where we need to learn how to think about a system of systems as an algorithm instead of an environment. Although in the middle of an outage or complex failure it might seem like things are happening at random, in reality each system has a defined set of rules that govern its behavior and choices, and each system it hands off to has a defined set of rules that govern its behavior and choices. Just because the exact set of inputs is unexpected does not make the behavior random.

We want this first model to be naive so we’re going to define an incident as a series of events that change the amount of resources being used by one of our VMs. You can think of these as processes eating up CPU or requests using memory, whatever.

Events == [target: VMs, size: 0..4]

This defines an event as having a target (one of our possible three VMs already defined) and a size (a range from not increasing resource use to increasing it by 4). We’ll also define an incident as being a set of four events. Don’t worry you’ll get to see this altogether in one file at the end.

Incidents(set) == set \X set \X set \X set

...

incident \in Incidents(Events)

Why four? It’s pretty much an arbitrary number at this point. We want to see how multiple incoming processes/requests affect our VMs so we need more than one, but the more events we have in an incident the more combinations TLA+ has to consider, the longer the full model takes to run. So we settle on four as the sweet spot where we have enough events to see problematic behavior but not so much that we need to grab a coffee and come back to check the model’s results.

Now the meat and potatoes of our algorithm. As an event occurs it increases the resource use of one of our VMs.

macro trigger_event(event) begin
 Cluster[event.target] := Cluster[event.target] + event.size
end macro;

begin
 while incident /= <<>> do
  curr := Head(incident);
  incident := Tail(incident);
  trigger_event(curr)
 end while;

end algorithm *)

I’m doing this as a macro trigger_event because we’ll want to add more complexity to it soon and breaking it out will keep things clean. Here’s what the full code looks like:

------------------ MODULE provisioning_naive --------------------
EXTENDS TLC, Integers, Sequences

VMs == {"Server1","Server2","Server3"}
Incidents(set) == set \X set \X set \X set
Events == [target: VMs, size: 0..4]

(*--algorithm provisioning
variables
 incident \in Incidents(Events),
 Cluster = [v \in VMs |-> 4],
 curr = ""; \* helper: current event

define
 ServersHealthy == \A vm \in VMs: Cluster[vm] <= 9
end define;

macro trigger_event(event) begin
 Cluster[event.target] := Cluster[event.target] + event.size
end macro;

begin
 while incident /= <<>> do
  curr := Head(incident);
  incident := Tail(incident);
  trigger_event(curr)
 end while;

end algorithm *)

===================================================================

Running this produces a sensible and predictably uninspiring result:

Finished computing initial states: 531441 distinct states generated.
Error: Invariant ServersHealthy is violated.
Error: The behavior up to this point is:
/\ incident = << [target |-> "Server1", size |-> 2],
   [target |-> "Server1", size |-> 4],
   [target |-> "Server1", size |-> 4],
   [target |-> "Server1", size |-> 4] >>
/\ curr = ""
/\ pc = "Lbl_1"
/\ Cluster = [Server1 |-> 4, Server2 |-> 4, Server3 |-> 4]

State 2: <Action line 67, col 10 to line 74, col 62 of module provisioning_naive>
/\ incident = << [target |-> "Server1", size |-> 4],
   [target |-> "Server1", size |-> 4],
   [target |-> "Server1", size |-> 4] >>
/\ curr = [target |-> "Server1", size |-> 2]
/\ pc = "Lbl_1"
/\ Cluster = [Server1 |-> 6, Server2 |-> 4, Server3 |-> 4]

State 3: <Action line 67, col 10 to line 74, col 62 of module provisioning_naive>
/\ incident = <<[target |-> "Server1", size |-> 4], [target |-> "Server1", size |-> 4]>>
/\ curr = [target |-> "Server1", size |-> 4]
/\ pc = "Lbl_1"
/\ Cluster = [Server1 |-> 10, Server2 |-> 4, Server3 |-> 4]

TLA+ let’s us know that if we have three VMs at 40% of resource use, a process that increases resource use by 20% followed by another increase in resource of 40% on the same server will result in that VM being unhealthy… which is not something you would need to build a model to figure out but is helpful at demonstrating the concept of using TLA+ to model systems integration.

The core problem with this model is that it doesn’t capture a few essential components of behavior. We have a magical load balancer that apparently has no logic defining which VMs get which traffic, and processes consuming resources indefinitely.

Let’s change some of that.

Example 2: Load Balancing

To add a load balancer to the mix we’re first going to change our VM names to integers. There was no particular reason to have their identifiers be strings, except that it made the code a bit easier to read, but by changing them to integers modeling a round robin load balancer becomes just a matter of counting to three over again.

We don’t need our events directed to a specific VM anymore so we’ll just get rid of that. Then we add some basic conditional logic to trigger_event so that the model directs the next event to the next VM in our round robin rotation. Altogether we have:

------------------- MODULE provisioning_load ---------------------
EXTENDS TLC, Integers, Sequences

VMs == {1,2,3}
Incidents(set) == set \X set \X set \X set
Events == [size: 1..4]

(*--algorithm provisioning
variables
 incident \in Incidents(Events),
 Cluster = [v \in VMs |-> 4],
 curr = "", \* helper: current event
 rrobin = 1;

define
 ServersHealthy == \A vm \in VMs: Cluster[vm] <= 9
end define;

macro trigger_event(event) begin
 Cluster[rrobin] := Cluster[rrobin] + event.size;
 if rrobin = 3 then
    rrobin := 1
 else
    rrobin := rrobin + 1
 end if;
end macro;

begin
 while incident /= <<>> do
  curr := Head(incident);
  incident := Tail(incident);
  trigger_event(curr)
 end while;

end algorithm *)

==================================================================

You probably don’t need to run the model to guess what’s going to happen. The fourth event will go back to the first VM and knock it over our limit. To improve our model we need to program in recovering resources when processes end.

There are a couple of different ways we could approach that. We could give each event a timeout after which its load on the VM is cleared away, but that creates an unhelpful amount of complexity in the model. We’re only doing four events per incident, it’s not likely that timeouts would make enough of an impact to give us any insight we didn’t have before.

Another way of approaching it is to think of the reclaiming of resources as garbage collection. One event is not one process or request raising the resource use by a single VM, it is just a state change that could have been triggered by any number of things. Maybe Event X increases VM 2 resource use by 20% and Event X is actually a number of processes that happened in an undefined period of time. Then we assume at various points that some of those processes have ended naturally, some have timed out, but that those resources are still “used” because the machine hasn’t released them yet.

To represent that we have to rework our algorithm into processes because processes are how TLA+ represents concurrency and garbage collection should happen independently of any events happening to the server. Because we’re breaking this up into processes, we’re also going to move the variable initializations around a little bit. Some variables are only relevant to certain processes, it makes sense to keep them local. Any macros we call within the process will be able to access them.

-------------------- MODULE provisioning_load ---------------------
EXTENDS TLC, Integers, Sequences

VMs == {1,2,3}
Incidents(set) == set \X set \X set \X set
Events == [size: 1..4]

(*--algorithm provisioning
variables
 Cluster = [v \in VMs |-> 4],

define
 ServersHealthy == \A vm \in VMs: Cluster[vm] <= 9
end define;

macro trigger_event(event) begin
 Cluster[rrobin] := Cluster[rrobin] + event.size;
 if rrobin = 3 then
  rrobin := 1;
 else
  rrobin := rrobin + 1
 end if;
end macro;

process garbage_collection = "recover resources"
 variables
  Gcollection \in [1..3 -> 1..4],

begin Collect:
  with i \in VMs do
   if Gcollection[i] >= Cluster[i] then
    Cluster[i] := 0;
   else
    Cluster[i] := Cluster[i] - Gcollection[i];
   end if;
  end with;
end process;

process incoming = "increasing resource usage"
 variables
  incident \in Incidents(Events),
  curr = "", \* helper: current event
  rrobin = 1;

begin Increase:
  while incident /= <<>> do
   curr := Head(incident);
   incident := Tail(incident);
   trigger_event(curr);
  end while;
end process;
end algorithm; *)

====================================================================

What’s important to keep in mind when designing TLA+ models is that the model checker will test all possible combinations of inputs. Not the most likely. So this code will include all the likely scenarios where some VMs free up a lot of resources and some free up only a few, but also scenarios where no one frees up anything.

Which obviously will put us back where we started, despite that scenario being unlikely.

Going back to the all models are wrong, but some are useful maxim. Is this a useful level of insight? Not any more than having no garbage collection at all was. It is tempting to force the model to always do garbage collection just to get the model to pass, which is also not useful.

What we could do instead is reconsider ifServersHealthy should be an invariant the way it is. When we define an invariant, TLA+ will error if that statement is false for any reason, at the end of every step. ServersHealthy defines our model as being in a failure state whenever any of our three VMs are unhealthy, but in reality VMs do occasionally become unhealthy and go offline and it does not generally end Western civilization as we know it.

If we change the \A (All VMs are good) in our invariant to \E (at least one good VM Exists) the model runs without any failure states:

ServersHealthy == \E vm \in VMs: Cluster[vm] <= 9

But that’s not enough… We can do better. We can add even more complexity.

Example 3: Autoscaling

There are lots of things about our models that are still lacking. Obviously if we were to move beyond four events our outcomes would look very different. And we’re missing a big piece of modern cloud architecture: autoscaling. So let’s rethink the model a bit.

We’re currently representing the VMs in a struct which in TLA is kind of like a hash map. This made assigning resource increases to various VMs super easy but it isn’t the best option when we want to add and remove VMs from the pool. Instead we’re going to store this information in a sequence, basically a list of numbers wherein each number represents the resource use of the VM.

(*--algorithm provisioning
variables
VMs \in [1..2 -> 0..10]

[1..2->0..10] creates a set of sequences that represents all possible combinations of two VMs with a potential resource use from 0% to 100%. Creating a series of traffic patterns as in previous models was a bit easier to conceptualize, but not very efficient. There’s also a question of whether the right combination of state changes will bring both VMs to a place that is unsustainable. In our previous model we survived 4 cycles, but probably would not survive 8. By creating a set of every possible combination we no longer need cycles at all.

But this change requires us to remove our invariant and replace with something else:

define
 ServersHealthy == <>(\E v \in 1..Len(VMs): VMs[v] <= 9)
end define;

This is a temporal property it’s defined and configured in much the same way as an invariant but it lets us use <> which in TLA+ means “eventually true”. If we were to keep the invariant then the model would fail as soon as TLA+ gave it the sequence<<10,10>>

This model doesn’t really load balance… honestly I went back and forth on this. Ultimately when a new VM is added to the pool, what we should expect to see is resource use even out as traffic is distributed across a larger group of machines. But if we aren’t doing cycles anymore I’m not sure that reflecting this behavior in the model is useful. So instead we have three processes: one that kills an unhealthy VM, one that adds a VM to the pool when resource use is high, and one that shuts down VMs when resource use is low.

fair process VM_dies = "kill a VM"
 begin Fail:
  await Len(VMs) > 1;
  VMs := SelectSeq(VMs, LAMBDA x: x < 8);
end process;

fair process scale_up = "autoscale up"
 variable
  load = FALSE;

begin Scale_up:
  load := \E v \in 1..Len(VMs): VMs[v] > 6;
  if load then
   VMs := Append(VMs, 4);
  end if;
end process;

fair process scale_down = "autoscale down"
variables
 load = FALSE

begin Scale_Down:
 await Len(VMs) > 1;
 load := \A v \in 1..Len(VMs): VMs[v] < 4;
 if load then
  VMs := Tail(VMs);
 end if;
end process;

There are a few unfamiliar things here. First await tells TLA+ not to run the process until the statement that follows it is true. VM_dies and scale_down will not run if the current pool has less than two VMs in it. This keeps all our servers from being turned off at once.

Oh except…. our model has found a case where that’s not true:

Error: Deadlock reached.
Error: The behavior up to this point is:
State 1: <Initial predicate>
/\ load_ = FALSE
/\ pc = ( "kill a VM" :> "Fail" @@
  "autoscale up" :> "Scale_up" @@
  "autoscale down" :> "Scale_Down" @@
  "modify load on VMs" :> "modify_load" )
/\ VMs = <<8, 8>>
/\ load = FALSE

State 2: <Action line 83, col 9 to line 87, col 38 of module provisioning_autoscale>
/\ load_ = FALSE
/\ pc = ( "kill a VM" :> "Done" @@
  "autoscale up" :> "Scale_up" @@
  "autoscale down" :> "Scale_Down" @@
  "modify load on VMs" :> "modify_load" )
/\ VMs = <<>>
/\ load = FALSE

State 3: <Action line 91, col 13 to line 98, col 27 of module provisioning_autoscale>
/\ load_ = FALSE
/\ pc = ( "kill a VM" :> "Done" @@
  "autoscale up" :> "Done" @@
  "autoscale down" :> "Scale_Down" @@
  "modify load on VMs" :> "modify_load" )
/\ VMs = <<>>
/\ load = FALSE

If both our VMs are at 80% usage and the kill process runs before the scale up process, they will both be killed. VMs := SelectSeq(VMs, LAMBDA x: x < 8); selects a new sequence from the original VMs, picking only the elements where the lambda returns true, in this case only VMs with less than 80% usage … in effect removing unhealthy machines from the pool.

And the pool doesn’t replace them because \E v \in 1..Len(VMs): VMs[v] > 6; returns false when applied to an empty sequence. So let’s change that by adding and Len(VMs) < 2 \/ to the beginning which will make it true if we have less than 2 VMs in our pool.

But even though we can control for this behavior by tweaking the model. This is not a fault in our model exactly. Actually it raises a really important question: what does our autoscaling service do when all the servers are unhealthy and it cannot spin up new ones? This actually happened to Buildkite a few years ago when some misconfigured settings triggered failure notices on otherwise healthy servers. In fact it’s exactly the sort of issue that tends to trigger cascading failures.

Right now we’re just going to update the model to prevent this, but if I were modeling a real system what I might want to do instead is build another model that looked at the process of spinning up new servers in detail. This is an important design practice for TLA+, because we are considering every possible state we don’t want to be adding more and more complexity to the same model. Instead we want to build more models. Using broad but simple business process models to find the edge cases, then building models that look at how we do those specific components in detail and testing for those edge cases.

Altogether here’s our finished model:

----------------- MODULE provisioning_autoscale -------------------
EXTENDS TLC, Integers, Sequences

(*--algorithm provisioning
variables
VMs \in [1..2 -> 0..10]

define
 ServersHealthy == <>(\E v \in 1..Len(VMs): VMs[v] <= 9)
end define;

fair process VM_dies = "kill a VM"
 begin Fail:
  await Len(VMs) > 1;
  VMs := SelectSeq(VMs, LAMBDA x: x < 8);
end process;

fair process scale_up = "autoscale up"
 variable
  load = FALSE;

begin Scale_up:
  load := Len(VMs) < 2 \/ \E v \in 1..Len(VMs): VMs[v] > 6;
  if load then
   VMs := Append(VMs, 4);
  end if;
end process;

fair process scale_down = "autoscale down"
variables
 load = FALSE

begin Scale_Down:
 await Len(VMs) > 1;
 load := \A v \in 1..Len(VMs): VMs[v] < 4;
 if load then
  VMs := Tail(VMs);
 end if;
end process;

end algorithm; *)

==================================================================

The fair keyword tells TLA+ that it is not necessary for those processes to run in order for the model to complete. We might never need to kill a server, for example, so TLA+ shouldn’t wait for us to have to.

Using Modeling as Part of the Development Process

All this seems like a lot of work, where does it connect to a normal development process? I see the benefit of modeling being primarily about communication of assumptions and gathering insight into the seams that join complex infrastructure. Good models can help you decide things like:

1. Technology selection. Too often we choose tools based on what we’re already familiar with or what is trendy and cool. Modeling can help you determine what behaviors you’re looking for from the components of your architecture
2. Monitoring and alerting strategy. Knowing how systems are likely to fail can help you figure out what to monitor without having to wait for failure to happen.
3. SLOs. Part of the process of modeling is figuring out what the desired outcomes actually are before you’ve written any code. You can take those conclusions and draft your SLOs from them.

Make no mistake, complex systems will always have unexpected failures. Nothing can completely prevent them, but modeling can improve your awareness around them and give you an edge in cutting them off before they lead to outages.

Other Models To Look At

• Zero Downtime Deployments
• Rate Limiting
• Batch Installer

If you’d like to see the code and configuration from my models, they’re here on Github. Also thanks as always to the amazing Hillel Wayne for helping me track down the occasional TLA+ bug. Go buy his book!

Using TLA+ to Model Cascading Failures was originally published in Software Safety on Medium, where people are continuing the conversation by highlighting and responding to this story.