What's Live? Understanding Distributed Consensus

TL;DR

This paper systematically compares various liveness properties of distributed consensus algorithms, introduces a formal language for specifying these properties, and analyzes their assumptions and strengths to improve understanding of consensus liveness.

Contribution

It introduces a formal language for specifying liveness properties, creates a hierarchy of these properties, and systematically compares over 30 consensus algorithms.

Findings

Identified issues with weak and strong assumptions in liveness properties.

Developed TLA+ specifications and used model checking to illustrate liveness patterns.

Discovered problems in stated liveness properties, including overly weak or strong assumptions.

Abstract

Distributed consensus algorithms such as Paxos have been studied extensively. They all use the same definition of safety. Liveness is especially important in practice despite well-known theoretical impossibility results. However, many different liveness properties and assumptions have been stated, and there are no systematic comparisons for better understanding of these properties. This paper systematically studies and compares different liveness properties stated for over 30 prominent consensus algorithms and variants. We introduce a precise high-level language and formally specify these properties in the language. We then create a hierarchy of liveness properties combining two hierarchies of the assumptions used and a hierarchy of the assertions made, and compare the strengths and weaknesses of algorithms that ensure these properties. Our formal specifications and systematic comparisons led to the discovery of a range of problems in various stated liveness properties, from too weak assumptions for which no liveness assertions can hold, to too strong assumptions making it trivial to achieve the assertions. We also developed TLA+ specifications of these liveness properties, and we use model checking of execution steps to illustrate liveness patterns for Paxos.