Module eventual_leader_detector 

Ω — an eventual leader detector.

Status: implementation. Space: bounded by membership.

Cachin, Guerraoui & Rodrigues, Module 2.9 and Algorithm 2.8 (“Monarchical Eventual Leader Detection”), quoted from the book:

Algorithm 2.8: Monarchical Eventual Leader Detection
Implements: EventualLeaderDetector, instance Ω.
Uses: EventuallyPerfectFailureDetector, instance ◇P.

upon event ⟨ Ω, Init ⟩ do
    suspected := ∅;
    leader := ⊥;

upon event ⟨ ◇P, Suspect | p ⟩ do
    suspected := suspected ∪ {p};

upon event ⟨ ◇P, Restore | p ⟩ do
    suspected := suspected \ {p};

upon leader ≠ maxrank(Π \ suspected) do
    leader := maxrank(Π \ suspected);
    trigger ⟨ Ω, Trust | leader ⟩;

The detector beneath is a parameter, and defaults to ◇P

Algorithm 2.8 says Uses: EventuallyPerfectFailureDetector, and crate::eventually_perfect_failure_detector is what that names. D defaults to it, so the plain EventualLeaderDetector is the algorithm as written.

It can also be composed over crate::perfect_failure_detector, which is strictly stronger: it never suspects a correct process and never retracts, so suspected only grows and the Restore arm is unreachable. That composition is named in crate::stacks and was this module’s only form until ◇P existed. The difference is not academic in the fail-recovery model: under P a suspicion is permanent, maxrank only ever walks downward through the membership, and a process that crashed and recovered can never lead again.

An Ω that is never wrong is a trap, and naming it is the point. It makes every test of the layers above vacuous: Paxos exists to stay safe while the leader detector lies, and over an honest detector that property is untestable. So the suites that matter withdraw the detector’s accuracy — the timing assumption both detectors rest on is what they remove — and this module is then wrong in exactly the way Ω is allowed to be. tests/eventual_leader_detector.rs checks that it can disagree before anything is built on it.

maxrank, and what rank means here

The book leaves rank as any fixed injective map from processes to integers. Here it is the [NodeId] ordering, and maxrank takes the greatest — so leadership passes downward through the membership as processes are suspected, and two processes with the same suspicions always agree. Which direction it runs does not matter for correctness; that it is a function of the suspected set alone does, and that is what the suite pins.

ELD1 [eventual]  Eventual accuracy — eventually every correct process trusts the same correct
                 process. Before then it may trust a crashed process, or disagree.

ELD1 inherits its condition from the detector beneath: over ◇P it holds while ◇P2 does, and ◇P2 is itself conditional on the delay cap and on the network settling. The chain is stated at each link rather than collapsed into one unqualified claim.

Structs

EventualLeaderDetector

Trust the highest-ranked process not currently suspected.

Enums

Ind

Indications to the layer above.

Type Aliases

Cmd

Requests from the layer above.