The objective of the state transfer sub-protocol is to allow a replica that is behind to catch up. The paper states:

“State transfer is used by a node that has gotten behind (but hasn’t crashed) to bring itself up-to-date. There are two cases, depending on whether the slow node has learned that it is missing requests in its current view, or has heard about a later view.”

The words “has heard about a later view” is pretty vague and immediately the question arises as to what this means concretely.

In part 1 I described the questions and doubts I had about the view changes sub-protocol. In this part of the analysis we’ll use TLA+ to answer those questions.

I wrote two specifications, one for increment-mode and assume-mode which only include the view changes and normal operations sub-protocols - leaving out client and replica recovery, client tables and cluster reconfiguration.

In this post, we’ll look at the view changes sub-protocol of the VR Revisited protocol and go over the questions that I had after reading the paper. I found the paper did not discuss a number of specific behaviours and situations which gave arise to a few doubts and questions. In following posts, we’ll look at how I used TLA+ to answer all these questions and test the validity of my thinking.

A couple of weeks ago I got nerd sniped into writing a TLA+ specification for the Viewstamped Replication Revisited paper. I have written specifications for multiple variants of Raft, Apache BookKeeper, SWIM, Kafka replication, Kafka consumer group protocol, RabbitMQ streams replication and many more including some protocols that are not publicly available. But VR Revisited has been more challenging than most, not because it is more complex, but because the paper is hard to interpret.