Why Extension-Based Proofs Fail

Dan Alistarh, James Aspnes, Faith Ellen, Rati Gelashvili, Leqi Zhu

We prove that a class of fundamental shared memory tasks are not amenable to certain standard proof techniques in the field. We formally define a class of extension-based proofs, which contains impossibility arguments like the valency proof by Fisher, Lynch and Paterson of the impossibility of wait-free consensus in an asynchronous system. We introduce a framework which models such proofs as an interaction between a prover and an adversarial protocol. Our main contribution is showing that extension-based proofs are inherently limited in power: for instance, they cannot establish the impossibility of solving (n-1)-set agreement among n > 2 processes in a wait-free manner. This impossibility result does have proofs based on combinatorial topology. However, it was unknown whether proofs based on simpler techniques were possible.

Knowledge Graph



Sign up or login to leave a comment