Blair Archibald

Modelling Zero-Downtime Deployments with Bigraphs

I’m a big fan of Hillel Wayne’s Blog which discusses a wide range of formal methods topics with a particular emphasis on system design (as opposed to code verification etc). The posts are accessible even to those with no training in formal methods, and I would recommend taking a look.

Often Hillel uses TLA+ or Alloy for system design tasks. In my new postdoc at Glasgow, I’ve been working with Bigraphs which may also be used for system design tasks. And so, inspired by Hillel’s post on modelling zero-downtime deployments using TLA+, we are going to replicate this here using Bigraphs. This is not meant to criticise Hillel’s model or to show TLA+ is a bad choice; I simply want to present an alternative approach and show how Bigraphs can be applied to system design.

Bigraphs are a formalisation by Robin Miler, which have essentially two purposes:

  1. To be a meta-model for encoding concurrent calculi such as pi-calculus
  2. To be a design/modelling language, mainly targeting cyber-physical/ubiquitous computing systems

Bigraphs are backed by a very rich and interesting theory. However, in this post I want to try and give an intuitive feel for them rather than presenting all the details. One really cool thing about Bigraphs is, as the name suggests, they are based on graphs (the pairing of two graphs to be precise). This means we can speak about them both algebraically and graphically. Being able to model systems graphically is extremely useful for bringing formal methods to domain experts who are often unfamiliar with set-theoretic tools. As we will see, the designs are often not too far from what we will might draw on a whiteboard (except now we get verfification/model checking almost for free!).

Problem and Tools

The zero-downtime upgrade problem is well explained in Hillel’s blog post so I won’t repeat the details here.

Essentially, we have a bunch of servers we want to upgrade, and want to schedule the upgrades such that there is always at least one server available to handle client requests, and that clients will always receive the same version of the application (whether upgraded or still vanilla).

To allow us to write our bigraph model, we can use the BigraphER tool developed at the University of Glasgow. BigraphER provides a host of features, in particular a language for describing bigraphs and features for exporting a transition system for model checking (unlike TLA+ the model checker is not built in, instead we rely on external tools which has the benefit of staying up to date with new model checking improvements for free).

Basic Elements

Bigraphs are based around entities/controls which represent objects/things that we want to represent in the system. Relationships between entities can be described spatially, by nesting enitities inside each other or placing them side-by-side, or by (hyper-)links between them. The basic zero-downtime model only uses placement I’ll discuss linking briefly in Bigraph Linking.

For our model we use the following basic entities:

ctrl Server = 0;
ctrl Stage = 0;
atomic ctrl Updated = 0;

In the algebraic definition, ctrl introduces a new entity/control with a given name, and the = 0 says: “this entity has no links”. atomic disallows nesting for a particular entity, i.e. the Updated token can’t contain anything else.

The idea here is that we will nest an Updated token within a Server once an update has been performed. With the goal to update all our servers with zero downtime.

The system is in error if two (or more) servers are running different versions of the code. We can describe this using the following bigraph, which we will call a predicate:

img
img
big same_version = Stage.(Server.1 | Server.Updated | id);

Where id (the gray region in the diagram) represents a site/hole in the bigraph which can be read as “there may be something else here”. In our case this means we don’t care if the third sever is upgraded or not (or even if it exists) since the error condition only requires a mismatch between any two servers.

Finally we need to implement the logic to update a server. Just like the predicate above, we described changes to the system by looking for a particular pattern and re-writing it to a different pattern. In this case:

img
img
react update_server = Server.1 --> Server.Updated;

Which says whenever we see a server with nothing inside it (there is no hole here so in this case it can’t contain anything), we can re-write it to a server with an Updated token inside.

Finally we create the initial bigraph and tell bigraphER which rules and predicates we want to use:

big s0 = Stage.(Server.1 | Server.1 | Server.1);

begin brs
  init s0;
  rules = [ { update_server } ];
  preds = { same_version };
end

As in the original posst, we use a system with three servers. | specifies that these should be placed them side-by-side in the stage area.

bigraphER can then generate an svg representation of the transition system:

bigrapher full -s -f svg -t transitions.svg  <fname.big>
img
img

We quickly see from the state labels that we, unsurprisingly, violate the same_version constraint in a single step.

An interesting point here is that we have less states than the TLA+ model. This is because we don’t identify the servers, i.e. we don’t have {“s1”,“s2”,“s3”}. This means that the state where two servers are updated is the same regardless of which server updates first. TODO: Check this

Applying the Fixes

We will follow the same fixes as Hillel by adding in a load balancer and making sure that all servers that are within the load balancer always have the same updated status, as those outside are not serving anything.

Let’s add some more controls to model the load balancing:

