Concepts › Shrinking quorum

Shrinking quorum

A redundancy policy: vote on three replicas, compare on two, self-check on one. It decides exactly as fixed TMR while TMR can run, and continues after TMR stops.

The trouble with a fixed threshold

Classic triple modular redundancy (TMR) runs three processors on the same work and takes the majority. Two can still detect a disagreement. One cannot outvote anything, so the system stops.

With a repair crew in reach, stopping is safe: someone swaps the board. With no one in reach, stopping throws away the last processor's whole remaining life.

Three modes

The policy picks a mode from the number of live replicas. This is the whole rule, from quorum::mode:

Live replicasFixed TMRShrinking quorum
3Vote · masks one bad resultVote · masks one bad result
2Compare · loses the tick on a mismatchCompare · runs a known-answer test to find the bad one
1Halted, for goodSelf-check · computes twice, delivers on a match, half speed
0HaltedHalted
pub fn mode(policy: Policy, alive: usize) -> Mode {
match (policy, alive) {
    (_, 0) => Mode::Halted,
    (Policy::Shrink, 1) => Mode::SelfCheck,
    (Policy::Tmr, 1) => Mode::Halted,
    (_, 2) => Mode::Compare,
    _ => Mode::Vote,
}
}

What it guarantees

  • Never less than fixed TMR. While TMR can still run, both policies make exactly the same decision. They differ only after TMR has stopped.
  • It halts only with nothing left. Fixed TMR stops below two replicas. The shrinking quorum stops at zero.
  • Only agreed results go out. A delivered value came from at least two replicas, or from both runs of the last replica's self-check.

Each property is a Kani proof over every possible input, run in CI on every change. See Kani proofs.

What it costs

On one replica, a stuck fault is caught only by the periodic known-answer test. Until then, a few wrong results can get out. Fixed TMR never produces those, because it never lives that long.

TradeIn Dusk's default run, fixed TMR comes out ahead only if one wrong result costs more than 136 years of useful work (95% CI 131 to 142).

Health and diagnosis

A replica outvoted STRIKES = 3 times within STRIKE_WINDOW = 200 ticks is diagnosed with a known-answer test: a fixed input whose result is known. Pass, and its strikes are cleared, because the upsets were transient. Fail, and it is retired.

Graceful Degradation Index

The whitepaper scores a degrading system by the ratio of capability delivered to hardware surviving. 1.0 means every surviving part is doing useful work. Dusk measures the simpler cousin, total useful work across the whole decline.

Updated 7 Oct 2026 · Edit on GitHub · Questions? Request information