amadan

carlos / platform Public

sim: the operator's replay of a stuck relocation excludes a released target, never a released source, which ruling 13 makes eligible again (final review minor 4)

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Paul Campbell pushed by claude 028150d03eff53a878a6d9ce53b29ba712e61725 parent 02ba19b
2 files changed, +52 −2
  • internal/sim/hostlife/console_test.go +5 −2
  • internal/sim/hostlife/regionha_round1_test.go +47 −0
diff --git a/internal/sim/hostlife/console_test.go b/internal/sim/hostlife/console_test.go
index d8aae4592..a821be364 100644
--- a/internal/sim/hostlife/console_test.go
+++ b/internal/sim/hostlife/console_test.go
@@ -1286,8 +1286,11 @@ func (w *world) operator() {
w.abandonPrepared(n)
n.Op.Stuck, n.Op.Replacements, n.Op.Excluded, n.Op.Resolved = "", 0, nil, true
n.Op.PinFailover = false // the replay enters pinning directly (rev 6)
- if released && op.Exec >= 0 {
- n.Op.Excluded = []int{op.Exec} // the target that just failed its probe is not the operator's fresh choice (rev 4)
+ if released && op.Exec >= 0 && op.Exec != op.Src {
+ // the target that just failed its probe is not the
+ // operator's fresh choice (rev 4); a released source is
+ // eligible again, as ruling 13 says (final review minor 4)
+ n.Op.Excluded = []int{op.Exec}
}
n.Op.Phase, n.Op.Exec, n.Op.Tgt = "pinning", -1, -1
n.Op.Pin, n.Op.Prepared, n.Op.Receipt = nil, "", nil
diff --git a/internal/sim/hostlife/regionha_round1_test.go b/internal/sim/hostlife/regionha_round1_test.go
index bc243e370..fba56eb3c 100644
--- a/internal/sim/hostlife/regionha_round1_test.go
+++ b/internal/sim/hostlife/regionha_round1_test.go
@@ -1269,3 +1269,50 @@ func TestTieHashFollowsTheHost(t *testing.T) {
t.Fatalf("host h2 chose %v, want %d", got, wantH2.ID)
}
}
+
+// ---------- the final review's minor 4: a released source stays eligible ----------
+
+// TestOperatorReplayKeepsAReleasedSourceEligible (model ruling 13; final
+// review minor 4): a drain's source journals its release in releasing,
+// still op.exec, and the target is then terminated with no spare (the
+// group launches none). The dead target's bound makes the operation
+// stuck with the released source as op.exec. The operator's replay
+// makes the source eligible again: it excludes only a failed target,
+// never the source, so the host serves on the source. Excluding the
+// released source left the replay waiting at pinning for a spare that
+// never comes.
+func TestOperatorReplayKeepsAReleasedSourceEligible(t *testing.T) {
+ w := twoBoxWitness()
+ from, to := w.boxes[0], w.boxes[3]
+ w.serve(from, 1, app0)
+ w.running(t, from)
+ w.published(t, from)
+ w.drainTo(t, to)
+ w.oneBoxRegion[0] = true // no replacement launches: no spare
+ if !w.stepUntil(t, 400, "the source's release journaled", func() bool {
+ c := w.claim
+ return c.Op.Release != nil && c.Op.Release.Box == from.ID
+ }) {
+ w.mustHold(t)
+ }
+ if c := w.claim; c.Op.Phase != "releasing" || c.Op.Exec != from.ID {
+ t.Fatalf("not released in releasing with the source op.exec: %s", w.state())
+ }
+ w.terminate(to)
+ if !w.reach(t, 3*releaseDeadline, "stuck", func() bool { return w.claim.Op.Stuck != "" }, w.act(from), w.recoveryPass) {
+ w.mustHold(t)
+ }
+ if c := w.claim; c.Op.Exec != from.ID || c.Op.Src != from.ID || c.Op.Release == nil || c.Op.Release.Box != from.ID {
+ t.Fatalf("not stuck with the released source as op.exec: %s", w.state())
+ }
+ w.resolveOnly()
+ if c := w.claim; c.Op.Phase != "pinning" || c.Op.Stuck != "" || !c.Op.Resolved {
+ t.Fatalf("the resolve did not replay from pinning: %s", w.state())
+ }
+ if c := w.claim; contains(c.Op.Excluded, from.ID) {
+ t.Fatalf("the replay excludes the released source %d: excluded=%v", from.ID, c.Op.Excluded)
+ }
+ w.servingOn(t, from)
+ w.finish(t)
+ w.mustHold(t)
+}