From 56303ba8ead3d30a4f3d61b8b2895f160dd7a19c Mon Sep 17 00:00:00 2001 From: npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d <011987e296fd5006292d2f930b574be47c7801048d1983c46c425d3c95f0cffd@buzz.block.builderlab.xyz> Date: Thu, 30 Jul 2026 12:10:28 -0400 Subject: [PATCH] docs: drain-reachability probe (M10) + B->A rollback session-loss note MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Review round 2 (Dawn) found the safety model could not distinguish the B2 fix from its absence: unguarded ExpireOld lets the C-gate be discharged by luck, so deleting MigrateB left all invariants green. Added DrainSpec/Probe_NotC — TLC from the stall state (full-B fleet, live old-key lease, no spontaneous expiry) with inverted verdict semantics: violation proves C reachable (93/44); mutant M10 (MigrateB removed = round-1 behavior) stays green, making the round-1 bug permanently visible. Main safety model unchanged (12636/3637, M1-M9 all killed). Also per Dawn N1: rollback matrix now names B->A as dropping every migrated session (A renews the old key; nobody renews the migrated lease; renewer treats Lost as fatal) — liveness cost, prefer forward-fix. Co-authored-by: npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d <011987e296fd5006292d2f930b574be47c7801048d1983c46c425d3c95f0cffd@buzz.block.builderlab.xyz> Signed-off-by: npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d <011987e296fd5006292d2f930b574be47c7801048d1983c46c425d3c95f0cffd@buzz.block.builderlab.xyz> --- docs/redis-cluster-mode.md | 39 +++++++++++++- docs/spec/RedisClusterFencingMigration.tla | 54 +++++++++++++++++++ .../RedisClusterFencingMigrationDrain.cfg | 11 ++++ 3 files changed, 102 insertions(+), 2 deletions(-) create mode 100644 docs/spec/RedisClusterFencingMigrationDrain.cfg diff --git a/docs/redis-cluster-mode.md b/docs/redis-cluster-mode.md index bc36c9b4b0..b8ea26629b 100644 --- a/docs/redis-cluster-mode.md +++ b/docs/redis-cluster-mode.md @@ -364,6 +364,17 @@ costs): - No phase rollback while in `compatible`; revert the mode to `disabled` first (the mode doors and phase machinery never move in the same step). + - **Rolling back B→A drops every session B has already migrated — + prefer forward-fix.** An A-pod's renew addresses the *old* key + (§Per-phase operation table), so a lease `MigrateB` moved to the new + key is renewed by nobody after the downgrade: it dies within one TTL + and the renewer treats the loss as fatal (session torn down, verified + live against `spawn_lease_renewer_with_interval`'s `Lost` handling). + Safety is unaffected — A's union check sees the new-key lease and + refuses to fork — but rollback from B is **not free**, and an + operator reaching for it should expect to shed exactly the sessions + the migration had already carried forward. (Liveness, so outside the + safety model's scope; found and reproduced live by review round 2.) 5. **Pre-G3 checklist:** compute `CLUSTER KEYSLOT` on both members of a real hash-tagged pair and require equality **before** entering compatible — a mis-tagged pair is invisible in disabled mode (slot @@ -421,6 +432,11 @@ $ java -cp tla2tools.jar tlc2.TLC RedisClusterFencingMigration.tla \ -config RedisClusterFencingMigration.cfg -deadlock Model checking completed. No error has been found. 12636 states generated, 3637 distinct states found. + +$ java -cp tla2tools.jar tlc2.TLC RedisClusterFencingMigration.tla \ + -config RedisClusterFencingMigrationDrain.cfg -deadlock +Error: Invariant Probe_NotC is violated. # INVERTED verdict: this is PASS +93 states generated, 44 distinct states found. ``` (`-deadlock` disables deadlock reporting because the model has *intended* @@ -431,8 +447,9 @@ writers; a fourth adds no qualitatively new interleaving. Bounded check, mutation-shown non-vacuous — the standard claim for a TLC-checked safety spec.) -**Every invariant is non-vacuous by mutation** (9 mutants, each run in -isolation, all killed): +**Every invariant is non-vacuous by mutation** (10 mutants, each run in +isolation, each distinguished from the true model — M1–M9 by a violated +safety invariant, M10 by the drain probe's inverted verdict): | Mutation | Models the real bug | Trips | |---|---|---| @@ -445,6 +462,24 @@ isolation, all killed): | M7: rollback into O drops the reverse max-merge | O re-issues generations B already issued | `Inv_Monotonic` | | M8: rollback allowed past a running downgrade | skipped-phase rollback: O and B pods coexist | `Inv_SingleAuthority` | | M9: compatible entered without fleet fully on C | A/B cross-slot scripts meet live slot rules | `Inv_SlotRulesSafe` | +| M10: `MigrateB` deleted (round-1 behavior: B renews old-key leases instead of migrating) | migration stalls at the C-gate forever | `Probe_NotC` **stays green** (inverted verdict — see below) | + +M10 needs a word, because it defends a fix the safety invariants cannot +see. The safety model lets leases expire spontaneously (`ExpireOld` +unguarded) — correct as the adversarial worst case for safety, but for +*drain* it is the friendly best case: it lets the C-gate's +`oldOwner = None` be discharged by luck, so deleting `MigrateB` from +`Next` leaves all five safety invariants green (found by review round 2). +The **drain-reachability probe** (`DrainSpec` + +`RedisClusterFencingMigrationDrain.cfg`) closes the hole: it starts TLC in +the stall state (fleet fully on B, backfilled, one live B-pod owning an +old-key lease), removes spontaneous expiry (faithful to a lease whose +owner is alive and renewing — renew is `PEXPIRE`), and checks +`Probe_NotC == phase /= 3` with **inverted verdict semantics**: TLC +reporting the "invariant" *violated* proves C is *reachable* (pass, 93/44 +states); TLC green means the migration deadlocks at the gate forever. +With `MigrateB`: violated (C reachable). M10 (without it): green — the +exact round-1 bug, now permanently visible to the model. M4 is the operationally scary one: it is exactly "someone deploys the final script version early because everything looks green." M6–M8 are the price diff --git a/docs/spec/RedisClusterFencingMigration.tla b/docs/spec/RedisClusterFencingMigration.tla index 0e9d4cd590..676b8ae212 100644 --- a/docs/spec/RedisClusterFencingMigration.tla +++ b/docs/spec/RedisClusterFencingMigration.tla @@ -343,4 +343,58 @@ Inv_LeaseGenGrounded == /\ (oldOwner /= None) => (oldLeaseGen > 0 /\ oldLeaseGen <= oldGen) /\ (newOwner /= None) => (newLeaseGen > 0 /\ newLeaseGen <= newGen) +(***************************************************************************) +(* Drain-reachability probe (spec S:B2 defense; found in review round 2). *) +(* *) +(* The safety model above lets ExpireOld/ExpireNew fire unguarded — the *) +(* adversarial worst case for SAFETY (leases may vanish at any moment). *) +(* But for DRAIN it is the friendly best case: an old-key lease whose *) +(* owner is alive and renewing never expires (renew is PEXPIRE — the exact *) +(* premise B2 falsified), so unguarded expiry lets the C-gate's *) +(* oldOwner = None conjunct be discharged by luck. Consequence: deleting *) +(* MigrateB from Next leaves every safety invariant green — the model *) +(* could not tell the B2 fix from its absence (found by Dawn, round 2). *) +(* *) +(* This probe closes that hole. DrainInit is the stall state: fleet fully *) +(* on B, backfill done, one live B-pod still owning an old-key lease. *) +(* DrainNext is Next WITHOUT spontaneous expiry — faithful to a lease *) +(* whose owner never crashes. Probe_NotC is checked as an "invariant" *) +(* with INVERTED verdict semantics: TLC reporting Probe_NotC VIOLATED *) +(* proves phase C is REACHABLE from the stall state (pass); TLC GREEN *) +(* means the migration deadlocks at the C-gate forever (fail). Run with *) +(* RedisClusterFencingMigrationDrain.cfg. Mutant M10 (drop MigrateB from *) +(* DrainNext = round-1 behavior, B renews the old key instead of *) +(* migrating) must leave this probe green — proving MigrateB is the only *) +(* mechanism that discharges the gate without luck. *) +(***************************************************************************) + +DrainInit == + /\ phase = 2 + /\ ver = [p \in Pods |-> 2] + /\ oldOwner = CHOOSE p \in Pods : TRUE + /\ oldLeaseGen = 1 + /\ newOwner = None /\ newLeaseGen = 0 + /\ oldGen = 1 /\ newGen = 1 + /\ backfilled = TRUE + /\ mode = 0 + /\ lastIssued = 1 + /\ monoOk = TRUE + +DrainNext == + \/ AdvancePhase + \/ RollbackPhase + \/ Backfill + \/ EnterCompatible + \/ RevertCompatible + \/ EnableCluster + \/ \E p \in Pods : UpgradePod(p) \/ DowngradePod(p) + \/ AcquireO(p) \/ AcquireA(p) \/ AcquireB(p) + \/ AcquireC(p) + \/ MigrateB(p) \* the B2 mechanism under test (M10) + +DrainSpec == DrainInit /\ [][DrainNext]_vars + +\* INVERTED verdict: a violation is the PASS (C reachable by participation). +Probe_NotC == phase /= 3 + ============================================================================= diff --git a/docs/spec/RedisClusterFencingMigrationDrain.cfg b/docs/spec/RedisClusterFencingMigrationDrain.cfg new file mode 100644 index 0000000000..0158550db2 --- /dev/null +++ b/docs/spec/RedisClusterFencingMigrationDrain.cfg @@ -0,0 +1,11 @@ +\* Drain-reachability probe (see module header of the Drain section). +\* INVERTED verdict: TLC reporting Probe_NotC VIOLATED = PASS (C reachable +\* from the stall state); TLC green = FAIL (migration deadlocks at the +\* C-gate). Mutant M10 removes MigrateB from DrainNext and must be green. +CONSTANTS + Pods = {p1, p2, p3} + None = None + MaxGen = 4 +SPECIFICATION DrainSpec +INVARIANTS + Probe_NotC