prisma-risk / tsoracle / 26414231663

95%

push

github

fix(paxos): seed barrier-nonce recovery from the durable log, not the non-synced decided_idx (#427)

`StandaloneHost::new` resumed `barrier_seq` from the recovered decided fold
(`applied_barrier_seq` over `[0, decided_idx)`). But `set_decided_idx` is a
`batch_async` (non-synced) write while log appends are `batch_sync` (fsynced),
so a crash can recover a `decided_idx` below a `Barrier { node: self, seq }`
that is still durably logged. That barrier is invisible to the decided fold,
yet the apply task folds it once the cluster re-confirms the decision — so a
freshly minted post-restart nonce could be falsely satisfied by the recovered
`(self, seq)` before the read's own barrier is folded. That is the exact
linearizability hazard the per-node nonce exists to close, reopened across a
restart, while relying on `decided_idx` durability the recovery path itself
disclaims.

Derive the seed from the durable log instead. New
`max_logged_barrier_seq(omnipaxos, node)` scans the whole accepted suffix via
`read_entries(..)` (`0..accepted_idx`, where `accepted_idx` is rebuilt from the
fsynced `get_log_len`), folding `Decided`/`Undecided` `Barrier { node: self }`
entries and the leading `Snapshotted` entry's barrier ledger (so an idle node
whose barriers were all compacted away still re-seeds correctly). `new` seeds
`barrier_seq` from this; the recovery fold still runs for the high-water, the
applied-barrier ledger, and the apply cursor. Including not-yet-decided entries
can only raise the seed, which is always safe: the nonce is an opaque monotonic
counter, so skipped values are free, whereas a lower seed reopens the
collision.

Tests: an in-crate wiring test stages the lost-decided-suffix shape and asserts
the seed lifts the next nonce above the durable barrier; helper tests cover the
empty-log, per-node, and compacted-snapshot paths; a new failpoints test binary
drops the real `set_decided_idx` write through the `async_write` failpoint and
asserts the decided fold... (continued)

135 of 140 new or added lines in 2 files covered. (96.43%)

10322 of 10687 relevant lines covered (96.58%)

489286.26 hits per line