Linearizability and State-Machine Replication: Is it a match?

TL;DR

This paper argues that interval linearizability is a more suitable correctness property than linearizability for state-machine replication, as it relaxes constraints and simplifies correctness proofs.

Contribution

It demonstrates that interval linearizability better fits SMR systems by removing restrictions of linearizability and enabling more flexible application behaviors.

Findings

Linearizability is too restrictive for SMR.

Interval linearizability relaxes constraints and is more suitable.

Correctness proofs are simplified under interval linearizability.

Abstract

Linearizability is a well-known correctness property for concurrent and distributed systems. In the past, it was also used to prove the design and implementation of replicated state-machines correct. State-machine replication (SMR) is a concept to achieve fault-tolerant services by replicating the application code and maintaining its deterministic execution in all correct replicas. Correctness of SMR needs to address both, the execution of the application code -- the state machine -- and the replication framework that takes care of communication, checkpointing and recovery. We show that linearizability is overly restrictive for SMR as it excludes many applications from being replicated. It cannot deal with conditional waits and bidirectional data flows between concurrent executions. Further, linearizability does not allow for vertical composition, e.g., nested invocations. In this work we argue that interval linearizability, a recently defined relaxation of linearizability, is the appropriate correctness criterion for SMR systems. This no longer puts any constraints on the application code. Instead the focus for correctness proofs of an SMR system is on the deterministic execution of the application within correct replicas under the assumptions of the chosen failure model. Thus, this work not only clears some myths about linearizable SMR but also relieves correctness proofs from linearizability proofs.