amadan
docs: two-box model plan rev 7, Astra round 4: the target named before any pin on every path, PinFailover in the phase predicates, Worker.Start's guards on a failover's start, the entry points compared with 1b-next in order, Task 5D and the round 4 dispositions
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
1 file changed,
+638
−11
docs/superpowers/plans/2026-10-07-region-ha-hostlife-two-box.md+638 −11
diff --git a/docs/superpowers/plans/2026-10-07-region-ha-hostlife-two-box.md b/docs/superpowers/plans/2026-10-07-region-ha-hostlife-two-box.md| index a4c6cef8b..fea58c6cb 100644 |
| --- a/docs/superpowers/plans/2026-10-07-region-ha-hostlife-two-box.md |
| +++ b/docs/superpowers/plans/2026-10-07-region-ha-hostlife-two-box.md |
| @@ -1,15 +1,47 @@ |
| -# Region HA: the joint model with two boxes per region (L18) Implementation Plan (rev 6) |
| +# Region HA: the joint model with two boxes per region (L18) Implementation Plan (rev 7) |
| > **For agentic workers:** REQUIRED SUB-SKILL: Use superpowers:subagent-driven-development (recommended) or superpowers:executing-plans to implement this plan task-by-task. Steps use checkbox (`- [ ]`) syntax for tracking. |
| **Goal:** Extend `internal/sim/hostlife`, the joint executable model of the host lifecycle claim and instance moves, from one box per region to one or two boxes per region, with region HA's `relocating` operation modelled as spec 1 §5.8 and plan 1b-next **rev 19** define it (drain, failover, pinning, the replacement table, `stuck`), every case claim rev 6.30 §11 and spec L18 name for region HA's validation milestone as a scenario in a one-box and in a two-box region, and one mutation check per guard; then write the brief for the joint round that gates the merge of relocation (claim §1.1, R18-3; plan 1b-next Task 11). |
| -**Architecture:** Nine tasks (rev 4 adds Task 5B, rev 5 Task 5C) over one Go test package (every file is `_test.go`; nothing here is product code). Task 1 generalises the world's shape (`boxesPerRegion`, 1 or 2) so the one-box sweep stays byte-identical to the baseline and a two-box sweep runs beside it. Task 2 replaces the collapsed `relocate` with spec §5.8's full phase table for a drain, with 1b-next rev 16's guards on it: the release sequence and its deadline, the acknowledgement barrier on every phase change, the pin bound to the claim version it was selected against and to an evidenced empty listing, the prepared generation, the local install with its receipt, EnsureLocal before P's first admission and VerifyReceipt after it, `prepared_opened` journaled, three probe attempts counted before they are made, `released` coverage, the row cases, nested relocation after `probe-failed` and the replacement cap. Task 3 adds termination by the cloud with the regional worker's fence (lost, timers declared, regional chores passed to the region, local chores discharged only on qualifying volume evidence), automatic enrollment, failover from `serving`, source loss, the target replacement table, the phase-sensitive exhausted-target fence and the park-local exclusion from replacement. Task 4 adds the files publisher, P's prepared manifest at sequence 0, the files pin and the files live set. Task 5 writes the scenarios: a witness for every safety guard, every L18 case in a one-box and in a two-box region, claim §11's extras, direct evidence for every bound, and three findings. Task 5B (rev 4) answers Astra's round 1 on this plan: faithful guards with a discriminating test each, the exact phase matrix and claim §11's remaining cases. Task 5C (rev 5, regenerated in rev 6) answers rounds 2 and 3: PinFailover's barrier before an initial failover's pin, the boundary between the published marker and the open replication, and the adverse volume under a failover. Task 6 wires the shape and the region HA rule group into `mutate.sh` and `expected-outcomes.txt`. Task 7 writes the joint-round brief against 1b-next rev 16. Every rule is a named guard in `rules_test.go` whose comment names the 1b-next function it mirrors. |
| +**Architecture:** Ten tasks (rev 4 adds Task 5B, rev 5 Task 5C, rev 7 Task 5D) over one Go test package (every file is `_test.go`; nothing here is product code). Task 1 generalises the world's shape (`boxesPerRegion`, 1 or 2) so the one-box sweep stays byte-identical to the baseline and a two-box sweep runs beside it. Task 2 replaces the collapsed `relocate` with spec §5.8's full phase table for a drain, with 1b-next rev 16's guards on it: the release sequence and its deadline, the acknowledgement barrier on every phase change, the pin bound to the claim version it was selected against and to an evidenced empty listing, the prepared generation, the local install with its receipt, EnsureLocal before P's first admission and VerifyReceipt after it, `prepared_opened` journaled, three probe attempts counted before they are made, `released` coverage, the row cases, nested relocation after `probe-failed` and the replacement cap. Task 3 adds termination by the cloud with the regional worker's fence (lost, timers declared, regional chores passed to the region, local chores discharged only on qualifying volume evidence), automatic enrollment, failover from `serving`, source loss, the target replacement table, the phase-sensitive exhausted-target fence and the park-local exclusion from replacement. Task 4 adds the files publisher, P's prepared manifest at sequence 0, the files pin and the files live set. Task 5 writes the scenarios: a witness for every safety guard, every L18 case in a one-box and in a two-box region, claim §11's extras, direct evidence for every bound, and three findings. Task 5B (rev 4) answers Astra's round 1 on this plan: faithful guards with a discriminating test each, the exact phase matrix and claim §11's remaining cases. Task 5C (rev 5, regenerated in rev 6) answers rounds 2 and 3: PinFailover's barrier before an initial failover's pin, the boundary between the published marker and the open replication, and the adverse volume under a failover. Task 5D (rev 7) answers round 4: the target is named before any pin on every path, the phase predicates know `PinFailover`, and a failover passes Worker.Start's guards. Task 6 wires the shape and the region HA rule group into `mutate.sh` and `expected-outcomes.txt`. Task 7 writes the joint-round brief against 1b-next rev 16. Every rule is a named guard in `rules_test.go` whose comment names the 1b-next function it mirrors. |
| **Tech Stack:** Go 1.26 test files, standard library only (the model imports nothing else; `hash/fnv` for the tie-break stand-in over the box id in Tasks 1 to 5A; from Task 5B `crypto/sha256` over the host, as 1b-next hashes it). `go test ./internal/sim/hostlife/` is the gate; `mutate.sh` runs the prebuilt binary per rule. |
| **Spec:** region HA spec 1 `docs/superpowers/specs/2026-10-04-region-ha-box-placement-design.md` on `origin/main` (rev 5.4 with §24; rulings H1 to H19 in §0; §2 words; §3 invariants HA1 to HA7; §5.2 create; §5.3 rows; §5.4 edges; §5.6 files; §5.8 relocation; §5.9 the fence; §5.10 updates; §7 failure modes; §9 L1 to L20). Plan 1b-next **rev 19** (rev 2 of this plan synced to rev 16; rev 3 adds rulings 25 to 27, the "Rev 17" to "Rev 19" dispositions and request L21) `git show origin/plan-region-ha-1b-next:docs/superpowers/plans/2026-10-07-region-ha-1b-next-relocation.md` (Astra's round 18: "stage A ready to build"; its rulings 1 to 24, its dispositions tables for revs 2 to 16, Task 1's transitions, Task 5's worker and pinner, Task 6's participant, Task 11's merge gate) and the review findings beside it, `CODEX-PLAN-REGION-HA-1BN-R1.md` to `R18.md`. Claim rev 6.30 `git show origin/design-replica-ownership:docs/superpowers/specs/2026-10-02-host-lifecycle-claim-design.md` (§4 "Same-region relocation (L1)"; §6.2a "Files in the live set (L13)"; §6.4a item 2; §7.3 D2 to D6; §11 "Region HA's validation milestone" and the additional witnesses). Moves rev 7.22 on this branch, `docs/superpowers/specs/2026-10-02-move-any-app-design.md` (§7.6, §7.10 the conversion; §14.2 the model, its evidence policy and the harness). The model's own rules are in `internal/sim/hostlife/rules_test.go`; read `world_test.go`'s package comment and §14.2 before Task 1. |
| +## Rev 7: round 4 dispositions |
| + |
| +Astra's round 4 (`CODEX-PLAN-REGION-HA-TWO-BOX-R4.md`, against `cc69376d`) found both round 3 findings resolved and raised three new P2 fidelity findings. Its verdict was "not ready". All three are accepted, and each is fixed in a new **Task 5D**, a patch on Task 5C's tree. Task 6's patch is regenerated on top of it. Tasks 1 to 5C are unchanged. |
| + |
| +| # | Evidence checked | Disposition | What changed | Where | Guard removed: the test that fails | |
| +|---|---|---|---|---|---| |
| +| R4 #1 (P2) | Correct. 1b-next rev 19's `Worker.pinning` names a missing target with `NameTarget` before it selects any pin. The model named it before the pin only while `PinFailover` was set, so a converted move or a replay could pin while no box was eligible and miss a manifest that landed meanwhile. | accepted | A relocation at `pinning` with no target names one before anything else, on every path. With no eligible box it waits. New rule `reloc-name-before-pin`; its mutation pins first, as rev 6 did. It is an expected miss (a loss bound). The acknowledgement barrier stays the initial failover's alone. | Task 5D | `TestConvertedMoveWaitsForATargetBeforeItsPin`: the source's newer manifest is in flight and no box of the region is eligible. No target and no pin appear past the delay. The manifest lands, a box becomes eligible, and the pin must name the newer manifest. `TestConvertedMovePinsBeforeAcknowledgement` is rewritten: the target is named while there is no pin, and its controller then does not run while another worker pins. The pin is journaled without its acknowledgement, and `installing` waits for it. | |
| +| R4 #2 (P2) | Correct. `atPhase("pinning")` held while `PinFailover` was still set, which is production's `starting`, and the one-box matrix skipped `starting`. | accepted | `relocPhaseName` names the model's `pinning` with `PinFailover` set as `starting`. `atPhase` and the matrix's assertion use it, and `pinning` must also have the flag cleared and no executor. The one-box matrix now includes target@starting, so it has 25 subtests. | Task 5D | (coverage) `TestL18TerminationAtEveryExactPhase` one-box target@starting and target@pinning. Also `TestFailoverTargetLossAroundPinFailover`: in a two-box region with a spare, the failover's target is terminated with `PinFailover` set and, in a second run, after it cleared but before installation. In both runs it must be replaced in the same phase. | |
| +| R4 #3 (P2) | Correct. The fence of a serving executor called `startFailover` unconditionally. 1b-next's `Worker.Start` needs an eligible target and the app's admission registration and its recheck. `StartRelocation` then applies `RelocationStartGuard` with the source fenced. | accepted | `failoverStart` runs Worker.Start's checks in its order before the fence CAS: an eligible target, then admission open. `failoverStartAllowed` runs in the CAS: the admission recheck, the target not on lost, and `relocationStartGuard(..., sourceFenced=true)`. The fenced source's own `park-local` does not block, as before, and a same-region `park-replica` does. Without a start nothing is fenced, so the claim still names the dead box and a later pass retries. The failover starts with its target named and as the only participant, as `StartRelocation` does. New rule `reloc-failover-start-guard`; its mutation starts at once with no target, as rev 6 did. It is an expected miss (no invariant tells the earlier start apart). | Task 5D | `TestFailoverStartWaitsForAdmission` (admission closed, then reopened). `TestFailoverStartWaitsForParkReplica`: a park-replica in region 0 and the source's own park-local (`DeleteOnTermination=false`). The start waits for the park-replica only, and the park-local stays open. `TestL18UnenrolledReference` and `TestUnenrolledReferenceNeverChosen` now expect the claim to stay serving, unfenced, until a box is eligible. | |
| + |
| +**Every entry point into a relocation, compared with 1b-next rev 19 in order.** The comparison covers each guard's order as well as its presence. "Fixed" marks an ordering difference this revision corrects. |
| + |
| +| Entry | 1b-next rev 19, in order | Model before rev 7 | Rev 7 | |
| +|---|---|---|---| |
| +| Drain start (`userRelocate`) | `Worker.Start`: serves on the source; `Relocatable`; `Eligible(target)`; roster and region; the source not fenced; a writer session (ruling 11); `CheckBoxStart`; census; `Admission.Register`; `Recheck`. Then `StartRelocation`'s CAS: op.exec is the source, the target not lost, `RelocationStartGuard`. | admission checked first, before the writer check and the target; no recheck in the CAS; no target-not-lost check | **Fixed:** writer check, eligible target, admission; the CAS rechecks admission, refuses a lost target, then applies the guard. The roster, census and H14 reservation checks have no model state. | |
| +| Failover start (`fence` of the serving executor) | the same `Worker.Start`, with the source's fence; `StartRelocation` cites it, names the target, enters `starting`, participants are the target alone; then `starting`: `requireAcks`, `PinFailover` | no target, no admission check, no start guard; target named later at pinning | **Fixed** (R4 #3): eligible target, then admission, before the CAS; recheck, target not lost and the guard (source fenced) in it; target named at the start; `PinFailover` flag for `starting`. | |
| +| Source lost in a drain (`fenceSource`) | `FenceSource`: in `starting` it stays in `starting` (then `PinFailover`); in `releasing` before a release it goes to `pinning`; after a release only the liveness changes | the same (rev 6) | unchanged | |
| +| Converted move (`convertToRelocating`) | moves §7.10's conversion enters `pinning` with no target; `Worker.pinning`: `NameTarget`, the fence delay, the pin under the lease, `requireAcks`, `ToInstalling` | pin first, then name the target | **Fixed** (R4 #1): name, delay, pin, acknowledgements, install. | |
| +| Nested failover (`replaceTarget` after P opened; `relocProbeFailed`) | `Worker.replace`: exhausted first, then `next`, with no spare the deadline; `ReplaceTarget` fences, names the replacement and goes to `pinning` in one CAS. `probe-failed`: release or its deadline, exhausted, `next` (none: deadline), `PinAfterRelease` names the target | the same order | unchanged; the target is named in the same CAS, so `pinning` starts with it | |
| +| Operator's replay (plan ruling 13) | no 1b-next code (the resolve is the claim's); it enters `pinning` like a converted move | pin first, then name | **Fixed** (R4 #1): it enters `pinning` with no target, so it names one first; `PinFailover` cleared. | |
| +| Committed landing (finding F5, model only) | none | flag set, target named at pinning | unchanged. It has no 1b-next path; its target is named first under the flag. | |
| + |
| +**Dry run (2026-10-08).** The scratch module was rebuilt from the baseline, with the identity tests and Task 1 from prose. The patches for Tasks 2 to 5C were applied from this document, then Task 5D and the regenerated Task 6. After each: build, vet, gofmt, the gate, and the COUNTERS and both trace files compared byte for byte with the baseline's. |
| + |
| +| After | One-box COUNTERS and traces | Two-box | Gate | |
| +|---|---|---|---| |
| +| Tasks 1 to 5C | identical | as in rev 6 | ok | |
| +| Task 5D | identical | 300, 0 failed, 486 (the sweep met "no eligible target yet" 5 times) | ok. `TestConvertedMoveWaitsForATargetBeforeItsPin` fails under `reloc-name-before-pin`. `TestFailoverStartWaitsForAdmission` and `TestFailoverStartWaitsForParkReplica` fail under `reloc-failover-start-guard`. `TestFailoverPinWaitsForTheAcknowledgement` still fails under its mutation. | |
| +| Task 6 | the same | the same | ok. `@regionha` lists 50 rules, 158 in all. | |
| + |
| +No mutation sweep was run, and the scratch module was then removed. |
| + |
| ## Rev 6: round 3 dispositions |
| Astra's round 3 (`CODEX-PLAN-REGION-HA-TWO-BOX-R3.md`, against `ee6e35f3`) found all three of round 2's items resolved. It raised one new P2 and one P3, with the verdict "not ready". Both are accepted. Task 5C's patch is regenerated with the fixes (it is still a patch on Task 5B's tree), and Task 6's patch is regenerated on top of it. Tasks 1 to 5B are unchanged. |
| @@ -215,12 +247,12 @@ The two-box sweep at Task 6 starts 15 drains and 4 failovers and completes 17 re |
| ## Rulings made while planning |
| -Each was a gap or a conflict between the authorities. Each says what it costs if it is wrong. Rulings 1 to 11 are rev 1's; 12 is amended; 13 to 19 are rev 2's; 20 to 25 are rev 4's, and rev 4 amends 1 and 15; rev 5 and rev 6 amend 4. |
| +Each was a gap or a conflict between the authorities. Each says what it costs if it is wrong. Rulings 1 to 11 are rev 1's; 12 is amended; 13 to 19 are rev 2's; 20 to 25 are rev 4's, and rev 4 amends 1 and 15; revs 5, 6 and 7 amend 4. |
| 1. **The one-box shape is a different random stream only where the two-box shape draws more.** Every seed of the one-box sweep must stay byte-identical to the baseline (spec §4: "a region with one box behaves exactly as today"). So a two-box world draws its extra values only after the one-box draws of the same step (`newWorld` adds its second boxes last; `step` draws for termination, drains and the publisher only when `perRegion > 1`), and no one-box code path calls the random source where it did not before. The gate proves it: every task compares the one-box `COUNTERS` line to the baseline's and, from rev 4, the whole trace of a one-box create's interruption and a hash of every one-box seed's trace (Task 1 Step 1). Rev 3's Task 1 passed the COUNTERS check while it cancelled an interrupted one-box create; region HA's create behaviour (the recovered-create cancellation, the eligibility of a sole box) is the two-box shape's alone. *Cost if wrong:* a seed reshuffle, which the gate shows at once; the fix is to move the draw. |
| 2. **The two-box sweep is the revision's one 3,000-seed sweep.** The evidence policy (moves §14.2, Paul 2026-10-06) allows one mutation sweep per revision. The one-box path is byte-identical at the gate's 300 seeds, so the one-box verdicts of rev 7.22 stand for it; the new guards are reachable only with two boxes, so the sweep runs with `HOSTLIFE_BOXES=2`. One caveat the brief states: Task 2 replaces the body of `relocate`, which the one-box shape reaches only through a converted move (`fence-converts-moving`); the 300-seed one-box sweep never converts, so its `COUNTERS` line cannot show a change there, and the `fence-converts-moving` witness is the evidence that the converted path still completes. *Cost if wrong:* a one-box regression in a guard this plan touches would show first in the gate's 300-seed one-box run, which every task runs. |
| 3. **A regional worker is any live, enrolled, non-lost box of the region.** Claim P6-D5 and spec §2 say correctness never depends on which worker acts; two make the same CAS and one fails. The model lets every such box run the region's chores and the relocation's worker steps. The one-box path is unchanged, since the region's one box was the only candidate. *Cost if wrong:* a chore run by two boxes at once that the park's idempotent copies and single manifest did not make safe; the sweep would show it as INV-10 or non-convergence, which is a finding for the claim, not a model bug. |
| -4. **Failover starts at `pinning` with the target named there. For an initial failover the D6 barrier is checked before the pin is selected (rev 5, narrowed in rev 6); for every relocation it is checked again at the installing CAS.** Spec §5.8 and 1b-next's `StartRelocation` name the target in the failover's start CAS and pass through `starting` for its acknowledgement (`PinFailover`). The model's converted move already enters at `pinning` with no target (moves §7.10), so one entry point serves both, and `to`'s execution lease must be current before `installing` (`requireAcks` in `ToInstalling`). A drain whose source is lost in `starting` goes to `pinning` at once for the same reason (1b-next keeps it in `starting` until `PinFailover`). **(Rev 5, Astra round 2 finding 1.)** Rev 4's collapse did move a guard: the pin was selected before any acknowledgement, where `PinFailover` waits for them all. **(Rev 6, Astra round 3 finding 1.)** Only an initial failover waits. `opState.PinFailover` stands for 1b-next's `starting` after `StartRelocation` with a fence: `startFailover` sets it, and so does a drain whose source is lost in `starting`. While it is set, the operation in `pinning` names its target, waits for `requireAcks`, and clears it in the PinFailover CAS before any pin is selected (rule `reloc-failover-ack-before-pin`). A converted move, a nested failover and an operator's replay enter `pinning` directly, as in 1b-next. There `Worker.pinning` journals the pin first and checks the acknowledgements only for `ToInstalling`. That is the same barrier at the same point in the order of events; only the phase's name differs. *Cost if wrong:* a phase the brief says is collapsed. The guard is 1b-next's. |
| +4. **Failover starts at `pinning` with the target named there. For an initial failover the D6 barrier is checked before the pin is selected (rev 5, narrowed in rev 6); for every relocation it is checked again at the installing CAS.** Spec §5.8 and 1b-next's `StartRelocation` name the target in the failover's start CAS and pass through `starting` for its acknowledgement (`PinFailover`). The model's converted move already enters at `pinning` with no target (moves §7.10), so one entry point serves both, and `to`'s execution lease must be current before `installing` (`requireAcks` in `ToInstalling`). A drain whose source is lost in `starting` goes to `pinning` at once for the same reason (1b-next keeps it in `starting` until `PinFailover`). **(Rev 5, Astra round 2 finding 1.)** Rev 4's collapse did move a guard: the pin was selected before any acknowledgement, where `PinFailover` waits for them all. **(Rev 6, Astra round 3 finding 1.)** Only an initial failover waits. `opState.PinFailover` stands for 1b-next's `starting` after `StartRelocation` with a fence: `startFailover` sets it, and so does a drain whose source is lost in `starting`. While it is set, the operation in `pinning` names its target, waits for `requireAcks`, and clears it in the PinFailover CAS before any pin is selected (rule `reloc-failover-ack-before-pin`). A converted move, a nested failover and an operator's replay enter `pinning` directly, as in 1b-next. There `Worker.pinning` journals the pin first and checks the acknowledgements only for `ToInstalling`. That is the same barrier at the same point in the order of events; only the phase's name differs. **(Rev 7, Astra round 4.)** The serving executor's failover now starts the way `Worker.Start` and `StartRelocation` start it: with an eligible target named, the admission registered and rechecked, and `RelocationStartGuard` passed, the fenced source excepted. The flag is that failover's `starting`, and `relocPhaseName` names it so. On every path a relocation at `pinning` with no target names one before it selects a pin (rule `reloc-name-before-pin`), as `Worker.pinning` does. *Cost if wrong:* a phase the brief says is collapsed. The guards are 1b-next's, in its order. |
| 5. **`released` coverage is modelled as the claim defines it, and relocation by drain is enabled in the model.** Spec §5.8 says a drain is not enabled until L9 is accepted; claim rev 6.30 §6.4a carries L9. The model implements it so the review can judge it, and the brief says so. *Cost if wrong:* the drain scenarios are evidence for L9, not against anything. |
| 6. **`stuck` is a journal entry; the operator resolves it** (plan ruling 13 says how). 1b-next ruling 9: `stuck` is not a phase. *Cost if wrong:* the operator's act is one function. |
| 7. **Terminated is not stopped.** The model's `Destroyed` box may come back with its disk in the final heal (a stopped instance started again). Termination is new, permanent and observable: a `Terminated` box never returns, and only a terminated, enrolled box is fenced (H1, H10, H19). A stopped box stays the operator's declare-lost (claim D2), as today. *Cost if wrong:* none to the one-box path, which never terminates. |
| @@ -8274,9 +8306,599 @@ Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>" |
| --- |
| +### Task 5D: Astra's round 4: the target before the pin on every path, the phase predicates and PinFailover, and Worker.Start's guards on a failover (rev 7) |
| + |
| +This is described in "Rev 7: round 4 dispositions" above. It contains: |
| +- Rule `reloc-name-before-pin`, in `relocPinning`. |
| +- Rule `reloc-failover-start-guard`: `failoverStart` and `failoverStartAllowed` in `fence`. `startFailover` gains its target, and `relocationStartGuard` gains `sourceFenced`. |
| +- `userRelocate` in Worker.Start's order, with the admission recheck and the target-not-lost check in its CAS. |
| +- `relocPhaseName` and `atPhase`; the one-box matrix with `starting`. |
| +- New tests: `TestConvertedMoveWaitsForATargetBeforeItsPin`, `TestFailoverStartWaitsForAdmission`, `TestFailoverStartWaitsForParkReplica` and `TestFailoverTargetLossAroundPinFailover`. |
| +- Rewritten tests: `TestConvertedMovePinsBeforeAcknowledgement`, with the helper `convertedMove`. `TestL18UnenrolledReference` and `TestUnenrolledReferenceNeverChosen` are updated. |
| + |
| +**Files:** |
| +- Modify: `regionha_test.go`, `rules_test.go`, `regionha_round1_test.go`, `regionha_cases_test.go`, `regionha_witness_test.go` |
| + |
| +- [ ] **Step 1: Apply the patch** |
| + |
| +```diff |
| +diff --git a/internal/sim/hostlife/regionha_cases_test.go b/internal/sim/hostlife/regionha_cases_test.go |
| +index 39e9b52..fb50f3d 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 3f56952..6cc4581 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 28784de..cb1d257 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 5757177..a1a955d 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 034684e..06b9849 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) |
| + } |
| +``` |
| + |
| +- [ ] **Step 2: Run the gate, the identity traces, and the new tests under their mutations** |
| + |
| +```bash |
| +gofmt -l internal/sim/hostlife/; nice -n 19 go vet ./internal/sim/hostlife/ |
| +nice -n 19 go test ./internal/sim/hostlife/ -count=1 -v 2>&1 | tee $TMPDIR/twobox/task5d.log | grep -E "seeds, |^--- FAIL|^ --- FAIL|^ok|^FAIL" |
| +diff $TMPDIR/twobox/baseline-counters.json <(grep COUNTERS $TMPDIR/twobox/task5d.log | head -1 | sed 's/.*COUNTERS //') && echo ONE-BOX-COUNTERS-IDENTICAL |
| +HOSTLIFE_TRACE_OUT=$TMPDIR/twobox/trace.txt HOSTLIFE_TRACE_OUT_SEEDS=$TMPDIR/twobox/seeds.txt nice -n 19 go test ./internal/sim/hostlife/ -run '^TestOneBox' -count=1 >/dev/null |
| +cmp $TMPDIR/twobox/baseline-trace.txt $TMPDIR/twobox/trace.txt && cmp $TMPDIR/twobox/baseline-seeds.txt $TMPDIR/twobox/seeds.txt && echo ONE-BOX-TRACES-IDENTICAL |
| +grep -c '^ --- PASS: TestL18TerminationAtEveryExactPhase/' $TMPDIR/twobox/task5d.log |
| +for pair in reloc-name-before-pin:TestConvertedMoveWaitsForATargetBeforeItsPin reloc-failover-start-guard:TestFailoverStartWaitsForAdmission reloc-failover-start-guard:TestFailoverStartWaitsForParkReplica reloc-failover-ack-before-pin:TestFailoverPinWaitsForTheAcknowledgement; do |
| + HOSTLIFE_MUTATE=${pair%%:*} nice -n 19 go test ./internal/sim/hostlife/ -run "^${pair#*:}\$" -count=1 2>&1 | grep -E '^(ok|--- FAIL)' | head -1 | sed "s/^/${pair%%:*}: /" |
| +done |
| +``` |
| + |
| +Expected (the dry run's): `300 seeds, 0 failed, 483 completed operations; mutated="" boxes=1`, `300 seeds, 0 failed, 486 completed operations; mutated="" boxes=2`, `ok`, `ONE-BOX-COUNTERS-IDENTICAL`, `ONE-BOX-TRACES-IDENTICAL`, `25`, and four `--- FAIL` lines. |
| + |
| +- [ ] **Step 3: Commit** |
| + |
| +```bash |
| +git add internal/sim/hostlife/ |
| +git commit -m "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>" |
| +``` |
| + |
| +--- |
| + |
| ### Task 6: The harness: `mutate.sh`'s shape and the region HA group, `expected-outcomes.txt`, and the revision's one sweep (moves §14.2; the evidence policy) |
| -`mutate.sh` already runs one mutation check per rule in `allRules`, so each of the 48 region HA rules is checked by the sweep once it exists. This task makes the shape explicit in every verdict (`[boxes=N]`), adds `@regionha` (the rules of the region HA block, one mutation check per guard, for a rerun of the new guards alone), adds `HOSTLIFE_LIST=1` (print the rules a run would check and run nothing), and lists the 22 region HA rules that are not caught alone, each with its reason and the direct test that shows it. |
| +`mutate.sh` already runs one mutation check per rule in `allRules`, so each of the 50 region HA rules is checked by the sweep once it exists. This task makes the shape explicit in every verdict (`[boxes=N]`), adds `@regionha` (the rules of the region HA block, one mutation check per guard, for a rerun of the new guards alone), adds `HOSTLIFE_LIST=1` (print the rules a run would check and run nothing), and lists the 24 region HA rules that are not caught alone, each with its reason and the direct test that shows it. |
| **Files:** |
| - Modify: `internal/sim/hostlife/mutate.sh`, `internal/sim/hostlife/expected-outcomes.txt` |
| @@ -8285,10 +8907,10 @@ Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>" |
| ```diff |
| diff --git a/internal/sim/hostlife/expected-outcomes.txt b/internal/sim/hostlife/expected-outcomes.txt |
| -index 72504e3..b6fc701 100644 |
| +index 72504e3..71ab604 100644 |
| --- a/internal/sim/hostlife/expected-outcomes.txt |
| +++ b/internal/sim/hostlife/expected-outcomes.txt |
| -@@ -21,3 +21,25 @@ admit-bind-op missed caught with claim-cas-opid: the model's general CAS conditi |
| +@@ -21,3 +21,27 @@ admit-bind-op missed caught with claim-cas-opid: the model's general CAS conditi |
| hostguard rare 30000 the guard's race is reached by the sweep at 30,000 (2 / 30,000 on rev 7.11; 5 / 3,000 on rev 7.10, before the admitting CAS moved ahead of the start) |
| stale-hold-release rare 30000 reached at 30,000 (15 / 30,000 on rev 7.11; 2 / 3,000 on rev 7.10) |
| strict-spawn rare 30000 its witness holds alone (the combination with evidence-whole-tree is the witness's); the sweep reaches it at 30,000 (1 / 30,000 on rev 7.11; 3 / 3,000 on rev 7.10) |
| @@ -8314,6 +8936,8 @@ index 72504e3..b6fc701 100644 |
| +reloc-deadline-from-observed-at missed liveness: a deadline from the termination marks stuck earlier than 1b-next would, which the operator then resolves; TestDeadTargetDeadlineFromObservation delays the observation past the deadline and fails under the mutation |
| +tie-hash-host missed a preference: either winner is a correct choice; TestTieHashFollowsTheHost computes both hosts' winners independently and fails under the mutation |
| +reloc-failover-ack-before-pin missed a loss bound like reloc-failover-pin-delay: an initial failover's pin selected before its target acknowledged misses only files that land later, and the sweep's controllers acknowledge within a step of being named; TestFailoverPinWaitsForTheAcknowledgement holds the target's controller while the newer manifest lands and fails under the mutation |
| ++reloc-name-before-pin missed a loss bound like reloc-failover-pin-delay: a converted move's or a replay's pin selected before a target is named misses only files that land while no box is eligible; TestConvertedMoveWaitsForATargetBeforeItsPin holds every box ineligible while the newer manifest lands and fails under the mutation |
| ++reloc-failover-start-guard missed a fidelity guard: the mutation starts the failover earlier (no target yet, admission closed, a park-replica outstanding), and no model invariant distinguishes the earlier start, whose target is then named at pinning; TestFailoverStartWaitsForAdmission and TestFailoverStartWaitsForParkReplica fail under the mutation |
| diff --git a/internal/sim/hostlife/mutate.sh b/internal/sim/hostlife/mutate.sh |
| index c583d97..883996e 100755 |
| --- a/internal/sim/hostlife/mutate.sh |
| @@ -8428,11 +9052,11 @@ HOSTLIFE_LIST=1 internal/sim/hostlife/mutate.sh 0 | wc -l |
| nice -n 19 go test ./internal/sim/hostlife/ -count=1 2>&1 | tail -1 |
| ``` |
| -Expected (the dry run's): `SYNTAX-OK`, `48`, `156`, `ok`. |
| +Expected (the dry run's): `SYNTAX-OK`, `50`, `158`, `ok`. |
| - [ ] **Step 3: The revision's sweep (the one allowed; serial, niced)** |
| -Run only when Tasks 1 to 5C are committed, nothing else is sweeping on the machine (`pgrep -f hostlife.test` empty), and the gate passes: |
| +Run only when Tasks 1 to 5D are committed, nothing else is sweeping on the machine (`pgrep -f hostlife.test` empty), and the gate passes: |
| ```bash |
| export GOFLAGS=-buildvcs=false |
| @@ -8476,7 +9100,7 @@ prompt (branch `region-ha-hostlife-two-box`) against plan 1b-next rev |
| - region HA spec 1 `docs/superpowers/specs/2026-10-04-region-ha-box-placement-design.md` on `origin/main` (rev 5.4, §24; H1 to H19; §2, §3, §5.2, §5.3, §5.4, §5.6, §5.8, §5.9, §5.10, §7, §9 L1 to L20); |
| - claim rev 6.30 `git show origin/design-replica-ownership:docs/superpowers/specs/2026-10-02-host-lifecycle-claim-design.md` (§4 L1, §6.2a L13, §6.4a item 2, §7.3 D2 to D6, §11); |
| - moves rev 7.22 on this branch (§7.6, §7.10, §14.2); |
| -- the plan that built it, `docs/superpowers/plans/2026-10-07-region-ha-hostlife-two-box.md` rev 6 (its rulings 1 to 25, ruling 4 as revs 5 and 6 amended it; rulings 14, 16 and 17 mirror 1b-next's fixes for F1 to F3; "Rev 4: round 1 dispositions" answers Astra's round 1 on the plan, `CODEX-PLAN-REGION-HA-TWO-BOX-R1.md`, and maps each past finding to its proving artifact; "Rev 5: round 2 dispositions" answers round 2, `CODEX-PLAN-REGION-HA-TWO-BOX-R2.md`; "Rev 6: round 3 dispositions" answers round 3, `CODEX-PLAN-REGION-HA-TWO-BOX-R3.md`). |
| +- the plan that built it, `docs/superpowers/plans/2026-10-07-region-ha-hostlife-two-box.md` rev 7 (its rulings 1 to 25, ruling 4 as revs 5 to 7 amended it; rulings 14, 16 and 17 mirror 1b-next's fixes for F1 to F3; "Rev 4: round 1 dispositions" answers Astra's round 1 on the plan, `CODEX-PLAN-REGION-HA-TWO-BOX-R1.md`, and maps each past finding to its proving artifact; "Rev 5: round 2 dispositions" answers round 2, `CODEX-PLAN-REGION-HA-TWO-BOX-R2.md`; "Rev 6: round 3 dispositions" answers round 3, `CODEX-PLAN-REGION-HA-TWO-BOX-R3.md`; "Rev 7: round 4 dispositions" answers round 4, `CODEX-PLAN-REGION-HA-TWO-BOX-R4.md`, and compares every entry point with 1b-next). |
| ## Fixed: do not re-argue |
| @@ -8537,6 +9161,8 @@ prompt (branch `region-ha-hostlife-two-box`) against plan 1b-next rev |
| | reloc-clear-after-cleanup | `Finish` after a successful scoped cleanup (ruling 20) | R4-5, claim §11 | §5.10 | witness INV-29 | |
| | fence-converts-committed-landing | none: model F5 (rev 4) | claim §11 (the record-commit race) | §5.9, moves §7.10 | witness INV-3 | |
| | reloc-failover-ack-before-pin | `PinFailover`'s `requireAcks`, the initial failover only | two-box R2 #1, R3 #1 | D6, §5.8 | expected miss (loss bound); `TestFailoverPinWaitsForTheAcknowledgement` | |
| +| reloc-name-before-pin | `Worker.pinning`'s `NameTarget` before `pinUnderLease` | two-box R4 #1 | §5.8, moves §7.10 | expected miss (loss bound); `TestConvertedMoveWaitsForATargetBeforeItsPin` | |
| +| reloc-failover-start-guard | `Worker.Start` (`Eligible`, `Admission.Register`, `Recheck`), `StartRelocation`'s `RelocationStartGuard` with the source fenced | two-box R4 #3 | §5.8, L11 | expected miss; `TestFailoverStartWaitsForAdmission`, `TestFailoverStartWaitsForParkReplica` | |
| ## Findings F1 to F3, closed, and the open window L21 |
| @@ -8569,6 +9195,7 @@ The model's rev 4 found two gaps that neither 1b-next rev 19 nor moves rev 7.22 |
| 13. (Rev 4) Astra round 1's fixes: stuck refuses admission; region HA checks a sole box; durable acknowledgements, kept apart from controller readiness, gate every transition; every fence observation is retained and the deadline runs from `observed_at`; `TestL18TerminationAtEveryExactPhase` stops in exactly each phase, `probe-failed` included; each named guard's direct test fails without it. |
| 15. (Rev 5) Astra round 2's fixes: PinFailover's barrier before the failover's pin (ruling 4 as amended: is the barrier at `pinning` equivalent to 1b-next's at `starting`?), the published-marker boundary, the adverse volume under a failover of the current executor, and the pinned manifest's generation parked at completion, which is the model's abstraction of the at-rest sweep (claim §6.2a) and the storage follow-up (1b-next ruling 21), not a `CompleteRelocation` step. |
| 16. (Rev 6) Astra round 3's fix: only an initial failover (`opState.PinFailover`) waits for the acknowledgements before its pin; a converted move, a nested failover and a replay pin first (`TestConvertedMovePinsBeforeAcknowledgement`). Is the flag a faithful stand-in for 1b-next's `starting`? |
| +17. (Rev 7) Astra round 4's fixes and the entry-point table in "Rev 7: round 4 dispositions": the target named before any pin on every path, `relocPhaseName`, and the failover started through Worker.Start's guards in their order. Is any entry point still ordered differently from 1b-next? |
| 14. (Rev 4) Claim §11's cases: the move with an unchanged file, the automatic target loss racing the record commit, the failed cleanup that blocks executable updates (INV-29), the forced open boundaries (four, the published marker before replication opens included). Are the file-object model (plan ruling 25) and the controller record faithful enough to stand for them, and is the coverage table in the plan's rev 4 section right about which findings only 1b-next's own tests can prove? |
| ## Output |
| @@ -8608,7 +9235,7 @@ Then hand the brief to the Codex second reader as memory `codex-second-reader.md |
| ## Self-review |
| -- **1b-next rev 19 coverage.** Every guard its dispositions list for stage A that a model step can reach has a rule (the guards table above, 47 rules; rev 3 added four for rev 17 to 19, rev 4 ten for Astra's round 1, rev 5 one for round 2); the findings the model cannot reach are mapped to 1b-next's own tests in "Rev 4: round 1 dispositions"; the stage B contracts (R1 to R10, the lifecycle property of revs 14 to 16, hostexec's controller recovery) have no model step and are named as such. Each rule's comment names its 1b-next function. |
| +- **1b-next rev 19 coverage.** Every guard its dispositions list for stage A that a model step can reach has a rule (the guards table above, 50 rules; rev 3 added four for rev 17 to 19, rev 4 ten for Astra's round 1, rev 5 one for round 2, rev 7 two for round 4); the findings the model cannot reach are mapped to 1b-next's own tests in "Rev 4: round 1 dispositions"; the stage B contracts (R1 to R10, the lifecycle property of revs 14 to 16, hostexec's controller recovery) have no model step and are named as such. Each rule's comment names its 1b-next function. |
| - **L18 and claim §11.** Every L18 case is a `TestL18*` with one-box and two-box subtests; claim §11's extras are direct tests or witnesses, each listed in "Rev 4: round 1 dispositions". §5.8's table (Task 2), the release (Tasks 2, 4), the pin (Tasks 2, 4), P's build (Tasks 2, 4), the local install, EnsureLocal and VerifyReceipt (Task 2), the probe (Task 2), the replacement table, source loss and the exhausted fence (Task 3), the cap and stuck (Tasks 2, 3), what a relocation leaves behind (Tasks 2, 4). §5.9 (Task 3). §5.2 (Tasks 1, 5). §5.3 (Task 2). §5.6 (Task 4). §5.10 is root's and the participant's controller: not modelled. |
| - **Placeholders.** Every task carries its dry-run patch. The brief's `<...>` fields are filled from logs in Task 7 Step 1 and may not remain. |
| - **Type consistency.** The patches compiled and passed in order; `go vet` was clean after each. |