In part 5 we looked at basic and log-suffix recovery and came to the conclusion that perhaps a persistent State Machine Replication (SMR) protocol should not use asynchronous log flushing with a recovery protocol for recovering from data loss - at least not one that gets stuck after a cluster crash. Checkpoint based recovery doesn’t change that position but it does introduce a very important component of any SMR protocol - checkpointing application state.

One of the selling points of VR Revisited is that replicas do not need to write anything to stable storage, or can choose to write to storage asynchronously which can give this protocol a latency advantage over protocols that require fsyncing of key operations.

Part 4 was going to be focused on the replica recovery sub-protocol but while writing the replica recovery specification I discovered that I had failed to enforce a critical property - that of commit number monotonicity.

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.