From 549fd58150ec55de2806a734052d8180fb1c81eb Mon Sep 17 00:00:00 2001 From: npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d <011987e296fd5006292d2f930b574be47c7801048d1983c46c425d3c95f0cffd@buzz.block.builderlab.xyz> Date: Thu, 30 Jul 2026 11:10:20 -0400 Subject: [PATCH 01/13] docs: Redis/Valkey cluster-mode migration spec with mechanized fencing 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> --- docs/redis-cluster-mode.md | 439 +++++++++++++++++++++ docs/spec/RedisClusterFencingMigration.cfg | 11 + docs/spec/RedisClusterFencingMigration.tla | 229 +++++++++++ 3 files changed, 679 insertions(+) create mode 100644 docs/redis-cluster-mode.md create mode 100644 docs/spec/RedisClusterFencingMigration.cfg create mode 100644 docs/spec/RedisClusterFencingMigration.tla diff --git a/docs/redis-cluster-mode.md b/docs/redis-cluster-mode.md new file mode 100644 index 0000000000..aff4cf514c --- /dev/null +++ b/docs/redis-cluster-mode.md @@ -0,0 +1,439 @@ +# Redis/Valkey Cluster Mode for the Buzz Relay: A Formal Specification + +`draft` + +## Abstract + +This document specifies the migration of the Buzz relay's Redis/Valkey usage +from a single-shard, cluster-mode-disabled ElastiCache replication group to a +cluster-mode-enabled, N-shard topology, and gives a formal proof of the +migration's safety-critical core. Valkey executes commands on one engine +thread per node; the deployed primary's engine core is the relay's hard +scaling ceiling, and it is filling on a measured doubling curve. Sharding the +keyspace across N primaries is the durable fix — **but only for keyed +commands**: classic pub/sub broadcasts every message to every node regardless +of shard count, so converting the relay's event fan-out to *sharded* pub/sub +(`SPUBLISH`/`SSUBSCRIBE`) is a prerequisite that feeds the sizing math, not a +migration detail. + +The safety-critical core is the **fenced session directory**: a per-session +`{lease, generation}` key pair mutated atomically by Lua, whose generation +counter is the relay mesh's fencing authority — non-expiring, never reset, +never forked. Cluster mode forces these keys into one hash slot, which forces +a key rename, which forces a live migration of fencing authority under a +rolling deploy. We prove three safety theorems over that migration — +**single-authority** (at no instant do two live leases exist for one session, +across both old and new keyspaces), **generation-monotonicity** (no generation +is ever issued twice across the counter handoff), and **one-way-door safety** +(cluster mode is enabled only after old-keyspace authority is provably +drained) — mechanized in TLA+ (`docs/spec/RedisClusterFencingMigration.tla`) +with every invariant shown non-vacuous by mutation. + +Everything else in the migration is specified as ordered, gated engineering +work with named failure modes: the split client architecture, the sharded +pub/sub conversion, the silently-wrong `SCAN` in mesh peer discovery, and the +staged ElastiCache mode change whose final step is irreversible. + +## Scope and Non-Goals + +This specification proves **safety** of the fencing-key migration and states +the rest of the migration as gated obligations. It deliberately does **not** +prove: + +- **Liveness or performance.** That N shards hold the growth curve, or that + resharding completes within a window, is empirical — characterized by the + profiling gate (G0) and load tests, not by theorem. +- **Shard count.** The shardable-keyspace vs. unshardable-broadcast ratio is + an unmeasured input (§Open Decisions, D1). Committing a shard count before + the profile exists would be fiction with units. +- **redis-rs / deadpool-redis / ElastiCache internals.** The cluster client's + MOVED/ASK routing, RESP3 push delivery, and ElastiCache's online resharding + are trusted vendor components, admitted per-deployment by conformance gates + (§Conformance), not reproven. +- **Valkey cluster correctness.** Hash-slot assignment (CRC16 mod 16384, hash + tags), single-slot Lua atomicity, and slot migration semantics are stated + as axioms with documentation cites. + +Stating this boundary is part of the claim, in the house style of +`docs/git-on-object-storage.md`: "provably safe migration" without naming the +trust boundary does not survive scrutiny; "the fencing handoff is +machine-checked relative to four stated axioms, and every vendor behavior is +gated by an explicit conformance test" does. + +## Problem Statement (measured, 2026-07-30) + +ElastiCache replication group `buzz-001` (acct 433851229429, us-west-2): +Valkey 8.0.1, `cache.r7g.8xlarge`, 1 primary + 1 replica, cluster mode +disabled, auto-failover **enabled**, Multi-AZ **enabled** (verified via +`describe-replication-groups` / `describe-cache-clusters`, +profile `bb-public-operations-ro`). + +- `EngineCPUUtilization` (primary): 0.3% (Jul 21) → 8.4% (Jul 27) → 19.2% + (Jul 30) — doubling every ~3.5–4 days. Saturation in ~8–10 days if the + curve holds. +- Driver is command volume: get/set/eval families each ~150x in two weeks, + pub/sub ~400x. Product growth (~80k users added), not a leak. +- Whole-instance CPU ~4%, memory 0.09%, replication lag <1ms. Vertical + scaling is dead: same-family bigger instances have identical single-core + speed; r8g (Graviton4) buys ~25–30% single-thread ≈ 1.5 days at the current + doubling rate. + +## System Model + +A **relay pod** is stateless compute (15 pods, HPA to 25). All pods share one +Redis endpoint through two client surfaces (today): a `deadpool-redis` +command pool built from one URL (`crates/buzz-relay/src/main.rs`), and three +dedicated single-node pub/sub subscriber connections +(`crates/buzz-pubsub/src/{subscriber,cache_invalidation,conn_control}.rs`). + +The relay's Redis state divides into **families with distinct consistency +obligations**. Making this distinction explicit is load-bearing for the whole +design; the two Lua-fenced keys and the discovery index must not be held to +the same standard: + +| Family | Keys | Obligation | Cluster-mode status | +|---|---|---|---| +| **Fencing directory** | `buzz::tunnel::{lease,generation}` (`tunnel/directory.rs`) | **Strict**: atomic two-key Lua; generation is non-expiring fencing authority — never fork, never repeat | **Blocker (loud)**: keys share no hash tag; every script fails cross-slot. Migration is the mechanized core of this spec | +| **Mesh ready registry** | `mesh:ready:` + `SCAN` discovery (`relay-mesh/registry.rs`) | **Hint, by its own contract** (`registry.rs:3-6`): entries are membership hints; the fenced directory arbitrates ownership. Bounded-staleness discovery is in-contract | **Blocker (silent)**: `SCAN` has no key, routes to one random node, returns a partial keyspace with no error | +| **Presence** | `buzz::presence:`, TTL 90s (`presence.rs`) | Ephemeral, self-healing | Safe: single-key ops; bulk `MGET` is auto-split per node by redis-rs (`MultipleNodeRoutingInfo::MultiSlot`, `cluster_handling/routing.rs`) | +| **Replay guard / rate limit** | `SET NX EX` (`nip98_replay.rs`); single-key Lua (`rate_limiter.rs`) | Per-key atomic | Safe once routed | +| **Event pub/sub** | `buzz::channel:`, `buzz::global` — exact topics (`topic.rs`) | At-most-once transport hint; relay re-checks access on fan-out | **Unsharded by default** (Axiom A4). Exact topics convert to `SSUBSCRIBE`/`SPUBLISH`; conversion is prerequisite P2 | +| **Broadcast pub/sub** | `PSUBSCRIBE buzz:*:cache-invalidate`, `buzz:*:conn-control` | Must-not-miss control signals (cache coherence, live bans) | No sharded equivalent (`SPSUBSCRIBE` does not exist). **Decision D2**: stays classic — a missed transition is worse than a low-volume broadcast | + +Command inventory provenance: deployed image `sha-22be8bb` = Buzz commit +`22be8bb35`, scoped `git grep` over `crates/buzz-pubsub`, `crates/buzz-relay`, +`crates/buzz-relay-mesh`; no `MULTI`/`EXEC`/pipeline found in that scope +(`RESEARCH/BB_PUBLIC_REDIS_CLUSTER_MODE_INVENTORY.md`). The two hot event-path +caches (`channel_visibility_cached`, `is_member_cached`) are in-process, not +Redis — they are not the get/set driver. + +## Axioms + +- **(A1) Deterministic slot assignment.** A key's slot is `CRC16(key) mod + 16384`; if the key contains a `{...}` hash tag, only the tagged substring is + hashed. Two keys sharing a tag always share a slot, on every topology. + (Valkey cluster spec, key distribution model.) +- **(A2) Single-slot Lua atomicity.** A Lua script whose declared `KEYS` all + map to one slot executes atomically on that slot's primary, exactly as on a + standalone node. A script whose keys span slots is **rejected** (loud + failure). Scripts must declare all keys via `KEYS`; ours do. +- **(A3) Staged mode change.** ElastiCache supports `cluster-mode: disabled → + compatible → enabled`. In *compatible*, one shard speaks both protocols and + exposes a configuration endpoint; `compatible → disabled` is a supported + revert. **`enabled` is irreversible** ("Reverting this configuration is not + possible" — modify-cluster-mode.md). While *compatible*: scaling and + engine-version changes are blocked. +- **(A4) Classic pub/sub is broadcast.** `PUBLISH` to any node is propagated + to every node in the cluster; each node's engine thread processes every + message. Sharded pub/sub (`SPUBLISH`/`SSUBSCRIBE`) confines propagation to + the channel's slot owner. (cluster-spec.md §pub/sub; pubsub.md §sharded.) + +A3 and A4 are the two facts that shape the entire plan: A4 makes sharded +pub/sub a sizing prerequisite; A3 makes compatible mode the last revert point. + +## Client Architecture (the split) + +Verified constraints, from vendored `redis 1.2.4` / `deadpool-redis 0.23.0` +source: + +1. `ssubscribe`/`sunsubscribe`/cluster `subscribe` **require RESP3** + (`check_resp3!`, hard error on RESP2). We run RESP2 today. +2. The cluster async connection has **no `get_async_pubsub()` and no + `split()`** — push messages arrive via an mpsc `push_sender` handed to + `ClusterClientBuilder` at build time, and the client **auto-resubscribes** + after disconnect, emitting duplicate subscription-confirmation pushes. +3. `deadpool-redis`'s cluster `Manager` builds its client internally and + exposes **no push-sender hook** — subscriptions need their own client + regardless of protocol choice. +4. Protocol is **per-connection**, set by URL (`?protocol=resp3`) — the two + clients can run different protocols with no global switch. + +Therefore the target architecture is a **split**: + +- **Command pool**: `deadpool-redis` cluster pool (feature `cluster` → + `redis/cluster-async`) for all routed traffic — `GET`/`SET`/`MGET`/Lua/ + `SPUBLISH`. Protocol (RESP2 vs RESP3) is a **test-backed decision**, not a + forced rewrite: typed command APIs may remain source-compatible, but the + choice is admitted only by the conformance gate (G2), never assumed. +- **Subscription client**: a separate raw `ClusterClientBuilder` with + `push_sender` on RESP3, owning all three subscriber loops. The loops are + **rearchitected** around push delivery (the `select!`-over-`split()` shape + does not exist here); reconnect handling must tolerate auto-resubscribe and + duplicate `SSubscribe` pushes. + +**Version floor:** `redis` ≥ **1.4.1** (prefer current 1.5.0), for: +non-blocking replica connection repair (#2120, 1.4.0), cluster retry-backoff +clamp (#2158, 1.3.0), and READONLY-path sleep removal (#2223, 1.4.1). +**Residual failure mode, not a fixed bug:** on every released version, a +**dead primary halts dispatch** pending topology refresh. Any degradation +argument that assumes graceful behavior during primary loss is wrong; this +belongs in shard-count risk math (more shards = smaller blast radius but more +primaries that can die). `deadpool-redis 0.23`'s `redis` requirement (`^1.0.3`) +admits 1.5.0 without a deadpool bump; the floor is admitted only by +`cargo update -p redis --precise ` plus a full workspace test run. + +## The Fencing Migration (mechanized core) + +### Why it exists + +The directory's four Lua scripts (acquire/renew/release/validate) each +atomically touch `…:lease` and `…:generation`. Under cluster mode those keys +must share a slot (A1, A2), so they must be **renamed** to carry a shared hash +tag — e.g. `buzz:tunnel:{:}:lease` / `…:generation`. The +generation counter is deliberately non-expiring and is the mesh's fencing +authority (`directory.rs:1-6`): renaming it is a live handoff of authority +under a rolling deploy, where old-script and new-script pods coexist. Done +naively, two failure classes appear: **fork** (old-key lease and new-key lease +alive simultaneously — two owners for one session) and **generation reuse** +(new counter re-issues a generation the old counter already issued — a stale +frame passes the fence). + +### The protocol + +Script versions, deployed as a phased rollout where the fleet spans at most +two adjacent versions (the model enforces this): + +- **O (legacy, deployed today):** old keys only. +- **A:** acquire checks **both** lease keys (union check); lease still + written to the **old** key; generation issued as + `max(oldGen, newGen) + 1`, written to **both** counters. +- **B:** union lease check; lease written to the **new** (hash-tagged) key; + generation `max(oldGen, newGen) + 1` written to the **new** counter. + (A/B read old keys cross-slot, so phases A and B run **before** cluster + mode is enabled — in disabled or compatible mode, where cross-slot access + on a single shard is legal.) +- **Backfill (once, after full-B):** fold `oldGen` into `newGen` by max-merge. + Idempotent. +- **C:** new keys only. No cross-slot access exists anywhere. Gate into C: + backfill has run **and** no live old-key lease remains (operationally: wait + ≥ one lease TTL — 30s, `DEFAULT_LEASE_TTL` — after full-B). +- **Enable:** `cluster-mode=enabled` only when the whole fleet runs C. Old + keys become unreachable garbage; the fence never consults them again. + +Renew/release in A/B operate on whichever key the caller's lease names — +they never create authority, so acquire is where the proof lives. + +### Safety theorems + +> **T1 (Single Authority).** At every instant of the migration, at most one +> live lease exists per session across both keyspaces. +> +> **T2 (Generation Monotonicity).** Generations issued to leases are strictly +> increasing per session across the old→new counter handoff; no generation is +> ever issued twice. +> +> **T3 (One-Way-Door Safety).** Cluster mode is enabled only in states where +> old-keyspace authority is drained (backfill complete, no live old-key +> lease), so no post-enable execution ever consults a stale fencing key. + +**Proof sketch.** T1: every acquire version checks the union of both lease +keys before creating authority, and phase adjacency means no pod that skips a +keyspace coexists with a pod that writes it (O writes old and checks old; the +last old-writer, A, checks new; the first new-writer, B, checks old; C checks +new after old is drained). T2: A and B issue `max(oldGen,newGen)+1` and write +it to the counter(s) subsequent versions read, so the issue sequence is +strictly increasing regardless of which version issues; the backfill max-merge +makes C's counter dominate every generation ever issued. T3: the phase gate +into C requires `backfilled ∧ oldOwner = None`, and enable requires full-C. ∎ + +The sketch is not the proof; the model is. + +### Mechanized verification + +`docs/spec/RedisClusterFencingMigration.tla` models one session (sessions are +independent — per-session keys), 3 pods, phased deployment with per-pod +upgrade interleaving, TTL expiry, backfill, and the enable action. TLC checks +five invariants; the history variables (`lastIssued`, `monoOk`) encode T2 as a +single-run safety invariant. + +``` +$ java -cp tla2tools.jar tlc2.TLC RedisClusterFencingMigration.tla \ + -config RedisClusterFencingMigration.cfg -deadlock +Model checking completed. No error has been found. +4153 states generated, 1487 distinct states found. +``` + +(`-deadlock` disables deadlock reporting because the model has *intended* +terminal states — migration complete, or the MaxGen finiteness bound reached — +which TLC would otherwise report as errors. Pods = {p1,p2,p3}, MaxGen = 4. Three pods exercise every adjacent-version +race — old/old, old/new, new/new 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** (each mutant run in isolation): + +| Mutation | Models the real bug | Trips | +|---|---|---| +| M1: `AcquireB` drops the old-lease check | new-script pod ignores legacy leases → two owners | `Inv_SingleAuthority` | +| M2: `AcquireA` drops the new-lease check | old-keyspace writer ignores new leases during rollback/mixed fleet | `Inv_SingleAuthority` | +| M3: `AcquireB` issues `newGen+1` without max-merge | fresh counter re-issues generation 1 → stale frame passes fence | `Inv_Monotonic` | +| M4: phase gate into C dropped (no backfill/drain requirement) | C deployed while an old-key lease is live → C-pod acquires over it | `Inv_SingleAuthority` | +| M5: `AcquireA` bumps only `oldGen`, skips dual-write | B never learns A's issues → reuse | `Inv_Monotonic` | + +M4 is the operationally scary one: it is exactly "someone deploys the final +script version early because everything looks green." + +## Sharded Pub/Sub Conversion (prerequisite P2) + +By A4, shard count does not touch the ~400x pub/sub term; conversion does. + +- **Exact event topics** (`buzz::channel:`, + `buzz::global`) convert to `SSUBSCRIBE`/`SPUBLISH`. The existing + dynamic per-topic subscribe pattern maps directly (separate `SSUBSCRIBE` + calls may span slots). Note: hash-tagging is deliberately **not** applied to + topic names — each topic hashing to its own slot is what spreads + propagation cost across shards; a `{community}` tag would recreate the hot + node per community. +- **The two pattern subscribers stay classic** (Decision D2, argued in-thread + and accepted): enumerating concrete channels would require a new + subscribe-before-reachable / unsubscribe-after-last protocol with discovery + races, and for cache invalidation and live-ban control a missed transition + is strictly worse than a low-volume broadcast path. This accepts a + permanently unsharded broadcast channel, gated by a volume measurement (G0 + must confirm these two channels are noise; if they are not, D2 reopens). + +## Mesh Registry Discovery (the silent one) + +`scan_ready()` (`relay-mesh/registry.rs`) discovers peers by `SCAN MATCH +mesh:ready:* COUNT 100`. `SCAN` carries no key; redis-rs routes it to **one +random node** (`RouteBy::Undefined` → `SingleNodeRoutingInfo::Random`) and the +cursor legitimately reaches 0 on that node — so under cluster mode discovery +**silently returns a per-call-varying subset** of peers. No error is ever +raised. This is the only cluster-unsafe site that fails silently, and it must +be tested by asserting **completeness** against a multi-shard cluster, not by +checking for errors. + +**Fix:** replace keyspace scanning with a **scored-expiry index** in one slot: +heartbeat does `ZADD ` alongside the existing +`SET EX` record; discovery reads live-scored members, `MGET`s their records, +filters, and opportunistically prunes dead scores. Staleness becomes +*representable* (a score in the past) rather than an agreement property +between two structures. The registry's own contract makes this sound: entries +are **membership hints** — the fenced directory arbitrates ownership — and the +read path already skips missing/undecodable/unattested records by design. The +invariant is **bounded discoverability** (a live runtime is discoverable +within one heartbeat interval; no unauthenticated record is ever returned), +*not* set equality. The single-slot concentration clears on measured load: +one `ZADD` per runtime per 15s across 15–25 pods ≈ 1–2 ops/s, three orders +below the hot path — deployment-global, so re-check if fleet size explodes. + +**This spec is explicit that the registry's consistency obligations are +weaker than the tunnel directory's *by design*.** Holding both to the fencing +standard would gold-plate a hint; holding the fence to the hint standard +would corrupt sessions. (Table in §System Model.) + +## Migration Plan (gates, in order) + +**G0 — Profile the hot path** *(informs everything; owner: option-3 owner)*. +Attribute the 150x get/set and 400x pub/sub growth to code paths; measure the +shardable-vs-broadcast ratio (this is the shard-count input) and the two +pattern-subscriber volumes (gates D2). Known: in-process caches are not the +driver; suspects are presence and per-event rate-limiter Lua — hypothesis, +not finding. If the driver is the rate limiter, "batch it" is not available +(atomic per-event counter); volume reduction takes a different shape. + +**G1 — Code prerequisites** *(can start now, independent of G0)*: + 1. Fencing migration phases A→B→backfill→C per the mechanized protocol. + 2. Registry scored-expiry index replacing `SCAN`. + 3. Split client architecture + `redis` ≥ 1.4.1 + feature flags. + 4. Subscriber loops rearchitected (push_sender, RESP3, auto-resubscribe). + 5. Sharded pub/sub conversion for exact topics (D2 leaves patterns classic). + +**G2 — Conformance against a real multi-shard Valkey cluster** (test matrix +below). No date is committed before this compiles and passes. + +**G3 — `cluster-mode=compatible`** (revert available). Client cutover to the +configuration endpoint; validate under real traffic. No scaling/engine +changes while here (A3) — **the r8g tourniquet and this migration are +mutually exclusive in flight**; entering compatible forecloses the vertical +escape hatch for the duration. + +**G4 — `cluster-mode=enabled`** — **the one-way door** (A3). Requires: fleet +fully on C-scripts (T3 gate), G2/G3 green, and a key-size sanity pass (slots +holding items >256MB silently refuse to migrate; our 0.09% memory makes this +unlikely — "unlikely" is not "checked"). + +**G5 — Add shards** (online resharding). Do it **early**: AWS guidance says +keep CPU <80% during resharding — resharding is compute-intensive, and doing +it while the engine core saturates is the worst time. The countdown clock is +the argument for starting G1 now, not for heroics at 90%. + +**Fallback (curve outruns the plan):** replica read offload +(`buzz-001-002` idles at 7%) buys roughly one doubling. Note the coupling: in +cluster mode, replica reads lean on exactly the replica-repair path fixed in +redis-rs #2120/#2223, so the version floor is a prerequisite for the fallback +too, not just hygiene. + +## Conformance (test matrix, gate G2) + +Run against a real multi-shard Valkey 8 cluster (not a mock, not a single +node in cluster mode). Two verdict columns — **errors** and **silently +wrong** — because three of our bugs would pass an error-only harness: + +| Surface | Must verify | +|---|---| +| Routing | MOVED/ASK redirects under slot migration; TLS/auth on the configuration endpoint | +| Fencing scripts | Hash-tagged pairs execute atomically; cross-slot rejection observed for un-tagged pairs (negative test); per-node script cache / NOSCRIPT handling | +| Fencing migration | A/B/backfill/C staged deploy against live traffic in compatible mode; generation strictly increases across the handoff (assert, don't assume) | +| Presence `MGET` | Nil/order preservation when split per node | +| Registry index | **Completeness**: every live runtime discoverable within one heartbeat; assert against known population, not absence of errors | +| Subscriptions | RESP3 push delivery; dynamic ssubscribe/sunsubscribe; reconnect with auto-resubscribe; duplicate subscription-confirmation pushes handled; message routing correct across shards | +| Failure drills | Replica connection repair **under load** (the #2120 path); primary failover — characterize the dispatch halt window; both clients (command pool + subscription client) have independent recovery behavior — drill both | +| Protocol choice | Command pool compiled and integration-tested under its chosen protocol (RESP2 or RESP3) — admitted by test, never assumed | + +## Failure Modes (named, with dispositions) + +| Failure | Loud/Silent | Disposition | +|---|---|---| +| Cross-slot Lua (fencing keys, pre-fix) | Loud | Fixed by design (hash tag + mechanized migration) | +| `SCAN` partial discovery | **Silent** | Fixed by design (scored-expiry index); completeness-asserting test | +| Dead primary halts client dispatch pending topology refresh | Loud-ish (latency wall) | Residual on all redis-rs versions; goes in shard-count risk math; drilled in G2 | +| Missed cache-invalidate / conn-control message | Silent | Avoided by D2 (patterns stay classic broadcast) | +| Generation fork/reuse during migration | Silent (fence passes stale frame) | Excluded by T1/T2 (mechanized, mutation-tested) | +| Premature `enabled` | Irreversible | Excluded by T3 gate + A3 named as one-way door | +| >256MB items refuse slot migration | Silent (permanent imbalance) | Key-size pass at G4 | +| Resharding under CPU pressure | Loud | G5 scheduled early, <80% CPU rule | + +## Implementation Correspondence + +Code pins are at deployed commit `22be8bb35` (verified against image tag +`sha-22be8bb`); symbols, not line numbers, are normative after refactors. + +| Spec element | Code | +|---|---| +| Fencing scripts (acquire/renew/release/validate) | `crates/buzz-relay/src/tunnel/directory.rs` (`ACQUIRE_SCRIPT` etc.) | +| Fencing keys needing hash tag | `SessionKeys::new` (`directory.rs`) | +| Lease TTL (drain window for C-gate) | `DEFAULT_LEASE_TTL` = 30s (`directory.rs`) | +| Registry `SCAN` to replace | `scan_ready` (`relay-mesh/registry.rs`) | +| Registry heartbeat to extend with `ZADD` | `publish_ready` (`registry.rs`), `spawn_registry_heartbeat` (`runtime.rs`) | +| Exact topics for sharded pub/sub | `EventTopicKey::redis_channel` (`buzz-pubsub/src/topic.rs`) | +| Pattern subscribers staying classic | `cache_invalidation.rs`, `conn_control.rs` (`psubscribe`) | +| Subscriber loops to rearchitect | `subscriber.rs` (`get_async_pubsub` + `split`) | +| Presence bulk read (auto-split, no change) | `get_presence_bulk` (`presence.rs`) | +| Command pool construction | `deadpool_redis::Config::from_url` (`buzz-relay/src/main.rs`) | +| Feature flags to add | workspace `Cargo.toml` `redis`/`deadpool-redis` entries | + +## Open Decisions + +- **D1 — Shard count.** Blocked on G0's shardable/broadcast ratio. The spec + deliberately refuses a number until the ratio exists. +- **D2 — Pattern subscribers stay classic.** Accepted in design; re-opens + only if G0 shows their volume is non-trivial. +- **D3 — Command-pool protocol (RESP2 vs RESP3).** Test-backed decision at + G2; the split architecture makes it independent of the subscription + client's hard RESP3 requirement. +- **D4 — G0 ownership.** Profiling was kicked off as option 3; needs an + owner and telemetry access. It gates D1, so it is on the critical path for + shard count but *not* for starting G1. + +## Summary + +| Property | Status | Discharged by | +|---|---|---| +| Fencing single-authority (T1) | Proved | TLA+ model, mutation-tested | +| Generation monotonicity (T2) | Proved | TLA+ model, mutation-tested | +| One-way-door safety (T3) | Proved | Phase gate + A3, mechanized | +| Vendor cluster behaviors | Empirical | Conformance matrix (G2) | +| Sharded pub/sub necessity | Documented fact | Axiom A4 (Valkey cluster spec) | +| Shard count | **Open** | G0 profile (D1) | +| Timeline | ~8–10 days of runway at current doubling | G1 starts now; fallback = replica offload | diff --git a/docs/spec/RedisClusterFencingMigration.cfg b/docs/spec/RedisClusterFencingMigration.cfg new file mode 100644 index 0000000000..1eaea9e707 --- /dev/null +++ b/docs/spec/RedisClusterFencingMigration.cfg @@ -0,0 +1,11 @@ +CONSTANTS + Pods = {p1, p2, p3} + None = None + MaxGen = 4 +SPECIFICATION Spec +INVARIANTS + TypeOK + Inv_SingleAuthority + Inv_Monotonic + Inv_ClusterSafe + Inv_LeaseGenGrounded diff --git a/docs/spec/RedisClusterFencingMigration.tla b/docs/spec/RedisClusterFencingMigration.tla new file mode 100644 index 0000000000..e839bbcd57 --- /dev/null +++ b/docs/spec/RedisClusterFencingMigration.tla @@ -0,0 +1,229 @@ +------------------- MODULE RedisClusterFencingMigration ------------------- +(***************************************************************************) +(* Fencing-key migration for Redis cluster mode. *) +(* *) +(* The relay's tunnel session directory fences mesh frames with a *) +(* {lease, generation} key pair per session (tunnel/directory.rs). Under *) +(* cluster mode the pair must share a hash slot, which forces a key *) +(* RENAME. The generation key is deliberately non-expiring and is the *) +(* fencing authority: it must never fork (two live leases for one *) +(* session) and never go backward or repeat (a generation, once issued, *) +(* is never issued again for that session). *) +(* *) +(* This module models the staged migration: *) +(* version O (0): legacy scripts — old keys only, checks old lease. *) +(* version A (1): union lease check; lease written to OLD key; *) +(* generation = max(oldGen,newGen)+1 written to BOTH. *) +(* version B (2): union lease check; lease written to NEW key; *) +(* generation = max(oldGen,newGen)+1 written to NEW. *) +(* backfill: after full-B, fold oldGen into newGen (max-merge). *) +(* version C (3): new keys only (cluster-safe: no cross-slot reads). *) +(* enable: cluster mode enabled; old keys become unreachable. *) +(* *) +(* Rolling deploys mean adjacent versions coexist; the phase variable *) +(* enforces that the fleet spans at most versions {phase-1, phase}. *) +(* *) +(* One session is modeled; sessions are independent (per-session keys). *) +(***************************************************************************) +EXTENDS Naturals, FiniteSets + +CONSTANTS Pods, \* set of relay pods + None, \* model value: no lease owner + MaxGen \* finiteness bound on generation counters + +ASSUME None \notin Pods + +VARIABLES + phase, \* deployment target version, 0..3 + ver, \* [Pods -> 0..3], each pod's deployed script version + oldOwner, \* lease on OLD key: owner pod or None + oldLeaseGen, \* generation carried by the live old-key lease (0 if none) + newOwner, \* lease on NEW (hash-tagged) key: owner pod or None + newLeaseGen, \* generation carried by the live new-key lease (0 if none) + oldGen, \* OLD non-expiring generation counter + newGen, \* NEW non-expiring generation counter + backfilled, \* one-time oldGen -> newGen max-merge has run + clusterOn, \* cluster mode enabled (the one-way door) + lastIssued, \* history: highest generation ever issued to a lease + monoOk \* history flag: FALSE iff an issue was <= a prior issue + +vars == <> + +Max(a, b) == IF a > b THEN a ELSE b + +TypeOK == + /\ phase \in 0..3 + /\ ver \in [Pods -> 0..3] + /\ oldOwner \in Pods \cup {None} + /\ newOwner \in Pods \cup {None} + /\ oldLeaseGen \in 0..MaxGen + /\ newLeaseGen \in 0..MaxGen + /\ oldGen \in 0..MaxGen + /\ newGen \in 0..MaxGen + /\ backfilled \in BOOLEAN + /\ clusterOn \in BOOLEAN + /\ lastIssued \in 0..MaxGen + /\ monoOk \in BOOLEAN + +Init == + /\ phase = 0 + /\ ver = [p \in Pods |-> 0] + /\ oldOwner = None /\ oldLeaseGen = 0 + /\ newOwner = None /\ newLeaseGen = 0 + /\ oldGen = 0 /\ newGen = 0 + /\ backfilled = FALSE + /\ clusterOn = FALSE + /\ lastIssued = 0 + /\ monoOk = TRUE + +(***************************************************************************) +(* Deployment machinery. *) +(***************************************************************************) + +\* The fleet may only chase the current phase; a phase only advances when +\* every pod has reached it. Gate into C (phase 3): backfill has run AND no +\* live old-key lease remains (operationally: wait >= lease TTL after +\* full-B before deploying C). +AdvancePhase == + /\ phase < 3 + /\ \A p \in Pods : ver[p] = phase + /\ (phase = 2) => (backfilled /\ oldOwner = None) + /\ phase' = phase + 1 + /\ UNCHANGED <> + +UpgradePod(p) == + /\ ver[p] < phase + /\ ver' = [ver EXCEPT ![p] = phase] + /\ UNCHANGED <> + +\* One-time backfill after the whole fleet is on B: fold the old counter +\* into the new one. Idempotent max-merge. +Backfill == + /\ phase = 2 + /\ \A p \in Pods : ver[p] = 2 + /\ newGen' = Max(newGen, oldGen) + /\ backfilled' = TRUE + /\ UNCHANGED <> + +\* The one-way door. Only after the whole fleet runs C scripts (which +\* never touch old keys, so no cross-slot access exists to break). +EnableCluster == + /\ ~clusterOn + /\ phase = 3 + /\ \A p \in Pods : ver[p] = 3 + /\ clusterOn' = TRUE + /\ UNCHANGED <> + +(***************************************************************************) +(* Acquire, per script version. Each is one atomic Lua script. *) +(***************************************************************************) + +RecordIssue(g) == + /\ lastIssued' = Max(lastIssued, g) + /\ monoOk' = (monoOk /\ (g > lastIssued)) + +\* Version O (legacy, deployed today): old keys only. +AcquireO(p) == + /\ ver[p] = 0 + /\ oldOwner = None + /\ oldGen + 1 <= MaxGen + /\ oldGen' = oldGen + 1 + /\ oldOwner' = p /\ oldLeaseGen' = oldGen + 1 + /\ RecordIssue(oldGen + 1) + /\ UNCHANGED <> + +\* Version A: union lease check; lease still on OLD key; generation is +\* max-merged and written to BOTH counters. (The max-merge here is +\* load-bearing: without it, an A-pod acquiring after a B-pod re-issues a +\* generation B already issued — see mutation M5.) +AcquireA(p) == + /\ ver[p] = 1 + /\ oldOwner = None /\ newOwner = None + /\ LET g == Max(oldGen, newGen) + 1 IN + /\ g <= MaxGen + /\ oldGen' = g /\ newGen' = g + /\ oldOwner' = p /\ oldLeaseGen' = g + /\ RecordIssue(g) + /\ UNCHANGED <> + +\* Version B: union lease check; lease moves to the NEW key; generation +\* max-merged into the NEW counter. +AcquireB(p) == + /\ ver[p] = 2 + /\ oldOwner = None /\ newOwner = None + /\ ~clusterOn \* B reads old keys: cross-slot, pre-cluster only + /\ LET g == Max(oldGen, newGen) + 1 IN + /\ g <= MaxGen + /\ newGen' = g + /\ newOwner' = p /\ newLeaseGen' = g + /\ RecordIssue(g) + /\ UNCHANGED <> + +\* Version C: new keys only. Cluster-safe. +AcquireC(p) == + /\ ver[p] = 3 + /\ newOwner = None + /\ newGen + 1 <= MaxGen + /\ newGen' = newGen + 1 + /\ newOwner' = p /\ newLeaseGen' = newGen + 1 + /\ RecordIssue(newGen + 1) + /\ UNCHANGED <> + +(***************************************************************************) +(* Lease loss: TTL expiry or explicit release. Generations survive. *) +(***************************************************************************) + +ExpireOld == + /\ oldOwner /= None + /\ oldOwner' = None /\ oldLeaseGen' = 0 + /\ UNCHANGED <> + +ExpireNew == + /\ newOwner /= None + /\ newOwner' = None /\ newLeaseGen' = 0 + /\ UNCHANGED <> + +Next == + \/ AdvancePhase + \/ EnableCluster + \/ Backfill + \/ ExpireOld + \/ ExpireNew + \/ \E p \in Pods : UpgradePod(p) \/ AcquireO(p) \/ AcquireA(p) + \/ AcquireB(p) \/ AcquireC(p) + +Spec == Init /\ [][Next]_vars + +(***************************************************************************) +(* Safety invariants. *) +(***************************************************************************) + +\* T1: fencing authority never forks — at most one live lease per session +\* across BOTH keyspaces, at every instant of the migration. +Inv_SingleAuthority == oldOwner = None \/ newOwner = None + +\* T2: generations are strictly monotonic per session — no generation is +\* ever issued twice, across the old/new counter handoff. +Inv_Monotonic == monoOk + +\* T3: the one-way door is only crossed with no old-keyspace authority +\* left: backfill done and no live old-key lease. (After this point C +\* scripts never read old keys, so any residual old-key state is inert.) +Inv_ClusterSafe == clusterOn => (backfilled /\ oldOwner = None) + +\* Sanity: a live lease always carries the generation its counter issued. +Inv_LeaseGenGrounded == + /\ (oldOwner /= None) => (oldLeaseGen > 0 /\ oldLeaseGen <= oldGen) + /\ (newOwner /= None) => (newLeaseGen > 0 /\ newLeaseGen <= newGen) + +============================================================================= From 2c7fdc55fa3be3eea4ed1908566583dc9c3fbdaa Mon Sep 17 00:00:00 2001 From: npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d <011987e296fd5006292d2f930b574be47c7801048d1983c46c425d3c95f0cffd@buzz.block.builderlab.xyz> Date: Thu, 30 Jul 2026 11:49:10 -0400 Subject: [PATCH 02/13] docs: fold review round 1 into cluster-mode spec (deployment gate, slot-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> --- docs/redis-cluster-mode.md | 430 ++++++++++++++++----- docs/spec/RedisClusterFencingMigration.cfg | 2 +- docs/spec/RedisClusterFencingMigration.tla | 200 +++++++--- 3 files changed, 498 insertions(+), 134 deletions(-) diff --git a/docs/redis-cluster-mode.md b/docs/redis-cluster-mode.md index aff4cf514c..bc36c9b4b0 100644 --- a/docs/redis-cluster-mode.md +++ b/docs/redis-cluster-mode.md @@ -23,11 +23,17 @@ never forked. Cluster mode forces these keys into one hash slot, which forces a key rename, which forces a live migration of fencing authority under a rolling deploy. We prove three safety theorems over that migration — **single-authority** (at no instant do two live leases exist for one session, -across both old and new keyspaces), **generation-monotonicity** (no generation -is ever issued twice across the counter handoff), and **one-way-door safety** -(cluster mode is enabled only after old-keyspace authority is provably -drained) — mechanized in TLA+ (`docs/spec/RedisClusterFencingMigration.tla`) -with every invariant shown non-vacuous by mutation. +across both old and new keyspaces, including under emergency rollback), +**generation-monotonicity** (no generation is ever issued twice across the +counter handoff or a rollback re-merge), and **slot-rules safety** (cluster +protocol modes are entered only after old-keyspace authority is provably +drained and the fleet runs only slot-clean scripts) — mechanized in TLA+ +(`docs/spec/RedisClusterFencingMigration.tla`) with every invariant shown +non-vacuous by mutation (9 mutants, all killed). The proof is scoped +precisely: it covers acquisition authority, generation issuance, lease +migration, and the mode doors, under a **deployment-gate assumption (E1) +that must be discharged operationally** — it is *not* a property of our +Kubernetes rollout machinery (§Deployment Gate). Everything else in the migration is specified as ordered, gated engineering work with named failure modes: the split client architecture, the sharded @@ -113,16 +119,38 @@ Redis — they are not the get/set driver. 16384`; if the key contains a `{...}` hash tag, only the tagged substring is hashed. Two keys sharing a tag always share a slot, on every topology. (Valkey cluster spec, key distribution model.) -- **(A2) Single-slot Lua atomicity.** A Lua script whose declared `KEYS` all - map to one slot executes atomically on that slot's primary, exactly as on a - standalone node. A script whose keys span slots is **rejected** (loud - failure). Scripts must declare all keys via `KEYS`; ours do. -- **(A3) Staged mode change.** ElastiCache supports `cluster-mode: disabled → - compatible → enabled`. In *compatible*, one shard speaks both protocols and - exposes a configuration endpoint; `compatible → disabled` is a supported - revert. **`enabled` is irreversible** ("Reverting this configuration is not - possible" — modify-cluster-mode.md). While *compatible*: scaling and - engine-version changes are blocked. +- **(A2) Single-slot Lua atomicity, declared-keys slot check.** A Lua script + whose declared `KEYS` all map to one slot executes atomically on that + slot's primary, exactly as on a standalone node. A script whose declared + keys span slots is **rejected with `CROSSSLOT`** (loud failure) on any + cluster-enabled node — **including a single-shard node that owns all + 16384 slots**: the check is on declared slot equality, not slot + ownership (falsified live: single-shard cluster-enabled node, all slots + assigned, `cluster_state:ok`, two-key `EVAL` on the un-tagged fencing + pair → `CROSSSLOT`; raw RESP, no client library involved). Scripts must + declare all keys via `KEYS`; ours do — and this is an **enforced + prohibition, not an observation**: keys accessed via `redis.call` but + not declared in `KEYS` bypass the slot check entirely and succeed on a + single shard, then break silently the moment slots split. That is the + deadline-pressure "fix" this spec explicitly forbids (verified live: + `numkeys=0` script reading a tagged + untagged key succeeds). The G2 + validator (§Conformance) mechanically rejects undeclared key access. +- **(A3) Staged mode change; slot rules start at compatible.** ElastiCache + supports `cluster-mode: disabled → compatible → enabled`. In *compatible*, + one shard speaks both protocols and exposes a configuration endpoint; + `compatible → disabled` is a supported revert. **`enabled` is + irreversible** ("Reverting this configuration is not possible" — + modify-cluster-mode.md). While *compatible*: scaling and engine-version + changes are blocked. **Working assumption: slot rules (A2's `CROSSSLOT` + rejection) are enforced from `compatible` onward** — compatible sets the + cluster-enabled parameter, and the OSS behavior A2 documents attaches to + cluster-enabled, not to shard count. We have not tested AWS compatible + mode itself (it could conceivably relax slot checks for + standalone-protocol clients); a one-command probe (`EVAL` on an + un-tagged two-key pair) is a **pre-G3 checklist item**, and even if AWS + turns out to permit it, the plan does not rely on that — vendor-tested + leniency is not a protocol property, and it would silently vanish at + `enabled`. - **(A4) Classic pub/sub is broadcast.** `PUBLISH` to any node is propagated to every node in the cluster; each node's engine thread processes every message. Sharded pub/sub (`SPUBLISH`/`SSUBSCRIBE`) confines propagation to @@ -161,16 +189,28 @@ Therefore the target architecture is a **split**: does not exist here); reconnect handling must tolerate auto-resubscribe and duplicate `SSubscribe` pushes. -**Version floor:** `redis` ≥ **1.4.1** (prefer current 1.5.0), for: +**Version floor:** `redis` ≥ **1.4.1** (target **1.5.0**), for: non-blocking replica connection repair (#2120, 1.4.0), cluster retry-backoff clamp (#2158, 1.3.0), and READONLY-path sleep removal (#2223, 1.4.1). **Residual failure mode, not a fixed bug:** on every released version, a **dead primary halts dispatch** pending topology refresh. Any degradation argument that assumes graceful behavior during primary loss is wrong; this belongs in shard-count risk math (more shards = smaller blast radius but more -primaries that can die). `deadpool-redis 0.23`'s `redis` requirement (`^1.0.3`) -admits 1.5.0 without a deadpool bump; the floor is admitted only by -`cargo update -p redis --precise ` plus a full workspace test run. +primaries that can die). **The 1.2.4 → 1.5.0 bump is verified free in the +current single-node world** (Dawn, on `origin/main` `73589408d`): +`cargo update -p redis --precise 1.5.0` resolves cleanly with no deadpool +bump and no other crate moved; `cargo build --workspace --all-targets` is +clean with zero source changes; all five redis-touching crates' tests pass +(buzz-core, buzz-pubsub, buzz-relay-mesh, buzz-admin, buzz-relay — 0 +failed), **including buzz-pubsub's 11 live-Redis `#[ignore]` tests** +(pub/sub roundtrip, cache invalidation, presence, nip98 replay, cross- +community isolation). The floor can therefore ship ahead of and +independently from the cluster work — one less thing moving during the +migration. That run proves nothing about cluster behavior (#2120/#2223 are +cluster-only paths); the multi-shard suite (G2) still owns those. One +additional known gap: async pub/sub reconnect fix redis-rs#2242 merged +*after* 1.5.0's release — G2 must force-disconnect the subscription client +and assert resubscription + delivery, never infer it from command tests. ## The Fencing Migration (mechanized core) @@ -190,51 +230,179 @@ frame passes the fence). ### The protocol -Script versions, deployed as a phased rollout where the fleet spans at most -two adjacent versions (the model enforces this): +Script versions, deployed as a phased rollout. **The fleet spanning at most +two adjacent versions is NOT something Kubernetes gives us — it is +environment assumption E1, discharged by the Deployment Gate below.** All of +O/A/B run in **`disabled` mode only**: A and B are cross-slot scripts, and +cross-slot access is illegal on *any* cluster-enabled topology including a +single shard (A2). There is no "compatible-mode grace period" for the +migration — compatible comes after C. - **O (legacy, deployed today):** old keys only. - **A:** acquire checks **both** lease keys (union check); lease still - written to the **old** key; generation issued as - `max(oldGen, newGen) + 1`, written to **both** counters. + written to the **old** key; generation issued as `max(oldGen, newGen) + 1`, + written to the old counter. (The union *read* of both counters is the + load-bearing part — mutation M5. An earlier draft also dual-wrote the + generation to the new counter; mutation testing showed that write + redundant, and it was removed: the smallest sufficient script wins.) - **B:** union lease check; lease written to the **new** (hash-tagged) key; generation `max(oldGen, newGen) + 1` written to the **new** counter. - (A/B read old keys cross-slot, so phases A and B run **before** cluster - mode is enabled — in disabled or compatible mode, where cross-slot access - on a single shard is legal.) -- **Backfill (once, after full-B):** fold `oldGen` into `newGen` by max-merge. - Idempotent. -- **C:** new keys only. No cross-slot access exists anywhere. Gate into C: - backfill has run **and** no live old-key lease remains (operationally: wait - ≥ one lease TTL — 30s, `DEFAULT_LEASE_TTL` — after full-B). -- **Enable:** `cluster-mode=enabled` only when the whole fleet runs C. Old - keys become unreachable garbage; the fence never consults them again. - -Renew/release in A/B operate on whichever key the caller's lease names — -they never create authority, so acquire is where the proof lives. + **B's renewer migrates**: when a B-pod's renew tick finds its own lease + still on the old key (acquired before the pod upgraded), it moves the + lease to the new key — same owner, **same generation** (no new issuance), + one atomic cross-slot Lua script, legal because we are in `disabled` + mode. This is what makes the drain *reachable* (see C-gate below). +- **Backfill (once, after full-B):** fold `oldGen` into `newGen` by + max-merge. Idempotent. +- **C:** new keys only. No cross-slot access exists anywhere. **C-gate + (participation-based, not temporal):** backfill has run **and** no live + old-key lease remains, verified **by direct observation** (count + old-keyspace leases = 0), *never* by waiting out a TTL. A fixed wait is + wrong on its face: `RENEW_SCRIPT` is `PEXPIRE` (`directory.rs`) on a 10s + cadence against the 30s TTL (`reliable.rs`), so a renewed lease **never + expires while its pod lives** — "wait one TTL after full-B" drains + nothing, and no session-lifetime bound exists in `tunnel/` or `audio/` + to save it. What actually drains the old keyspace: B-pods migrate their + own leases at the next renew tick (≤10s), and leases whose owners died + expire by TTL because nobody renews them. Full-B therefore implies + drain within bounded time — but the gate checks the *state*, not the + clock. (The huddle lane, `audio/join.rs`, mirrors the reliable lane's + 10s/30s renewer against the same directory and is expected to behave + identically; that expectation is read, not traced, and the G2 drill + covers both lanes explicitly.) +- **Enter compatible (G3):** only with the whole fleet on C. Slot rules + turn on here (A3); C is the only slot-clean script version. Revert to + `disabled` remains available. +- **Enable (G4):** `compatible → enabled` — the one-way door. Old keys + become unreachable garbage; the fence never consults them again. + +### Per-phase operation table + +"Renew/release operate on whichever key the caller's lease names" is not +implementable with today's `SessionLease` — it carries no keyspace +discriminator (`directory.rs`, `SessionLease` fields). The migration does +not add one: instead each script version has a **fixed, version-local key +rule**, and the table below is the normative statement per operation. A +pod always addresses the keyspace its own script version dictates; the one +cross-version case (a B-pod holding a lease acquired while it ran A-code +on the old key) is handled by B's renew-migrate, not by lease-carried +state. This version-local rule is an assumption the conformance suite +tests across pod termination and rollback, not something the type system +enforces. + +| Op | O | A | B | C | +|---|---|---|---|---| +| `acquire` | old key; `INCR` old ctr | union check; write old key; `max(old,new)+1` → old ctr | union check; write new key; `max(old,new)+1` → new ctr | new key; `INCR` new ctr | +| `renew` | old key `PEXPIRE` | old key `PEXPIRE` | **migrate-then-renew**: own lease on old key → move to new key (same gen, atomic); then new key `PEXPIRE` | new key `PEXPIRE` | +| `release` | old key | old key | try new key; fall back old key (owner+gen guarded, so wrong-key release is a no-op) | new key | +| `lookup` | old key | union (new wins) | union (new wins) | new key | +| `known_generation` | old ctr | `max(old, new)` ctrs | `max(old, new)` ctrs | new ctr | +| `validate_fenced_header` | old pair | union pair, `max` of counters | union pair, `max` of counters | new pair | + +`validate_fenced_header` is the hop-by-hop fence (`directory.rs`); its A/B +variants read both pairs in one cross-slot script (legal: disabled mode) +and fence against the max — a frame that passes validation under A/B +would pass under whichever single keyspace currently holds authority, +because T1 guarantees at most one does. + +### Scope of the mechanized proof + +The TLA+ model covers **acquisition authority, generation issuance, lease +migration (B's renew-migrate), lease loss, phase machinery including +emergency rollback, and the mode doors**. It does not model renew, release, +lookup, or validate as distinct transitions, and that is a scoping decision, +not an omission: + +- **renew** (TTL extension) is subsumed by the model's untimed + nondeterminism — a renewed lease is exactly one where `Expire` has not + yet fired. The renew-*migrate* step, which does change authority + location, **is** modeled (`MigrateB`). +- **release** is state-identical to expiry (lease loss, generation + preserved) — `Expire` covers both. +- **lookup / known_generation / validate** are read-only; they cannot + violate T1/T2. Their per-phase read rules (table above) are specified + and belong to the G2 test matrix. + +So the honest claim is: **T1/T2 are proved for every write to fencing +state, under assumption E1; the read-side per-phase rules are specified +and tested, not proved.** + +### Deployment Gate (discharging E1) + +The model's phase machinery assumes: the fleet chases one target phase, +a phase advances only when every pod runs it, and rollback never skips a +phase or overlaps a running downgrade. **Kubernetes gives none of this.** +bb-public deploys a plain `RollingUpdate` (`maxSurge: 1`, +`maxUnavailable: 0`) via GitOps; nothing prevents applying B while A is +still rolling, rolling back two phases at once, or a new ReplicaSet +coexisting with two older ones. E1 is therefore an **operational gate**, +with these rules (each maps to a mutation that shows what its absence +costs): + +1. **One image per phase.** Each of A, B, C is a separately released, + separately tagged image. No phase is a config flag on a shared image. +2. **Advance gate:** the next image change is blocked until (a) every + live pod reports the expected phase and (b) all older ReplicaSets are + at zero. Pods expose their script phase as a **metric/readiness fact** + (e.g. a `buzz_fencing_phase` gauge), so the gate checks *behavior*, + not an image tag. (Absence → mutants M1/M2-class forks: O+B coexist + and fork authority.) +3. **C-gate addition:** backfill complete **and** observed old-keyspace + lease count = 0 (direct observation, per §The protocol). (Absence → + M4.) +4. **Rollback matrix** (emergency path, modeled as `RollbackPhase`): + - Roll back **one adjacent phase at a time**; never start a second + rollback while pods are still above the current target (absence → + M8). + - Any rollback **invalidates the backfill**; it must re-run before the + C-gate can ever pass again. + - Rolling back past A into O additionally requires the **new keyspace + lease-drained** (observed zero; absence → M6) and an operator-run + **reverse max-merge** of the new counter into the old one — O issues + from the old counter alone and would otherwise re-issue generations + B already issued (absence → M7). + - No phase rollback while in `compatible`; revert the mode to + `disabled` first (the mode doors and phase machinery never move in + the same step). +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 + rules unenforced) and becomes a `CROSSSLOT` outage at G3. This is the + only point the bug is catchable cheaply. Also run the one-command AWS + compatible-mode probe from A3. ### Safety theorems -> **T1 (Single Authority).** At every instant of the migration, at most one -> live lease exists per session across both keyspaces. +> **T1 (Single Authority).** At every instant of the migration — including +> under emergency rollback — at most one live lease exists per session +> across both keyspaces. > > **T2 (Generation Monotonicity).** Generations issued to leases are strictly -> increasing per session across the old→new counter handoff; no generation is -> ever issued twice. +> increasing per session across the old→new counter handoff, the +> renew-migrate, and any rollback re-merge; no generation is ever issued +> twice. > -> **T3 (One-Way-Door Safety).** Cluster mode is enabled only in states where -> old-keyspace authority is drained (backfill complete, no live old-key -> lease), so no post-enable execution ever consults a stale fencing key. +> **T3 (Slot-Rules Safety).** A cluster-protocol mode (compatible or +> enabled) is entered only in states where old-keyspace authority is +> drained (backfill complete, no live old-key lease) and the whole fleet +> runs slot-clean C scripts — so no post-door execution ever attempts a +> cross-slot fencing script or consults a stale fencing key. That +> `enabled` is one-way is an environment axiom (A3), encoded as an action +> guard, not a theorem. + +All three hold **under environment assumption E1** (Deployment Gate). **Proof sketch.** T1: every acquire version checks the union of both lease -keys before creating authority, and phase adjacency means no pod that skips a -keyspace coexists with a pod that writes it (O writes old and checks old; the -last old-writer, A, checks new; the first new-writer, B, checks old; C checks -new after old is drained). T2: A and B issue `max(oldGen,newGen)+1` and write -it to the counter(s) subsequent versions read, so the issue sequence is -strictly increasing regardless of which version issues; the backfill max-merge -makes C's counter dominate every generation ever issued. T3: the phase gate -into C requires `backfilled ∧ oldOwner = None`, and enable requires full-C. ∎ +keys before creating authority; the renew-migrate moves a lease atomically +(delete-old and write-new in one script) so no interleaving observes two; +E1's phase adjacency means no pod that skips a keyspace coexists with a pod +that writes it. T2: A and B issue `max(oldGen,newGen)+1`; the migrate +carries an existing generation without issuing; the backfill max-merge makes +C's counter dominate every generation ever issued; the rollback reverse +max-merge restores that dominance to the old counter before O can issue +again. T3: the mode door requires `backfilled ∧ oldOwner = None ∧ fleet +fully C`, and phase rollback is disallowed while any cluster-protocol mode +is active. ∎ The sketch is not the proof; the model is. @@ -242,36 +410,48 @@ The sketch is not the proof; the model is. `docs/spec/RedisClusterFencingMigration.tla` models one session (sessions are independent — per-session keys), 3 pods, phased deployment with per-pod -upgrade interleaving, TTL expiry, backfill, and the enable action. TLC checks -five invariants; the history variables (`lastIssued`, `monoOk`) encode T2 as a -single-run safety invariant. +upgrade **and downgrade** interleaving, emergency rollback, TTL expiry, +B's renew-migrate, backfill, and the three-position mode variable +(disabled/compatible/enabled) with slot-rule enforcement from compatible +onward. TLC checks five invariants; the history variables (`lastIssued`, +`monoOk`) encode T2 as a single-run safety invariant. ``` $ java -cp tla2tools.jar tlc2.TLC RedisClusterFencingMigration.tla \ -config RedisClusterFencingMigration.cfg -deadlock Model checking completed. No error has been found. -4153 states generated, 1487 distinct states found. +12636 states generated, 3637 distinct states found. ``` (`-deadlock` disables deadlock reporting because the model has *intended* -terminal states — migration complete, or the MaxGen finiteness bound reached — -which TLC would otherwise report as errors. Pods = {p1,p2,p3}, MaxGen = 4. Three pods exercise every adjacent-version -race — old/old, old/new, new/new writers; a fourth adds no qualitatively new -interleaving. Bounded check, mutation-shown non-vacuous — the standard claim -for a TLC-checked safety spec.) +terminal states — migration complete, or the MaxGen finiteness bound reached +— which TLC would otherwise report as errors. Pods = {p1,p2,p3}, MaxGen = 4. +Three pods exercise every adjacent-version race — old/old, old/new, new/new +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** (each mutant run in isolation): +**Every invariant is non-vacuous by mutation** (9 mutants, each run in +isolation, all killed): | Mutation | Models the real bug | Trips | |---|---|---| | M1: `AcquireB` drops the old-lease check | new-script pod ignores legacy leases → two owners | `Inv_SingleAuthority` | | M2: `AcquireA` drops the new-lease check | old-keyspace writer ignores new leases during rollback/mixed fleet | `Inv_SingleAuthority` | | M3: `AcquireB` issues `newGen+1` without max-merge | fresh counter re-issues generation 1 → stale frame passes fence | `Inv_Monotonic` | -| M4: phase gate into C dropped (no backfill/drain requirement) | C deployed while an old-key lease is live → C-pod acquires over it | `Inv_SingleAuthority` | -| M5: `AcquireA` bumps only `oldGen`, skips dual-write | B never learns A's issues → reuse | `Inv_Monotonic` | +| M4: C-gate dropped (no backfill/drain requirement) | C deployed while an old-key lease is live → C-pod acquires over it | `Inv_SingleAuthority` | +| M5: `AcquireA` drops the union max-merge read | A never sees B's issues → reuse | `Inv_Monotonic` | +| M6: rollback into O drops the new-keyspace drain check | O-pod acquires on the old key while a B-era lease lives on the new key → fork | `Inv_SingleAuthority` | +| 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` | M4 is the operationally scary one: it is exactly "someone deploys the final -script version early because everything looks green." +script version early because everything looks green." M6–M8 are the price +of admitting that rollbacks happen; they are what the Deployment Gate's +rollback matrix discharges. Mutation testing also *removed* a mechanism: +A's dual-write of the generation counter survived every invariant when +deleted, so the protocol no longer carries it (§The protocol). ## Sharded Pub/Sub Conversion (prerequisite P2) @@ -324,6 +504,14 @@ would corrupt sessions. (Table in §System Model.) ## Migration Plan (gates, in order) +The ordering headline (changed from the first draft, per Dawn's live +falsification): **the entire fencing sequence A→B→backfill→drain→C happens +in `disabled` mode.** Compatible mode is not a grace period for cross-slot +work — slot rules are assumed live from compatible onward (A3). This is +strictly safer than the original ordering and costs nothing; it also means +the vertical escape hatch (r8g) stays available for the whole of G1, since +the scaling freeze only starts at G3. + **G0 — Profile the hot path** *(informs everything; owner: option-3 owner)*. Attribute the 150x get/set and 400x pub/sub growth to code paths; measure the shardable-vs-broadcast ratio (this is the shard-count input) and the two @@ -332,26 +520,35 @@ driver; suspects are presence and per-event rate-limiter Lua — hypothesis, not finding. If the driver is the rate limiter, "batch it" is not available (atomic per-event counter); volume reduction takes a different shape. -**G1 — Code prerequisites** *(can start now, independent of G0)*: - 1. Fencing migration phases A→B→backfill→C per the mechanized protocol. - 2. Registry scored-expiry index replacing `SCAN`. - 3. Split client architecture + `redis` ≥ 1.4.1 + feature flags. - 4. Subscriber loops rearchitected (push_sender, RESP3, auto-resubscribe). - 5. Sharded pub/sub conversion for exact topics (D2 leaves patterns classic). +**G1 — Code prerequisites, all in `disabled` mode** *(can start now, +independent of G0)*: + 1. `redis` 1.2.4 → 1.5.0 (verified free; ship first, separately). + 2. Fencing migration phases A→B→backfill→C per the mechanized protocol + and the Deployment Gate (one image per phase, phase metric, advance + gates, rollback matrix). + 3. Registry scored-expiry index replacing `SCAN`. + 4. Split client architecture + feature flags. + 5. Subscriber loops rearchitected (push_sender, RESP3, auto-resubscribe). + 6. Sharded pub/sub conversion for exact topics (D2 leaves patterns classic). **G2 — Conformance against a real multi-shard Valkey cluster** (test matrix -below). No date is committed before this compiles and passes. - -**G3 — `cluster-mode=compatible`** (revert available). Client cutover to the -configuration endpoint; validate under real traffic. No scaling/engine -changes while here (A3) — **the r8g tourniquet and this migration are -mutually exclusive in flight**; entering compatible forecloses the vertical -escape hatch for the duration. - -**G4 — `cluster-mode=enabled`** — **the one-way door** (A3). Requires: fleet -fully on C-scripts (T3 gate), G2/G3 green, and a key-size sanity pass (slots -holding items >256MB silently refuse to migrate; our 0.09% memory makes this -unlikely — "unlikely" is not "checked"). +below). The A/B/backfill/C staged deploy gets its own **disabled-mode +integration/chaos gate** (it can never legally run on a cluster-enabled +topology); everything else tests C-scripts on multi-shard. No date is +committed before this compiles and passes. + +**G3 — `cluster-mode=compatible`** (revert available). Entered only with +the fleet fully on C (T3). Pre-G3 checklist: `CLUSTER KEYSLOT` equality +assertion on a real tagged pair; the AWS compatible-mode cross-slot probe +(A3). Client cutover to the configuration endpoint; validate under real +traffic. No scaling/engine changes while here (A3) — **the r8g tourniquet +and compatible-onward are mutually exclusive in flight**; entering G3 +forecloses the vertical escape hatch for the duration. + +**G4 — `cluster-mode=enabled`** — **the one-way door** (A3). Requires: +G2/G3 green and a key-size sanity pass (slots holding items >256MB silently +refuse to migrate; our 0.09% memory makes this unlikely — "unlikely" is not +"checked"). **G5 — Add shards** (online resharding). Do it **early**: AWS guidance says keep CPU <80% during resharding — resharding is compute-intensive, and doing @@ -367,30 +564,39 @@ too, not just hygiene. ## Conformance (test matrix, gate G2) Run against a real multi-shard Valkey 8 cluster (not a mock, not a single -node in cluster mode). Two verdict columns — **errors** and **silently +node in cluster mode) — except the fencing-migration row, which by +construction runs on a standalone node (disabled mode is the only place +A/B legally execute). Two verdict columns — **errors** and **silently wrong** — because three of our bugs would pass an error-only harness: | Surface | Must verify | |---|---| | Routing | MOVED/ASK redirects under slot migration; TLS/auth on the configuration endpoint | -| Fencing scripts | Hash-tagged pairs execute atomically; cross-slot rejection observed for un-tagged pairs (negative test); per-node script cache / NOSCRIPT handling | -| Fencing migration | A/B/backfill/C staged deploy against live traffic in compatible mode; generation strictly increases across the handoff (assert, don't assume) | +| **Locality contract** | Atomic-looking work is never silently scattered: multi-key ops either share a slot or are explicitly per-key pipelines with partial-failure handling declared at the call site (the ioredis production resolution; Stripe's narrow-tag rule). A **GitLab-style executable cross-slot validator** in CI computes slots for every Lua `KEYS` declaration, pipeline, and multi-key command in the workspace, and rejects undeclared `redis.call` key access (A2's prohibition) | +| Fencing scripts | Hash-tagged pairs execute atomically; `CROSSSLOT` observed for un-tagged pairs (negative test); `CLUSTER KEYSLOT` equality asserted on real tagged pairs; per-node script cache / NOSCRIPT handling | +| Fencing migration | A/B/backfill/drain/C staged deploy against live traffic **on a standalone (disabled-mode) node** with chaos (pod kill mid-phase, rollback per the matrix, both tunnel lanes — reliable and huddle); generation strictly increases across the handoff and the renew-migrate (assert, don't assume); old-keyspace lease count observed to reach zero | | Presence `MGET` | Nil/order preservation when split per node | | Registry index | **Completeness**: every live runtime discoverable within one heartbeat; assert against known population, not absence of errors | -| Subscriptions | RESP3 push delivery; dynamic ssubscribe/sunsubscribe; reconnect with auto-resubscribe; duplicate subscription-confirmation pushes handled; message routing correct across shards | +| Subscriptions | RESP3 push delivery; dynamic ssubscribe/sunsubscribe; **forced disconnect** of the subscription client with asserted resubscription + delivery (redis-rs#2242 merged after 1.5.0 — never infer this from command tests); duplicate subscription-confirmation pushes handled; message routing correct across shards | | Failure drills | Replica connection repair **under load** (the #2120 path); primary failover — characterize the dispatch halt window; both clients (command pool + subscription client) have independent recovery behavior — drill both | | Protocol choice | Command pool compiled and integration-tested under its chosen protocol (RESP2 or RESP3) — admitted by test, never assumed | +| Telemetry | Per-shard/slot/channel metrics exist before G5: aggregate CPU cannot attribute a hot slot, and the phase gauge (`buzz_fencing_phase`) feeds the Deployment Gate | ## Failure Modes (named, with dispositions) | Failure | Loud/Silent | Disposition | |---|---|---| | Cross-slot Lua (fencing keys, pre-fix) | Loud | Fixed by design (hash tag + mechanized migration) | +| Mis-tagged fencing pair (looks fine in disabled mode) | **Silent until G3**, then loud outage | Pre-G3 `CLUSTER KEYSLOT` equality assertion; G2 validator | +| Undeclared `redis.call` key access (bypasses slot check) | **Silent** until slots split | Prohibited by A2; G2 validator rejects mechanically | +| Deployment gate breach (phase skip, overlapping rollback, early phase apply) | **Silent** (authority fork / generation reuse) | E1 discharged operationally (§Deployment Gate); mutants M6–M8 show the cost | +| Old-keyspace drain assumed temporal ("wait one TTL") | **Silent** (renew = `PEXPIRE`; renewed leases never expire) | C-gate is participation-based + observed-zero; B renew-migrates | | `SCAN` partial discovery | **Silent** | Fixed by design (scored-expiry index); completeness-asserting test | | Dead primary halts client dispatch pending topology refresh | Loud-ish (latency wall) | Residual on all redis-rs versions; goes in shard-count risk math; drilled in G2 | | Missed cache-invalidate / conn-control message | Silent | Avoided by D2 (patterns stay classic broadcast) | | Generation fork/reuse during migration | Silent (fence passes stale frame) | Excluded by T1/T2 (mechanized, mutation-tested) | -| Premature `enabled` | Irreversible | Excluded by T3 gate + A3 named as one-way door | +| Premature `compatible`/`enabled` | Loud (`CROSSSLOT`) / Irreversible | Excluded by T3 gate + A3 named as one-way door | +| Subscription client fails to resubscribe after disconnect | **Silent** (missed events) | Forced-disconnect drill in G2 (#2242 postdates 1.5.0) | | >256MB items refuse slot migration | Silent (permanent imbalance) | Key-size pass at G4 | | Resharding under CPU pressure | Loud | G5 scheduled early, <80% CPU rule | @@ -409,9 +615,49 @@ Code pins are at deployed commit `22be8bb35` (verified against image tag | Exact topics for sharded pub/sub | `EventTopicKey::redis_channel` (`buzz-pubsub/src/topic.rs`) | | Pattern subscribers staying classic | `cache_invalidation.rs`, `conn_control.rs` (`psubscribe`) | | Subscriber loops to rearchitect | `subscriber.rs` (`get_async_pubsub` + `split`) | +| Huddle-lane lease renewer (mirrors reliable lane; drilled in G2) | `audio/join.rs` | | Presence bulk read (auto-split, no change) | `get_presence_bulk` (`presence.rs`) | | Command pool construction | `deadpool_redis::Config::from_url` (`buzz-relay/src/main.rs`) | | Feature flags to add | workspace `Cargo.toml` `redis`/`deadpool-redis` entries | +| Phase gauge for the Deployment Gate | new metric (`buzz_fencing_phase`), exported per pod | + +## Prior Art (what this spec adopts, and from where) + +Three source-linked briefs inform this design (`RESEARCH/ +REDIS_CLUSTER_PRODUCTION_PRIOR_ART.md`, `…_OPEN_SOURCE_PRIOR_ART.md`, +`…_OPERATIONAL_PRIOR_ART.md`): + +- **Stripe** (brandur.org/redis-cluster): a single hot engine core at scale, + fixed by cluster mode with **narrow, entity-scoped hash tags** — adopted + as the per-session fencing tag and the no-`{community}`-tag rule for + topics. Their hardest part was hardening the client, not operating the + cluster; this spec's weight distribution (client architecture + G2 over + cluster ops) follows. +- **GitLab** (`multi_store.rb`, `redis_cluster_validator`): treats the move + as an application migration with an old/dual/new state machine and an + executable cross-slot validator — adopted as the O/A/B/C protocol shape + (with the fencing-specific monotonic-generation handling GitLab doesn't + need) and the G2 validator row. +- **BullMQ**: smallest-atomic-domain hash tags, spread across shards — + corroborates per-session tagging; its years of cluster-fix changelog is + the cautionary tale behind the version floor and G2's chaos rows. +- **Sidekiq** (negative prior art): refuses cluster configuration except a + narrow cluster-safe subsystem — adopted as the per-family obligations + table: cluster readiness is a capability boundary, not a client flag. +- **Grafana Alertmanager HA**: classic pub/sub coexisting with a cluster + client — supports D2 (patterns stay classic) as viable, while proving + nothing about fan-out capacity. +- **ioredis #1842** (maintainer resolution): the locality contract — atomic + work gets a narrow tag; unrelated multi-key work becomes per-slot + pipelines with *visible* partial-failure semantics — adopted verbatim as + the G2 locality row. +- **No published production precedent** exists for sharded pub/sub at + Buzz-like fan-out scale (searched; Stripe validates command sharding + only). The `SPUBLISH`/`SSUBSCRIBE` conversion therefore carries its own + Buzz-specific load/reconnect gate rather than an appeal to prior art. +- **AWS guidance** (modify-cluster-mode.md, online-resharding best + practices): compatible-as-revert-point (A3) and the <80% CPU resharding + rule (G5). ## Open Decisions @@ -430,10 +676,14 @@ Code pins are at deployed commit `22be8bb35` (verified against image tag | Property | Status | Discharged by | |---|---|---| -| Fencing single-authority (T1) | Proved | TLA+ model, mutation-tested | -| Generation monotonicity (T2) | Proved | TLA+ model, mutation-tested | -| One-way-door safety (T3) | Proved | Phase gate + A3, mechanized | +| Fencing single-authority (T1) | Proved (write-side, under E1) | TLA+ model, 9 mutants killed | +| Generation monotonicity (T2) | Proved (write-side, under E1) | TLA+ model, incl. rollback re-merge | +| Slot-rules safety (T3) | Proved (under E1) | Mode-door gate + A3, mechanized | +| Deployment gate E1 | **Operational obligation** | §Deployment Gate (phase images, advance gates, rollback matrix, phase metric) | +| Read-side per-phase rules (lookup/validate/renew/release) | Specified + tested | §Per-phase operation table; G2 | +| `redis` 1.2.4 → 1.5.0 | Verified free (single-node) | Dawn's build+test run on `73589408d`; cluster paths remain G2's | | Vendor cluster behaviors | Empirical | Conformance matrix (G2) | | Sharded pub/sub necessity | Documented fact | Axiom A4 (Valkey cluster spec) | +| Sharded pub/sub at scale | **No prior art** | Buzz-specific load/reconnect gate in G2 | | Shard count | **Open** | G0 profile (D1) | | Timeline | ~8–10 days of runway at current doubling | G1 starts now; fallback = replica offload | diff --git a/docs/spec/RedisClusterFencingMigration.cfg b/docs/spec/RedisClusterFencingMigration.cfg index 1eaea9e707..e4687250b9 100644 --- a/docs/spec/RedisClusterFencingMigration.cfg +++ b/docs/spec/RedisClusterFencingMigration.cfg @@ -7,5 +7,5 @@ INVARIANTS TypeOK Inv_SingleAuthority Inv_Monotonic - Inv_ClusterSafe + Inv_SlotRulesSafe Inv_LeaseGenGrounded diff --git a/docs/spec/RedisClusterFencingMigration.tla b/docs/spec/RedisClusterFencingMigration.tla index e839bbcd57..830d5ccbe4 100644 --- a/docs/spec/RedisClusterFencingMigration.tla +++ b/docs/spec/RedisClusterFencingMigration.tla @@ -16,12 +16,40 @@ (* generation = max(oldGen,newGen)+1 written to BOTH. *) (* version B (2): union lease check; lease written to NEW key; *) (* generation = max(oldGen,newGen)+1 written to NEW. *) +(* B's renewer MIGRATES any old-key lease it owns to the *) +(* new key (same generation, atomic pre-cluster Lua) — *) +(* this is what makes the old keyspace DRAIN by *) +(* participation instead of by hope: renew is PEXPIRE, *) +(* so a renewed lease never expires and no fixed wait *) +(* drains anything (spec S:B2). *) (* backfill: after full-B, fold oldGen into newGen (max-merge). *) -(* version C (3): new keys only (cluster-safe: no cross-slot reads). *) -(* enable: cluster mode enabled; old keys become unreachable. *) +(* version C (3): new keys only (cluster-safe: no cross-slot access). *) +(* mode: 0 = disabled, 1 = compatible, 2 = enabled. *) +(* SLOT RULES (CROSSSLOT rejection) are enforced from *) +(* mode 1 onward: "one shard owns all slots" grants no *) +(* cross-slot exemption (falsified live on a single-shard *) +(* cluster-enabled node — spec S:B1). O/A/B/migrate are *) +(* cross-slot scripts, so they are guarded on mode = 0; *) +(* under slot rules those scripts fail loudly and mutate *) +(* nothing. 1 -> 0 is a supported revert; 1 -> 2 is the *) +(* one-way door. *) (* *) -(* Rolling deploys mean adjacent versions coexist; the phase variable *) -(* enforces that the fleet spans at most versions {phase-1, phase}. *) +(* ENVIRONMENT ASSUMPTION E1 (deployment gate): the phase machinery below *) +(* — AdvancePhase requiring the whole fleet at the current phase, and *) +(* RollbackPhase requiring the downgrade to settle before rolling back *) +(* further — is NOT a property of Kubernetes RollingUpdate. It must be *) +(* discharged operationally (spec §Deployment Gate): one image per phase, *) +(* next image change blocked until all live pods report the expected *) +(* phase and old ReplicaSets are at zero, skipped-phase rollback *) +(* prohibited. Mutations M6–M8 show the invariants fail without E1. *) +(* *) +(* SCOPE OF PROOF: the model covers acquisition authority, generation *) +(* issuance, lease migration/loss, and the mode doors. Renew (TTL *) +(* extension) is subsumed by the untimed nondeterminism (a renewed lease *) +(* is one where Expire has not yet fired); release is subsumed by Expire *) +(* (both are lease loss without generation change); validate is read-only *) +(* and its per-phase read rule is specified and tested, not modeled *) +(* (spec §Per-phase operation table). *) (* *) (* One session is modeled; sessions are independent (per-session keys). *) (***************************************************************************) @@ -43,12 +71,12 @@ VARIABLES oldGen, \* OLD non-expiring generation counter newGen, \* NEW non-expiring generation counter backfilled, \* one-time oldGen -> newGen max-merge has run - clusterOn, \* cluster mode enabled (the one-way door) + mode, \* 0 = disabled, 1 = compatible, 2 = enabled (one-way) lastIssued, \* history: highest generation ever issued to a lease monoOk \* history flag: FALSE iff an issue was <= a prior issue vars == <> + oldGen, newGen, backfilled, mode, lastIssued, monoOk>> Max(a, b) == IF a > b THEN a ELSE b @@ -62,7 +90,7 @@ TypeOK == /\ oldGen \in 0..MaxGen /\ newGen \in 0..MaxGen /\ backfilled \in BOOLEAN - /\ clusterOn \in BOOLEAN + /\ mode \in 0..2 /\ lastIssued \in 0..MaxGen /\ monoOk \in BOOLEAN @@ -73,31 +101,60 @@ Init == /\ newOwner = None /\ newLeaseGen = 0 /\ oldGen = 0 /\ newGen = 0 /\ backfilled = FALSE - /\ clusterOn = FALSE + /\ mode = 0 /\ lastIssued = 0 /\ monoOk = TRUE (***************************************************************************) -(* Deployment machinery. *) +(* Deployment machinery (environment assumption E1 — see header). *) (***************************************************************************) \* The fleet may only chase the current phase; a phase only advances when \* every pod has reached it. Gate into C (phase 3): backfill has run AND no -\* live old-key lease remains (operationally: wait >= lease TTL after -\* full-B before deploying C). +\* live old-key lease remains. The drain conjunct is participation-based +\* (B migrates owned old-key leases; orphaned leases expire by TTL), NOT a +\* fixed wait — renew resets the TTL, so "wait one TTL" drains nothing. AdvancePhase == /\ phase < 3 /\ \A p \in Pods : ver[p] = phase /\ (phase = 2) => (backfilled /\ oldOwner = None) /\ phase' = phase + 1 /\ UNCHANGED <> + oldGen, newGen, backfilled, mode, lastIssued, monoOk>> UpgradePod(p) == /\ ver[p] < phase /\ ver' = [ver EXCEPT ![p] = phase] /\ UNCHANGED <> + oldGen, newGen, backfilled, mode, lastIssued, monoOk>> + +DowngradePod(p) == + /\ ver[p] > phase + /\ ver' = [ver EXCEPT ![p] = phase] + /\ UNCHANGED <> + +\* Emergency rollback: one adjacent phase at a time, only in disabled mode +\* (from compatible, revert the mode first), never past a running +\* downgrade (no pod may still be above the current target — dropping +\* this guard is mutation M8). Rolling back into O (phase 0) additionally +\* requires the new keyspace to be lease-drained (dropping this is M6) and +\* re-syncs the old counter by reverse max-merge: O issues from the old +\* counter alone, so without the merge it re-issues generations B already +\* issued (dropping the merge is M7). Every rollback conservatively +\* invalidates the backfill; it must re-run before the C-gate can pass. +RollbackPhase == + /\ phase > 0 + /\ mode = 0 + /\ \A p \in Pods : ver[p] <= phase + /\ IF phase = 1 + THEN /\ newOwner = None + /\ oldGen' = Max(oldGen, newGen) + ELSE UNCHANGED oldGen + /\ phase' = phase - 1 + /\ backfilled' = FALSE + /\ UNCHANGED <> \* One-time backfill after the whole fleet is on B: fold the old counter \* into the new one. Idempotent max-merge. @@ -107,20 +164,39 @@ Backfill == /\ newGen' = Max(newGen, oldGen) /\ backfilled' = TRUE /\ UNCHANGED <> + oldGen, mode, lastIssued, monoOk>> -\* The one-way door. Only after the whole fleet runs C scripts (which -\* never touch old keys, so no cross-slot access exists to break). -EnableCluster == - /\ ~clusterOn +(***************************************************************************) +(* Mode doors. Slot rules turn on at compatible (S:B1), so the whole *) +(* fleet must already run C — the only slot-clean script version. *) +(* compatible -> disabled is the supported revert; enabled is one-way. *) +(***************************************************************************) + +EnterCompatible == + /\ mode = 0 /\ phase = 3 /\ \A p \in Pods : ver[p] = 3 - /\ clusterOn' = TRUE + /\ mode' = 1 + /\ UNCHANGED <> + +RevertCompatible == + /\ mode = 1 + /\ mode' = 0 + /\ UNCHANGED <> + +EnableCluster == + /\ mode = 1 + /\ mode' = 2 /\ UNCHANGED <> (***************************************************************************) -(* Acquire, per script version. Each is one atomic Lua script. *) +(* Acquire, per script version. Each is one atomic Lua script. O, A, B *) +(* and the B-migrate touch both keyspaces (cross-slot), so they are *) +(* guarded on mode = 0: under slot rules they fail loudly and mutate *) +(* nothing, which the guard models by absence. *) (***************************************************************************) RecordIssue(g) == @@ -130,43 +206,66 @@ RecordIssue(g) == \* Version O (legacy, deployed today): old keys only. AcquireO(p) == /\ ver[p] = 0 + /\ mode = 0 /\ oldOwner = None /\ oldGen + 1 <= MaxGen /\ oldGen' = oldGen + 1 /\ oldOwner' = p /\ oldLeaseGen' = oldGen + 1 /\ RecordIssue(oldGen + 1) /\ UNCHANGED <> + mode>> \* Version A: union lease check; lease still on OLD key; generation is -\* max-merged and written to BOTH counters. (The max-merge here is -\* load-bearing: without it, an A-pod acquiring after a B-pod re-issues a -\* generation B already issued — see mutation M5.) +\* max-merged over BOTH counters but written only to the OLD one. (An +\* earlier draft dual-wrote the generation to both counters; mutation +\* testing showed the dual-write redundant — the mutant removing it +\* passes the full state space, because B's union max-merge read and the +\* backfill already carry A's issues forward. The max-merge READ is the +\* load-bearing part: dropping it is mutation M5.) AcquireA(p) == /\ ver[p] = 1 + /\ mode = 0 /\ oldOwner = None /\ newOwner = None /\ LET g == Max(oldGen, newGen) + 1 IN /\ g <= MaxGen - /\ oldGen' = g /\ newGen' = g + /\ oldGen' = g /\ oldOwner' = p /\ oldLeaseGen' = g /\ RecordIssue(g) - /\ UNCHANGED <> + /\ UNCHANGED <> \* Version B: union lease check; lease moves to the NEW key; generation \* max-merged into the NEW counter. AcquireB(p) == /\ ver[p] = 2 + /\ mode = 0 /\ oldOwner = None /\ newOwner = None - /\ ~clusterOn \* B reads old keys: cross-slot, pre-cluster only /\ LET g == Max(oldGen, newGen) + 1 IN /\ g <= MaxGen /\ newGen' = g /\ newOwner' = p /\ newLeaseGen' = g /\ RecordIssue(g) /\ UNCHANGED <> + mode>> + +\* Version B renew-migrate: a B-pod that still owns an old-key lease +\* (acquired before its upgrade) moves it to the new key at its next renew +\* tick — same owner, SAME generation (no new issuance; monotonicity is +\* untouched), atomic cross-slot Lua, legal only in disabled mode. The +\* script requires the new key empty; the counter is max-merged so the +\* moved lease stays grounded. This action is what discharges the C-gate's +\* oldOwner = None conjunct by participation. +MigrateB(p) == + /\ ver[p] = 2 + /\ mode = 0 + /\ oldOwner = p + /\ newOwner = None + /\ newOwner' = p /\ newLeaseGen' = oldLeaseGen + /\ newGen' = Max(newGen, oldLeaseGen) + /\ oldOwner' = None /\ oldLeaseGen' = 0 + /\ UNCHANGED <> -\* Version C: new keys only. Cluster-safe. +\* Version C: new keys only. Slot-clean; runs in every mode. AcquireC(p) == /\ ver[p] = 3 /\ newOwner = None @@ -175,32 +274,37 @@ AcquireC(p) == /\ newOwner' = p /\ newLeaseGen' = newGen + 1 /\ RecordIssue(newGen + 1) /\ UNCHANGED <> + mode>> (***************************************************************************) -(* Lease loss: TTL expiry or explicit release. Generations survive. *) +(* Lease loss: TTL expiry or explicit release (same state effect). *) +(* Generations survive. *) (***************************************************************************) ExpireOld == /\ oldOwner /= None /\ oldOwner' = None /\ oldLeaseGen' = 0 /\ UNCHANGED <> + backfilled, mode, lastIssued, monoOk>> ExpireNew == /\ newOwner /= None /\ newOwner' = None /\ newLeaseGen' = 0 /\ UNCHANGED <> + backfilled, mode, lastIssued, monoOk>> Next == \/ AdvancePhase - \/ EnableCluster + \/ RollbackPhase \/ Backfill + \/ EnterCompatible + \/ RevertCompatible + \/ EnableCluster \/ ExpireOld \/ ExpireNew - \/ \E p \in Pods : UpgradePod(p) \/ AcquireO(p) \/ AcquireA(p) - \/ AcquireB(p) \/ AcquireC(p) + \/ \E p \in Pods : UpgradePod(p) \/ DowngradePod(p) + \/ AcquireO(p) \/ AcquireA(p) \/ AcquireB(p) + \/ MigrateB(p) \/ AcquireC(p) Spec == Init /\ [][Next]_vars @@ -209,19 +313,29 @@ Spec == Init /\ [][Next]_vars (***************************************************************************) \* T1: fencing authority never forks — at most one live lease per session -\* across BOTH keyspaces, at every instant of the migration. +\* across BOTH keyspaces, at every instant of the migration, including +\* rollbacks. Inv_SingleAuthority == oldOwner = None \/ newOwner = None \* T2: generations are strictly monotonic per session — no generation is -\* ever issued twice, across the old/new counter handoff. +\* ever issued twice, across the old/new counter handoff and across +\* rollback re-merges. Inv_Monotonic == monoOk -\* T3: the one-way door is only crossed with no old-keyspace authority -\* left: backfill done and no live old-key lease. (After this point C -\* scripts never read old keys, so any residual old-key state is inert.) -Inv_ClusterSafe == clusterOn => (backfilled /\ oldOwner = None) +\* T3: slot rules (compatible or enabled) are only ever on with the old +\* keyspace fully drained and the whole fleet on slot-clean scripts — +\* so no post-door execution ever attempts a cross-slot fencing script, +\* and any residual old-key state is inert garbage. +Inv_SlotRulesSafe == + (mode >= 1) => /\ backfilled + /\ oldOwner = None + /\ phase = 3 + /\ \A p \in Pods : ver[p] = 3 + +\* The door is one-way: this is an axiom of the environment (A3), recorded +\* as an action guard (no transition leaves mode = 2), not an invariant. -\* Sanity: a live lease always carries the generation its counter issued. +\* Sanity: a live lease always carries a generation its counter dominates. Inv_LeaseGenGrounded == /\ (oldOwner /= None) => (oldLeaseGen > 0 /\ oldLeaseGen <= oldGen) /\ (newOwner /= None) => (newLeaseGen > 0 /\ newLeaseGen <= newGen) From 127bb17cf785a285e2ec1d15af4cdc1f68f954cd Mon Sep 17 00:00:00 2001 From: npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d <011987e296fd5006292d2f930b574be47c7801048d1983c46c425d3c95f0cffd@buzz.block.builderlab.xyz> Date: Thu, 30 Jul 2026 11:52:49 -0400 Subject: [PATCH 03/13] docs: fix two stale model comments from review round 2 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> --- docs/spec/RedisClusterFencingMigration.tla | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/docs/spec/RedisClusterFencingMigration.tla b/docs/spec/RedisClusterFencingMigration.tla index 830d5ccbe4..0e9d4cd590 100644 --- a/docs/spec/RedisClusterFencingMigration.tla +++ b/docs/spec/RedisClusterFencingMigration.tla @@ -13,7 +13,9 @@ (* This module models the staged migration: *) (* version O (0): legacy scripts — old keys only, checks old lease. *) (* version A (1): union lease check; lease written to OLD key; *) -(* generation = max(oldGen,newGen)+1 written to BOTH. *) +(* generation = max(oldGen,newGen)+1 written to OLD ctr *) +(* (an earlier draft dual-wrote both; mutation testing *) +(* proved the new-counter write redundant). *) (* version B (2): union lease check; lease written to NEW key; *) (* generation = max(oldGen,newGen)+1 written to NEW. *) (* B's renewer MIGRATES any old-key lease it owns to the *) @@ -193,10 +195,11 @@ EnableCluster == oldGen, newGen, backfilled, lastIssued, monoOk>> (***************************************************************************) -(* Acquire, per script version. Each is one atomic Lua script. O, A, B *) -(* and the B-migrate touch both keyspaces (cross-slot), so they are *) -(* guarded on mode = 0: under slot rules they fail loudly and mutate *) -(* nothing, which the guard models by absence. *) +(* Acquire, per script version. Each is one atomic Lua script. A, B and *) +(* the B-migrate touch both keyspaces; O touches only the old pair, but *) +(* that pair is itself cross-slot (un-tagged lease + generation keys). *) +(* All four are therefore guarded on mode = 0: under slot rules they fail *) +(* loudly and mutate nothing, which the guard models by absence. *) (***************************************************************************) RecordIssue(g) == 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 04/13] 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 From 34275c9b58c9ceed11c8e00edeb8b6d22d469a4b Mon Sep 17 00:00:00 2001 From: npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d <011987e296fd5006292d2f930b574be47c7801048d1983c46c425d3c95f0cffd@buzz.block.builderlab.xyz> Date: Thu, 30 Jul 2026 12:14:17 -0400 Subject: [PATCH 05/13] docs: drain-probe state counts are nondeterministic on violating runs MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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> --- docs/redis-cluster-mode.md | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/docs/redis-cluster-mode.md b/docs/redis-cluster-mode.md index b8ea26629b..06725f48ed 100644 --- a/docs/redis-cluster-mode.md +++ b/docs/redis-cluster-mode.md @@ -436,9 +436,14 @@ Model checking completed. No error has been 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. ``` +(State counts on the drain probe's violating run are **not reproducible**: +TLC halts at the first violation, so the count varies with worker count +and scheduling — 9/8 at `-workers 1`, ~100/~45 at `-workers 4`. Only the +verdict is the check. Exhaustive-pass counts, like the main model's +12636/3637 and M10's green run, are deterministic.) + (`-deadlock` disables deadlock reporting because the model has *intended* terminal states — migration complete, or the MaxGen finiteness bound reached — which TLC would otherwise report as errors. Pods = {p1,p2,p3}, MaxGen = 4. @@ -476,8 +481,9 @@ 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. +reporting the "invariant" *violated* proves C is *reachable* (pass; state +counts on a violating run vary with worker scheduling — the verdict is +the check); 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. From f1957c945c429ba80dda16052e877a4319519f77 Mon Sep 17 00:00:00 2001 From: tlongwell-block <109685178+tlongwell-block@users.noreply.github.com> Date: Thu, 30 Jul 2026 12:36:30 -0400 Subject: [PATCH 06/13] ci: machine-check the Redis cluster-mode TLA+ specs MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The drain-reachability probe (M10) guaranteed nothing mechanically: it was a documented procedure a reviewer had to remember to run. Deleting MigrateB leaves all five safety invariants green, so nothing in CI would have caught the round-1 bug coming back. scripts/check-tla-specs.sh runs both configs with opposite pass conditions: the safety model must complete with no violation, and the drain probe must report `Invariant Probe_NotC is violated` — a green drain run means phase C is unreachable from the stall state and fails the build. The inverted assertion greps the specific invariant name rather than checking TLC's exit status: a parse error or missing module also exits non-zero, and treating that as the expected violation would make the check useless exactly when the spec is broken. tla2tools is pinned by release tag and by sha256, since release assets can be re-uploaded. Verified in four directions on the committed script: unmodified specs exit 0; MigrateB stripped from DrainNext exits 1 via the green-drain branch; a spec that fails to parse exits 1 via the neither-verdict branch; a jar with the wrong checksum exits 1 before TLC runs. Runtime is ~3s including the jar download. The module allow-list is deliberately just RedisClusterFencingMigration, not a glob over docs/spec/*.cfg: MultiTenantRelay does not finish in a reasonable CI budget and GitOnObjectStore explores ~12.4M states, so attaching them to every PR would buy flakiness rather than safety. Co-authored-by: Dawn (sprout agent) Signed-off-by: tlongwell-block <109685178+tlongwell-block@users.noreply.github.com> --- .github/workflows/ci.yml | 22 +++++++ docs/redis-cluster-mode.md | 8 +++ scripts/check-tla-specs.sh | 119 +++++++++++++++++++++++++++++++++++++ 3 files changed, 149 insertions(+) create mode 100755 scripts/check-tla-specs.sh diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index d4826d985f..f03ab31389 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -27,6 +27,7 @@ jobs: desktop-rust: ${{ steps.filter.outputs.desktop-rust }} web: ${{ steps.filter.outputs.web }} mobile: ${{ steps.filter.outputs.mobile }} + spec: ${{ steps.filter.outputs.spec }} steps: - uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6 with: @@ -74,6 +75,10 @@ jobs: - 'scripts/test-mobile-worktree-overrides.sh' - '.github/workflows/mobile-release-candidate.yml' - '.github/workflows/ci.yml' + spec: + - 'docs/spec/**' + - 'scripts/check-tla-specs.sh' + - '.github/workflows/ci.yml' - name: Release workflow source contract run: scripts/test-release-ref-contract.sh - name: Mobile release contract @@ -882,6 +887,23 @@ jobs: fi echo "No dead token references found." + tla-specs: + name: TLA+ Spec Checks + runs-on: ubuntu-latest + timeout-minutes: 10 + needs: [changes] + if: github.event_name == 'push' || needs.changes.outputs.spec == 'true' + permissions: + contents: read + steps: + - uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6 + - uses: actions/setup-java@03ad4de0992f5dab5e18fcb136590ce7c4a0ac95 # v5.6.0 + with: + distribution: temurin + java-version: '17' + - name: Model-check TLA+ specs + run: scripts/check-tla-specs.sh + server-cross-compile: name: Server Cross-Compile runs-on: ubuntu-latest diff --git a/docs/redis-cluster-mode.md b/docs/redis-cluster-mode.md index 06725f48ed..5996d0309f 100644 --- a/docs/redis-cluster-mode.md +++ b/docs/redis-cluster-mode.md @@ -487,6 +487,14 @@ the check); 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. +Both configs run in CI (`scripts/check-tla-specs.sh`, job `TLA+ Spec +Checks`, triggered by `docs/spec/**`), so the inverted verdict is +machinery rather than discipline: the script asserts on the specific +string `Invariant Probe_NotC is violated` rather than on TLC's exit +status, because a parse error also exits non-zero and must fail the build +instead of counting as the expected violation. tla2tools is pinned by +release tag *and* sha256. Deleting `MigrateB` fails the job. + 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 of admitting that rollbacks happen; they are what the Deployment Gate's diff --git a/scripts/check-tla-specs.sh b/scripts/check-tla-specs.sh new file mode 100755 index 0000000000..c0ceba1d2d --- /dev/null +++ b/scripts/check-tla-specs.sh @@ -0,0 +1,119 @@ +#!/usr/bin/env bash +set -euo pipefail + +# Machine-check the TLA+ specs in docs/spec/ with TLC. +# +# Two kinds of check, with OPPOSITE pass conditions: +# +# 1. Safety models — TLC must complete with no invariant violation. +# 2. The drain-reachability probe (docs/redis-cluster-mode.md §Mechanized +# verification) — an INVERTED verdict. `Probe_NotC == phase /= 3` is +# checked as an "invariant" so that TLC reporting it VIOLATED proves the +# C phase is REACHABLE from the stall state. A green run means the +# migration deadlocks at the C-gate forever, which is the bug (mutant +# M10: MigrateB deleted). So green = FAIL here. +# +# The inverted assertion greps for the specific invariant name rather than +# "TLC exited non-zero": a parse error or a missing-module error also exits +# non-zero, and treating that as a pass would make this check useless exactly +# when the spec is broken. + +TLA_VERSION="v1.7.4" +TLA_SHA256="936a262061c914694dfd669a543be24573c45d5aa0ff20a8b96b23d01e050e88" +TLA_URL="https://github.com/tlaplus/tlaplus/releases/download/${TLA_VERSION}/tla2tools.jar" + +SPEC_DIR="docs/spec" +JAR="${TLA_JAR:-}" + +# Modules checked on every run. Deliberately a small allow-list, not a glob: +# the older specs in docs/spec/ have state spaces that run for many minutes +# (MultiTenantRelay does not finish inside a reasonable CI budget, and +# GitOnObjectStore explores ~12.4M states), so gluing them onto every PR would +# buy flakiness and queue time rather than safety. Add a module here only with +# a measured runtime. +SAFETY_MODULES=( + "RedisClusterFencingMigration" +) + +if [[ -z "$JAR" ]]; then + JAR="$(mktemp -d)/tla2tools.jar" + echo "Downloading tla2tools ${TLA_VERSION}..." + curl -sSL --retry 3 -o "$JAR" "$TLA_URL" +fi + +# Pin by content, not just by tag: release assets can be re-uploaded. +# sha256sum on Linux runners, shasum on macOS/dev machines. +if command -v sha256sum >/dev/null 2>&1; then + actual="$(sha256sum "$JAR" | cut -d' ' -f1)" +else + actual="$(shasum -a 256 "$JAR" | cut -d' ' -f1)" +fi +if [[ "$actual" != "$TLA_SHA256" ]]; then + echo "::error::tla2tools.jar checksum mismatch." >&2 + echo " expected $TLA_SHA256" >&2 + echo " actual $actual" >&2 + exit 1 +fi +echo "tla2tools ${TLA_VERSION} verified ($TLA_SHA256)" + +run_tlc() { + # $1 = module, $2 = config basename + ( cd "$SPEC_DIR" && java -XX:+UseParallelGC -cp "$JAR" tlc2.TLC \ + -deadlock -workers 4 -config "$2" "$1" 2>&1 ) +} + +failed=0 + +# ---- 1. Safety models: must be green. ------------------------------------- +for module in "${SAFETY_MODULES[@]}"; do + base="${module}.cfg" + if [[ ! -f "$SPEC_DIR/$base" ]]; then + echo "::error::missing config $SPEC_DIR/$base for module $module" + failed=1 + continue + fi + + echo "" + echo "=== $module ($base): expecting NO violation ===" + out="$(run_tlc "$module" "$base")" || true + + if grep -q "Model checking completed. No error has been found." <<<"$out"; then + grep -E "states generated" <<<"$out" | tail -1 || true + echo "PASS: $module" + else + echo "::error::$module ($base) did not complete cleanly." + grep -E "Error|Invariant .* is violated|violated" <<<"$out" | head -5 || true + failed=1 + fi +done + +# ---- 2. Drain-reachability probe: INVERTED verdict. ----------------------- +drain_cfg="$SPEC_DIR/RedisClusterFencingMigrationDrain.cfg" +if [[ -f "$drain_cfg" ]]; then + echo "" + echo "=== Drain-reachability probe: expecting Probe_NotC VIOLATED (= C reachable) ===" + out="$(run_tlc "RedisClusterFencingMigration" "RedisClusterFencingMigrationDrain.cfg")" || true + + if grep -q "Invariant Probe_NotC is violated" <<<"$out"; then + echo "PASS: phase C is reachable from the stall state (MigrateB discharges the C-gate)." + elif grep -q "Model checking completed. No error has been found." <<<"$out"; then + echo "::error::Drain probe is GREEN, which is a FAILURE under the inverted verdict." + echo "::error::Phase C is UNREACHABLE from the stall state: the migration would" + echo "::error::deadlock at the C-gate forever. This is mutant M10 — most likely" + echo "::error::MigrateB was removed or its guard broken. See" + echo "::error::docs/redis-cluster-mode.md §Mechanized verification." + failed=1 + else + # Neither verdict: parse error, missing module, bad config. Not a pass. + echo "::error::Drain probe produced neither verdict — TLC failed to run the check." + grep -E "Error" <<<"$out" | head -5 || true + failed=1 + fi +fi + +echo "" +if (( failed )); then + echo "TLA+ spec checks FAILED." + exit 1 +fi +echo "All TLA+ spec checks passed." From acfb537fbcc4a6c58a493b73c50fced8a5a0b82d Mon Sep 17 00:00:00 2001 From: npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d <011987e296fd5006292d2f930b574be47c7801048d1983c46c425d3c95f0cffd@buzz.block.builderlab.xyz> Date: Thu, 30 Jul 2026 13:36:08 -0400 Subject: [PATCH 07/13] docs: fold G0/P2 measured findings into pub/sub conversion and open decisions MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Dawn's G0 profile and P2 measurements (2026-07-30, receipts in RESEARCH/BB_PUBLIC_REDIS_G0_PROFILE.md and in-thread) landed three corrections to spec claims: - "per-topic slot spreading" overstated the spread unit: 87.8% of publish volume targets buzz::global (presence 60.8% + observer frames 27.0%), so the effective unit is per-community. Simulated hottest-shard imbalance ~1.5x fair share at 4 shards (p95) — D1 must not size by current/N. - P2 payoff is bounded by measured amplification (~5.3 pod-deliveries per publish on 15 pods), not worst-case broadcast. - D2 is now measured-closed (all pattern publishers lifecycle/admin-rate, ~10x margin), and D1 records its first inputs plus the honest caveat that per-family rate x latency explains under a quarter of engine CPU. Also replaces the stale ~400x figure with the fitted 9-day x12.4 and the rising per-op cost (1.18x/9d) as the P2 motivation. Model and configs untouched; doc only. Co-authored-by: npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d <011987e296fd5006292d2f930b574be47c7801048d1983c46c425d3c95f0cffd@buzz.block.builderlab.xyz> Signed-off-by: npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d <011987e296fd5006292d2f930b574be47c7801048d1983c46c425d3c95f0cffd@buzz.block.builderlab.xyz> --- docs/redis-cluster-mode.md | 34 +++++++++++++++++++++++++++++++--- 1 file changed, 31 insertions(+), 3 deletions(-) diff --git a/docs/redis-cluster-mode.md b/docs/redis-cluster-mode.md index 5996d0309f..9c2b690648 100644 --- a/docs/redis-cluster-mode.md +++ b/docs/redis-cluster-mode.md @@ -504,7 +504,11 @@ deleted, so the protocol no longer carries it (§The protocol). ## Sharded Pub/Sub Conversion (prerequisite P2) -By A4, shard count does not touch the ~400x pub/sub term; conversion does. +By A4, shard count does not touch the pub/sub term; conversion does. It is +the fastest-growing command family (x12.4 over the fitted 9-day window; the +kickoff "~400x" was a coarser 14-day eyeball — cite the fitted number) and +the only one whose per-op cost is rising (1.18x/9d, tracking channel count +x12.7). - **Exact event topics** (`buzz::channel:`, `buzz::global`) convert to `SSUBSCRIBE`/`SPUBLISH`. The existing @@ -513,6 +517,20 @@ By A4, shard count does not touch the ~400x pub/sub term; conversion does. topic names — each topic hashing to its own slot is what spreads propagation cost across shards; a `{community}` tag would recreate the hot node per community. +- **The effective unit of spread is per-community, not per-channel** + (measured, G0 profile 2026-07-30): 87.8% of publish volume targets + `buzz::global` (presence kind 20001 = 60.8%, agent observer + frames kind 24200 = 27.0%); only typing and channel messages use + per-channel topics. Slot spreading still works — no community exceeded + ~4% of publish volume — but it is sub-linear: CRC16 simulation over real + topic names and measured weights puts the hottest shard at ~1.5x its fair + share at 4 shards (p95), growing with shard count. D1's arithmetic must + size for the hottest shard, not `current/N`. +- **Conversion payoff is bounded by measured amplification, not worst-case + broadcast**: cross-pod deliveries run ~5.3 pod-deliveries per publish on a + 15-pod fleet (dynamic interest subscription already avoids full broadcast), + so P2 buys back at most that flowing cost. Real but bounded; see + `RESEARCH/BB_PUBLIC_REDIS_G0_PROFILE.md` for receipts. - **The two pattern subscribers stay classic** (Decision D2, argued in-thread and accepted): enumerating concrete channels would require a new subscribe-before-reachable / unsubscribe-after-last protocol with discovery @@ -711,9 +729,19 @@ REDIS_CLUSTER_PRODUCTION_PRIOR_ART.md`, `…_OPEN_SOURCE_PRIOR_ART.md`, ## Open Decisions - **D1 — Shard count.** Blocked on G0's shardable/broadcast ratio. The spec - deliberately refuses a number until the ratio exists. + deliberately refuses a number until the ratio exists. First G0 inputs are + in (2026-07-30): keyed-command growth is uniform (no hot path in the + command mix), and the hottest-shard imbalance factor is ~1.5x fair share + at 4 shards (see §Sharded Pub/Sub Conversion) — do not size by + `current/N`. Caveat: per-family `rate x latency` accounts for well under a + quarter of measured engine CPU, so the decomposition is not a complete + cost model; D1 stays open. - **D2 — Pattern subscribers stay classic.** Accepted in design; re-opens - only if G0 shows their volume is non-trivial. + only if G0 shows their volume is non-trivial. **Measured 2026-07-30: D2 + holds.** All publishers are lifecycle/admin-rate (code trace, verified + independently); the events-stored ceiling (131/s fleet-summed) sits ~10x + under the total pub/sub term. Per-pattern publish counters land with G2 + per-shard telemetry. - **D3 — Command-pool protocol (RESP2 vs RESP3).** Test-backed decision at G2; the split architecture makes it independent of the subscription client's hard RESP3 requirement. From 3292b35db1bad838a9e0ff508a728d0376d814e7 Mon Sep 17 00:00:00 2001 From: npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d <011987e296fd5006292d2f930b574be47c7801048d1983c46c425d3c95f0cffd@buzz.block.builderlab.xyz> Date: Thu, 30 Jul 2026 14:01:46 -0400 Subject: [PATCH 08/13] docs: fold P3 engine-CPU decomposition into D1, fallback, and fit window MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Dawn's P3 replica-subtraction measurement (2026-07-30, receipts in RESEARCH/BB_PUBLIC_REDIS_P3_ENGINE_CPU_DECOMPOSITION.md) resolves the open <25%-decomposition caveat and lands three spec updates: - D1 gets its gated input: ~40% of primary engine CPU is write-apply + publish propagation (the never-read replica carries 7.8pp of 19.5pp); ~60% is client-facing and divides only as connections/subscriptions redistribute. Notes the A4 dependency (propagation confines to the owning shard only after P2) plus two measurement cautions: the pub/sub-vs-keyed regression split is unidentifiable (r=0.997), and the apparent sublinearity is a ~1.1% fixed baseline. - Fallback row corrected: the replica is not idle — 7.8% is its own unsheddable load on a ~3.8d doubling, saturating alone in ~14 days. Kickoff's 'idles at 7%' framing removed. - Problem statement gains the measured fit window: sharp onset 2026-07-21 ~18:00Z; fits must start post-onset; curr_connections moves in pool-config plateaus, not demand. Onset unattributed pending deploy history. Summary timeline row updated to the fitted ~7d-to-80% with the degraded-fallback note. Model and configs untouched; doc only. Co-authored-by: npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d <011987e296fd5006292d2f930b574be47c7801048d1983c46c425d3c95f0cffd@buzz.block.builderlab.xyz> Signed-off-by: npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d <011987e296fd5006292d2f930b574be47c7801048d1983c46c425d3c95f0cffd@buzz.block.builderlab.xyz> --- docs/redis-cluster-mode.md | 42 ++++++++++++++++++++++++++++++-------- 1 file changed, 33 insertions(+), 9 deletions(-) diff --git a/docs/redis-cluster-mode.md b/docs/redis-cluster-mode.md index 9c2b690648..b321c1d695 100644 --- a/docs/redis-cluster-mode.md +++ b/docs/redis-cluster-mode.md @@ -83,6 +83,13 @@ profile `bb-public-operations-ro`). scaling is dead: same-family bigger instances have identical single-core speed; r8g (Graviton4) buys ~25–30% single-thread ≈ 1.5 days at the current doubling rate. +- **Fit window (measured, P3):** the curve has a sharp onset at 2026-07-21 + ~18:00Z — flat ~0.55% for the preceding five days, then exponential within + one 15-min bin (subscribed channels 74→1303 in four hours at a pinned + connection count). Growth fits must start after the onset or they mix two + regimes. `curr_connections` moves in pool-config plateaus (40.0 → 74.9 → + ~280) and must not be read as demand. The onset is unattributed; confirming + what reached bb-public at 18:00Z needs deploy-history access. ## System Model @@ -622,11 +629,15 @@ keep CPU <80% during resharding — resharding is compute-intensive, and doing it while the engine core saturates is the worst time. The countdown clock is the argument for starting G1 now, not for heroics at 90%. -**Fallback (curve outruns the plan):** replica read offload -(`buzz-001-002` idles at 7%) buys roughly one doubling. Note the coupling: in -cluster mode, replica reads lean on exactly the replica-repair path fixed in -redis-rs #2120/#2223, so the version floor is a prerequisite for the fallback -too, not just hygiene. +**Fallback (curve outruns the plan):** replica read offload. Downgraded but +not dead (P3, measured 2026-07-30): the replica is **not idle** — its 7.8% +engine CPU is its own write-apply + propagation load, unsheddable, on its own +exponential (doubling ~3.8d; saturates alone in ~14 days serving zero reads). +Offload still buys primary time, but the destination is a node ~6 days behind +the primary on the same clock — size against its remaining headroom, not +"93% free". Note the coupling: in cluster mode, replica reads lean on exactly +the replica-repair path fixed in redis-rs #2120/#2223, so the version floor +is a prerequisite for the fallback too, not just hygiene. ## Conformance (test matrix, gate G2) @@ -733,9 +744,22 @@ REDIS_CLUSTER_PRODUCTION_PRIOR_ART.md`, `…_OPEN_SOURCE_PRIOR_ART.md`, in (2026-07-30): keyed-command growth is uniform (no hot path in the command mix), and the hottest-shard imbalance factor is ~1.5x fair share at 4 shards (see §Sharded Pub/Sub Conversion) — do not size by - `current/N`. Caveat: per-family `rate x latency` accounts for well under a - quarter of measured engine CPU, so the decomposition is not a complete - cost model; D1 stays open. + `current/N`. The earlier caveat that per-family `rate x latency` explains + under a quarter of engine CPU is now resolved by measurement (P3, + replica-subtraction natural experiment: the never-read replica carries + 7.8pp of the primary's 19.5pp): **~40% of primary engine CPU is + write-apply + publish propagation; ~60% is client-facing** (reads, Lua, + connection I/O, subscriber delivery) and divides only as connections and + subscriptions redistribute across shards. One dependency inside the 40%: + write-apply partitions by key unconditionally, but by A4 the propagation + component confines to the owning shard **only after P2 lands** — with + classic pub/sub, every node processes every publish. So the ~40% is the + shardable fraction *with* P2, an upper bound without it. Two further + cautions from the same measurement set: engine CPU cannot be split + pub/sub-vs-keyed by regression (rates collinear at r=0.997; subsampled + shares swing 4%→37%), and the apparent sublinearity of CPU vs. rate is a + ~1.1% fixed baseline, not economies of scale — do not project on the + exponent. D1 stays open pending the P2/imbalance-adjusted arithmetic. - **D2 — Pattern subscribers stay classic.** Accepted in design; re-opens only if G0 shows their volume is non-trivial. **Measured 2026-07-30: D2 holds.** All publishers are lifecycle/admin-rate (code trace, verified @@ -763,4 +787,4 @@ REDIS_CLUSTER_PRODUCTION_PRIOR_ART.md`, `…_OPEN_SOURCE_PRIOR_ART.md`, | Sharded pub/sub necessity | Documented fact | Axiom A4 (Valkey cluster spec) | | Sharded pub/sub at scale | **No prior art** | Buzz-specific load/reconnect gate in G2 | | Shard count | **Open** | G0 profile (D1) | -| Timeline | ~8–10 days of runway at current doubling | G1 starts now; fallback = replica offload | +| Timeline | ~7 days to 80% on the primary (fitted, post-onset window) | G1 starts now; fallback = replica offload (degraded — replica not idle, ~14d to its own saturation) | From 1f80be5cce8f0254c6778030aa0865fb28e11bf8 Mon Sep 17 00:00:00 2001 From: npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d <011987e296fd5006292d2f930b574be47c7801048d1983c46c425d3c95f0cffd@buzz.block.builderlab.xyz> Date: Thu, 30 Jul 2026 14:09:18 -0400 Subject: [PATCH 09/13] docs: re-anchor problem-statement clock to the fitted post-onset window MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Dawn's delta review at 3292b35db caught the doc carrying two runways: the problem statement still held kickoff's eyeballed ~3.5-4d doubling / 8-10d saturation, while the summary row read the fitted ~7d-to-80% — and the eyeball figure was fitted across exactly the Jul-21-18:00Z regime boundary the adjacent fit-window bullet forbids. Problem statement now leads with the fitted post-onset clock (~3.4-3.5d doubling, ~7d to 80%, r2=0.92) and demotes the kickoff figures to a declared pre-onset eyeball. Same treatment for the ~150x/~400x family growth (fitted: x9.6-12.4 over 9 days). G0's gate description (line ~595) keeps its original tasking text deliberately. Model and configs untouched; doc only. Co-authored-by: npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d <011987e296fd5006292d2f930b574be47c7801048d1983c46c425d3c95f0cffd@buzz.block.builderlab.xyz> Signed-off-by: npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d <011987e296fd5006292d2f930b574be47c7801048d1983c46c425d3c95f0cffd@buzz.block.builderlab.xyz> --- docs/redis-cluster-mode.md | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) diff --git a/docs/redis-cluster-mode.md b/docs/redis-cluster-mode.md index b321c1d695..cda7cb0eb6 100644 --- a/docs/redis-cluster-mode.md +++ b/docs/redis-cluster-mode.md @@ -74,11 +74,16 @@ disabled, auto-failover **enabled**, Multi-AZ **enabled** (verified via `describe-replication-groups` / `describe-cache-clusters`, profile `bb-public-operations-ro`). -- `EngineCPUUtilization` (primary): 0.3% (Jul 21) → 8.4% (Jul 27) → 19.2% - (Jul 30) — doubling every ~3.5–4 days. Saturation in ~8–10 days if the - curve holds. -- Driver is command volume: get/set/eval families each ~150x in two weeks, - pub/sub ~400x. Product growth (~80k users added), not a leak. +- `EngineCPUUtilization` (primary): 0.3% (Jul 21) → 8.4% (Jul 27) → 19.5% + (Jul 30). **Fitted post-onset clock (P3, log-linear, r²=0.92): doubling + every ~3.4–3.5 days; ~7 days to 80%, ~8 to saturation.** (Kickoff's + eyeballed "~3.5–4 days / 8–10 days" spanned the pre-onset regime — see the + fit-window bullet below — and understated the urgency; the fitted number + is the citable one.) +- Driver is command volume — product growth (~80k users added), not a leak. + Fitted 9-day post-onset growth is x9.6–12.4 across all command families + (kickoff's "~150x / ~400x in two weeks" were coarser eyeballs over a + window spanning the onset). - Whole-instance CPU ~4%, memory 0.09%, replication lag <1ms. Vertical scaling is dead: same-family bigger instances have identical single-core speed; r8g (Graviton4) buys ~25–30% single-thread ≈ 1.5 days at the current From ef88988dff0e9b2b8c84596d9481286042f22c3f Mon Sep 17 00:00:00 2001 From: npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d <011987e296fd5006292d2f930b574be47c7801048d1983c46c425d3c95f0cffd@buzz.block.builderlab.xyz> Date: Thu, 30 Jul 2026 14:38:49 -0400 Subject: [PATCH 10/13] =?UTF-8?q?docs:=20fold=20D1=20composed=20arithmetic?= =?UTF-8?q?=20=E2=80=94=20corrected=20shardable=20fraction,=20runway=20ban?= =?UTF-8?q?d,=20optionality=20framing?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d <011987e296fd5006292d2f930b574be47c7801048d1983c46c425d3c95f0cffd@buzz.block.builderlab.xyz> Signed-off-by: npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d <011987e296fd5006292d2f930b574be47c7801048d1983c46c425d3c95f0cffd@buzz.block.builderlab.xyz> --- docs/redis-cluster-mode.md | 49 ++++++++++++++++++++++++++++---------- 1 file changed, 37 insertions(+), 12 deletions(-) diff --git a/docs/redis-cluster-mode.md b/docs/redis-cluster-mode.md index cda7cb0eb6..c94af08feb 100644 --- a/docs/redis-cluster-mode.md +++ b/docs/redis-cluster-mode.md @@ -50,8 +50,9 @@ prove: resharding completes within a window, is empirical — characterized by the profiling gate (G0) and load tests, not by theorem. - **Shard count.** The shardable-keyspace vs. unshardable-broadcast ratio is - an unmeasured input (§Open Decisions, D1). Committing a shard count before - the profile exists would be fiction with units. + a measured input, not a theorem (§Open Decisions, D1 — composed + 2026-07-30). Committing a shard count before that profile existed would + have been fiction with units; with it, initial N is an ops/cost trade. - **redis-rs / deadpool-redis / ElastiCache internals.** The cluster client's MOVED/ASK routing, RESP3 push delivery, and ElastiCache's online resharding are trusted vendor components, admitted per-deployment by conformance gates @@ -754,17 +755,41 @@ REDIS_CLUSTER_PRODUCTION_PRIOR_ART.md`, `…_OPEN_SOURCE_PRIOR_ART.md`, replica-subtraction natural experiment: the never-read replica carries 7.8pp of the primary's 19.5pp): **~40% of primary engine CPU is write-apply + publish propagation; ~60% is client-facing** (reads, Lua, - connection I/O, subscriber delivery) and divides only as connections and - subscriptions redistribute across shards. One dependency inside the 40%: - write-apply partitions by key unconditionally, but by A4 the propagation - component confines to the owning shard **only after P2 lands** — with - classic pub/sub, every node processes every publish. So the ~40% is the - shardable fraction *with* P2, an upper bound without it. Two further - cautions from the same measurement set: engine CPU cannot be split + connection I/O, subscriber delivery). That split answers *what the + replica pays*, not *what sharding divides* — reads and Lua are keyed and + divide by N exactly like writes, so the genuinely non-dividing terms are + narrower: classic pub/sub propagation (pre-P2 only — by A4 every node + processes every publish until P2 lands, after which propagation confines + to the owning shard) and client connection I/O (every pod dials every + shard). Estimated shardable fraction: **f ≈ 0.60 pre-P2 (band + 0.45–0.70), f ≈ 0.75 post-P2 (band 0.60–0.85)**. Two further cautions + from the same measurement set: engine CPU cannot be split pub/sub-vs-keyed by regression (rates collinear at r=0.997; subsampled shares swing 4%→37%), and the apparent sublinearity of CPU vs. rate is a ~1.1% fixed baseline, not economies of scale — do not project on the - exponent. D1 stays open pending the P2/imbalance-adjusted arithmetic. + exponent. **Composed arithmetic (2026-07-30, + `RESEARCH/BB_PUBLIC_REDIS_D1_SHARD_COUNT_ARITHMETIC.md`):** with + `scale(N,f) = (1-f) + f·IMB(N)/N` applied to the variable load only (the + ~1.1% baseline must not be scaled), at the central 3.45-day doubling the + do-nothing runway is 7.2d — **band 5.2–9.0d across fit windows; plan + against the band, not the point** — and N=4 buys **+2.3d pre-P2 / +3.1d + post-P2** (N=8 post-P2: +4.3d). Any one-time capacity gain of factor M + buys exactly `Td·log₂(M)` days, so no N reachable this week buys two + doublings, and every available lever — sharding, r8g (+1.4d), presence + reduction, all stacked (~3.4d) — is smaller than the migration's own + duration estimate (14d aggressive / 21d likely / 35d conservative; soft, + LOC-derived, not a bottom-up plan). **Shard count is therefore not a + runway purchase, and the honest case for cluster mode is optionality, + not headroom**: G5 online resharding makes N a repeatable dial — each + doubling of N buys another Td on demand, without another one-way door — + while single-shard has no dial left (r8g is one-shot and forecloses G3 + while in flight). This case does not depend on the growth curve holding; + the runway numbers do, and at 3.45d the curve implies unreachable user + counts within a month, so *when it flattens* is a product question, and + if it does not flatten on its own, the gap closes with product-side load + reduction, not any infra lever. D1's remaining open item is the choice + of initial N — an ops/cost trade within 2–8, no longer a capacity + computation. - **D2 — Pattern subscribers stay classic.** Accepted in design; re-opens only if G0 shows their volume is non-trivial. **Measured 2026-07-30: D2 holds.** All publishers are lifecycle/admin-rate (code trace, verified @@ -791,5 +816,5 @@ REDIS_CLUSTER_PRODUCTION_PRIOR_ART.md`, `…_OPEN_SOURCE_PRIOR_ART.md`, | Vendor cluster behaviors | Empirical | Conformance matrix (G2) | | Sharded pub/sub necessity | Documented fact | Axiom A4 (Valkey cluster spec) | | Sharded pub/sub at scale | **No prior art** | Buzz-specific load/reconnect gate in G2 | -| Shard count | **Open** | G0 profile (D1) | -| Timeline | ~7 days to 80% on the primary (fitted, post-onset window) | G1 starts now; fallback = replica offload (degraded — replica not idle, ~14d to its own saturation) | +| Shard count | **Arithmetic composed** — N=4 buys +2.3d pre-P2 / +3.1d post-P2; value is the repeatable dial, not runway. Open only on initial N (ops/cost, 2–8) | D1 composed arithmetic | +| Timeline | ~7 days to 80% on the primary (fitted central; band 5.2–9.0d across fit windows) | G1 starts now; fallback = replica offload (degraded — replica not idle, ~14d to its own saturation) | From 5baf0a10a7c86628cae56f1b279a90bd85735308 Mon Sep 17 00:00:00 2001 From: npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d <011987e296fd5006292d2f930b574be47c7801048d1983c46c425d3c95f0cffd@buzz.block.builderlab.xyz> Date: Thu, 30 Jul 2026 14:51:59 -0400 Subject: [PATCH 11/13] docs: fix stacked-levers figure (~3.4d -> ~5.1d) and reconcile r8g to 1.4d MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Dawn's Correction 2: stacked levers multiply M, days add — 1.882 x 1.330 x 1.111 = 2.782 -> 5.09d at Td=3.45d (4.93d interaction-aware). The ~3.4d figure required Td=2.55d, a fast-edge result reported as central. Also reconciles the kickoff-era r8g '~1.5 days' at line 90 to the fitted 1.4d used everywhere else. Conclusion unchanged: no infra lever outruns the curve. Co-authored-by: npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d <011987e296fd5006292d2f930b574be47c7801048d1983c46c425d3c95f0cffd@buzz.block.builderlab.xyz> Signed-off-by: npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d <011987e296fd5006292d2f930b574be47c7801048d1983c46c425d3c95f0cffd@buzz.block.builderlab.xyz> --- docs/redis-cluster-mode.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/docs/redis-cluster-mode.md b/docs/redis-cluster-mode.md index c94af08feb..b230d09186 100644 --- a/docs/redis-cluster-mode.md +++ b/docs/redis-cluster-mode.md @@ -87,8 +87,8 @@ profile `bb-public-operations-ro`). window spanning the onset). - Whole-instance CPU ~4%, memory 0.09%, replication lag <1ms. Vertical scaling is dead: same-family bigger instances have identical single-core - speed; r8g (Graviton4) buys ~25–30% single-thread ≈ 1.5 days at the current - doubling rate. + speed; r8g (Graviton4) buys ~25–30% single-thread ≈ 1.4 days at the fitted + 3.45-day doubling (1.33x → Td·log₂(1.33)). - **Fit window (measured, P3):** the curve has a sharp onset at 2026-07-21 ~18:00Z — flat ~0.55% for the preceding five days, then exponential within one 15-min bin (subscribed channels 74→1303 in four hours at a pinned @@ -776,7 +776,7 @@ REDIS_CLUSTER_PRODUCTION_PRIOR_ART.md`, `…_OPEN_SOURCE_PRIOR_ART.md`, post-P2** (N=8 post-P2: +4.3d). Any one-time capacity gain of factor M buys exactly `Td·log₂(M)` days, so no N reachable this week buys two doublings, and every available lever — sharding, r8g (+1.4d), presence - reduction, all stacked (~3.4d) — is smaller than the migration's own + reduction, all stacked (~5.1d; 4.9d interaction-aware) — is smaller than the migration's own duration estimate (14d aggressive / 21d likely / 35d conservative; soft, LOC-derived, not a bottom-up plan). **Shard count is therefore not a runway purchase, and the honest case for cluster mode is optionality, From de1fc0a1ffd8287ad8f266c118de0a1c9b5fad2e Mon Sep 17 00:00:00 2001 From: npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d <011987e296fd5006292d2f930b574be47c7801048d1983c46c425d3c95f0cffd@buzz.block.builderlab.xyz> Date: Thu, 30 Jul 2026 14:56:03 -0400 Subject: [PATCH 12/13] docs: r8g figure to honest range 1.1-1.3d (1.25-1.30x); stacked ~5.0d MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Dawn's residual on 5baf0a10a: the inline derivation used 1.33x, above the doc's own cited ~25-30% single-thread range — a kickoff eyeball rounded up past its ceiling and presented as derived. Restated as the vendor range 1.25-1.30x -> 1.1-1.3d, explicitly unbenchmarked. Wall sentence takes the optimistic edge (+1.3d) and restacks: M = 1.882 x 1.30 x 1.111 = 2.718 -> ~5.0d (interaction-aware 2.633 -> 4.8d). Conclusion unchanged: still ~4x short of the 21d likely migration. Co-authored-by: npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d <011987e296fd5006292d2f930b574be47c7801048d1983c46c425d3c95f0cffd@buzz.block.builderlab.xyz> Signed-off-by: npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d <011987e296fd5006292d2f930b574be47c7801048d1983c46c425d3c95f0cffd@buzz.block.builderlab.xyz> --- docs/redis-cluster-mode.md | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/docs/redis-cluster-mode.md b/docs/redis-cluster-mode.md index b230d09186..faa8bbc4de 100644 --- a/docs/redis-cluster-mode.md +++ b/docs/redis-cluster-mode.md @@ -87,8 +87,9 @@ profile `bb-public-operations-ro`). window spanning the onset). - Whole-instance CPU ~4%, memory 0.09%, replication lag <1ms. Vertical scaling is dead: same-family bigger instances have identical single-core - speed; r8g (Graviton4) buys ~25–30% single-thread ≈ 1.4 days at the fitted - 3.45-day doubling (1.33x → Td·log₂(1.33)). + speed; r8g (Graviton4) buys ~25–30% single-thread ≈ 1.1–1.3 days at the + fitted 3.45-day doubling (1.25–1.30x → Td·log₂(M); vendor range, not + benchmarked by anyone in this effort). - **Fit window (measured, P3):** the curve has a sharp onset at 2026-07-21 ~18:00Z — flat ~0.55% for the preceding five days, then exponential within one 15-min bin (subscribed channels 74→1303 in four hours at a pinned @@ -775,8 +776,9 @@ REDIS_CLUSTER_PRODUCTION_PRIOR_ART.md`, `…_OPEN_SOURCE_PRIOR_ART.md`, against the band, not the point** — and N=4 buys **+2.3d pre-P2 / +3.1d post-P2** (N=8 post-P2: +4.3d). Any one-time capacity gain of factor M buys exactly `Td·log₂(M)` days, so no N reachable this week buys two - doublings, and every available lever — sharding, r8g (+1.4d), presence - reduction, all stacked (~5.1d; 4.9d interaction-aware) — is smaller than the migration's own + doublings, and every available lever — sharding, r8g (+1.3d at the + optimistic 1.30x edge), presence + reduction, all stacked (~5.0d; 4.8d interaction-aware) — is smaller than the migration's own duration estimate (14d aggressive / 21d likely / 35d conservative; soft, LOC-derived, not a bottom-up plan). **Shard count is therefore not a runway purchase, and the honest case for cluster mode is optionality, From bfb1cc58fe764bbc0de176358ed10aa1ad5c68d2 Mon Sep 17 00:00:00 2001 From: npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d <011987e296fd5006292d2f930b574be47c7801048d1983c46c425d3c95f0cffd@buzz.block.builderlab.xyz> Date: Thu, 30 Jul 2026 15:26:52 -0400 Subject: [PATCH 13/13] =?UTF-8?q?docs:=20fold=20onset=20attribution=20?= =?UTF-8?q?=E2=80=94=2016:40Z=20organic=20community=20creation,=20not=20a?= =?UTF-8?q?=20deploy?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Dawn's onset-attribution finding (RESEARCH/BB_PUBLIC_REDIS_ONSET_ATTRIBUTION.md): onset moves 18:00Z -> 16:40Z (15-min bins blurred it); attributed to organic community creation (58 -> 425 in 2h, same 5-min bin as the Redis breakout, flat subs-per-connection ratio excludes a code change). Community creation is now linear (~3,100/day) but Redis load stays exponential — intensification within communities — so the watch metric is channels-per-community. Adds the four-account cacheclusterid Datadog trap (must scope aws_account:433851229429). No planning number changes: 3.45d doubling and 5.2-9.0d band stand. Co-authored-by: npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d <011987e296fd5006292d2f930b574be47c7801048d1983c46c425d3c95f0cffd@buzz.block.builderlab.xyz> Signed-off-by: npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d <011987e296fd5006292d2f930b574be47c7801048d1983c46c425d3c95f0cffd@buzz.block.builderlab.xyz> --- docs/redis-cluster-mode.md | 22 +++++++++++++++++----- 1 file changed, 17 insertions(+), 5 deletions(-) diff --git a/docs/redis-cluster-mode.md b/docs/redis-cluster-mode.md index faa8bbc4de..d1a2332168 100644 --- a/docs/redis-cluster-mode.md +++ b/docs/redis-cluster-mode.md @@ -90,13 +90,25 @@ profile `bb-public-operations-ro`). speed; r8g (Graviton4) buys ~25–30% single-thread ≈ 1.1–1.3 days at the fitted 3.45-day doubling (1.25–1.30x → Td·log₂(M); vendor range, not benchmarked by anyone in this effort). -- **Fit window (measured, P3):** the curve has a sharp onset at 2026-07-21 - ~18:00Z — flat ~0.55% for the preceding five days, then exponential within - one 15-min bin (subscribed channels 74→1303 in four hours at a pinned +- **Fit window (measured, P3; onset attributed 2026-07-30):** the curve has a + sharp onset at 2026-07-21 **16:40Z** (5-min bins; the earlier ~18:00Z was a + 15-min-bin artifact) — flat ~0.55% for the preceding five days, then + exponential (subscribed channels 74→1303 in four hours at a pinned connection count). Growth fits must start after the onset or they mix two regimes. `curr_connections` moves in pool-config plateaus (40.0 → 74.9 → - ~280) and must not be read as demand. The onset is unattributed; confirming - what reached bb-public at 18:00Z needs deploy-history access. + ~280) and must not be read as demand. **The onset is not a deploy** — it is + organic community creation (58 → 425 communities in two hours, first move in + the same 5-min bin as the Redis breakout; one pub/sub topic per community + makes the chain mechanical, and subscriptions-per-connection stayed flat + across the onset, which excludes a subscription-behavior code change). + Community creation has since gone **linear** (~3,100/day) while Redis load + remains **exponential** — the exponential is carried by intensification + within communities, so the curve-break indicator to watch is + **channels-per-community** (rising as of Jul 30), not community count. + Receipts: `RESEARCH/BB_PUBLIC_REDIS_ONSET_ATTRIBUTION.md`. Measurement + trap: `cacheclusterid:buzz-001-001` exists in **four** AWS accounts, so + every ElastiCache query must scope `aws_account:433851229429` — a bare-tag + `avg:` dilutes engine CPU ~3.4x. ## System Model