amadan
docs: region HA plan 1b-next rev 16 marks a lost receipt stuck after P opens, and crashes abruptly in the lifecycle property
Astra round 15, two P2s, both accepted. After P's first admission, a new VerifyReceipt step runs before every attempt. It checks only the box's durable install receipt against the journaled one. If the receipt is missing or different, the operation goes stuck, as spec 5.8 requires: no admission and no reinstall. Post-admission changes are never reverted. The property test's restart becomes an abrupt crash: no hooks run, faults persist, and recovery is a separate event. A new invariant (h) keeps records and update denial until a clear. Building it exposed an in-process artefact, a dead generation's held directory fd; the test now cuts each dead generation off. 200 seeds pass, niced; results of removing each guard are in the dispositions. Dry-run in task order on 3407d114.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
1 file changed,
+284
−24
docs/superpowers/plans/2026-10-07-region-ha-1b-next-relocation.md+284 −24
diff --git a/docs/superpowers/plans/2026-10-07-region-ha-1b-next-relocation.md b/docs/superpowers/plans/2026-10-07-region-ha-1b-next-relocation.md| index f7a526a9c..d1e392e37 100644 |
| --- a/docs/superpowers/plans/2026-10-07-region-ha-1b-next-relocation.md |
| +++ b/docs/superpowers/plans/2026-10-07-region-ha-1b-next-relocation.md |
| @@ -1,15 +1,41 @@ |
| -# Region HA 1b-next: Relocation, Row Cases, Create Choice and Fences Implementation Plan (rev 15) |
| +# Region HA 1b-next: Relocation, Row Cases, Create Choice and Fences Implementation Plan (rev 16) |
| > **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:** Build what region HA spec 1 had to leave until the host lifecycle claim was on main: the `relocating` operation within one region, released by the source's stop evidence (drain) or by its termination fence (failover); reconcile's row cases for it; create's once-only choice of executor box with `boxchoice.Choose`; and every claim CAS that consumes a termination fence. All of it dormant behind `CARLOS_REGION_HA`, and none of it mergeable until the joint two-box simulation round passes (L18). |
| -**Architecture:** Two stages (ruling 24). **Stage A, build now:** Tasks 1 to 7 and 9a, buildable on main today and dry-run on every revision: the claim library's relocation transitions and `released` coverage (`internal/hostclaim`), create's executor selection (`internal/hostclaim`, `internal/hostops`), the row and wake decisions (`internal/hostbox`), the writers-stopped observation (`internal/stopevidence`), the regional worker and the participant driver (new `internal/hostrelocate`), and the box-side release adapter with its receipt verifier (`internal/host`). **Stage B, gated:** Tasks 8a, 8b, 8c, 9 and 10 bind to claim Plan 6b and moves Plans 1 and 2, none merged. They keep their design and contracts here; their code is rewritten against the real 6b code after it merges and re-reviewed then (the "Stage B re-plan" step before Task 8a lists every obligation rounds 1 to 14 placed on them). What those need and no plan declares is a numbered request, never an assumption. The last task is the merge gate. The worker only reads termination fences: `hostfence.TerminationWorker` writes them, and `hostactors.Directory` is the only roster reader. |
| +**Architecture:** Two stages (ruling 24). **Stage A, build now:** Tasks 1 to 7 and 9a, buildable on main today and dry-run on every revision: the claim library's relocation transitions and `released` coverage (`internal/hostclaim`), create's executor selection (`internal/hostclaim`, `internal/hostops`), the row and wake decisions (`internal/hostbox`), the writers-stopped observation (`internal/stopevidence`), the regional worker and the participant driver (new `internal/hostrelocate`), and the box-side release adapter with its receipt verifier (`internal/host`). **Stage B, gated:** Tasks 8a, 8b, 8c, 9 and 10 bind to claim Plan 6b and moves Plans 1 and 2, none merged. They keep their design and contracts here; their code is rewritten against the real 6b code after it merges and re-reviewed then (the "Stage B re-plan" step before Task 8a lists every obligation rounds 1 to 15 placed on them). What those need and no plan declares is a numbered request, never an assumption. The last task is the merge gate. The worker only reads termination fences: `hostfence.TerminationWorker` writes them, and `hostactors.Directory` is the only roster reader. |
| **Tech Stack:** Go 1.26, module `github.com/carlosframework/platform`; `release.Store` (create-only and ETag compare-and-swap puts); the claim library (`hostclaim`), roster (`hostactors`), fences (`hostfence`, `termfence`), box choice (`boxchoice`), files (`hostfiles`), generation selection (`genselect`), stop evidence (`stopevidence`, `internal/host` stop receipts), execution controller (`hostexec`). |
| **Spec:** `docs/superpowers/specs/2026-10-04-region-ha-box-placement-design.md`, rev 5.4 with §24 (rulings H1 to H19 final). Read §0, §2, §5.2, §5.3, §5.8, §5.9, §5.10, §9 (L1 to L20, accepted) and §24 first. Then the claim spec rev 6.30 on `origin/design-replica-ownership` (`docs/superpowers/specs/2026-10-02-host-lifecycle-claim-design.md`): §1.1's activation gate, §4 ("Same-region relocation (L1)" and the relocation exception to CC11), §5.1 and P5-D2/P5-D6 (the create intent), §6.1 ("Release before full stop (L10)"), §6.4a item 2 (`released`), §7.3 D2 ("Automatic termination (L2, L4)", "The fence's journal reference") and D4 ("Automatic loss persistence"). Then moves rev 7.22 on `origin/design-moves-any-region` §7.6 ("One install routine, two sources", L16 and L17) and §7.10 (the pre-flip conversion). The contracts note `docs/superpowers/notes/2026-10-07-region-ha-contracts.md` gives `hostfiles` v2, `CopyManifest`, `Publish` and `boxchoice`. Plan 1b (`docs/superpowers/plans/2026-10-06-region-ha-1b-claim-readers.md`) lists in "Waits for the claim" what this plan now builds. |
| +## Rev 16: round 15 dispositions |
| + |
| +Astra's round 15 (`CODEX-PLAN-REGION-HA-1BN-R15.md`) resolved all four round 14 items and raised two P2s. I checked both against spec §5.8 (line 847, "a box that finds its receipt missing after that point … the op goes to `stuck`") and against the rev 15 property code. Both are accepted; none is declined. |
| + |
| +Stage A was dry-run on a clean 3407d114 in task order. The lifecycle property passed 200 seeds, niced, in about four and a half minutes. Each new guard was then removed in turn. |
| + |
| +| # | Stage | Evidence checked | Disposition | What changed | Where | |
| +|---|---|---|---|---|---| |
| +| 1 (P2) | A, B | Rev 15's `Step` called `EnsureLocal` only while P was unopened. After P opened it went straight to the next attempt, so a lost receipt never made the operation `stuck` as §5.8 requires. | accepted | Receipt verification is now separate from restoration. A new effect, `VerifyReceipt`, runs before every attempt once P is opened. It compares this box's durable receipt (the new `Receipt` provider: the install journal under its `install_stamp`) with the journaled `local_install`, and reads nothing else. If the receipt is missing or different, `Step` marks the operation `stuck` (`MarkStuck`, allowed in `probing` once P is opened) and makes no admission and no reinstall. Files, env and timers changed by the admitted writers are never compared or reverted. Stage B: the production `Receipt`, with named tests. | Task 6 (`TestAParticipantIsStuckWhenItsReceiptIsLostAfterPOpens`: P is opened and the agent restarts. With the receipt lost, the claim goes `stuck` and no admission follows. With it intact, the next attempt goes ahead and nothing is reinstalled or verified against content.) Task 7 (`TestVerifyReceiptChecksTheReceiptOnly`). Stage B re-plan | |
| +| 2 (P2) | A | Rev 15's `restart` repaired the faults it was meant to survive: it unblocked and un-failed the cleanup, and closed the old controllers in the background, so their hooks ran. | accepted | `restart` becomes `crash`, an abrupt death. No controller is closed and no hook runs or completes. A dead generation's cleanups, including ones waiting when it died, never return. Its clock never fires again, and the next generation uses fresh lock files: the kernel releases a dead process's locks. Durable records and every external fault persist; recovery stays its own later event. New invariant (h): a record goes only through a successful clear or a successor's open over it, never through a crash or any other step, and while a record exists root's §5.10 check refuses an executable update. | Task 7 (the property, 200 seeds) | |
| +| C1 | A | Found by the new crash event. In-process, a dead generation's hostexec goroutines still run: `publish` retries its "lost" write through a directory fd it already holds open. After a repair it recreated a record a live generation had just cleared (seed 75). | fixed in the test | Each generation reaches the data directory through its own symlink, and a crash removes the dead one, so newly opened paths fail. The repair waits 300 ms so a write already in flight through an open fd lands as part of the repair. A real dead process writes nothing, so production code is unchanged. | Task 7 (the property's `dataLink`, `recoverAll`) | |
| + |
| +Mutation check, with the property at 200 seeds and `-failfast`, plus targeted tests: |
| + |
| +| Guard removed | Result | |
| +|---|---| |
| +| `Step` marking `stuck` on a lost receipt after P opens | killed: `TestAParticipantIsStuck…` | |
| +| `VerifyReceipt` comparing the receipt exactly | killed: `TestVerifyReceiptChecksTheReceiptOnly` | |
| +| both `EnsureLocal` calls | killed, seed 182: (e) | |
| +| `EnsureLocal` before an attempt alone / before entering probing alone | each survived: the other covers it | |
| +| rev 14's ten lifecycle guards | all killed again; the crash event now kills "journal before the open" at (b) and the handover at (h) | |
| + |
| +While building C1 I also tried an in-flight-open guard: no forgetting while an abandoned open might still write. It survived 200 seeds, so I removed it. `ClearStale` already refuses while such an open holds the host's lock, and `recordIsMine` refuses on anything unclear. |
| + |
| +Astra's readings of rulings 1 to 24 stand. |
| + |
| ## Rev 15: round 14 dispositions |
| Astra's round 14 (`CODEX-PLAN-REGION-HA-1BN-R14.md`) resolved the lease-recovery finding. It left round 13's finding 2 partly resolved and raised three new P2s. All four are accepted; none is declined. |
| @@ -344,7 +370,7 @@ Left out, with where it goes: |
| - **Go environment.** `GOFLAGS=-buildvcs=false`. Leave `GOCACHE` at its default; if the sandbox refuses it, `GOCACHE=$TMPDIR/gocache` for that command. Socket tests need `TMPDIR=/tmp/k` (`mkdir -p /tmp/k`). Run tests niced (`nice -n 19`), targeted with `-run`; never the full `-race` suite, and no simulation sweeps. Scratch goes under `$TMPDIR`. |
| - **Gate before each commit:** `go build ./... && go vet ./<pkgs>/ && gofmt -l <dirs>` (empty), the task's targeted tests, then `GOOS=darwin go build ./... && GOOS=windows go build ./...`. (`GOOS=windows go vet ./internal/...` fails on main's own test files, `release/versions_test.go`, `appconfig/syncexec_test.go` and `activator/activator_test.go`; vet the task's packages instead.) |
| - Commit messages: lowercase `area:` prefix and a sentence stating the behaviour, then a blank line and `Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>`. Work on a branch cut from `origin/main` (suggested `region-ha-1b-next`). Merging is Paul's call, through `amadan branch merge`, and only after Task 11. |
| -- **Dry run.** Tasks 1 to 7 were applied in order to `origin/main` at 3407d114, built, vetted, cross-built for darwin, windows and linux/arm64, and their tests run; nineteen guards were each removed in turn and their test watched to fail (rev 1), then rev 2's twenty-five, rev 3's eleven, rev 4's eight, rev 5's seven, rev 6's eleven, rev 7's three, rev 8's two, rev 9's two, rev 10's one, rev 11's four, rev 12's four, rev 13's four, rev 14's ten killed mutations of the lifecycle property and rev 15's twelve (listed in the Self-review); from rev 10 on, stage A is also applied one task at a time in plan order, building and testing after each. Then the code was removed; only this document is committed. |
| +- **Dry run.** Tasks 1 to 7 were applied in order to `origin/main` at 3407d114, built, vetted, cross-built for darwin, windows and linux/arm64, and their tests run; nineteen guards were each removed in turn and their test watched to fail (rev 1), then rev 2's twenty-five, rev 3's eleven, rev 4's eight, rev 5's seven, rev 6's eleven, rev 7's three, rev 8's two, rev 9's two, rev 10's one, rev 11's four, rev 12's four, rev 13's four, rev 14's ten killed mutations of the lifecycle property, rev 15's twelve and rev 16's (listed in the Self-review); from rev 10 on, stage A is also applied one task at a time in plan order, building and testing after each. Then the code was removed; only this document is committed. |
| ## Review Focus |
| @@ -7135,7 +7161,7 @@ A participant box acknowledges first (D6, after §5.10's pending-state and updat |
| **Interfaces:** |
| - Consumes: Tasks 1 and 5 (the worker fixture in `worker_test.go`). |
| -- Produces: `hostrelocate.Effects` (`Acknowledge`, `Ready`, `Release`, `Build`, `InstallLocal`, `EnsureLocal` (rev 15), `Probe`, `Retained() ([]Participation, error)`, `Finish`), `hostrelocate.Participation{Host, Op}`, `hostrelocate.Participant{Claims, Box, Enrollment, Effects, Now}` with `Step(ctx, host) (hostclaim.Observed, error)` and `Sweep(ctx) error`. |
| +- Produces: `hostrelocate.Effects` (`Acknowledge`, `Ready`, `Release`, `Build`, `InstallLocal`, `EnsureLocal` (rev 15), `VerifyReceipt` (rev 16), `Probe`, `Retained() ([]Participation, error)`, `Finish`), `hostrelocate.Participation{Host, Op}`, `hostrelocate.Participant{Claims, Box, Enrollment, Effects, Now}` with `Step(ctx, host) (hostclaim.Observed, error)` and `Sweep(ctx) error`. |
| - [ ] **Step 1: Write the failing tests** |
| @@ -7147,6 +7173,7 @@ package hostrelocate |
| import ( |
| "context" |
| "errors" |
| + "fmt" |
| "strconv" |
| "strings" |
| "testing" |
| @@ -7176,6 +7203,8 @@ type fakeBox struct { |
| // reinstalls and probedMissing count what EnsureLocal and Probe saw. |
| retired bool |
| restores, reinstalls, probedMissing int |
| + // receiptLost: the box's durable local install receipt is gone. |
| + receiptLost bool |
| } |
| func (b *fakeBox) Acknowledge(_ context.Context, o hostclaim.Observed) (hostclaim.ExecutionAcknowledgement, error) { |
| @@ -7211,6 +7240,7 @@ func (b *fakeBox) Build(context.Context, hostclaim.Observed) error { |
| return nil |
| } |
| func (b *fakeBox) InstallLocal(_ context.Context, o hostclaim.Observed) (hostclaim.LocalInstall, error) { |
| + b.effects = append(b.effects, "install") |
| n, _ := strconv.ParseUint(o.Claim.Op.Journal["install_stamp"], 10, 64) |
| return hostclaim.LocalInstall{Box: b.box, Enrollment: enrollment(b.box), InstallStamp: n, FilesManifestVersion: 1, JournalSHA256: strings.Repeat("e", 64)}, nil |
| } |
| @@ -7224,6 +7254,10 @@ func (b *fakeBox) EnsureLocal(_ context.Context, o hostclaim.Observed) error { |
| } |
| return nil |
| } |
| +func (b *fakeBox) VerifyReceipt(context.Context, hostclaim.Observed) (bool, error) { |
| + b.effects = append(b.effects, "verify-receipt") |
| + return !b.receiptLost, nil |
| +} |
| func (b *fakeBox) Probe(ctx context.Context, o hostclaim.Observed, coverage string) (uint64, bool, error) { |
| if b.retired { |
| b.probedMissing++ // a probe admission over a missing local install |
| @@ -7450,6 +7484,55 @@ func TestAParticipantRestoresARetiredLocalInstallBeforeTheFirstAdmission(t *test |
| t.Fatalf("restores %d, probes over a missing install %d, reinstalls after P %d", dst.restores, dst.probedMissing, dst.reinstalls) |
| } |
| } |
| + |
| +// Round 15 finding 1: after P's first admission the local install is |
| +// never remade, and a box that has lost its receipt cannot rebuild it from |
| +// P: the next admission is refused and the operation is stuck (§5.8, |
| +// B2-5), across a restart. With the receipt intact, the later attempt goes |
| +// ahead and nothing is reinstalled or reverted: the files, env and timers |
| +// the admitted writers changed are theirs. |
| +func TestAParticipantIsStuckWhenItsReceiptIsLostAfterPOpens(t *testing.T) { |
| + for _, lost := range []bool{true, false} { |
| + t.Run(fmt.Sprintf("receipt lost %v", lost), func(t *testing.T) { |
| + f := newFixture(t) |
| + ctx := context.Background() |
| + src, dst := &fakeBox{f: f, box: "src"}, &fakeBox{f: f, box: "dst", failProbes: true} |
| + if _, err := f.w.Start(ctx, host, Request{Reason: hostclaim.ReasonDrain, Source: "src", Target: "dst"}); err != nil { |
| + t.Fatal(err) |
| + } |
| + ps := Participant{Claims: f.s, Box: "src", Enrollment: enrollment("src"), Effects: src, Now: f.clock} |
| + pd := Participant{Claims: f.s, Box: "dst", Enrollment: enrollment("dst"), Effects: dst, Now: f.clock} |
| + for i := 0; i < 60 && len(dst.coverages) == 0; i++ { |
| + _, _ = f.w.Step(ctx, host) |
| + ps.Step(ctx, host) |
| + pd.Step(ctx, host) |
| + } |
| + if len(dst.coverages) != 1 || !hostclaim.PreparedOpened(f.claim().Claim) { |
| + t.Fatalf("P was not opened: %d admissions", len(dst.coverages)) |
| + } |
| + dst.receiptLost, dst.restarted = lost, true // and the agent restarts |
| + dst.effects = nil |
| + for i := 0; i < 6; i++ { |
| + pd.Step(ctx, host) |
| + } |
| + c := f.claim().Claim |
| + for _, e := range dst.effects { |
| + if e == "ensure-local" || e == "install" { |
| + t.Fatalf("the local install was touched after P opened: %v", dst.effects) |
| + } |
| + } |
| + if lost { |
| + if c.Op.Journal["stuck"] == "" || len(dst.coverages) != 1 { |
| + t.Fatalf("a lost receipt after P opened: stuck %q, admissions %d", c.Op.Journal["stuck"], len(dst.coverages)) |
| + } |
| + return |
| + } |
| + if c.Op.Journal["stuck"] != "" || len(dst.coverages) < 2 { |
| + t.Fatalf("an intact receipt: stuck %q, admissions %d", c.Op.Journal["stuck"], len(dst.coverages)) |
| + } |
| + }) |
| + } |
| +} |
| ``` |
| - [ ] **Step 2: Run them to see them fail** |
| @@ -7512,6 +7595,15 @@ type Effects interface { |
| // install_stamp from P's files manifest. It is never called once P is |
| // opened: an opened P is never reinstalled (rev 15, round 14). |
| EnsureLocal(context.Context, hostclaim.Observed) error |
| + // VerifyReceipt is called before every admission after P is opened: |
| + // it reports whether this box's durable local install receipt is |
| + // still the one the claim journaled (box, enrollment, install_stamp, |
| + // journal digest). It checks the receipt and its binding only, never |
| + // the files, env or timers, which the admitted writers have changed |
| + // legitimately since. A missing or different receipt is false: the |
| + // local state cannot be rebuilt from P, so the operation is stuck |
| + // (§5.8, B2-5; rev 16, round 15). |
| + VerifyReceipt(context.Context, hostclaim.Observed) (bool, error) |
| // Probe makes one cold probe admission (AdmitWriter, with coverage the |
| // caller names) and runs the probe. passed is false while it runs. |
| Probe(ctx context.Context, obs hostclaim.Observed, coverage string) (session uint64, passed bool, err error) |
| @@ -7607,6 +7699,16 @@ func (p Participant) Step(ctx context.Context, host string) (hostclaim.Observed, |
| if err := p.Effects.EnsureLocal(ctx, obs); err != nil { |
| return obs, err |
| } |
| + } else { |
| + // After it, the install is never remade; its receipt must |
| + // still be this box's, or the operation is stuck. |
| + ok, err := p.Effects.VerifyReceipt(ctx, obs) |
| + if err != nil { |
| + return obs, err |
| + } |
| + if !ok { |
| + return p.update(ctx, obs, hostclaim.MarkStuck(id, "the local install receipt is missing after P was admitted (§5.8, B2-5)")) |
| + } |
| } |
| // The attempt is counted in the claim before it is made (§5.8: |
| // at most three); the fourth is probe-failed, by this CAS. |
| @@ -8484,6 +8586,42 @@ func TestEnsureLocalRestoresARetiredInstallOnlyBeforePOpens(t *testing.T) { |
| t.Fatalf("an opened P was reinstalled: %v installs=%d", err, installs) |
| } |
| } |
| + |
| +// Round 15 finding 1: after P opens, VerifyReceipt compares the box's |
| +// durable receipt with the journaled one and nothing else: a missing or |
| +// different receipt is false (the participant marks the operation stuck); |
| +// changed files never trigger a restore. |
| +func TestVerifyReceiptChecksTheReceiptOnly(t *testing.T) { |
| + ctx := context.Background() |
| + e, obs, _, _ := effectsFixture(t) |
| + receipt := hostclaim.LocalInstall{Box: "dst", Enrollment: "enr-d", InstallStamp: 9, FilesManifestVersion: 1, JournalSHA256: strings.Repeat("e", 64)} |
| + raw, _ := json.Marshal(receipt) |
| + obs.Claim.Op.Journal = map[string]string{"local_install": string(raw), "prepared": "P1", "prepared_opened": "P1", "install_stamp": "9"} |
| + stored, present := receipt, true |
| + e.Receipt = func(context.Context, hostclaim.Observed) (hostclaim.LocalInstall, bool, error) { |
| + return stored, present, nil |
| + } |
| + touched := 0 |
| + e.VerifyLocal = func(context.Context, hostclaim.Observed, hostclaim.LocalInstall) (bool, error) { |
| + touched++ |
| + return false, nil |
| + } |
| + e.Install = func(context.Context, hostclaim.Observed) (hostclaim.LocalInstall, error) { |
| + touched++ |
| + return receipt, nil |
| + } |
| + if ok, err := e.VerifyReceipt(ctx, obs); !ok || err != nil || touched != 0 { |
| + t.Fatalf("an intact receipt over changed files: %v %v touched=%d", ok, err, touched) |
| + } |
| + present = false |
| + if ok, err := e.VerifyReceipt(ctx, obs); ok || err != nil { |
| + t.Fatalf("a missing receipt: %v %v", ok, err) |
| + } |
| + present, stored.InstallStamp = true, 8 |
| + if ok, err := e.VerifyReceipt(ctx, obs); ok || err != nil { |
| + t.Fatalf("another installation's receipt: %v %v", ok, err) |
| + } |
| +} |
| ``` |
| - [ ] **Step 2: Run them to see them fail** |
| @@ -9263,8 +9401,17 @@ type lifeWorld struct { |
| // Install provider makes it, a scoped cleanup of an operation whose P |
| // is unopened retires it, VerifyLocal reads it. |
| installed map[string]bool |
| - saved []byte // a record the seed corrupted, to restore on recovery |
| - violated []string |
| + // gen is the agent process's generation: a crash starts the next one. |
| + // A dead generation's hooks never complete (rev 16). |
| + gen int |
| + // clears and opens count durable records cleared and controllers |
| + // opened in the current step, for invariant (h). |
| + clears, opens int |
| + // the record as the previous step left it. |
| + prevExists, prevReadable bool |
| + prevOp string |
| + saved []byte // a record the seed corrupted, to restore on recovery |
| + violated []string |
| } |
| const lifeDeadline = 400 * time.Millisecond |
| @@ -9288,7 +9435,7 @@ func newLifeWorld(t *testing.T) *lifeWorld { |
| w.claim(hostclaim.BeginCreateOn(nh, body, "c1", "console", created, hostclaim.ExecutorSelection{Box: "src", Enrollment: strings.Repeat("a", 32)})) |
| w.claim(hostclaim.CompleteCreate("c1", "src")) |
| w.claim(hostclaim.AdmitWriter(hostclaim.Admission{Box: "src", Mode: "cold", NewGeneration: "g1", Region: "ie", KeepStamp: true})) |
| - w.cfg = execctl.Config{Store: w.store, Guard: hostguard.Guard{DataDir: w.dataDir, LockDir: filepath.Join(w.dataDir, "locks"), Claims: hostguard.StoreReader{Store: w.store}}, |
| + w.cfg = execctl.Config{Store: w.store, Guard: hostguard.Guard{DataDir: w.dataLink(0), LockDir: filepath.Join(w.dataDir, "locks"), Claims: hostguard.StoreReader{Store: w.store}}, |
| Directory: activeDirectory{}, Clock: w.clock, LockDir: filepath.Join(w.dataDir, "exec-locks"), |
| CloseAdmission: func() {}, CancelWork: func() {}} |
| lifetime, stop := context.WithCancel(ctx) |
| @@ -9302,11 +9449,15 @@ func newLifeWorld(t *testing.T) *lifeWorld { |
| c.Binding = b |
| // hostexec's own Cleanup hook is the same scoped cleanup, |
| // bound to the binding (Task 8a); it does not count for (a). |
| - c.Cleanup = func(context.Context) error { return w.cleanupScoped(context.Background(), b.Op, false) } |
| + gen := w.generation() |
| + c.Cleanup = func(context.Context) error { return w.cleanupScoped(context.Background(), b.Op, false, gen) } |
| opened, err := OpenRelocationController(ctx, c) |
| if err != nil { |
| return nil, err |
| } |
| + w.mu.Lock() |
| + w.opens++ |
| + w.mu.Unlock() |
| return &lifeController{RelocationController: opened, w: w, op: b.Op}, nil |
| }, |
| Install: func(_ context.Context, o hostclaim.Observed) (hostclaim.LocalInstall, error) { |
| @@ -9320,6 +9471,13 @@ func newLifeWorld(t *testing.T) *lifeWorld { |
| n, _ := strconv.ParseUint(c.Op.Journal["install_stamp"], 10, 64) |
| return hostclaim.LocalInstall{Box: "src", Enrollment: strings.Repeat("a", 32), InstallStamp: n, FilesManifestVersion: 1, JournalSHA256: strings.Repeat("e", 64)}, nil |
| }, |
| + Receipt: func(_ context.Context, o hostclaim.Observed) (hostclaim.LocalInstall, bool, error) { |
| + var l hostclaim.LocalInstall |
| + _ = json.Unmarshal([]byte(o.Claim.Op.Journal["local_install"]), &l) |
| + w.mu.Lock() |
| + defer w.mu.Unlock() |
| + return l, w.installed[o.Claim.Op.ID], nil |
| + }, |
| VerifyLocal: func(_ context.Context, o hostclaim.Observed, _ hostclaim.LocalInstall) (bool, error) { |
| w.mu.Lock() |
| defer w.mu.Unlock() |
| @@ -9357,17 +9515,36 @@ type lifeController struct { |
| func (c *lifeController) Clear(ctx context.Context) error { |
| c.w.clearing(c.op) |
| - return c.RelocationController.Clear(ctx) |
| + err := c.RelocationController.Clear(ctx) |
| + c.w.cleared(err) |
| + return err |
| +} |
| + |
| +func (w *lifeWorld) cleared(err error) { |
| + if err == nil { |
| + w.mu.Lock() |
| + w.clears++ |
| + w.mu.Unlock() |
| + } |
| +} |
| + |
| +func (w *lifeWorld) generation() int { |
| + w.mu.Lock() |
| + defer w.mu.Unlock() |
| + return w.gen |
| } |
| func (w *lifeWorld) controllers() *RelocationControllers { |
| + gen := w.generation() |
| return &RelocationControllers{Journal: filepath.Join(w.dataDir, "relocate", "participations"), DataDir: w.dataDir, |
| - Cleanup: func(ctx context.Context, b execctl.Binding) error { return w.cleanupScoped(ctx, b.Op, true) }, |
| + Cleanup: func(ctx context.Context, b execctl.Binding) error { return w.cleanupScoped(ctx, b.Op, true, gen) }, |
| Clear: func(ctx context.Context, b execctl.Binding) error { |
| w.clearing(b.Op) |
| c := w.cfg |
| c.Binding = b |
| - return execctl.ClearStale(ctx, c) |
| + err := execctl.ClearStale(ctx, c) |
| + w.cleared(err) |
| + return err |
| }} |
| } |
| @@ -9375,9 +9552,14 @@ func (w *lifeWorld) controllers() *RelocationControllers { |
| // it retires the operation's local install unless the claim has opened |
| // that operation's P (it never stops what serves). counts says whether it |
| // is RelocationControllers' own call, the one invariant (a) asks for. |
| -func (w *lifeWorld) cleanupScoped(ctx context.Context, op string, counts bool) error { |
| +func (w *lifeWorld) cleanupScoped(ctx context.Context, op string, counts bool, gen int) error { |
| + w.mu.Lock() |
| + block, fail, dead := w.block, w.cleanErr, gen != w.gen |
| + w.mu.Unlock() |
| + if dead { |
| + select {} // a crashed process's hooks never complete |
| + } |
| w.mu.Lock() |
| - block, fail := w.block, w.cleanErr |
| if counts { |
| w.cleanOK[op] = false |
| } |
| @@ -9389,6 +9571,9 @@ func (w *lifeWorld) cleanupScoped(ctx context.Context, op string, counts bool) e |
| return ctx.Err() |
| } |
| } |
| + if gen != w.generation() { |
| + select {} // the process died while its cleanup waited |
| + } |
| if fail { |
| return errors.New("cleanup: a partial install would not go") |
| } |
| @@ -9555,17 +9740,61 @@ func (w *lifeWorld) check(step string) { |
| if n := len(w.open()); n > 1 { |
| w.violate(fmt.Sprintf("(c) after %s: %d controllers for one host", step, n)) |
| } |
| + // (h): a record goes only by a clear or by a successor's open over it, |
| + // never by a crash or any other step; while one exists, an executable |
| + // update is refused (root's §5.10 check). |
| + w.mu.Lock() |
| + clears, opens := w.clears, w.opens |
| + w.clears, w.opens = 0, 0 |
| + w.mu.Unlock() |
| + if w.prevExists && w.prevReadable && (!exists || (readable && st.Op != w.prevOp)) && clears == 0 && opens == 0 { |
| + w.violate(fmt.Sprintf("(h) after %s: %s's record went with no clear and no successor's open", step, w.prevOp)) |
| + } |
| + if exists && hostexecParticipation(w.dataDir) == nil { |
| + w.violate(fmt.Sprintf("(h) after %s: a record exists but an executable update is not refused", step)) |
| + } |
| + w.prevExists, w.prevReadable, w.prevOp = exists, readable, st.Op |
| } |
| -func (w *lifeWorld) restart() { |
| - w.recoverCleanup() |
| - // The kernel releases a dead process's locks. In-process the old |
| - // controllers are joined in the background: hostexec keeps retrying a |
| - // "lost" write until it is durable, so with an invalid local record a |
| - // join waits for the storage to recover. |
| - for _, c := range w.open() { |
| - go func() { _ = c.Close(context.Background()) }() |
| +// dataLink is generation gen's path to the data directory: a symlink, so |
| +// a crash can cut a dead generation off from it. A dead process writes |
| +// nothing; in-process, a dead controller's goroutines are still running |
| +// (hostexec's save loop retries a "lost" write until it lands), so the |
| +// link it opens through is removed. |
| +func (w *lifeWorld) dataLink(gen int) string { |
| + link := filepath.Join(filepath.Dir(w.dataDir), fmt.Sprintf("data-%d", gen)) |
| + if err := os.Symlink(w.dataDir, link); err != nil && !os.IsExist(err) { |
| + w.t.Fatal(err) |
| + } |
| + return link |
| +} |
| + |
| +// crash is the agent process dying abruptly (rev 16, round 15): no |
| +// controller is closed and none of its hooks run or complete; its durable |
| +// records stay, and every external fault (a blocked or failing cleanup, a |
| +// store that refuses) stays as it was. The kernel releases a dead |
| +// process's locks: the next generation uses fresh lock files, and the dead |
| +// generation's clock never fires again, so its controllers never renew, |
| +// lose or clean up. Recovery is a separate, later event. |
| +func (w *lifeWorld) crash() { |
| + w.mu.Lock() |
| + w.gen++ |
| + gen := w.gen |
| + w.mu.Unlock() |
| + now, boot, _ := w.clock.Now() |
| + w.clock = &lifeClock{wall: now, boot: boot} |
| + for _, d := range []string{fmt.Sprintf("exec-locks-%d", gen), fmt.Sprintf("locks-%d", gen)} { |
| + if err := os.MkdirAll(filepath.Join(w.dataDir, d), 0o770); err != nil { |
| + w.t.Fatal(err) |
| + } |
| + } |
| + w.cfg.Clock = w.clock |
| + w.cfg.LockDir = filepath.Join(w.dataDir, fmt.Sprintf("exec-locks-%d", gen)) |
| + w.cfg.Guard.LockDir = filepath.Join(w.dataDir, fmt.Sprintf("locks-%d", gen)) |
| + if err := os.Remove(w.cfg.Guard.DataDir); err != nil { |
| + w.t.Fatal(err) |
| } |
| + w.cfg.Guard.DataDir = w.dataLink(gen) |
| w.e.Controllers = w.controllers() |
| } |
| @@ -9588,6 +9817,12 @@ func (w *lifeWorld) recoverAll() { |
| path := filepath.Join(w.dataDir, ".hostexec", w.host+".json") |
| if raw, err := os.ReadFile(path); err == nil && string(raw) == "{" { |
| _ = os.WriteFile(path, w.saved, 0o660) |
| + // hostexec retries a "lost" write every 100ms through a |
| + // directory it already holds open, so a controller that met |
| + // the invalid record (a dead generation's included: in-process |
| + // its goroutine outlives the crash) lands its write now, as |
| + // part of the repair, never after a later clear. |
| + time.Sleep(300 * time.Millisecond) |
| } |
| w.saved = nil |
| } |
| @@ -9639,8 +9874,8 @@ func (w *lifeWorld) event(r *rand.Rand) string { |
| } |
| return "local record invalid" |
| case 10: |
| - w.restart() |
| - return "agent restart" |
| + w.crash() |
| + return "agent crash (no hooks run, faults persist)" |
| case 11: |
| w.complete() |
| w.startRelocation() // the successor starts before this box's sweep |
| @@ -10287,7 +10522,11 @@ type RelocationEffects struct { |
| // manifest lists it, the env file and the wake state, under the |
| // receipt's install_stamp (Task 8c's production body). |
| VerifyLocal func(context.Context, hostclaim.Observed, hostclaim.LocalInstall) (bool, error) |
| - Admit func(context.Context, hostclaim.Observed, string) (uint64, bool, error) |
| + // Receipt reads this box's durable local install receipt for the |
| + // claim's host (Task 8c: the install journal written under its |
| + // install_stamp); false when there is none. |
| + Receipt func(context.Context, hostclaim.Observed) (hostclaim.LocalInstall, bool, error) |
| + Admit func(context.Context, hostclaim.Observed, string) (uint64, bool, error) |
| } |
| var _ hostrelocate.Effects = (*RelocationEffects)(nil) |
| @@ -10584,6 +10823,25 @@ func (e *RelocationEffects) EnsureLocal(ctx context.Context, obs hostclaim.Obser |
| return err |
| } |
| +// VerifyReceipt is hostrelocate.Effects' check before every admission |
| +// after P is opened: the box's durable receipt must be the one the claim |
| +// journaled, exactly. It reads the receipt alone: the files, env and |
| +// timers are the admitted writers' now, and nothing is restored. |
| +func (e *RelocationEffects) VerifyReceipt(ctx context.Context, obs hostclaim.Observed) (bool, error) { |
| + if e.Receipt == nil || obs.Claim == nil { |
| + return false, ErrClaimStopUnavailable |
| + } |
| + var want hostclaim.LocalInstall |
| + if err := json.Unmarshal([]byte(obs.Claim.Op.Journal["local_install"]), &want); err != nil || want.InstallStamp == 0 { |
| + return false, nil // no journaled receipt to match: nothing vouches for the local state |
| + } |
| + got, ok, err := e.Receipt(ctx, obs) |
| + if err != nil { |
| + return false, err |
| + } |
| + return ok && got == want, nil |
| +} |
| + |
| func (e *RelocationEffects) Probe(ctx context.Context, obs hostclaim.Observed, coverage string) (uint64, bool, error) { |
| if e.Admit == nil { |
| return 0, false, ErrClaimStopUnavailable |
| @@ -11004,6 +11262,7 @@ When claim Plan 6b and moves Plans 1 and 2 are on main, rewrite Tasks 8a, 8b, 8c |
| | P's prepared files manifest is create-only at sequence 0, bound to `{location, P, op, install_stamp}`; the verifier (`PreparedFromInstallManifest`) reports `FilesSeq` 0, `SourceFilesSeq` the pin's, and the digest it read; the first admission takes that exact manifest, by digest, as the publisher's baseline, and the session's first publication is sequence 1 | 14 (1) | Task 5's `CopyPinnedManifest`, Task 1's `ToInstalled`; R1 (rev 15) | `TestPreparedFromInstallManifestReportsSequenceZero`, `TestRelocationProbeAdmissionConsumesThePreparedManifestByDigest` (a digest mismatch refuses the admission; the first commit is sequence 1) | |
| | Before P's first admission, `EnsureLocal`'s production body: `VerifyLocal` checks the receipt's files (against P's prepared manifest), env file and wake state under its `install_stamp`; a retired or partial install is restored by the same `Install` under the same stamp, then verified; an opened P is never reinstalled | 14 (2) | Task 7's `EnsureLocal`; Task 8c's `VerifyLocal` and `Install` | `TestRelocationLocalInstallIsRestoredAfterALostLeaseBeforeTheProbe` (journal the receipt, lose the lease, scoped cleanup retires the install, recover, the probe sees a complete install); `TestRelocationOpenedPIsNeverReinstalled` | |
| | A source's ordinary cold wake in `starting` and `releasing` dispatches through the wake inputs while its admission fence is open; refused once the fence closes or the claim no longer names it; a target's ordinary wake stays refused | 14 (3) | R1 (rev 15) | `TestRelocationSourceWakesInStarting`, `TestRelocationSourceWakesInReleasing`, `TestRelocationSourceWakeRefusedAfterItsFenceCloses`, `TestRelocationSourceWakeRefusedWithoutAuthority`, `TestRelocationTargetOrdinaryWakeStaysRefused` | |
| +| After P's first admission, `Receipt`'s production body reads this box's durable local install receipt (the install journal written under its `install_stamp`) and `VerifyReceipt` compares it with the journaled one; a missing or different receipt marks the operation `stuck` before any later admission, never a reinstall; legitimate post-admission changes to files, env and timers are never compared or reverted | 15 (1) | Task 6's participant, Task 7's `VerifyReceipt`; Task 8c's `Receipt` | `TestRelocationLostReceiptAfterPOpensIsStuckAcrossARestart` (open P, delete the install journal, restart the agent, the next probe attempt is refused and the claim is stuck); `TestRelocationPostAdmissionChangesSurviveTheReceiptCheck` | |
| | The producers' drain is idempotent: a second `DrainClaim` for the same stop and fence, after the producers have closed, acknowledges again with the same digest (Task 7's resumed drain relies on it after root fails between the drain and its receipt) | 7 (1) | 6b's `Wake.Producers` / `ClaimProducers.DrainClaim` | over the assembly: drain, root fails before `CompleteFence`, retry; one flush, two acknowledgements, a receipt | |
| | The complete writers-stopped scan is root's, authenticated, over the control socket | 2 (N3) | R3 (root half), `CollectWritersStopped` | the root endpoint under the production uid | |
| | `Region` on every stop request; `Recover` for the recorded owner after a restart | 2 (9), 3 (R1-9), 4 (R1-9) | 6b's `StopRequest.Region`, `Recover` | `…ReplaysOnlyRecordedPositions/after_a_restart…` against 6b's coordinator | |
| @@ -12825,3 +13084,4 @@ Expected: exit 0. Exit 2 is pending: wait and read again. Exit 1: read the log a |
| - **Rev 13 guards**, each removed in turn and its test watched to fail: `Acknowledge`'s handover (B's acknowledgement waits out the pass); `openBounded` (the open under the agent's lifetime never returns: the test's own timeout); the superseded case for hostexec's `ErrInactive` (the handover fails); removing the superseded journal entry once B opens (A is still retained). Four in all. |
| - **Rev 14 guards**, removed one at a time under `TestRelocationControllerLifecycleProperties` with 200 seeds (the table in the Rev 14 dispositions): ten killed, each with its seed and invariant. One, the extra scoped cleanup before a recovery reopen, survives as defence in depth, because `hostexec.Open` runs the same cleanup and refuses on its failure. Rev 13's guard "removing the superseded journal entry once B opens" is gone with that code (C3). |
| - **Rev 15 guards**, removed one at a time (the table in the Rev 15 dispositions): twelve killed. The survivors are defence in depth: `EnsureLocal` before entering probing is covered by the attempt-time check, and `EnsureLocal`'s own short-circuit for an opened P is covered because the participant never calls it after P opens. |
| +- **Rev 16 guards** (the table in the Rev 16 dispositions): the stuck-on-lost-receipt step and the exact receipt comparison are killed by their tests; both `EnsureLocal` calls removed together are killed by the property, seed 182. Rev 14's lifecycle guards are killed again under the crash event. |