Finding bugs in systems through formalization

The queue

The queue we want to model is a FIFO. Like every queue, it supports two operations: put for adding an element and take to pop an element from the queue. To keep the specification as simple as possible, we simply begin the model checking with all status messages that we want to have processed already enqueued. That leaves us with only needing to model the take operation.

EXTENDS Sequences, TLC

\* Receive a message from the queue
macro recv(queue, receiver)
begin
  await queue # <<>>;
  receiver := Head(queue);
  queue := Tail(queue);
end macro

Hopefully, this doesn’t look too surprising. On the other hand, it’s the first PlusCal code in this post, hence it’s probably worth looking at it a bit closer in detail:

• Line comments begin with \*
• It defines the macro recv which takes two arguments. A macro will be expanded at the call site at compile time.
• # means unequal (alternatively, /= can be used as well)
• <<>> is an empty tuple
• The macro consists of three different parts:
  • wait until the queue passed as argument is not empty
  • take the head
  • set the queue to the tail elements

Let’s see if this works! We define our queue queue with two messages, another variable msg where we will store the received messages, add a bit of required boilerplate and then receive the two messages:

EXTENDS Sequences, TLC

(* --algorithm queue
variable queue = <<"first message", "second message">>,
  msg = "";

\* Receive a message from the queue
macro recv(queue, receiver)
begin
  await queue # <<>>;
  receiver := Head(queue);
  queue := Tail(queue);
end macro

begin
  recv(queue, msg);
  print msg;
  recv(queue, msg);
  print msg;

end algorithm *)

print is of course a debug utility and nothing that would have a place in a real specification. If we now translate this PlusCal to TLA+ and execute it, the output will be first message and then second message. How you are actually able to execute this specification is out of scope for this post, but fortunately Leslie Lamport explains it in his video course, in the video "Resources and Tools". The specification can be found on Github, in case you want to toy around with it.

The real progress handler, the one we want to model, is of course more complex. First of all, it not only receives one message, it rather never stops to receive messages. There can also be more than one instance of it. Of course PlusCal also provides a way to model this, in the form of loops and processes.

process handler \in 1..2
variable msg = "";
begin
loop:
  while TRUE do
    recv(queue, msg);
  end while
end process

Note that the loop: is not part of the begin but defines a label. Basically everything in one label happens at once and only between labels the model and its invariants will be checked. Process switches also happen between labels. TLA+ will choose an arbitrary process and execute one step, again and again, indefinitely.

If we now run this model, TLA+ will eventually produce an error: Deadlock reached. That is because TLA+ also checks for deadlocks, and eventually all our processes will wait for a new message to appear in the queue.

Cassandra

Now that we have successfully modelled the queue, let’s move on to Cassandra. Cassandra is used to persist the set of completed processing steps. In Cassandra, it's possible to specify a replication factor that tells Cassandra on how many nodes data should be replicated. If one writes data to only one node, Cassandra will replicate the data in the background to the number of other nodes specified in the replication factor. It means though that it's possible to not always read the latest data, for example in the case data is written to one node and then immediately read from another node and the data is not replicated yet. Cassandra also offers a consistency level for every query, where one can specify on how many nodes data needs to be written before a write query completes as successful (or, in the case of read query, from how many different nodes data needs to be read).

In the blog post's model, the background replication (in other words, the replication factor) is omitted and the consistency level is modelled by taking a set of nodes for the write operation.

procedure appendProgress(writeNodes, status)
variable nodes = writeNodes;
begin P0:
  while (nodes # {}) do
  P1:
    with n \in nodes do
      progress[n] := progress[n] \union {status};
      nodes := nodes \ {n};
    end with
  end while;
  return;
end procedure

A procedure is similar to a macro, but it can can have labels, so a process switch in the middle of the execution of the procedure is possible, and it can have a return value. The with n \in nodes statement is executed by choosing any element out of nodes and then executing the statement’s body. This will be done for every possible execution of the statement, so for every possible element. That means that ultimately this procedure makes TLA+ check every possible combination of the order in which the progress is written to the individual nodes.

Modelling the read could be done in a similar fashion. In this specification, it’s simplified to the following:

\* Reads the progress set from the given nodes
ReadProgress(nodes) == UNION {progress[n] : n \in nodes}

What can be seen here is one of the pitfalls of extracting a system’s behaviour into a specification. The modelling of how Cassandra behaves is of course based on the the author’s understanding of how Cassandra behaves. If Cassandra behaves differently for whatever reason (maybe because the author’s understanding was plain wrong, or maybe because Cassandra might have a bug itself), then the specification will not reflect how the real system behaves. In this instance, it’s assumed that when reading a set and different nodes return different sets, Cassandra will merge the sets of all nodes into one resulting set.

The final progress handler

Having modelled the queue and Cassandra, there is one final missing part: the progress handler itself. As mentioned before, it executes the following steps:

• Wait for a status queue message. That also increases the number of unacknowledged queue messages.
• Load the job from the database
• Append the new status and write it to the database
• Load the job again and check if its overall status switched from pending to completed
• Acknowledge the queue message (mark it as processed).

For consistency reasons, we instruct Cassandra to always read and write from a majority number of nodes before an operation is considered complete. We also consider the possibility that the read and write operations use a different set of nodes. To do so, another helper is introduced to give all subsets of nodes of a given size:

\* Returs a set with all subsets of nodes with the given cardinality
NNodes(n) == {x \in SUBSET Nodes : Cardinality(x) = n}

That helper can then be used to describe the variables in the process that describes the process handler:

\* Handles a progress message from the queue
fair process progressHandler \in {"handler1", "handler2"}
variable
  writeQuorumNodes \in NNodes(Quorum),
  readQuorumNodes \in NNodes(Quorum),
  secondReadQuorumNodes \in NNodes(Quorum),
  completedBefore = FALSE,
  message = "";

Once again, TLA+ will check every possible combination of read and write nodes.

The remaining part of the progress handler is pretty straight forward:

begin P0:
  while TRUE do
  Poll:
    recv(queue, message);
    unacked := unacked + 1;
  Read:
    completedBefore := ProcessingComplete(ReadProgress(readQuorumNodes));
  Write:
    call appendProgress(writeQuorumNodes, message);
  ReadAfterWrite:
    if ~completedBefore /\ ProcessingComplete(ReadProgress(secondReadQuorumNodes)) then
      \* The real progress handler would trigger some action here
      switchHappened := switchHappened + 1;
    end if;
  Ack:
    unacked := unacked - 1;
  end while;
end process;

As a final step, an invariance called Correctness is added to the specification. TLA+ will check that the invariant holds after every step. One invariant that should hold at every time for the progress handler is that there are either still some messages to process (in other words, the queue is not empty), or that the handler is still in the act of processing a message (number of unacknowledged messages is not zero) or that the progress switch was observed by a handler:

Correctness == \/ queue # <<>>
               \/ unacked > 0
               \/ switchHappened > 0

With the complete specification now in place, the model can be checked. And it completes without error! The complete specification can be found on Github in case you want to check yourself.