| Comment: | Prove sync liveness under a degraded, never-healed wire
The sync sweep proved convergence only after the network fully healed, so a protocol that converges on a perfect wire but livelocks under sustained loss would still pass. Phase 2b runs a fresh session over a wire held at a fixed drop/dup rate, never healed, asserting the same convergence and termination oracles within a window scaled from the loss rate: expected rounds are the clean window over (1 - p_loss) squared per direction, times a safety factor, recomputed in a comment rather than a magic number. No corruption is injected -- a corrupted body is already a lost round. The protocol converges comfortably: over 200 seeds the worst run took 7, 13, and 18 rounds at 10, 25, and 40 percent loss, against windows of 160, 228, and 356 -- no livelock. The gate joins at 10 percent; the soak sweeps the wider rate set. Pinning the window below the real need trips the liveness oracle, so the check is not vacuous. The liveness-under-faults discipline follows TigerBeetle's VOPR. |
|---|---|
| Timelines: | family | ancestors | descendants | both | h7-degraded |
| Files: | files | file ages | folders |
| SHA3-256: |
464b82c888084e65fec7bea9864e4aba |
| User & Date: | dmestas on 2026-07-20 04:37:48.413 |
| Original Comment: | Prove sync liveness under a degraded, never-healed wire
The sync sweep proved convergence only once the network fully healed (every fault probability to zero), so a protocol that converges on a perfect wire but livelocks under sustained loss would still pass. Phase 2b runs a fresh session over a wire held at a fixed drop/dup rate that is never healed, and asserts the same convergence and termination oracles within a window scaled from the loss rate: expected rounds are the clean window over (1 - p_loss) squared per direction, times a safety factor, recomputed in a comment rather than left a magic number. No corruption is injected -- a corrupted body is already a modeled lost round. The protocol converges comfortably. Over 200 seeds the worst run took 7, 13, and 18 rounds at 10, 25, and 40 percent loss, against windows of 160, 228, and 356 -- no livelock surfaced. The gate joins at 10 percent so it stays fast and deterministic; the deeper soak sweeps the wider rate set. Pinning the window below the real convergence need trips the liveness oracle, so the check is not vacuous. The liveness-under-faults discipline follows TigerBeetle's VOPR. |
| Other Links: | branch diff | manifest | tags |
|
2026-07-20
| ||
| 04:43 |
Compute the degraded liveness window without catch unreachable
The loss-scaled convergence window used divCeil with a catch unreachable for the divide-by-zero arm, which the precommit guard flags outside tests. The delivered-percent denominator is provably at least one, so plain integer ceil division gives the same bound with no error union. closed check-in: 0fbc9225bf user: dmestas tags: h7-degraded | |
| 04:37 |
Prove sync liveness under a degraded, never-healed wire
The sync sweep proved convergence only after the network fully healed, so a protocol that converges on a perfect wire but livelocks under sustained loss would still pass. Phase 2b runs a fresh session over a wire held at a fixed drop/dup rate, never healed, asserting the same convergence and termination oracles within a window scaled from the loss rate: expected rounds are the clean window over (1 - p_loss) squared per direction, times a safety factor, recomputed in a comment rather than a magic number. No corruption is injected -- a corrupted body is already a lost round. The protocol converges comfortably: over 200 seeds the worst run took 7, 13, and 18 rounds at 10, 25, and 40 percent loss, against windows of 160, 228, and 356 -- no livelock. The gate joins at 10 percent; the soak sweeps the wider rate set. Pinning the window below the real need trips the liveness oracle, so the check is not vacuous. The liveness-under-faults discipline follows TigerBeetle's VOPR. check-in: 464b82c888 user: dmestas tags: h7-degraded | |
| 04:28 |
Merge h2-checkout-dst: crash-test the working tree, and a finding it surfaces
The working tree -- the one place a version-control tool can lose a user's data -- had no crash simulation; only the log store did. A new faulty directory layer tears and freezes writes at a seeded crash point, and a sweep replays an update across every crash cut, reopens, and checks four invariants. Three hold: an untracked file the update must preserve is never touched, a crashed update recovers to its target through the undo journal, and the checkout record never names a check-in whose tree did not finish materializing. The fourth does not, and that is the point of the harness: the payload write lands in place rather than through the write-temp-and-rename the metadata already uses, so a crash mid-write can leave a managed file spliced from old and new bytes -- torn, but recoverable. The gate runs the three that hold; the fourth is pinned by a test asserting the splice IS produced, so it flips the day the write is made atomic. Crash-point enumeration follows TigerBeetle's storage model. check-in: 5401ce245f user: dmestas tags: trunk | |