prisma-risk / tsoracle / 26350643476

95%

push

github

fix(driver-paxos): gate submit_advance on a per-call barrier nonce (#256) (#278)

submit_advance waited on a threshold — `new_decided > snapshot_decided
&& high_water() >= at_least` — that a racing caller's Advance can satisfy
before this call's own Advance is applied. Both halves can be caused by
an unrelated entry, so the returned high-water was not provably
attributable to this call; the apply-wait contract was not actually
enforced, leaving the epoch fence as the only real safety net.

Mirror current_high_water: append a Barrier { node, seq } nonce
immediately after the Advance and wait until the apply path folds that
specific barrier. A folded barrier proves every earlier decided entry —
this call's own Advance among them — has been folded, so the returned
value is provably this call's. The trailing high_water() >= at_least
guard preserves submit_advance's floor postcondition (absent from the
read path) in the corner where a mid-call leadership change drops the
Advance while the barrier still decides under the new leader.

0 of 3 new or added lines in 1 file covered. (0.0%)

10606 of 11186 relevant lines covered (94.81%)

502999.35 hits per line