Why Extension-Based Proofs Fail
Dan Alistarh, James Aspnes, Faith Ellen, Rati Gelashvili, Leqi Zhu

TL;DR
The paper demonstrates the limitations of extension-based proofs in establishing certain impossibility results in distributed computing, showing they cannot prove some known results based on combinatorial topology.
Contribution
It proves that extension-based proofs are insufficient to establish some classical impossibility results in asynchronous distributed systems.
Findings
Extension-based proofs cannot establish the impossibility of deterministic k-set agreement in certain models.
Shows limitations of simpler proof techniques compared to combinatorial topology.
Highlights the need for more complex methods in proving distributed impossibility results.
Abstract
We introduce extension-based proofs, a class of impossibility proofs that includes valency arguments. They are modelled as an interaction between a prover and a protocol. Using proofs based on combinatorial topology, it has been shown that it is impossible to deterministically solve k-set agreement among n > k > 1 processes in a wait-free manner in certain asynchronous models. However, it was unknown whether proofs based on simpler techniques were possible. We show that this impossibility result cannot be obtained for one of these models by an extension-based proof and, hence, extension-based proofs are limited in power.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
Why Extension-Based Proofs Fail· youtube
Taxonomy
TopicsDistributed systems and fault tolerance · Formal Methods in Verification · Petri Nets in System Modeling
