throttlekit
View source ↗

08 · Federation

One global per-window budget shared across regions/clusters, with total admissions ≤ the limit regardless of region count, while pooling capacity under skew. Source: src/federation/, src/twotier/federated-weighted-fair-escrow.ts, spec/GaleFederatedLeasing.tla.

Purpose

When K regional clusters must jointly honor one global limit L, statically slicing L/K strands capacity: a hot region binds at its slice while idle regions sit on unused budget. Federation pools the budget instead (a hot region borrows idle regions’ capacity) while keeping total admissions ≤ L with overshoot Δ = 0 independent of K. It is GALE’s window-coupled leasing lifted one level: nodes become regions, local credits become regional escrow, and the L2 store becomes a cross-region coordinator.

The coordinator abstraction

GlobalCoordinator (the “L3”) has three core methods (src/federation/types.ts:45):

  • lease(key, tokens, expiresAt) → granted ∈ [0, tokens]: a partial grant is legitimate (other regions raced the budget down).
  • reconcile(key, leftover, windowStart) is idempotent on windowStart, so a retry through a partition converges and can only ever lose next-window capacity, never violate the bound.
  • isHealthy?() is optional, for outage detection.

The load-bearing contract: the coordinator must be window-coupled, with leases expiring at the window boundary (enforced via PEXPIRE on the Redis path). That expiry is the entire basis of the Δ = 0 proof.

leaseWindowed: returning the authoritative store-clock boundary (optional)

lease(key, tokens, expiresAt) takes the boundary the caller wants the grant coupled to, but the server-time coordinators (RedisCoordinator, PostgresCoordinator) ignore that argument and recompute the window from the store’s clock (Redis TIME / Postgres clock_timestamp()). For a caller that must discard leftover credits at exactly the instant the budget resets (the Tier-2 fleet lease, whose client may run on a skewed node clock), that gap is a correctness hole: it can be told to discard at a different instant than the budget actually drained against.

leaseWindowed(key, tokens) → { granted, expiresAt } (src/federation/types.ts:80) closes it. It returns the authoritative window boundary the coordinator itself used (derived from the same clock that caps the budget), atomically with the grant (one round trip, no two-read race). The Redis Lua now returns {granted, expiresAt} with the Redis-TIME-derived boundary; the Postgres path derives it from clock_timestamp(). So a Tier-2 client discards at precisely the store window, closing the node↔store skew the ignored-expiresAt lease() left open.

It is optional and backward-compatible: lease() is preserved (and is implemented by delegating to the windowed path); granted is in [0, tokens] exactly as before. A coordinator that already windows on the passed expiresAt (the in-memory TestCoordinator) has no divergence and need not implement it. Callers feature-detect leaseWindowed and fall back to a node-clock window when it’s absent.

Window-coupled federated leasing (the contribution)

Per-key escrow state carries a balance, the window bounds, an in-flight pending lease, and the last-reconciled window (src/federation/window-coupled.ts:124). The mechanism:

  • Window-coupling (the Δ = 0 lever). When the prior window expires, the engine captures leftover = balance, resets balance = 0, drops the in-flight lease (it would credit the wrong window), and reconciles the leftover back to L3 once per boundary. Credits expire at the boundary and do not carry over, which is provably the sole source of overshoot, so the bound collapses to admitted ≤ Limit independent of K.
  • The check loop. While balance < cost: try L2 (regional escrow) first if configured, else lease max(batch, cost) from L3, with at most one outstanding lease per region per key (the safety coalescing). After every await, re-resolve the entry (the window may have rolled or reset() may have run). Admit ⇒ balance -= cost.
  • Regional escrow (L2). Sits between the per-process in-process L1 and the cross-region L3, so multiple processes in a region share one atomic regional store and in-flight per-region escrow is bounded by the per-key budget instead of processes × batch. Three ops: lease (consume), refill (additive within a window, dropping stale-window grants, the window-coupling mechanism), release (capture-and-zero at the boundary, idempotent so the first releaser wins).

Static partition (the baseline foil)

staticPartition splits L evenly across regions (remainder to the earliest regions so Σ slice = L exactly). Δ = 0 trivially (each slice is independent), but it loses pooling under skew. It is kept deliberately as the foil the window-coupled scheme must beat on utilization: lopsided allocation doesn’t matter because the real scheme pools anyway.

Federated weighted-fair escrow

federatedWeightedFairEscrow + regionFairPool compose two levels of weighted-fair escrow so each tenant’s global total (summed across regions) equals the flat global weighted-max-min ideal (src/twotier/federated-weighted-fair-escrow.ts):

  1. Cross-region WFE: a weighted-fair reservation layer whose “tenants” are regions; region r’s weight is its dynamic active aggregate tenant weight W_r = Σ w_{t,r}. It reserves each region at least its guarantee and lets a region grow into the others’ idle surplus.
  2. In-region WFE is the per-tenant fair split over the region’s pool-granted budget.
  3. Demand-proportional weight split: a tenant active in several regions splits its global weight w_{t,r} = w_t · d_{t,r}/d_t, so a tenant active in k regions isn’t k×-counted.

