Skip to main content

LivenessScope

Trait LivenessScope 

Source
pub trait LivenessScope:
    UnboundedProgress
    + RoundsWithoutTimeout
    + ActiveCorrectDriver
    + LockRecovery { }
Expand description

Remark (What liveness does not claim). Five exclusions, each of which a reader may reasonably expect UnboundedProgress to cover.

  • No progress without a client. ActiveCorrectDriver is indispensable: a validator never proposes and never advances a round unprompted. A microchain whose owners have all gone away makes no progress and is not thereby faulty. This is the deepest structural difference from a validator-driven BFT protocol, and it is what makes a Linera validator’s per-chain cost proportional to use.

  • The fast round can wedge a height permanently. By RoundsWithoutTimeout, with the default TimeoutConfig the fast round has no timeout at all, and while the current round is fast only a super owner may open a later one. A super owner that issues two conflicting fast proposals splits the correct validators — each locks onto the first it sees, by FastConfirmationNeedsEmptyLock — so neither reaches a quorum, and the height stops until that same super owner proposes again in a higher round. CommitAgreement is untouched; this is exactly the trade the fast path makes, and the reason ChainClient::process_pending_block_inner refuses to replace a pending fast proposal whose signing key it no longer holds.

  • Multi-leader rounds are not covered by RoundProgress. The theorem is stated for SingleLeader and Validator rounds, where a unique leader is guaranteed by LeaderEligibility. In a multi-leader round several owners may propose simultaneously; correct validators then vote for whichever proposal they see first, quorums may not form, and by RoundsWithoutTimeout a non-final multi-leader round has no timeout — it is left only by a proposal in a higher round. This is by design (multi-leader rounds are the uncontended fast path) and costs nothing, because the round sequence passes through them into single-leader rounds where the theorem applies.

  • No bound on the number of rounds, and no bound before GST. RoundProgress asserts the existence of a successful round, not a bound on how many precede it. Faulty leaders and pre-GST delays each cost rounds.

  • Nothing is claimed about the content of the committed blocks. A driver competing with other owners may find its own block superseded: LockRecovery obliges it to re-propose whatever is locked rather than its own pending block. process_pending_block then returns the committed certificate for the other block and keeps the driver’s proposal pending for a later height. Liveness of the chain does not imply liveness of any particular transaction.

Implementors§