carlos / platform Public

sim: Astra's round 4 on the two-box model: a target named before any pin on every path, PinFailover as the phase predicates' starting, and a failover started only through Worker.Start's guards; the drain start in Worker.Start's order

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Paul Campbell pushed by claude agent, operated by paul@keymail.dev 6b991069dd8d37f96a64b5c265724b56830c8e3f parent 8439910
5 files changed, +314 −52
  • internal/sim/hostlife/regionha_cases_test.go +5 −3
  • internal/sim/hostlife/regionha_round1_test.go +215 −34
  • internal/sim/hostlife/regionha_test.go +87 −8
  • internal/sim/hostlife/regionha_witness_test.go +5 −7
  • internal/sim/hostlife/rules_test.go +2 −0
diff --git a/internal/sim/hostlife/regionha_cases_test.go b/internal/sim/hostlife/regionha_cases_test.go
index 39e9b52df..fb50f3d5e 100644
--- a/internal/sim/hostlife/regionha_cases_test.go
+++ b/internal/sim/hostlife/regionha_cases_test.go
@@ -206,9 +206,11 @@ func TestL18UnenrolledReference(t *testing.T) {
if c.Op.Exec == nb.ID || c.Op.Tgt == nb.ID {
t.Fatalf("an unenrolled box was named: %s", w.state())
}
- if boxes == 2 && (c.Op.Kind != "relocating" || c.Op.Tgt != -1 || c.Op.Exec != -1) {
- // the peer fenced the executor; the failover waits at pinning
- t.Fatalf("the relocation did not wait at pinning with no target: %s", w.state())
+ if boxes == 2 && (c.Op.Kind != "serving" || contains(c.Lost, from.ID)) {
+ // Worker.Start needs an eligible target (rev 7, Astra round 4
+ // finding 3): the failover does not start, and the claim still
+ // names the dead box, until the replacement enrolls
+ t.Fatalf("the failover started with no eligible target: %s", w.state())
}
if boxes == 1 && c.Op.Kind != "serving" {
// no enrolled worker of the region exists to write the fence: the
diff --git a/internal/sim/hostlife/regionha_round1_test.go b/internal/sim/hostlife/regionha_round1_test.go
index 3f56952b1..6cc45814f 100644
--- a/internal/sim/hostlife/regionha_round1_test.go
+++ b/internal/sim/hostlife/regionha_round1_test.go
@@ -73,9 +73,23 @@ func (w *world) stepUntil(t *testing.T, max int, what string, done func() bool)
return false
}
-// atPhase: the relocation is exactly in phase p (not beyond it).
+// atPhase: the relocation is exactly in phase p (not beyond it), as
+// 1b-next names it: an initial failover at pinning with PinFailover set
+// is in starting (rev 7, Astra round 4 finding 2).
func (w *world) atPhase(p string) func() bool {
- return func() bool { c := w.claim; return c.Op.Kind == "relocating" && c.Op.Phase == p && c.Op.Stuck == "" }
+ return func() bool {
+ c := w.claim
+ return c.Op.Kind == "relocating" && relocPhaseName(c.Op) == p && c.Op.Stuck == ""
+ }
+}
+
+// relocPhaseName is the operation's phase as 1b-next names it: the
+// model's pinning with op.PinFailover set is production's starting.
+func relocPhaseName(op opState) string {
+ if op.Phase == "pinning" && op.PinFailover {
+ return "starting"
+ }
+ return op.Phase
}
// liveIn counts region r's live boxes.
@@ -97,8 +111,8 @@ func TestL18TerminationAtEveryExactPhase(t *testing.T) {
for _, boxes := range []int{1, 2} {
for _, who := range []string{"source", "target"} {
for _, phase := range phases {
- if boxes == 1 && (who == "source" || phase == "starting" || phase == "releasing") {
- continue // a one-box region relocates only by failover, which starts at pinning with the source fenced
+ if boxes == 1 && (who == "source" || phase == "releasing") {
+ continue // a one-box region relocates only by failover, whose source is fenced at its start; its starting is PinFailover's wait (rev 7)
}
if phase == "probe-failed" && who == "source" {
continue // the source has released before any probe; its loss is the pinning case
@@ -117,9 +131,12 @@ func TestL18TerminationAtEveryExactPhase(t *testing.T) {
target = func() *box { return w.boxByID(w.claim.Op.Tgt) }
} else {
w.terminate(from)
- if !w.stepUntil(t, 400, "a target named", func() bool { c := w.claim; return c.Op.Kind == "relocating" && c.Op.Tgt >= 0 }) {
+ if !w.stepUntil(t, 400, "the failover started with its target", func() bool { c := w.claim; return c.Op.Kind == "relocating" && c.Op.Tgt >= 0 }) {
w.mustHold(t)
}
+ if c := w.claim; relocPhaseName(c.Op) != "starting" {
+ t.Fatalf("the failover did not start in starting (PinFailover unset): %s", w.state())
+ }
w.boxByID(w.claim.Op.Tgt).FailApp = phase == "probe-failed"
target = func() *box { return w.boxByID(w.claim.Op.Tgt) }
}
@@ -128,9 +145,12 @@ func TestL18TerminationAtEveryExactPhase(t *testing.T) {
}
// immediately before the injection: the exact phase, and the
// region's live topology (no spare)
- if c := w.claim; c.Op.Phase != phase {
+ if c := w.claim; relocPhaseName(c.Op) != phase {
t.Fatalf("not at %s: %s", phase, w.state())
}
+ if c := w.claim; phase == "pinning" && (c.Op.PinFailover || c.Op.Pin != nil && c.Op.Exec >= 0) {
+ t.Fatalf("pinning is after PinFailover and before installing: %s", w.state())
+ }
if n := w.liveIn(0); n != boxes {
t.Fatalf("region 0 has %d live boxes before the injection, want %d", n, boxes)
}
@@ -469,20 +489,19 @@ func TestFailoverPinWaitsForTheAcknowledgement(t *testing.T) {
w.mustHold(t)
}
-// TestConvertedMovePinsBeforeAcknowledgement (rev 6, Astra round 3
-// finding 1): a move whose source is terminated before the flip becomes
-// a relocation at pinning (moves §7.10). It enters pinning directly, as
-// it does in 1b-next, where Worker.pinning selects and journals the pin
-// first and checks the acknowledgements only for ToInstalling: the pin is
-// journaled before the box that installs has acknowledged, and that box's
-// acknowledgement still comes before the installing CAS. Under rev 5's
-// wider guard the target acknowledged first, and this test fails.
-func TestConvertedMovePinsBeforeAcknowledgement(t *testing.T) {
- w := twoBoxWitness()
+// convertedMove serves the host on box 0 of a two-box witness world with
+// a spare box 30 in region 0, starts a move to region 1, and terminates
+// the source before the flip, so the regional worker converts the move
+// to a relocation at pinning with no target (moves §7.10). before runs
+// before the move starts.
+func (w *world) convertedMove(t *testing.T, before func()) *box {
src := w.boxes[0]
w.serve(src, 1, app0)
w.running(t, src)
w.published(t, src)
+ if before != nil {
+ before()
+ }
w.moveTo(1)
if w.claim.Op.Kind != "moving" {
t.Fatalf("no move: %s", w.state())
@@ -493,27 +512,147 @@ func TestConvertedMovePinsBeforeAcknowledgement(t *testing.T) {
return c.Op.Kind == "moving" && c.Op.Phase == "preparing" && contains(c.Regions, tgt.Region)
}, w.act(src, tgt))
w.terminate(src)
- var acksAtPin []int
- if !w.stepUntil(t, 400, "the converted move's pin", func() bool {
+ if !w.stepUntil(t, 400, "the move converted", func() bool {
c := w.claim
- if c.Op.Kind == "relocating" && c.Op.Pin != nil {
- acksAtPin = append([]int(nil), c.Op.Acks...)
- return true
- }
- return false
+ return c.Op.Kind == "relocating" && c.Op.FenceBox == src.ID
}) {
w.mustHold(t)
}
- if c := w.claim; c.Op.FenceBox != src.ID || c.Op.PinFailover {
- t.Fatalf("not a converted move: %s", w.state())
+ if c := w.claim; c.Op.PinFailover || c.Op.Pin != nil {
+ t.Fatalf("not a converted move at pinning without a pin: %s", w.state())
+ }
+ return src
+}
+
+// TestConvertedMovePinsBeforeAcknowledgement (rev 6, Astra round 3
+// finding 1; rev 7, round 4 finding 1): a converted move enters pinning
+// directly, as in 1b-next, and Worker.pinning names its target first,
+// then selects and journals the pin, and checks the acknowledgements only
+// for ToInstalling. The named target's controller does not run while the
+// region's other box works: the pin is journaled without the target's
+// acknowledgement, and installing waits for it.
+func TestConvertedMovePinsBeforeAcknowledgement(t *testing.T) {
+ w := twoBoxWitness()
+ spare := w.extraBox(0, 30)
+ w.convertedMove(t, nil)
+ if !w.stepUntil(t, 400, "the target named", func() bool { c := w.claim; return c.Op.Tgt >= 0 || c.Op.Pin != nil }) {
+ w.mustHold(t)
+ }
+ c := w.claim
+ if c.Op.Pin != nil {
+ t.Fatalf("pinned before a target was named: %s", w.state())
+ }
+ tgt := w.boxByID(c.Op.Tgt)
+ worker := spare
+ if tgt == spare {
+ worker = w.boxes[3]
+ }
+ w.drive(failoverPinDelay+20, never, w.act(worker)) // the target's controller does not run
+ c = w.claim
+ if contains(c.Op.Acks, tgt.ID) {
+ t.Fatalf("the target acknowledged without running")
+ }
+ if c.Op.Pin == nil {
+ t.Fatalf("the converted move waited for an acknowledgement before its pin: %s", w.state())
+ }
+ if c.Op.Phase != "pinning" || c.Op.Exec >= 0 {
+ t.Fatalf("installing without the target's acknowledgement: %s", w.state())
+ }
+ w.servingOn(t, tgt)
+ w.finish(t)
+ w.mustHold(t)
+}
+
+// TestConvertedMoveWaitsForATargetBeforeItsPin (reloc-name-before-pin;
+// rev 7, Astra round 4 finding 1): the source's newer files manifest is
+// in flight when the move starts and when the source is terminated. No
+// box of the region is eligible (the spare has no key), so the converted
+// move names no target and selects no pin; the manifest lands; the
+// spare becomes eligible, is named, and the pin names the newer
+// manifest. The mutation pins first, without the manifest.
+func TestConvertedMoveWaitsForATargetBeforeItsPin(t *testing.T) {
+ w := twoBoxWitness()
+ peer := w.boxes[3]
+ var newer string
+ w.convertedMove(t, func() {
+ src, c := w.boxes[0], w.claim
+ src.Files.Env++ // a newer files state: the admin token rotated
+ newer = manifestKey(c.Holder.Location, c.Holder.Gen, src.pubSeq+1)
+ w.holdKey(newer)
+ w.publishFiles(src)
+ w.hold = nil
+ peer.HasKey = false // the region's other box may work, never take the host
+ })
+ if newer == "" || w.boxes[0].pubSeq == 0 {
+ t.Fatalf("the newer manifest was not issued")
+ }
+ w.drive(failoverPinDelay+20, never, w.act(peer))
+ if c := w.claim; c.Op.Pin != nil || c.Op.Tgt >= 0 {
+ t.Fatalf("pinned or named with no eligible box: %s", w.state())
+ }
+ if n := w.completeHeld(newer); n != 1 {
+ t.Fatalf("held manifest PUTs completed: %d, want 1", n)
}
- var installer int = -1
- if !w.stepUntil(t, 1500, "installing", func() bool {
+ peer.HasKey = true
+ if !w.reach(t, 400, "the pin", func() bool { return w.claim.Op.Pin != nil }, w.act(peer)) {
+ w.mustHold(t)
+ }
+ if p := w.claim.Op.Pin; p.ManKey != newer {
+ t.Fatalf("the pin names %s, want the manifest that landed while no box was eligible, %s", p.ManKey, newer)
+ }
+ w.servingOn(t, peer)
+ 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
+// Admission.Register); once it reopens, it starts and serves on the
+// region's other box.
+func TestFailoverStartWaitsForAdmission(t *testing.T) {
+ w := twoBoxWitness()
+ from := w.boxes[0]
+ w.serve(from, 1, app0)
+ w.running(t, from)
+ w.published(t, from)
+ ad := w.admit[app0]
+ ad.Closed = true
+ w.terminate(from)
+ w.drive(60, never, w.actAll(), w.recoveryPass)
+ if c := w.claim; c.Op.Kind != "serving" || contains(c.Lost, from.ID) {
+ t.Fatalf("a failover started while the app's admission was closed: %s", w.state())
+ }
+ ad.Closed = false
+ if to := w.failedOver(t, from); to == nil || to.Region != from.Region {
+ t.Fatalf("no failover in the region: %s", w.state()) // the peer, or the group's replacement, whichever choose() prefers
+ }
+ w.finish(t)
+ w.mustHold(t)
+}
+
+// TestFailoverStartWaitsForParkReplica (reloc-failover-start-guard; rev
+// 7, Astra round 4 finding 3): a park-replica chore is outstanding in the
+// region when the serving executor is terminated. RelocationStartGuard
+// refuses the failover's start until the chore is done; the source's own
+// park-local (the fenced source) would not have.
+func TestFailoverStartWaitsForParkReplica(t *testing.T) {
+ w := twoBoxWitness()
+ from := w.boxes[0]
+ w.serve(from, 1, app0)
+ w.running(t, from)
+ w.published(t, from)
+ w.claim.Obl = append(w.claim.Obl, w.scoped(obligation{ID: "pr", Op: "old-op", Kind: "park-replica", Region: 0, Box: -1, Prefix: "moves/" + host + "/", Quiet: w.now + 20}, w.now, 1))
+ w.claim.Obl = append(w.claim.Obl, obligation{ID: "pl", Op: "old-op", Kind: "park-local", Box: from.ID, Region: -1, Ret: "old-op"})
+ from.DeleteOnTermination = false // the fence keeps the park-local open
+ w.terminate(from)
+ if !w.stepUntil(t, 400, "the failover's start", func() bool {
c := w.claim
- if c.Op.Kind == "relocating" && c.Op.Phase == "installing" {
- installer = c.Op.Exec
- if !acked(c) {
- t.Fatalf("installing without the acknowledgements: %s", w.state())
+ if c.Op.Kind == "relocating" {
+ for _, o := range c.Obl {
+ if o.Kind == "park-replica" && o.Region == 0 {
+ t.Fatalf("the failover started with a park-replica outstanding in its region: %s", w.state())
+ }
}
return true
}
@@ -521,14 +660,56 @@ func TestConvertedMovePinsBeforeAcknowledgement(t *testing.T) {
}) {
w.mustHold(t)
}
- if contains(acksAtPin, installer) {
- t.Fatalf("box %d acknowledged before the pin: a converted move waited for PinFailover's barrier", installer)
+ if !w.owesLocal(w.claim, from) {
+ t.Fatalf("the fenced source's park-local was not kept open: %s", w.state())
+ }
+ if to := w.failedOver(t, from); to == nil || to.Region != from.Region {
+ t.Fatalf("no failover in the region: %s", w.state())
}
- w.servingOn(t, w.boxByID(installer))
w.finish(t)
w.mustHold(t)
}
+// TestFailoverTargetLossAroundPinFailover (rev 7, Astra round 4 finding
+// 2): an initial failover's target is terminated while PinFailover is
+// pending (production's starting) and, in a second run, after it has
+// cleared and before installing (pinning). In a two-box region with a
+// spare, the target is replaced in the same phase and the host serves.
+func TestFailoverTargetLossAroundPinFailover(t *testing.T) {
+ for _, phase := range []string{"starting", "pinning"} {
+ t.Run(phase, func(t *testing.T) {
+ w := twoBoxWitness()
+ from := w.boxes[0]
+ w.extraBox(0, 30)
+ w.serve(from, 1, app0)
+ w.running(t, from)
+ w.published(t, from)
+ w.terminate(from)
+ if !w.stepUntil(t, 400, "the failover exactly at "+phase, w.atPhase(phase)) {
+ w.mustHold(t)
+ }
+ c := w.claim
+ if (phase == "starting") != c.Op.PinFailover || c.Op.Exec >= 0 || c.Op.Tgt < 0 {
+ t.Fatalf("not at %s: %s", phase, w.state())
+ }
+ victim := w.boxByID(c.Op.Tgt)
+ w.terminate(victim)
+ if !w.stepUntil(t, 400, "the target replaced", func() bool {
+ c := w.claim
+ return contains(c.Lost, victim.ID) && c.Op.Tgt >= 0 && c.Op.Tgt != victim.ID
+ }) {
+ w.mustHold(t)
+ }
+ if got := relocPhaseName(w.claim.Op); got != phase {
+ t.Fatalf("the replacement left %s for %s: %s", phase, got, w.state())
+ }
+ w.servingOn(t, nil)
+ w.finish(t)
+ w.mustHold(t)
+ })
+ }
+}
+
// TestPinNeverShortOfTheRelease (reloc-pin-reaches-release): the listing
// lags behind the journaled release (its newest file is not yet visible);
// no pin is journaled short of the release's final_txid.
diff --git a/internal/sim/hostlife/regionha_test.go b/internal/sim/hostlife/regionha_test.go
index 28784de7d..cb1d257d0 100644
--- a/internal/sim/hostlife/regionha_test.go
+++ b/internal/sim/hostlife/regionha_test.go
@@ -40,9 +40,9 @@ func (w *world) userRelocate() {
if from == nil || from.Destroyed || from.Old || !from.Enrolled {
return
}
- if ad := w.admit[c.Holder.App]; ad != nil && ad.Closed {
- return // a box-started relocation needs the app's admission registration (1b-next ruling 4): a purge closed it
- }
+ // Worker.Start's order (rev 7): the source unfenced, a writer to
+ // release, an eligible target, the admission registration; the CAS
+ // rechecks the admission and applies the start guard
if on("reloc-drain-needs-writer") && c.Holder.Session == 0 {
w.stats["drain refused: the host never had a writer"]++
return
@@ -51,9 +51,18 @@ func (w *world) userRelocate() {
if to == nil || to.Old {
return
}
+ if ad := w.admit[c.Holder.App]; ad != nil && ad.Closed {
+ return // a box-started relocation needs the app's admission registration (1b-next ruling 4): a purge closed it
+ }
id := w.newID("rl")
if w.cas(c, func(n *claim) bool {
- if n.Holder == nil || n.Op.Kind != "serving" || n.Op.Exec != from.ID || !w.relocationStartAllowed(n, from, to) {
+ if n.Holder == nil || n.Op.Kind != "serving" || n.Op.Exec != from.ID || contains(n.Lost, to.ID) {
+ return false
+ }
+ if ad := w.admit[n.Holder.App]; ad != nil && ad.Closed {
+ return false // Admission.Recheck
+ }
+ if !w.relocationStartAllowed(n, from, to) {
return false
}
n.Op = opState{Kind: "relocating", ID: id, Phase: "starting", Exec: from.ID, Parts: []int{from.ID, to.ID},
@@ -74,6 +83,12 @@ func (w *world) userRelocate() {
// one being retired. The mutation of reloc-start-guard starts over
// anything.
func (w *world) relocationStartAllowed(c *claim, from, to *box) bool {
+ return w.relocationStartGuard(c, from, to, false)
+}
+
+// relocationStartGuard is RelocationStartGuard(c, region, source, target,
+// sourceFenced): a failover's fenced source's park-local does not block.
+func (w *world) relocationStartGuard(c *claim, from, to *box, sourceFenced bool) bool {
if !on("reloc-start-guard") {
return true
}
@@ -82,7 +97,7 @@ func (w *world) relocationStartAllowed(c *claim, from, to *box) bool {
case o.Kind == "park-generation":
continue // L11
case o.Kind == "park-local":
- if o.Box == to.ID || o.Box == from.ID && !contains(c.Lost, from.ID) {
+ if o.Box == to.ID || o.Box == from.ID && !sourceFenced && !contains(c.Lost, from.ID) {
return false
}
case o.Region == from.Region:
@@ -697,6 +712,16 @@ func (w *world) relocPinning(b *box, c *claim) {
}
return
}
+ if op.Tgt < 0 && on("reloc-name-before-pin") {
+ // Worker.pinning names a missing target before it selects any pin
+ // (1b-next rev 19; rev 7, Astra round 4 finding 1), on every path
+ // that enters pinning without one: a converted move, an operator's
+ // replay. With no eligible box it waits, and a manifest that lands
+ // meanwhile is in the later pin. The mutation pins first, as rev 6
+ // did for these paths
+ w.relocNameTarget(c)
+ return
+ }
if op.Pin == nil {
if on("reloc-failover-pin-delay") && (op.Release == nil || on("reloc-pin-delay-every-fence")) && w.now < latestObservation(op)+failoverPinDelay {
return
@@ -1504,7 +1529,7 @@ func (w *world) fence(b *box, c *claim, x *box) {
if !sameOp(n.Op.ID, id) || n.Op.Kind != "landing" || !n.Op.Committed || contains(n.Lost, x.ID) {
return false
}
- w.startFailover(n, x)
+ w.startFailover(n, x, nil) // the model's conversion (plan ruling 20): its target is named at pinning
w.fenceBox(n, x)
return true
}) {
@@ -1526,13 +1551,24 @@ func (w *world) fence(b *box, c *claim, x *box) {
return // Worker.Step consumes no fence of a stuck operation: the operator's resolve does
}
id := op.ID
+ var to *box
+ if c.Holder != nil && op.Kind == "serving" && op.Exec == x.ID {
+ var ok bool
+ if to, ok = w.failoverStart(c, x); !ok {
+ return // no start yet: the claim, and the fence, wait for a later pass
+ }
+ }
if w.cas(c, func(n *claim) bool {
if !sameOp(n.Op.ID, id) || n.Op.Kind != op.Kind || contains(n.Lost, x.ID) {
return false
}
switch {
case n.Holder != nil && n.Op.Kind == "serving" && n.Op.Exec == x.ID:
- w.startFailover(n, x)
+ if !w.failoverStartAllowed(n, x, to) {
+ w.stats["failover start: refused by the start CAS"]++
+ return false
+ }
+ w.startFailover(n, x, to)
case n.Op.Kind == "relocating" && n.Op.Stuck != "":
return false
case n.Op.Kind == "relocating" && n.Op.Src == x.ID:
@@ -1668,12 +1704,55 @@ func (w *world) deadBoxFiles(x *box) *filesDir {
// pin is selected (PinFailover's barrier, rule
// reloc-failover-ack-before-pin, rev 5 and 6), and the pin waits out
// failoverPinDelay from the fence.
-func (w *world) startFailover(n *claim, x *box) {
+func (w *world) startFailover(n *claim, x *box, to *box) {
n.Op = opState{Kind: "relocating", ID: w.newID("rl"), Phase: "pinning", Exec: -1, Src: x.ID, Tgt: -1, SrcRegion: x.Region,
RelocReason: "failover", ReqAt: w.now, App: n.Holder.App, SrcGen: n.Holder.Gen, SrcStamp: n.Holder.Stamp, StopFiles: w.deadBoxFiles(x), PinFailover: true}
+ if to != nil {
+ // StartRelocation names the target and makes it the only
+ // participant (rev 7, Astra round 4 finding 3)
+ n.Op.Tgt, n.Op.Parts = to.ID, []int{to.ID}
+ }
w.stats["relocation started: failover"]++
}
+// failoverStart is Worker.Start for a failover (1b-next rev 19; rev 7,
+// Astra round 4 finding 3), the checks before the start CAS in its order:
+// the claim serves on the fenced source, an eligible target exists
+// (Eligible), and the app admits the registration (Admission.Register).
+// It returns the target, or nil when the start must wait for a later
+// pass; the CAS rechecks the admission and applies RelocationStartGuard
+// with the source fenced (failoverStartAllowed). The mutation of
+// reloc-failover-start-guard starts at once with no target, as rev 6 did.
+func (w *world) failoverStart(c *claim, x *box) (*box, bool) {
+ if !on("reloc-failover-start-guard") {
+ return nil, true
+ }
+ to := w.chooseBoxExcept(x.Region, c.Holder.App, x.ID)
+ if to == nil {
+ w.stats["failover start: no eligible target yet"]++
+ return nil, false
+ }
+ if ad := w.admit[c.Holder.App]; ad != nil && ad.Closed {
+ w.stats["failover start: app admission closed"]++
+ return nil, false
+ }
+ return to, true
+}
+
+// failoverStartAllowed is the start CAS's own checks for a failover:
+// the admission recheck (Admission.Recheck), the target not on lost, and
+// RelocationStartGuard with the source fenced, so the source's own
+// park-local does not block (L11) and a park-replica in the region does.
+func (w *world) failoverStartAllowed(n *claim, x, to *box) bool {
+ if !on("reloc-failover-start-guard") {
+ return true
+ }
+ if ad := w.admit[n.Holder.App]; ad != nil && ad.Closed {
+ return false
+ }
+ return to != nil && !contains(n.Lost, to.ID) && w.relocationStartGuard(n, x, to, true)
+}
+
// fenceSource is §5.8's source loss (B1-6, FenceSource): a drain whose
// source is terminated before its release is journaled becomes a
// failover in the same CAS, op.exec none, the stamp kept, the source off
diff --git a/internal/sim/hostlife/regionha_witness_test.go b/internal/sim/hostlife/regionha_witness_test.go
index 575717734..a1a955d8e 100644
--- a/internal/sim/hostlife/regionha_witness_test.go
+++ b/internal/sim/hostlife/regionha_witness_test.go
@@ -73,14 +73,12 @@ func TestUnenrolledReferenceNeverChosen(t *testing.T) {
t.Fatalf("no unenrolled replacement in region 0: %+v", nb)
}
nb.EnrollAt = w.now + 10*enrollDelay // its confirmation is slow
- w.reach(t, 100, "the executor fenced by the peer", func() bool {
- return contains(w.claim.Lost, from.ID) && w.claim.Op.Kind == "relocating"
- }, w.act(peer), w.recoveryPass)
- // nb stays unenrolled, and the relocation must wait at pinning with no
- // target
+ // nb stays unenrolled and the peer has no key: no box is eligible, so
+ // the failover does not start (Worker.Start's Eligible, rev 7) and no
+ // unenrolled box is named
w.drive(enrollDelay, func() bool { return false }, w.actAll(), w.recoveryPass)
- if c := w.claim; c.Op.Kind != "relocating" || c.Op.Tgt != -1 || c.Op.Exec != -1 {
- t.Fatalf("an unenrolled box was named, or the relocation moved on: %s", w.state())
+ if c := w.claim; c.Op.Kind != "serving" || c.Op.Exec != from.ID || c.Op.Tgt == nb.ID {
+ t.Fatalf("an unenrolled box was named, or the failover started with no eligible target: %s", w.state())
}
nb.EnrollAt = w.now - enrollDelay
w.enrollStep()
diff --git a/internal/sim/hostlife/rules_test.go b/internal/sim/hostlife/rules_test.go
index 034684e3b..06b9849c3 100644
--- a/internal/sim/hostlife/rules_test.go
+++ b/internal/sim/hostlife/rules_test.go
@@ -197,5 +197,7 @@ var allRules = []string{
"files-live-set-moves-parks", // finding F4 (rev 4), claim §6.2a: moves' parks (a push's whole-location park, a landing's install park, a rollback's return park) keep the files live set; the mutation archives it with the rest and the next failover can never pin the live files (INV-3)
"reloc-clear-after-cleanup", // 1b-next ruling 20 and rev 6 R4-5 (Finish clears the record only after a successful scoped cleanup): a failed cleanup keeps the controller record, which blocks executable updates (claim §11's witness); the mutation clears it and an update runs over the unfinished cleanup (INV-29)
"fence-converts-committed-landing", // finding F5 (rev 4; claim §11 "automatic target loss racing the record commit CAS"): a landing whose record committed and whose target is then terminated becomes a failover in the target's region; the mutation leaves it to the operator, and it never completes (INV-3)
+ "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)
}