Skip to content

docs: Redis/Valkey cluster-mode migration spec with mechanized fencing model #3756

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
tlongwell-block wants to merge 14 commits into
base: main
Choose a base branch
from
Draft

docs: Redis/Valkey cluster-mode migration spec with mechanized fencing model #3756

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
14 commits
Select commit Hold shift + click to select a range
549fd58
docs: Redis/Valkey cluster-mode migration spec with mechanized fencin…
Jul 30, 2026
2c7fdc5
docs: fold review round 1 into cluster-mode spec (deployment gate, sl…
Jul 30, 2026
127bb17
docs: fix two stale model comments from review round 2
Jul 30, 2026
56303ba
docs: drain-reachability probe (M10) + B->A rollback session-loss note
Jul 30, 2026
34275c9
docs: drain-probe state counts are nondeterministic on violating runs
Jul 30, 2026
f1957c9
ci: machine-check the Redis cluster-mode TLA+ specs
tlongwell-block Jul 30, 2026
acfb537
docs: fold G0/P2 measured findings into pub/sub conversion and open d…
Jul 30, 2026
3292b35
docs: fold P3 engine-CPU decomposition into D1, fallback, and fit window
Jul 30, 2026
1f80be5
docs: re-anchor problem-statement clock to the fitted post-onset window
Jul 30, 2026
ef88988
docs: fold D1 composed arithmetic — corrected shardable fraction, run…
Jul 30, 2026
59d761d
Merge origin/main into eva/redis-cluster-mode-spec (branch-skew: ci.y…
Jul 30, 2026
5baf0a1
docs: fix stacked-levers figure (~3.4d -> ~5.1d) and reconcile r8g to…
Jul 30, 2026
de1fc0a
docs: r8g figure to honest range 1.1-1.3d (1.25-1.30x); stacked ~5.0d
Jul 30, 2026
bfb1cc5
docs: fold onset attribution — 16:40Z organic community creation, not…
Jul 30, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
22 changes: 22 additions & 0 deletions .github/workflows/ci.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -27,6 +27,7 @@
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:
Expand Down Expand Up @@ -74,6 +75,10 @@
- '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: Desktop release candidate contract
Expand Down Expand Up @@ -884,6 +889,23 @@
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

Check warning

Code scanning / zizmor

detects commit SHAs that don't match their version comment tags Warning

detects commit SHAs that don't match their version comment tags
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
Expand Down
Loading
Loading