prisma-risk / tsoracle / 26339765961 / 1
97%
main: 97%

DEFAULT BRANCH: main
Ran
Files 74
Run time 2s
Badge
Embed ▾
README BADGES
x

If you need to use a raster PNG badge, change the '.svg' to '.png' in the link

Markdown

Textile

RDoc

HTML

Rst
coverage: 94.85% (+0.02%) from 94.835%
26339765961.1

push

github

web-flow 
fix(driver-paxos): linearize current_high_water via per-node barrier nonces (#209)

StandaloneHost::current_high_water used the predicate `decided_idx > snapshot_decided` to decide when its appended Barrier had committed. That predicate fires whenever ANY entry decides — including prior-leader entries the local node was lagging on — so the read could return a stale `apply_state.high_water()` while its own Barrier was still undecided. In failover this lets the new leader's allocator seed `next_physical_ms` below the prior leader's true ceiling and re-issue timestamps the prior leader had already served, violating the no-duplicate / no-regression invariant the timestamp oracle relies on.

The fix tags every Barrier with a `(node, seq)` nonce. `HighWaterCommand::Barrier` becomes `Barrier { node: u64, seq: u64 }`. `ApplyState` gains a per-appending-node `applied_barriers: HashMap<u64, u64>` ledger; `drain_decided_into` records each Barrier into it. `StandaloneHost` carries `my_node_id` plus a monotonic `barrier_seq` counter; `current_high_water` mints a fresh `(self, seq)`, appends it, and waits for `applied_barrier_seq(self) >= seq` — i.e. for that specific Barrier to be folded, not just for the log to advance. Per-node keying lets multiple appending nodes coexist without trampling each other's seq spaces; size is bounded by cluster membership.

Snapshot-recovery edge case: `HighWaterSnapshot` now carries the ledger too. Without this, a node that catches up via snapshot transfer would never see its own pre-snapshot Barriers as applied, hanging future reads.

Mirror the same fix in the paxos-piggyback example (`HighWaterCommand`'s shape ripples through `MyAppCommand`/`MyAppSnap`/`PiggybackHost`).

Regression coverage: tests/linearized_barrier.rs uses the existing yield-point gating to construct the exact interleaving — pause the apply task, decide an Advance, park the reader between append and wait, let the Barrier decide while apply stays paused, then re... (continued)

10019 of 10563 relevant lines covered (94.85%)

516648.63 hits per line

Source Files on job 26339765961.1