amadan
sim: Astra's round 5 on the two-box model: a relocation participant's fence that cannot be consumed yet holds the regional phase, as Worker.Step returns before its phase switch, and the worker fences the source, then the target, then any other box
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
5 files changed,
+131
−10
internal/sim/hostlife/moves_test.go+21 −1internal/sim/hostlife/regionha_round1_test.go+57 −0internal/sim/hostlife/regionha_test.go+51 −9internal/sim/hostlife/rules_test.go+1 −0internal/sim/hostlife/world_test.go+1 −0
diff --git a/internal/sim/hostlife/moves_test.go b/internal/sim/hostlife/moves_test.go| index 6150cf544..fd657a53a 100644 |
| --- a/internal/sim/hostlife/moves_test.go |
| +++ b/internal/sim/hostlife/moves_test.go |
| @@ -51,10 +51,18 @@ func (w *world) workerMode(b *box, obl bool) { |
| } else if w.rng.Intn(10) == 0 { |
| b.stale = c.clone() |
| } |
| - if w.fenceStep(b, c) { |
| + changed, pending := w.fenceStep(b, c) |
| + if changed { |
| return // the regional worker's termination fence (region HA §5.9), before its role |
| } |
| + // a relocation participant's fence this worker could not consume yet |
| + // (a dead target with no spare before its deadline): Worker.Step |
| + // returns w.replace(...) before the phase switch, so the regional |
| + // transitions wait; the participant work that does not go through |
| + // Worker.Step still runs (rev 8, Astra round 5) |
| + b.fencePending = pending |
| w.role(b, c) |
| + b.fencePending = false |
| } |
| // initRecord is claim rev 6.5 §6.4's initialization (R5-4): a box creates |
| @@ -295,6 +303,18 @@ func (w *world) relocate(b *box, c *claim) { |
| if b.Region != op.SrcRegion || b.Destroyed || contains(c.Lost, b.ID) || !b.Enrolled || op.Stuck != "" { |
| return |
| } |
| + if b.fencePending && on("reloc-fence-pending-blocks") { |
| + // Worker.Step returned w.replace(...) before its phase switch (rev |
| + // 8, Astra round 5): no regional transition while a participant's |
| + // fence is pending. A live executor's own release sequence is the |
| + // participant's (1b-next Task 7), not Worker.Step's, so it runs. |
| + // The mutation goes on into the phase switch, as rev 7 did |
| + w.stats["relocation: phase held, a participant's fence is pending"]++ |
| + if (op.Phase == "releasing" || op.Phase == "probe-failed") && b.ID == op.Exec && (op.Release == nil || op.Release.Box != op.Exec) { |
| + w.relocJournalRelease(b, c) |
| + } |
| + return |
| + } |
| switch op.Phase { |
| case "starting": |
| w.relocStarting(b, c) |
diff --git a/internal/sim/hostlife/regionha_round1_test.go b/internal/sim/hostlife/regionha_round1_test.go| index 6cc45814f..28f7dd703 100644 |
| --- a/internal/sim/hostlife/regionha_round1_test.go |
| +++ b/internal/sim/hostlife/regionha_round1_test.go |
| @@ -710,6 +710,63 @@ func TestFailoverTargetLossAroundPinFailover(t *testing.T) { |
| } |
| } |
| +// TestPendingTargetFenceHoldsThePhase (reloc-fence-pending-blocks; rev |
| +// 8, Astra round 5): a drain's target has acknowledged and is terminated, |
| +// once in starting and once in pinning before a pin; the region's group |
| +// launches no replacement, so the fence cannot be consumed until its |
| +// deadline. Until then the source's worker makes no regional transition: |
| +// starting does not go to releasing, and pinning selects no pin. Under |
| +// the mutation the worker goes on into the phase switch and this test |
| +// fails. Past the deadline the fence is consumed and the operation is |
| +// stuck, as FenceTargetWithoutSpare makes it. |
| +func TestPendingTargetFenceHoldsThePhase(t *testing.T) { |
| + for _, phase := range []string{"starting", "pinning"} { |
| + t.Run(phase, func(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.oneBoxRegion[0] = true // no replacement launches: no spare |
| + w.drainTo(t, to) |
| + if phase == "starting" { |
| + // the target's controller acknowledges (AcknowledgeExecution); |
| + // the source has not yet, so the operation stays in starting |
| + to.ExecUntil = w.localNow(to) + execTTL |
| + w.recordAck(to, w.claim.clone()) |
| + } else if !w.stepUntil(t, 1500, "the target acknowledged at "+phase, func() bool { |
| + c := w.claim |
| + return contains(c.Op.Acks, to.ID) && w.atPhase(phase)() && c.Op.Pin == nil |
| + }) { |
| + w.mustHold(t) |
| + } |
| + if c := w.claim; !contains(c.Op.Acks, to.ID) || !w.atPhase(phase)() || c.Op.Pin != nil { |
| + t.Fatalf("not at %s with the target acknowledged: %s", phase, w.state()) |
| + } |
| + w.oneBoxRegion[0] = false |
| + w.terminate(to) |
| + w.oneBoxRegion[0] = true |
| + for i := 0; i < releaseDeadline-10; i++ { |
| + w.tick(w.act(from)) |
| + c := w.claim |
| + if relocPhaseName(c.Op) != phase || c.Op.Pin != nil { |
| + t.Fatalf("the phase moved on while the target's fence was pending (step %d): %s", i, w.state()) |
| + } |
| + if contains(c.Lost, to.ID) { |
| + t.Fatalf("the dead target was fenced with no spare before its deadline: %s", w.state()) |
| + } |
| + } |
| + w.mustHold(t) |
| + if w.stats["relocation: phase held, a participant's fence is pending"] == 0 { |
| + t.Fatalf("no worker step held the phase") |
| + } |
| + if !w.reach(t, 100, "the fence consumed into stuck", func() bool { c := w.claim; return contains(c.Lost, to.ID) && c.Op.Stuck != "" }, w.act(from)) { |
| + 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 cb1d257d0..376e15129 100644 |
| --- a/internal/sim/hostlife/regionha_test.go |
| +++ b/internal/sim/hostlife/regionha_test.go |
| @@ -2,6 +2,7 @@ package hostlife |
| import ( |
| "fmt" |
| + "sort" |
| "strings" |
| ) |
| @@ -1440,9 +1441,9 @@ func (w *world) regionHAOwnsLoss(b *box) bool { |
| // destroyed box. An unenrolled box has no roster entry to bind the fence |
| // to (HA7) and is never fenced. The source's fence is consumed before the |
| // target's, as Worker.Step orders them. |
| -func (w *world) fenceStep(b *box, c *claim) bool { |
| +func (w *world) fenceStep(b *box, c *claim) (changed, pending bool) { |
| if c == nil || !b.Enrolled || contains(c.Lost, b.ID) { |
| - return false |
| + return false, false |
| } |
| var cands []*box |
| for _, x := range w.boxes { |
| @@ -1455,15 +1456,23 @@ func (w *world) fenceStep(b *box, c *claim) bool { |
| if !w.claimNames(c, x) { |
| continue |
| } |
| - if c.Op.Kind == "relocating" && x.ID == c.Op.Src { |
| - cands = append([]*box{x}, cands...) |
| - } else { |
| - cands = append(cands, x) |
| - } |
| + cands = append(cands, x) |
| } |
| if len(cands) == 0 { |
| - return false |
| + return false, false |
| + } |
| + // Worker.Step's order (rev 8): the source's fence, then the target's, |
| + // then any other box the claim names (a chore's owner) |
| + rank := func(x *box) int { |
| + switch { |
| + case c.Op.Kind == "relocating" && x.ID == c.Op.Src: |
| + return 0 |
| + case c.Op.Kind == "relocating" && x.ID == c.Op.Tgt: |
| + return 1 |
| + } |
| + return 2 |
| } |
| + sort.SliceStable(cands, func(i, j int) bool { return rank(cands[i]) < rank(cands[j]) }) |
| if x := cands[0]; x.FenceObservedAt == 0 { |
| // hostfence.TerminationWorker: the first worker to observe the |
| // terminated state writes the box-fences record with that |
| @@ -1474,7 +1483,12 @@ func (w *world) fenceStep(b *box, c *claim) bool { |
| } |
| before := w.claim.Ver |
| w.fence(b, c, cands[0]) |
| - return w.claim.Ver != before |
| + if w.claim.Ver != before { |
| + return true, false |
| + } |
| + // nothing written: for a relocation's source or target the fence is |
| + // pending (rule reloc-fence-pending-blocks) |
| + return false, c.Op.Kind == "relocating" && rank(cands[0]) < 2 |
| } |
| // claimNames: the claim gives x a role, so a fence changes it. |
| @@ -2258,3 +2272,31 @@ func (w *world) preparedManifestHere(b *box, c *claim, gen string) bool { |
| bl := &blob{Kind: "files", Inc: h.Inc, Gen: gen, Seq: 0, Files: b.Files.clone(), Timers: append([]int(nil), b.Timers...), Text: c.Op.ID, Base: w.issued} |
| return w.ackedPut(b, manifestKey(h.Location, gen, 0), bl, true) |
| } |
| + |
| +// relocJournalRelease is the participant's release (1b-next Task 7): the |
| +// live executor runs its release sequence and journals it |
| +// (JournalRelease), the source in releasing, a failed target in |
| +// probe-failed. It is the release branch of relocReleasing and |
| +// relocProbeFailed, run by itself while a fence is pending (rev 8). |
| +func (w *world) relocJournalRelease(b *box, c *claim) { |
| + op := c.Op |
| + phase := op.Phase |
| + r := w.relocRelease(b, c) |
| + if r == nil { |
| + return |
| + } |
| + if w.cas(c, func(n *claim) bool { |
| + ok := sameOp(n.Op.ID, op.ID) && n.Op.Kind == "relocating" && n.Op.Phase == phase && n.Op.Exec == b.ID && (n.Op.Release == nil || phase == "probe-failed" && n.Op.Release.Box != b.ID) |
| + if ok { |
| + n.Op.Release = r |
| + } |
| + return ok |
| + }) { |
| + if phase == "releasing" { |
| + w.stats["release journaled: source"]++ |
| + } else { |
| + w.stats["release journaled: failed target"]++ |
| + } |
| + w.logf("relocation %s: box %d released the host at TXID %d (flushed=%v), a fence pending", op.ID, b.ID, r.FinalTX, r.Flushed) |
| + } |
| +} |
diff --git a/internal/sim/hostlife/rules_test.go b/internal/sim/hostlife/rules_test.go| index 06b9849c3..ed233915e 100644 |
| --- a/internal/sim/hostlife/rules_test.go |
| +++ b/internal/sim/hostlife/rules_test.go |
| @@ -197,6 +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-fence-pending-blocks", // rev 8 (Astra round 5; 1b-next rev 19 Worker.Step returns w.replace(...) before its phase switch): while a relocation participant's fence is pending (a dead target, no spare, before its deadline) no regional phase transition runs; the participant's own release still does; the mutation goes on into the phase switch (TestPendingTargetFenceHoldsThePhase) |
| "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) |
diff --git a/internal/sim/hostlife/world_test.go b/internal/sim/hostlife/world_test.go| index f901aeded..5cb9f479f 100644 |
| --- a/internal/sim/hostlife/world_test.go |
| +++ b/internal/sim/hostlife/world_test.go |
| @@ -373,6 +373,7 @@ type box struct { |
| execRecord string |
| cleanupPending bool |
| cleanupFails bool |
| + fencePending bool // (rev 8) this worker step found a relocation participant's fence it could not consume |
| FenceObservedAt int // the box-fences record's observed_at: when a worker first saw it terminated; 0 no record (rev 4) |
| Enrolled bool // the roster holds an active entry with its proven cloud identity (H11); a replacement box is enrolled automatically enrollDelay steps after it launches (H16, H17) |
| EnrollAt int |