Fault-tolerant consensus

Roughly speaking, a distributed consensus algorithm can tolerate f faults if up to f processes can be "faulty" and yet the non-faulty processes can still reach a consensus. The fault we consider here is limited to the crash fault, in which a process stops responding to messages from some point onward. We do not consider Byzantine faults.

def Cslib.FLP.ProcFaulty {P : Type u_1} {M : Type u_2} {S : Type u_3} (p : P) (ss : ωSequence (State P M S)) (xs : ωSequence (Action P M)) : Prop

A process p is faulty in an infinite execution iff there is a time k from which onward there is a message in-flight to p but p has stopped receiving messages.

Equations

• Cslib.FLP.ProcFaulty p ss xs = ∃ (k : ℕ), (∃ m ∈ (ss k).msgs, m.dest = p) ∧ ∀ (j : ℕ), k ≤ j → ∀ (m' : Cslib.FLP.Message P M), xs j = some m' → m'.dest ≠ p

def Cslib.FLP.ProcFair {P : Type u_1} {M : Type u_2} {S : Type u_3} (p : P) (ss : ωSequence (State P M S)) (xs : ωSequence (Action P M)) : Prop

A process p is fair in an infinite execution iff every message in-flight to p is received by p.

Equations

• Cslib.FLP.ProcFair p ss xs = ∀ (m : Cslib.FLP.Message P M), m.dest = p → ∀ (k : ℕ), m ∈ (ss k).msgs → ∃ (j : ℕ), k ≤ j ∧ xs j = some m

theorem Cslib.FLP.not_procFaulty_and_procFair {P : Type u_1} {M : Type u_2} {S : Type u_3} (p : P) (ss : ωSequence (State P M S)) (xs : ωSequence (Action P M)) : ¬(ProcFaulty p ss xs ∧ ProcFair p ss xs)

A process p cannot be both faulty and fair in an infinite execution. Note, however, that it is possible for p to be neither faulty nor fair, because p can keep on receiving messages but at the same time keep ignoring some messages sent to it.

def Cslib.FLP.FairRun {P : Type u_1} {M : Type u_2} {S : Type u_3} (ss : ωSequence (State P M S)) (xs : ωSequence (Action P M)) : Prop

An infinite execution is fair iff every process is either faulty or fair (cf. the comment for the theorem not_procFaulty_and_procFair).

Equations

• Cslib.FLP.FairRun ss xs = ∀ (p : P), Cslib.FLP.ProcFaulty p ss xs ∨ Cslib.FLP.ProcFair p ss xs

noncomputable def Cslib.FLP.numProcFaulty {P : Type u_1} {M : Type u_2} {S : Type u_3} (ss : ωSequence (State P M S)) (xs : ωSequence (Action P M)) : ℕ

The number of faulty processes in an infinite execution.

Equations

• Cslib.FLP.numProcFaulty ss xs = {p : P | Cslib.FLP.ProcFaulty p ss xs}.ncard

theorem Cslib.FLP.not_procFaulty_of_numProcFaulty {P : Type u_1} {M : Type u_2} {S : Type u_3} [Fintype P] {ss : ωSequence (State P M S)} {xs : ωSequence (Action P M)} (h : numProcFaulty ss xs < Fintype.card P) : ∃ (p : P), ¬ProcFaulty p ss xs

If the number of faulty processes in an infinite execution is less than the total number of processes, then at least one process is not faulty.

theorem Cslib.FLP.numProcFaulty_le_not_procFair {P : Type u_1} {M : Type u_2} {S : Type u_3} [Fintype P] {ss : ωSequence (State P M S)} {xs : ωSequence (Action P M)} {ps : Set P} (h : ∀ p ∈ ps, ProcFair p ss xs) : numProcFaulty ss xs ≤ Fintype.card P - ps.ncard

If every process in a set ps is fair, then the number of faulty processes is bounded by the total number of processes minus the cardinality of ps.

def Cslib.FLP.Algorithm.AdmissibleRun {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) (f : ℕ) (ss : ωSequence (State P M S)) (xs : ωSequence (Action P M)) : Prop

The notion of an infinite admissible execution for an algorithm a with input inp and containing at most f faulty processes.

Equations

• a.AdmissibleRun inp f ss xs = (ss 0 = a.start inp ∧ a.lts.OmegaExecution ss xs ∧ Cslib.FLP.FairRun ss xs ∧ Cslib.FLP.numProcFaulty ss xs ≤ f)

def Cslib.FLP.ProcTermination {P : Type u_1} {M : Type u_2} {S : Type u_3} (p : P) (ss : ωSequence (State P M S)) (xs : ωSequence (Action P M)) : Prop

A process terminates in an infinite execution iff either it crashes or it decides on a boolean value at some point.

Equations

• Cslib.FLP.ProcTermination p ss xs = (Cslib.FLP.ProcFaulty p ss xs ∨ ∃ (k : ℕ) (b : Bool), (ss k).ProcDecided p b)

def Cslib.FLP.Algorithm.Termination {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] [Fintype P] (a : Algorithm P M S) (f : ℕ) : Prop

An algorithm a terminates with up to f faulty processes iff all its processes terminate in every infinite admissible execution containing at most f faulty processes.

Equations

• One or more equations did not get rendered due to their size.

def Cslib.FLP.Algorithm.Consensus {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] [Fintype P] (a : Algorithm P M S) (f : ℕ) : Prop

An algorithm a is a consensus algorithm tolerating up to f faulty processes iff it both satisfies the consensus safety property a.SafeConsensus and terminates with up to f faulty processes.

Equations

• a.Consensus f = (a.SafeConsensus ∧ a.Termination f)

theorem Cslib.FLP.AdmissibleRun.fault_mono {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] {a : Algorithm P M S} {inp : P → Bool} [Fintype P] {f f' : ℕ} {xs : ωSequence (Action P M)} {ss : ωSequence (State P M S)} (hle : f ≤ f') (ha : a.AdmissibleRun inp f ss xs) : a.AdmissibleRun inp f' ss xs

If an infinite execution is admissible with up tp f faulty processes, then it is also admissible with with up tp f' ≥ f faulty processes.

theorem Cslib.FLP.Consensus.fault_mono {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] {a : Algorithm P M S} [Fintype P] {f f' : ℕ} (hle : f ≥ f') (hc : a.Consensus f) : a.Consensus f'

If a is a consensus algorithm tolerating up to f faulty processes, then it is also a consensus algorithm tolerating up to f' ≤ f faulty processes.

theorem Cslib.FLP.Algorithm.not_fair_stay_enabled {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] {a : Algorithm P M S} {ss : ωSequence (State P M S)} {xs : ωSequence (Action P M)} {p : P} (he : a.lts.OmegaExecution ss xs) (hnf : ¬ProcFair p ss xs) : ∃ (m : Message P M), m.dest = p ∧ ∃ (k : ℕ), m ∈ (ss k).msgs ∧ ∀ (j : ℕ), k ≤ j → m ∈ (ss j).msgs ∧ xs j ≠ some m

If a process p is not fair in an infinite execution of an algorithm a, then there is a message that is in-flight to, but never received, by p from some point onward.

theorem Cslib.FLP.Algorithm.drop_procFair_iff {P : Type u_1} {M : Type u_2} {S : Type u_3} [DecidableEq P] [DecidableEq M] {a : Algorithm P M S} {ss : ωSequence (State P M S)} {xs : ωSequence (Action P M)} (he : a.lts.OmegaExecution ss xs) (p : P) (n : ℕ) : ProcFair p (ωSequence.drop n ss) (ωSequence.drop n xs) ↔ ProcFair p ss xs

In an infinite execution of an algorithm a, a process p is fair iff p is fair in all suffixes of the execution.