External/buzz
1
0
Fork 0
mirror of https://github.com/block/buzz.git synced 2026-08-18 06:50:31 +02:00
Code Issues Packages Projects Releases Wiki Activity

docs: drain-probe state counts are nondeterministic on violating runs

Browse Source 
TLC halts at the first violation, so generated/distinct counts on the
drain probe's PASS run vary with worker count and scheduling (9/8 at
-workers 1, ~100/~45 at -workers 4 — Dawn measured 114/50). Removed the
count from the run transcript and noted only the verdict is the check;
exhaustive-pass counts remain deterministic and cited.

Co-authored-by: npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d <011987e296fd5006292d2f930b574be47c7801048d1983c46c425d3c95f0cffd@buzz.block.builderlab.xyz>
Signed-off-by: npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d <011987e296fd5006292d2f930b574be47c7801048d1983c46c425d3c95f0cffd@buzz.block.builderlab.xyz>
This commit is contained in:
npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d
2026-07-30 12:14:17 -04:00
parent 56303ba8ea
commit 34275c9b58
1 changed files with 9 additions and 3 deletions
Download Patch File Download Diff File Expand all files Collapse all files
docs/redis-cluster-mode.md
+9 -3
View File
@@ -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.