amadan
sim: naming a converted move's same-region target takes the move's own target off the participants in the same CAS (rule reloc-name-drops-move-target, mirroring 1b-next 151261fe); a stopped move target no longer holds the relocation at pinning
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
5 files changed,
+94
−3
internal/sim/hostlife/regionha_round1_test.go+29 −0internal/sim/hostlife/regionha_test.go+27 −3internal/sim/hostlife/regionha_witness_test.go+34 −0internal/sim/hostlife/rules_test.go+1 −0internal/sim/hostlife/witness_test.go+3 −0
diff --git a/internal/sim/hostlife/regionha_round1_test.go b/internal/sim/hostlife/regionha_round1_test.go| index 59c8f7bb0..bc243e370 100644 |
| --- a/internal/sim/hostlife/regionha_round1_test.go |
| +++ b/internal/sim/hostlife/regionha_round1_test.go |
| @@ -605,6 +605,35 @@ func TestConvertedMoveWaitsForATargetBeforeItsPin(t *testing.T) { |
| w.mustHold(t) |
| } |
| +// TestConvertedMoveDropsTheMoveTargetFromTheBarrier |
| +// (reloc-name-drops-move-target; final review Important 1, 1b-next |
| +// 151261fe): the move's source is terminated before the flip, and the |
| +// move's own target in region 1, the one participant the conversion |
| +// left, is stopped before it acknowledges. Naming the same-region target |
| +// takes the move's target off the participants in the same CAS, and the |
| +// relocation reaches installing and serves while that box stays |
| +// stopped. The mutation keeps it on the barrier: the relocation waits at |
| +// pinning for ever. |
| +func TestConvertedMoveDropsTheMoveTargetFromTheBarrier(t *testing.T) { |
| + w := twoBoxWitness() |
| + mt := w.convertedMoveTargetStopped(t) |
| + if !w.reach(t, 400, "the target named", func() bool { return w.claim.Op.Tgt >= 0 }, w.actAll(), w.recoveryPass) { |
| + w.mustHold(t) |
| + } |
| + if c := w.claim; contains(c.Op.Parts, mt.ID) || len(c.Op.Parts) != 1 || c.Op.Parts[0] != c.Op.Tgt { |
| + t.Fatalf("the move's target %d is still on the barrier: parts=%v target=%d", mt.ID, c.Op.Parts, c.Op.Tgt) |
| + } |
| + if !w.relocPhase(t, "installing", w.actAll(), w.recoveryPass) { |
| + w.mustHold(t) |
| + } |
| + if !mt.Destroyed { |
| + t.Fatalf("the move's target started again") |
| + } |
| + w.servingOn(t, nil) |
| + w.finish(t) |
| + w.mustHold(t) |
| +} |
| + |
| // TestFailoverStartWaitsForAdmission (reloc-failover-start-guard; rev |
| // 7, Astra round 4 finding 3): with the app's admission closed, a |
| // terminated serving executor's failover does not start (Worker.Start's |
diff --git a/internal/sim/hostlife/regionha_test.go b/internal/sim/hostlife/regionha_test.go| index ee54ac62d..b13fcb347 100644 |
| --- a/internal/sim/hostlife/regionha_test.go |
| +++ b/internal/sim/hostlife/regionha_test.go |
| @@ -810,20 +810,44 @@ func (w *world) relocPinning(b *box, c *claim) { |
| } |
| // relocNameTarget is NameTarget at pinning: choose() in the source region |
| -// over the eligible boxes, the excluded ones left out. |
| +// over the eligible boxes, the excluded ones left out. A converted move's |
| +// own target (1b-next's move_target_box, in the region the move was |
| +// going to) leaves the participants in the same CAS (rule |
| +// reloc-name-drops-move-target, 1b-next 151261fe): readiness binds to the |
| +// box named here (moves §7.10) and a failover's participant is its |
| +// target alone (§5.8); the move's target never held op.exec on the |
| +// converted operation. A relocation's participants are otherwise all in |
| +// its region, so the model drops every participant outside op.SrcRegion, |
| +// which only a converted move leaves there. The mutation keeps it, and |
| +// the barrier waits for a box that may never acknowledge: a stopped move |
| +// target holds the relocation at pinning with no deadline and no stuck |
| +// (INV-3; TestConvertedMoveDropsTheMoveTargetFromTheBarrier). |
| func (w *world) relocNameTarget(c *claim) { |
| op := c.Op |
| to := w.chooseBoxExcept(op.SrcRegion, c.Holder.App, relocExcept(op)...) |
| if to == nil { |
| return // no eligible box: the recovery pass alerts once (moves §7.10) |
| } |
| - w.cas(c, func(n *claim) bool { |
| + dropped := false |
| + if w.cas(c, func(n *claim) bool { |
| ok := sameOp(n.Op.ID, op.ID) && n.Op.Kind == "relocating" && n.Op.Phase == "pinning" && n.Op.Tgt < 0 |
| + if ok && on("reloc-name-drops-move-target") { |
| + var parts []int |
| + for _, p := range n.Op.Parts { |
| + if x := w.boxByID(p); x == nil || x.Region == n.Op.SrcRegion { |
| + parts = append(parts, p) |
| + } |
| + } |
| + dropped = len(parts) < len(n.Op.Parts) |
| + n.Op.Parts = parts |
| + } |
| if ok { |
| ok = w.nameReplacement(n, to.ID, "pinning") |
| } |
| return ok |
| - }) |
| + }) && dropped { |
| + w.stats["name target: the move's target left the participants"]++ |
| + } |
| } |
| // abandonPrepared is abandonPrepared(c) in hostclaim (1b-next ruling |
diff --git a/internal/sim/hostlife/regionha_witness_test.go b/internal/sim/hostlife/regionha_witness_test.go| index a1a955d8e..4195f2778 100644 |
| --- a/internal/sim/hostlife/regionha_witness_test.go |
| +++ b/internal/sim/hostlife/regionha_witness_test.go |
| @@ -965,3 +965,37 @@ func wPushKeepsLiveFiles(t *testing.T, w *world) { |
| w.servingOn(t, w.boxes[3]) |
| w.finish(t) |
| } |
| + |
| +// convertedMoveTargetStopped converts a move (convertedMove: the source, |
| +// box 0, is terminated before the flip) and stops the move's own target, |
| +// the one participant the conversion left, before it acknowledges; it |
| +// returns that box. Stopped is not terminated: nothing fences it, and |
| +// it never acknowledges the converted operation. |
| +func (w *world) convertedMoveTargetStopped(t *testing.T) *box { |
| + w.convertedMove(t, nil) |
| + c := w.claim |
| + if len(c.Op.Parts) != 1 || len(c.Op.Acks) != 0 || c.Op.Tgt >= 0 { |
| + t.Fatalf("not a converted move whose one participant is the move's target: %s", w.state()) |
| + } |
| + mt := w.boxByID(c.Op.Parts[0]) |
| + if mt == nil || mt.Region == c.Op.SrcRegion { |
| + t.Fatalf("the converted move's participant %d is not the move's target in another region: %s", c.Op.Parts[0], w.state()) |
| + } |
| + w.stop(mt) |
| + return mt |
| +} |
| + |
| +// wConvertedMoveTargetStopped (reloc-name-drops-move-target; final |
| +// review Important 1, 1b-next 151261fe): a move's source is terminated |
| +// before the flip, the move converts to a relocation at pinning, and the |
| +// move's target in region 1 is stopped before it acknowledges. Naming |
| +// the region's other box takes the move's target off the barrier in the |
| +// same CAS, and the host serves on the named box; without the rule the |
| +// barrier waits for the stopped box, with no deadline and no stuck, and |
| +// nothing moves (INV-3). |
| +func wConvertedMoveTargetStopped(t *testing.T, w *world) { |
| + w.twoBox() |
| + w.convertedMoveTargetStopped(t) |
| + w.servingOn(t, nil) |
| + w.finish(t) |
| +} |
diff --git a/internal/sim/hostlife/rules_test.go b/internal/sim/hostlife/rules_test.go| index eef576edf..892fdf82a 100644 |
| --- a/internal/sim/hostlife/rules_test.go |
| +++ b/internal/sim/hostlife/rules_test.go |
| @@ -204,4 +204,5 @@ var allRules = []string{ |
| "reloc-name-before-pin", // rev 7 (Astra round 4 finding 1; 1b-next rev 19 Worker.pinning): a relocation at pinning with no target names one before it selects a pin, on every path; the mutation pins first, and a manifest that lands while no box is eligible is left out (a loss bound: TestConvertedMoveWaitsForATargetBeforeItsPin) |
| "reloc-failover-start-guard", // rev 7 (Astra round 4 finding 3; 1b-next rev 19 Worker.Start, StartRelocation): a serving executor's failover starts only with an eligible target, the app admitting the registration (and its recheck) and RelocationStartGuard with the source fenced; the mutation starts at once (TestFailoverStartWaitsForAdmission, TestFailoverStartWaitsForParkReplica) |
| "reloc-failover-ack-before-pin", // rev 5 and 6 (Astra rounds 2 and 3; 1b-next rev 19 PinFailover): an initial failover (op.PinFailover, the model's starting) selects its pin only after the target is named and every participant acknowledged; converted moves, nested failovers and replays pin first, as Worker.pinning does; the mutation pins first, and a manifest that lands while the target's controller is unavailable is left out (a loss bound: TestFailoverPinWaitsForTheAcknowledgement) |
| + "reloc-name-drops-move-target", // final review Important 1 (1b-next 151261fe, NameTarget; moves §7.10, region HA §5.8): naming a converted move's same-region target takes the move's own target (move_target_box, in the other region) off the participants in the same CAS; the mutation keeps it on the barrier, and a stopped move target holds the relocation at pinning for ever (INV-3; TestConvertedMoveDropsTheMoveTargetFromTheBarrier, witness) |
| } |
diff --git a/internal/sim/hostlife/witness_test.go b/internal/sim/hostlife/witness_test.go| index a93c223cf..96d461349 100644 |
| --- a/internal/sim/hostlife/witness_test.go |
| +++ b/internal/sim/hostlife/witness_test.go |
| @@ -258,6 +258,9 @@ var witnesses = []witness{ |
| "F1: a drain's target fails its probe in a two-box region with no spare; with the bound the operation is stuck and the operator's resolve returns the host to the source, without it it waits for ever", wNoSpareBound}, |
| {"reloc-dead-target-bound", "reloc-dead-target-bound", "INV-3", |
| "rev 18 finding 2: the target dies at installing and no spare is launched; with the bound the fence is consumed into stuck and the operator's replay serves on the source, without it nothing moves", wDeadTargetBound}, |
| + // the final review's fixes |
| + {"reloc-name-drops-move-target", "reloc-name-drops-move-target", "INV-3", |
| + "1b-next 151261fe: a move converts to a relocation when its source is terminated before the flip, and the move's target in the other region is stopped before it acknowledges; naming the region's other box takes the move's target off the barrier and the host serves there, without the rule the barrier waits for the stopped box for ever", wConvertedMoveTargetStopped}, |
| } |
| // TestWitnesses is the deterministic half of the mutation evidence. |