Viewstamped Replication — Analyses — Jack Vanlightly

Viewstamped Replication

Paper: VR Revisited - Checkpoint-Based Replica Recovery (part 6)

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.

Paper: VR Revisited - State Transfer (part 3)

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.

Paper: VR Revisited - View changes - Answers (part 2)

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.

Paper: VR Revisited - View changes - Questions (part 1)

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.

Paper: VR Revisited - An analysis with TLA+

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.