amadan
sim: a committed landing's failover keeps the landing's op id
Joint round J3. The fence's conversion of a committed landing whose target has terminated (rule fence-converts-committed-landing) minted a new op id for the same-region failover. hostclaim ConvertCommittedLanding (region-ha-1b-next-build 2ced0c5d) keeps the landing's id, because the move's admission registration is the move id and judgeRegistration drains it 90 seconds in unless the claim's operation carries that id (hostops RegisterMove). The model's pre-flip conversion (convertToRelocating) already kept it. startFailover now takes the operation's id: a serving executor's failover passes a fresh one, minted at the same point as before; the committed landing's conversion passes the landing's own and mints none. TestAutomaticTargetLossRacesRecordCommit's "after the commit" case now checks the relocation carries the landing's id. One-box COUNTERS ae19edaec4491fd3 and traces unchanged; two-box COUNTERS at 300 seeds unchanged (fea529f94642f661): no random seed reaches the conversion, at 300 or 3000 seeds; only its witness and direct test do.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
2 files changed,
+25
−6
internal/sim/hostlife/regionha_round1_test.go+12 −0internal/sim/hostlife/regionha_test.go+13 −6
CI failed — run details
diff --git a/internal/sim/hostlife/regionha_round1_test.go b/internal/sim/hostlife/regionha_round1_test.go| index 0f8555f01..a7620b164 100644 |
| --- a/internal/sim/hostlife/regionha_round1_test.go |
| +++ b/internal/sim/hostlife/regionha_round1_test.go |
| @@ -1244,7 +1244,19 @@ func TestAutomaticTargetLossRacesRecordCommit(t *testing.T) { |
| if !ok { |
| w.mustHold(t) |
| } |
| + landing := w.claim.Op.ID |
| w.terminate(tgt) |
| + if when == "after the commit" { |
| + // the failover keeps the landing's op id, as hostclaim |
| + // ConvertCommittedLanding does: the move's admission |
| + // registration is drained unless the claim carries it |
| + if !w.stepUntil(t, 400, "the committed landing converted", func() bool { return w.claim.Op.Kind == "relocating" }) { |
| + w.mustHold(t) |
| + } |
| + if w.claim.Op.ID != landing { |
| + t.Fatalf("the committed landing %s converted to relocation %s, want the landing's op id kept: %s", landing, w.claim.Op.ID, w.state()) |
| + } |
| + } |
| w.servingOn(t, nil) |
| w.finish(t) |
| w.mustHold(t) |
diff --git a/internal/sim/hostlife/regionha_test.go b/internal/sim/hostlife/regionha_test.go| index bb4644a2a..270735ccb 100644 |
| --- a/internal/sim/hostlife/regionha_test.go |
| +++ b/internal/sim/hostlife/regionha_test.go |
| @@ -1596,13 +1596,18 @@ func (w *world) fence(b *box, c *claim, x *box) { |
| // rollback is possible, and its dead target can never finish it. |
| // The fence makes it a failover in the target's region, as a |
| // serving executor's fence does (plan ruling 20); the mutation |
| - // leaves it to the operator's path, which has nothing to do |
| + // leaves it to the operator's path, which has nothing to do. The |
| + // failover keeps the landing's op id, as hostclaim |
| + // ConvertCommittedLanding does (and as convertToRelocating does |
| + // before the flip): the move's admission registration is the move |
| + // id, and judgeRegistration drains it 90 seconds in unless the |
| + // claim's operation carries that id (hostops RegisterMove) |
| id := op.ID |
| if w.cas(c, func(n *claim) bool { |
| if !sameOp(n.Op.ID, id) || n.Op.Kind != "landing" || !n.Op.Committed || contains(n.Lost, x.ID) { |
| return false |
| } |
| - w.startFailover(n, x, nil) // the model's conversion (plan ruling 20): its target is named at pinning |
| + w.startFailover(n, x, nil, id) // the model's conversion (plan ruling 20): its target is named at pinning |
| w.fenceBox(n, x) |
| return true |
| }) { |
| @@ -1641,7 +1646,7 @@ func (w *world) fence(b *box, c *claim, x *box) { |
| w.stats["failover start: refused by the start CAS"]++ |
| return false |
| } |
| - w.startFailover(n, x, to) |
| + w.startFailover(n, x, to, w.newID("rl")) |
| case n.Op.Kind == "relocating" && n.Op.Stuck != "": |
| return false |
| case n.Op.Kind == "relocating" && n.Op.Src == x.ID: |
| @@ -1795,9 +1800,11 @@ func (w *world) deadBoxFiles(x *box) *filesDir { |
| // reloc-failover-start-guard starts with none, and pinning names one. |
| // The target acknowledges before the 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, to *box) { |
| - n.Op = opState{Kind: "relocating", ID: w.newID("rl"), Phase: "pinning", Exec: -1, Src: x.ID, Tgt: -1, SrcRegion: x.Region, |
| +// waits out failoverPinDelay from the fence. id is the operation's id: a |
| +// fresh one for a serving executor's failover, the landing's own for a |
| +// committed landing's conversion (ConvertCommittedLanding keeps it). |
| +func (w *world) startFailover(n *claim, x *box, to *box, id string) { |
| + n.Op = opState{Kind: "relocating", ID: id, 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 |