ctrl LoadBalancer = 0;
ctrl NotLoadBalancer = 0;
atomic ctrl Update_Flag = 0;

We also introduce a NotLoadBalancer control to give our servers somewhere else to go when they are being updated. The UpdateFlag operates just like Updated.

Now our predicate changes to check only when two servers in the load balancer have different versions:

big same_version = LoadBalancer.(Server.1 | Server.Updated | id);

We can then add reacts that start the update process. This is a two step process, firstly we move all but one server out of the load balancer:

react start_update_1 =
  LoadBalancer.(Server.1 | id) || NotLoadBalancer.1
  -->
  LoadBalancer.Server.Update_Flag || NotLoadBalancer.id;

Then we set the update flag on each server:

react start_update_2 =
  NotLoadBalancer.(Server.1 | id) --> NotLoadBalancer.(Server.Update_Flag | id);

This rule only sets the update flag on the servers we removed from the load balancer. The update flag for the load balancer server is set during start_update_1 to avoid an additional rule.

Running this through bigraphER everything works:

img
img

Except of course we can’t update the server in the load balancer in a single time step! Let’s add in downtime.

atomic ctrl Updating = 0;

react update_server = Server.Update_Flag --> Server.Updating;
react finish_update = Server.Updating --> Server.Updated;

big zero_downtime = LoadBalancer.(Server.Updating | id);

Where the zero_downtime predicate signals the error condition where any server in the load balancer is inaccessible due to undertaking an update.

img
img

Finally we need to switch our LoadBalancer and NotLoadBalancer in order to let the final server update before being added back into the system.

react switch_states =
  LoadBalancer.id || NotLoadBalancer.(Server.Updated | Server.Updated)
  -->
  LoadBalancer.(Server.Updated | Server.Updated) || NotLoadBalancer.id;

react finish =
  NotLoadBalancer.Server.Updated || LoadBalancer.id
  -->
  NotLoadBalancer.1 || LoadBalancer.(id | Server.Updated);

TODO: Describe this?

This gives us the final model:

ctrl Server = 0;
ctrl LoadBalancer = 0;
ctrl NotLoadBalancer = 0;

atomic ctrl Updated = 0;
atomic ctrl Update_Flag = 0;
atomic ctrl Updating = 0;

big same_version = LoadBalancer.(Server.1 | Server.Updated);
big zero_downtime = LoadBalancer.Server.Updating;

react update_server = Server.Update_Flag --> Server.Updating;
react finish_update = Server.Updating --> Server.Updated;

react start_update_1 =
  LoadBalancer.(Server.1 | id) || NotLoadBalancer.1
  -->
  LoadBalancer.Server.1 || NotLoadBalancer.id;

react start_update_2 =
  NotLoadBalancer.(Server.1 | id) --> NotLoadBalancer.(Server.Update_Flag | id);

react switch_states =
  LoadBalancer.id || NotLoadBalancer.(Server.Updated | Server.Updated)
  -->
  LoadBalancer.(Server.Updated | Server.Updated) || NotLoadBalancer.id;

react finish =
  NotLoadBalancer.Server.Updated || LoadBalancer.id
  -->
  NotLoadBalancer.1 || LoadBalancer.(id | Server.Updated);

big s0 = LoadBalancer.(Server.1 | Server.1 | Server.1) || NotLoadBalancer.1;

# TODO: Didn't describe this anywhere
big done = LoadBalancer.(Server.Updated | Server.Updated | Server.Updated);

begin brs
  init s0;
  rules = [ { switch_states, update_server, finish_update,
              start_update_1, start_update_2, finish } ];
  preds = { same_version, zero_downtime, done };
end

Generating the transition diagram we see it now works as expected

## Bigraph Linking

In this model we have only used half of the bigraph theory: entity placement. Bigraphs also have a notion of linking, allowing us to relate one entity to another.

To quickly show how this works, assume the servers are paired and one of each pair must be available at all times, i.e. we can no longer leave just one server in the load balancer during the update.

How can we model this? First we change the definition of Server to include a single link.

ctrl Server = 1;

# New initial state with 4 servers
big s0 = LoadBalancer.(Server{s1}.1 | Server{s1}.1
                     | Server{s2}.1 | Server{s2}.1)
      || NotLoadBalancer.1;

Where Servers with equivalent {s1} names share a link. These links are actually hyper-edges linking of as many entities as we like.

A new predicate tells us if we violate the constraint that one of two linked servers must be in the load balancer at all times:

big missing_server = NotLoadBalancer.(Server{s1}.1 | Server{s1}.1);

Of course this is quickly violoated:

TODO: svg

This is a bit harder than I thought. I should sketch it out first.

Conclusion