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.

翻译：本文比较了在分布式计算中推导下界和不可能性结果的两种通用技术。首先，针对无等待无色算法，我们证明了一个加速定理（类似Brandt, 2019），旨在捕捉通过逆向归纳进行的、奠定三染色环（Linial, 1992）轮数下界的经典轮数缩减证明的精髓。其次，我们考虑FLP式证明，旨在捕捉通过正向归纳进行的、奠定经典共识不可能性证明（Fischer, Lynch, and Paterson, 1985）的精髓。我们表明，尽管这两种证明形式性质迥异，但它们紧密相连。特别地，我们证明对于任意无色任务$\Pi$，如果存在一个轮数缩减证明，确立了使用无等待无色算法无法解决$\Pi$，那么也存在一个FLP式证明，能确立相同的不可能性。对于一维无色任务（任意进程数$n\geq 2$），我们证明这两种证明技术具有完全相同的效力，更重要的是，它们都是完备的：如果一个一维无色任务无法被$n\geq 2$个进程以无等待方式解决，那么这两种证明技术都能证明其不可能性。此外，可以自动推导出轮数缩减证明，并从中自动生成FLP式证明。最后，我们通过证明任意维度的无色覆盖任务无法被无等待算法解决，展示了这两种技术的应用。