One Step Forward, One Step Back: FLP-Style Proofs and the Round-Reduction Technique for Colorless Tasks

TL;DR

This paper explores the connection between round-reduction and FLP-style proofs in distributed computing, showing their equivalence for certain tasks and enabling automatic derivation of impossibility proofs for wait-free colorless tasks.

Contribution

It establishes a formal link between two major proof techniques, demonstrating their equivalence and completeness for 1-dimensional colorless tasks, and introduces methods for automatic proof generation.

Findings

Round-reduction proofs and FLP-style proofs are tightly connected.

Both proof techniques are complete for 1-dimensional colorless tasks.

Impossibility of solving colorless covering tasks is established using these techniques.

Abstract

The paper compares two generic techniques for deriving lower bounds and impossibility results in distributed computing. First, we prove a speedup theorem (a-la Brandt, 2019), for wait-free colorless algorithms, aiming at capturing the essence of the seminal round-reduction proof establishing a lower bound on the number of rounds for 3-coloring a cycle (Linial, 1992), and going by backward induction. Second, we consider FLP-style proofs, aiming at capturing the essence of the seminal consensus impossibility proof (Fischer, Lynch, and Paterson, 1985) and using forward induction. We show that despite their very different natures, these two forms of proof are tightly connected. In particular, we show that for every colorless task $\Pi$, if there is a round-reduction proof establishing the impossibility of solving $\Pi$ using wait-free colorless algorithms, then there is an FLP-style proof establishing the same impossibility. For 1-dimensional colorless tasks (for an arbitrary number $n\geq 2$ of processes), we prove that the two proof techniques have exactly the same power, and more importantly, both are complete: if a 1-dimensional colorless task is not wait-free solvable by $n\geq 2$ processes, then the impossibility can be proved by both proof techniques. Moreover, a round-reduction proof can be automatically derived, and an FLP-style proof can be automatically generated from it. Finally, we illustrate the use of these two techniques by establishing the impossibility of solving any colorless covering task of arbitrary dimension by wait-free algorithms.