The insight: hierarchical max-min ≠ flat max-min unless an internal node is weighted by the sum of its children’s weights (the Parekh–Gallager GPS-decomposition condition). Setting region weight = Σ of its tenants’ weights is exactly that condition, collapsing the two-level hierarchy to a single global water-fill (exact in the fluid limit, within a two-level DRR residual under discrete granting). A plain shared counter cannot reserve, which is the root of the cross-region isolation gap a weighted-fair reservation layer fills.

The cross-region pool can be store-backed. The cross-region reservation layer is a RegionFairPool; the shipped in-process regionFairPool is one arbiter, but a fleet of separate region processes draws from one global budget through RedisRegionFairPool (src/twotier/redis-region-fair-pool.ts), the production AsyncRegionFairPool. It holds each region’s {weight, granted} in a shared Redis hash and runs the exact weighted-max-min reservation+borrow arithmetic of the in-process pool as a single atomic Lua script (the same EVALSHA-with-EVAL-fallback pattern as RedisCoordinator/RedisRegionalEscrow, one layer up), so Σ_r granted ≤ L holds across the fleet regardless of region count or interleaving. The hash carries PEXPIRE to the window boundary and reads Redis TIME (useServerTime) so node-clock skew never moves the boundary on the shared state; a conformance test pins it grant-for-grant against the in-process oracle. It is Redis-only (the weighted-max-min ceiling math is ported to one atomic hash op).

Outage modes

  • fail-closed (default): serve whatever escrow the region already holds, then deny until the coordinator returns. Δ = 0 preserved.
  • regional-only (requires an L2). Keep serving from the regional balance until depleted; mark the coordinator unhealthy on a lease() throw and re-probe isHealthy() lazily (clock-driven, no background timer). Δ degrades to the regional sub-bound during the outage; without an L2 it silently degrades to fail-closed.

Design decisions & rationale

  • A coordinator interface, not a concrete store. One coordinator serves all regions for a key prefix, and Redis / Postgres / a future Raft-via-etcd implement the same window-coupled lease/reconcile contract without the federation engine changing.
  • Window-coupling is the load-bearing safety commitment: the Δ = 0 proof depends entirely on leases expiring at the boundary with no carryover; the relabeled spec shows carryover is the sole overshoot source.
  • Reconcile is idempotent on windowStart. Fire-and-forget through partitions; without the per-window marker a retried reconcile would double-credit the next window. A reconcile failure can only lose next-window capacity, never violate the bound.
  • At most one outstanding lease per region per key: concurrent shortages await one lease rather than racing parallel L3 leases.
  • The WFE∘WFE composition theorem. Naive pooling (per-region WFE over a plain shared counter) gives in-region fairness but cross-region FCFS, starving a heavily-weighted late-arriving region; a plain counter can’t reserve, so the cross-region weighted-fair reservation layer is exactly what cross-region weights require.
  • batch is a utilization knob, not a safety one: a larger batch means fewer cross-region round trips at the cost of worst-case unused escrow, which under window-coupling does not contribute to overshoot.

Caveats

  • No sync path: federation always crosses a region boundary (intrinsically async, 80–150 ms RTT); checkSync throws.
  • SPOF. The default Redis coordinator is a single global Redis; mitigate with synchronous replication
    • failover.
  • Multi-process leftover loss: with multiple processes per region, only the L2-release winner recovers leftover; others lose their L1 leftover (a utilization cost; Δ = 0 preserved either way).
  • Only windowed strategies federate. Window-coupling needs a discrete boundary, so fixedWindow / slidingWindow / quota federate; gcra/tokenBucket throw at construction.
  • Federated WFE is not strategy-proof (inherited from WFE / FairRide); window-coupling bounds the gain to one window. The shipped regionFairPool is in-process (one arbiter); distributing it is a documented store-backed path.
  • A bounded near-boundary utilization dip remains (a busy region re-leases after each boundary), which adaptive lease sizing minimizes.

What proves it

  • spec/GaleWindowCoupledLeasing.tla: admitted ≤ Limit for any N (credits expire at the boundary).
  • spec/GaleFederatedLeasing.tla. A literal relabeling (Nodes→Regions, credits→escrow, l2→globalBudget) lifting the same bound to K regions: admitted ≤ Limit independent of K.
  • test/gale/federated/leasing-variants.test.ts: the CI BFS twin, reproducing the spec’s distinct-state counts byte-for-byte (harness validation) then proving the bound.
  • test/federation/window-coupled.test.ts confirms Δ = 0 independent of K.
  • test/federation/property.test.ts: dual-path TestCoordinator ≡ RedisCoordinator over adversarial timelines (Redis-gated).
  • test/federation/failure-modes.test.ts. The three outage shapes all hold Δ = 0; federation fails closed.
  • test/federation/federated-skew.test.ts: recovers the utilization static partition strands (vs the static-skew.test.ts foil).
  • test/federation/{static-partition,regional-escrow,redis-regional-escrow,regional-only,redis-coordinator, postgres-coordinator}.test.ts.

Source map

src/federation/types.ts (the coordinator/escrow contracts, incl. the optional leaseWindowed) · window-coupled.ts (the engine) · static-partition.ts (the baseline) · redis-coordinator.ts, postgres-coordinator.ts (both implement leaseWindowed) · redis-regional-escrow.ts, test-regional-escrow.ts, test-coordinator.ts · src/twotier/federated-weighted-fair-escrow.ts, redis-region-fair-pool.ts (the store-backed cross-region fair-budget pool) · spec/GaleFederatedLeasing.tla.