docs: Redis/Valkey cluster-mode migration spec with mechanized fencing model - #3756
Draft
tlongwell-block wants to merge 5 commits into
Draft
docs: Redis/Valkey cluster-mode migration spec with mechanized fencing model#3756tlongwell-block wants to merge 5 commits into
tlongwell-block wants to merge 5 commits into
Conversation
added 5 commits
July 30, 2026 11:10
…g model Specifies the bb-public relay's migration from single-shard cluster-mode- disabled Valkey to a sharded cluster, in the house style of docs/git-on-object-storage.md and docs/multi-tenant-relay.md. The mechanized core is the fenced session directory key migration: the tunnel lease/generation pair must be renamed to share a hash slot, which is a live handoff of fencing authority under a rolling deploy. The TLA+ model (docs/spec/RedisClusterFencingMigration.tla) proves single-authority, generation-monotonicity, and one-way-door safety across the O->A->B-> backfill->C phase protocol; all five invariants are mutation-tested non-vacuous (5 mutants, each trips its intended invariant). The rest is gated engineering: split client architecture (deadpool cluster pool + separate RESP3 push_sender subscription client), sharded pub/sub as a sizing prerequisite (classic PUBLISH broadcasts to every node), the silently-partial SCAN in mesh discovery replaced by a scored-expiry index, and the staged ElastiCache mode change with cluster-mode=enabled named as irreversible. Inputs: Wren's deployed-source inventory and Dawn's migration-mechanics digs (channel buzz-redis-cluster-mode, thread 3440fed6). Co-authored-by: npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d <011987e296fd5006292d2f930b574be47c7801048d1983c46c425d3c95f0cffd@buzz.block.builderlab.xyz> Signed-off-by: npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d <011987e296fd5006292d2f930b574be47c7801048d1983c46c425d3c95f0cffd@buzz.block.builderlab.xyz>
…ot-rules corrections, drain fix) Review blockers from Wren (three: E1 deployment-gate assumption, compatible- mode cross-slot legality unsupported, proof-surface overclaim) and Dawn (two: CROSSSLOT enforced on single-shard cluster-enabled nodes falsifies the A/B-in- compatible premise; renew=PEXPIRE makes any temporal drain gate unsound). Spec: A2/A3 rewritten (declared-keys slot check, undeclared-KEYS prohibition, slot rules from compatible onward as working assumption + pre-G3 probe); migration reordered A->B->backfill->drain->C entirely in disabled mode with compatible after C; C-gate now participation-based (B renew-migrates old-key leases; observed-zero, never wait-a-TTL); per-phase operation table for all six directory ops; proof scope stated honestly (write-side under E1); Deployment Gate section discharging E1 with rollback matrix and phase gauge; 1.5.0 receipts (verified free single-node); prior-art section (Stripe, GitLab, BullMQ, Sidekiq, Grafana, ioredis #1842) with locality contract and executable cross-slot validator in G2; failure-modes table extended. Model: mode variable disabled/compatible/enabled with slot rules from compatible; MigrateB (renew-migrate, same generation); RollbackPhase + DowngradePod with drain + reverse-max-merge guards; EnterCompatible/ RevertCompatible/EnableCluster doors; Inv_ClusterSafe -> Inv_SlotRulesSafe. A's generation dual-write removed: mutation testing proved it redundant. TLC green (12636 states, 3637 distinct); 9 mutants (M1-M9) all killed by their intended invariants. Co-authored-by: npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d <011987e296fd5006292d2f930b574be47c7801048d1983c46c425d3c95f0cffd@buzz.block.builderlab.xyz> Signed-off-by: npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d <011987e296fd5006292d2f930b574be47c7801048d1983c46c425d3c95f0cffd@buzz.block.builderlab.xyz>
Header still said A dual-writes the generation (removed after mutation testing); acquire-section comment lumped O in with the both-keyspace scripts (O touches only the old pair, itself cross-slot). Comments only; TLC re-run green, state count unchanged. Co-authored-by: npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d <011987e296fd5006292d2f930b574be47c7801048d1983c46c425d3c95f0cffd@buzz.block.builderlab.xyz> Signed-off-by: npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d <011987e296fd5006292d2f930b574be47c7801048d1983c46c425d3c95f0cffd@buzz.block.builderlab.xyz>
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>
TLC halts at the first violation, so generated/distinct counts on the drain probe's PASS run vary with worker count and scheduling (9/8 at -workers 1, ~100/~45 at -workers 4 — Dawn measured 114/50). Removed the count from the run transcript and noted only the verdict is the check; exhaustive-pass counts remain deterministic and cited. Co-authored-by: npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d <011987e296fd5006292d2f930b574be47c7801048d1983c46c425d3c95f0cffd@buzz.block.builderlab.xyz> Signed-off-by: npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d <011987e296fd5006292d2f930b574be47c7801048d1983c46c425d3c95f0cffd@buzz.block.builderlab.xyz>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What
Formal spec + mechanized model for migrating the bb-public relay's Redis/Valkey usage to cluster mode, before the single engine core saturates (EngineCPUUtilization doubling ~every 3.5–4 days; ~8–10 days runway measured 2026-07-30).
docs/redis-cluster-mode.md— the spec, in the house style ofgit-on-object-storage.md/multi-tenant-relay.md: axioms, safety theorems, conformance gates, failure modes, implementation correspondence.docs/spec/RedisClusterFencingMigration.tla+.cfg— TLA+ model of the safety-critical core: live migration of the tunnel directory's fencing keys (lease + non-expiring generation counter) to hash-tagged names under a rolling deploy.Mechanized claims
TLC (with
-deadlock; the model has intended terminal states): no error, 4153 states / 1487 distinct. Invariants: single-authority (no two live leases per session across old+new keyspaces), generation monotonicity (no generation issued twice across the counter handoff), one-way-door safety (cluster mode enabled only after old-keyspace authority drained), plus TypeOK and lease-generation groundedness.All five invariant-bearing mutations trip their intended invariant (each run in isolation): dropped union checks (A and B variants), skipped max-merge (A and B variants), and a dropped phase gate into the final script version.
Key design facts encoded
cluster-mode=enabledis irreversible; compatible mode is the last revert point, and scaling/engine changes are blocked while in it.push_sendersubscription client (deadpool exposes no push hook — structural).SCANfails silently under cluster mode (random single-node routing) → replaced by a scored-expiry index with a completeness-asserting conformance test.rediscrate floor ≥ 1.4.1; dead-primary dispatch halt named as a residual failure mode on every released version.Provenance
Code pins at deployed commit
22be8bb35(imagesha-22be8bb). Inputs: Wren's deployed-source inventory and Dawn's migration-mechanics digs (channelbuzz-redis-cluster-mode). AWS facts verified viabb-public-operations-ro(auto-failover enabled, Multi-AZ enabled, Valkey 8.0.1).Draft until Tyler + Dawn + Wren review lands 9/10+.