Documentation

Cslib.Computability.Distributed.FLP.Impossibility

Impossibility of asynchronous distributed consensus in the presence of a single fault #

This file formalizes the main theorem (Theorem 1) of [Vol04] and uses it to prove the impossibility of asynchronous distributed consensus in the presence of a single fault.

source
@[reducible, inline]
abbrev Cslib.FLP.Algorithm.ReachableNonUniform {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] [Fintype P] (a : Algorithm P M S) (inp : P → Bool) (s : State P M S) :
Prop

a.ReachableNonUniform inp s means that s is a reachable and non-uniform state of algorithm a on input inp.

Equations
Instances For
    source
    noncomputable def Cslib.FLP.Algorithm.nonUniformInp {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] [Fintype P] (a : Algorithm P M S) (hpc1 : a.PseudoConsensus 1) (hc : Fintype.card P ≥ 2) :
    P → Bool

    Choose an arbitrary non-uniform input.

    Equations
    Instances For
      source
      theorem Cslib.FLP.OnePseudoConsensus.nonUniform_init {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] {a : Algorithm P M S} [Fintype P] (hpc1 : a.PseudoConsensus 1) (hc : Fintype.card P ≥ 2) :
      have inp := a.nonUniformInp hpc1 hc; a.ReachableNonUniform inp (a.start inp)

      Assuming a.PseudoConsensus 1 and there are at least 2 processes, the input chosen by a.nonUniformInp does indeed give rise to a non-uniform initial state.

      source
      theorem Cslib.FLP.OnePseudoConsensus.nonUniform_step_exists {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] {a : Algorithm P M S} [Fintype P] {inp : P → Bool} (hpc1 : a.PseudoConsensus 1) {s : State P M S} {m : Message P M} (hs : a.ReachableNonUniform inp s) (hm : m ∈ s.msgs) :
      ∃ (xl : List (Action P M)) (t : State P M S), a.lts.MTr s xl t ∧ some m ∈ xl ∧ a.ReachableNonUniform inp t

      Assuming a.PseudoConsensus 1, starting from any reachable non-uniform state of a and any message m that is in-flight in s, there exists a finite execution of a in which m is received and which ends in another non-uniform state.

      source
      theorem Cslib.FLP.OnePseudoConsensus.nonUniform_step_aux {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] {a : Algorithm P M S} [Fintype P] (inp : P → Bool) (hpc1 : a.PseudoConsensus 1) (s : State P M S) (m : Message P M) :
      ∃ (xl_t : List (Action P M) × State P M S), m ∈ s.msgs ∧ a.ReachableNonUniform inp s → match xl_t with | (xl, t) => a.lts.MTr s xl t ∧ some m ∈ xl ∧ a.ReachableNonUniform inp t
      source
      noncomputable def Cslib.FLP.Algorithm.nonUniformStep {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] [Fintype P] (a : Algorithm P M S) (inp : P → Bool) (hpc1 : a.PseudoConsensus 1) :
      DeliverMsg P M S

      Choose an arbitrary finite execution guaranteed to exist by the theorem OnePseudoConsensus.nonUniform_step_exists.

      Equations
      Instances For
        source
        theorem Cslib.FLP.OnePseudoConsensus.fair_nonUniform_step {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] {a : Algorithm P M S} [Fintype P] (inp : P → Bool) (hpc1 : a.PseudoConsensus 1) :
        a.FairDeliverMsg (a.nonUniformStep inp hpc1) Set.univ (a.ReachableNonUniform inp)

        Assuming a.PseudoConsensus 1, a.nonUniformStep does have the property guaranteed by the theorem OnePseudoConsensus.nonUniform_step_exists.

        source
        theorem Cslib.FLP.OnePseudoConsensus.fair_nonUniform {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] {a : Algorithm P M S} [Fintype P] (inp : P → Bool) (hpc1 : a.PseudoConsensus 1) (s0 : State P M S) (hs0 : a.ReachableNonUniform inp s0) :
        ∃ (ss : ωSequence (State P M S)) (xs : ωSequence (Action P M)), a.lts.OmegaExecution ss xs ∧ ss 0 = s0 ∧ (∀ (p : P), ProcFair p ss xs) ∧ ∃ᶠ (n : ℕ) in Filter.atTop, a.ReachableNonUniform inp (ss n)

        Assuming a.PseudoConsensus 1, starting from any reachable non-uniform state s0 of a, use the fair scheduler developed in FairSchedular.lean to construct an infinite fair execution in which there are infinitely many non-uniform states.

        source
        theorem Cslib.FLP.OnePseudoConsensus.not_terminating {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] {a : Algorithm P M S} [Fintype P] (hpc1 : a.PseudoConsensus 1) (hc : Fintype.card P ≥ 2) :
        ∃ (inp : P → Bool) (ss : ωSequence (State P M S)) (xs : ωSequence (Action P M)), a.AdmissibleRun inp 0 ss xs ∧ ∀ (p : P), ¬ProcTermination p ss xs

        Assuming a.PseudoConsensus 1 and there are at least 2 processes, there must exist an infinite admissible execution in which no process is faulty but no process terminates, either. This theorem formalizes Theorem 1 of [Vol04].

        source
        theorem Cslib.FLP.Consensus.one_not_exists {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] [Fintype P] (hc : Fintype.card P ≥ 2) :
        ¬∃ (a : Algorithm P M S), a.Consensus 1

        As long as there are at least 2 processes, there does not exist a distributed consensus algorithm that can tolerate 1 fault.

        source
        theorem Cslib.FLP.Consensus.ge_one_not_exists {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] [Fintype P] {f : ℕ} (hc : Fintype.card P ≥ 2) (hf : f ≥ 1) :
        ¬∃ (a : Algorithm P M S), a.Consensus f

        As long as there are at least 2 processes, there does not exist a distributed consensus algorithm that can tolerate f faults for any f ≥ 1.