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] 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 830d5ccbe..0e9d4cd59 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) ==