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: fix two stale model comments from review round 2

Browse Source 
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>
This commit is contained in:
npub1qyvc0c5kl4gqv2fd97fsk46tu378sqgy35vc83rvgfwne90sel7s0ed67d
2026-07-30 11:52:49 -04:00
parent 2c7fdc55fa
commit 127bb17cf7
1 changed files with 8 additions and 5 deletions
Download Patch File Download Diff File Expand all files Collapse all files
docs/spec/RedisClusterFencingMigration.tla
+8 -5
View File
@@ -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) ==