amadan

carlos / platform Public

sim: Astra's round 7 on the two-box model: only a terminated box's volume evidence discharges its local cleanup, so a stopped box keeps it, and INV-26 checks the operation's discharges; the operator stops a target only when its release is unrecoverable and otherwise resumes it

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Paul Campbell pushed by claude 33f684bbeccd67d388332f8534109af2baf479ac parent a206447
4 files changed, +165 −4
  • internal/sim/hostlife/console_test.go +23 −1
  • internal/sim/hostlife/regionha_round1_test.go +127 −0
  • internal/sim/hostlife/regionha_test.go +14 −3
  • internal/sim/hostlife/rules_test.go +1 −0
diff --git a/internal/sim/hostlife/console_test.go b/internal/sim/hostlife/console_test.go
index ca3a2b689..9c219e278 100644
--- a/internal/sim/hostlife/console_test.go
+++ b/internal/sim/hostlife/console_test.go
@@ -1252,7 +1252,7 @@ func (w *world) operator() {
if dead != nil && !dead.Destroyed {
dead = nil
}
- if ex := w.boxByID(op.Exec); ex != nil && !ex.Destroyed && op.Phase == "probe-failed" && !released && !contains(c.Lost, ex.ID) && on("reloc-release-needs-flush") {
+ if ex := w.boxByID(op.Exec); ex != nil && !ex.Destroyed && op.Phase == "probe-failed" && !released && !contains(c.Lost, ex.ID) && on("reloc-release-needs-flush") && w.releaseUnrecoverable(ex, c) {
// a live target that cannot release (its replicator and its
// files are gone and nothing recorded a flush, rev 9): no
// release will ever come, so the operator stops the box, and
@@ -1344,6 +1344,28 @@ func (w *world) operator() {
w.declareTargetLost(c)
}
+// releaseUnrecoverable is the operator's check before it stops a live
+// target that has not released (rev 10, Astra round 7): only when no
+// release can ever come. That needs no flush recorded for this stop, and
+// either the session's replicator or the box's files directory gone for
+// good (relocRelease refuses without either). Any other release, a slow
+// acknowledgement or a recorded flush not yet journaled, is resumed: the
+// resolve clears stuck and sends the target back to probe-failed. The
+// mutation of operator-stop-unrecoverable-only stops every such target,
+// as rev 9 did.
+func (w *world) releaseUnrecoverable(b *box, c *claim) bool {
+ if !on("operator-stop-unrecoverable-only") {
+ return true
+ }
+ h := c.Holder
+ if r := b.relRecord; r != nil && r.Op == c.Op.ID && r.Phase == c.Op.Phase && r.E.Session == h.Session && r.E.Gen == h.Gen {
+ return false // a recorded flush: the release replays it
+ }
+ replicator := b.DB != nil && b.DB.Inc == h.Inc && b.DB.Gen == h.Gen && b.DB.Epoch == b.Epoch && b.DB.Session == h.Session
+ files := b.Files != nil && b.Files.Inc == h.Inc
+ return !replicator || !files
+}
+
// declareTargetLost is the declared loss of a landing's or a rollback's
// target that is gone (claim D2, moves §7.10): the operator's path, and,
// for a terminated target, the regional worker's automatic fence (claim
diff --git a/internal/sim/hostlife/regionha_round1_test.go b/internal/sim/hostlife/regionha_round1_test.go
index 24937fab6..4e8d93b9d 100644
--- a/internal/sim/hostlife/regionha_round1_test.go
+++ b/internal/sim/hostlife/regionha_round1_test.go
@@ -849,6 +849,133 @@ func TestReleaseReplaysTheRecordedFlush(t *testing.T) {
w.mustHold(t)
}
+// probeFailedTarget drains the host from box 0 to box 3, whose app
+// fails its probe, with a spare box 30 for the nested relocation, and
+// stops once the operation is in probe-failed with box 3 op.exec and no
+// release journaled.
+func (w *world) probeFailedTarget(t *testing.T) (from, to *box) {
+ from, to = w.boxes[0], w.boxes[3]
+ to.FailApp = true
+ w.serve(from, 1, app0)
+ w.running(t, from)
+ w.published(t, from)
+ w.drainTo(t, to)
+ w.extraBox(0, 30)
+ if !w.stepUntil(t, 1500, "probe-failed on the target", func() bool {
+ c := w.claim
+ return c.Op.Phase == "probe-failed" && c.Op.Exec == to.ID && c.Op.Release == nil
+ }) {
+ w.mustHold(t)
+ }
+ return from, to
+}
+
+// resolveOnly is the operator's resolve of a stuck relocation and
+// nothing else (the destroyed-local declaration is left out).
+func (w *world) resolveOnly() {
+ if c := w.claim; c != nil && c.Op.Kind == "relocating" && c.Op.Stuck != "" {
+ w.operator()
+ }
+}
+
+// TestOperatorResumesASlowRelease (operator-stop-unrecoverable-only; rev
+// 10, Astra round 7 finding 2): the failed target's final manifest PUT is
+// not acknowledged before the release deadline, so the operation is
+// stuck. Its replicator and files are intact: the operator's resolve
+// resumes the release rather than stopping the box; once the PUT lands
+// the release is journaled and the nested relocation serves. The
+// mutation stops the box.
+func TestOperatorResumesASlowRelease(t *testing.T) {
+ w := twoBoxWitness()
+ _, to := w.probeFailedTarget(t)
+ h := w.claim.Holder
+ held := dataKey(h.Location, h.Gen, "files/")
+ w.holdKey(held)
+ if !w.reach(t, 2*releaseDeadline, "stuck at the release deadline", func() bool { return w.claim.Op.Stuck != "" }, w.actAll(), w.recoveryPass) {
+ w.mustHold(t)
+ }
+ if c := w.claim; c.Op.Phase != "probe-failed" || c.Op.Release != nil {
+ t.Fatalf("not stuck in probe-failed without a release: %s", w.state())
+ }
+ w.resolveOnly()
+ if c := w.claim; to.Destroyed || c.Op.Stuck != "" || c.Op.Phase != "probe-failed" || c.Op.Exec != to.ID {
+ t.Fatalf("the resolve did not resume the target's release (stopped %v): %s", to.Destroyed, w.state())
+ }
+ w.hold = nil
+ w.completeHeld(held)
+ w.servingOn(t, nil)
+ if w.stats["operator stopped a target that cannot release"] != 0 || w.stats["release journaled: failed target"] == 0 {
+ t.Fatalf("the target was stopped, or never released: %v", w.stats)
+ }
+ w.finish(t)
+ w.mustHold(t)
+}
+
+// TestOperatorResumesARecordedFlush (operator-stop-unrecoverable-only;
+// rev 10, Astra round 7 finding 2): the failed target completes its
+// release sequence and records it, then its agent restarts (the
+// session's replicator is gone) before the release is journaled, and the
+// deadline passes. The recorded flush is a release waiting to be
+// journaled: the resolve resumes it, the target replays the record, and
+// the nested relocation serves. The mutation stops the box.
+func TestOperatorResumesARecordedFlush(t *testing.T) {
+ w := twoBoxWitness()
+ from, to := w.probeFailedTarget(t)
+ var r *releaseEntry
+ for i := 0; i < 60 && r == nil; i++ {
+ r = w.relocRelease(to, w.claim.clone()) // steps 1 to 3 and the record, not journaled
+ w.tick()
+ }
+ if r == nil {
+ t.Fatalf("the target's release sequence did not complete: %s", w.state())
+ }
+ w.crash(to)
+ spare := w.boxByID(30)
+ if !w.reach(t, 2*releaseDeadline, "stuck at the release deadline", func() bool { return w.claim.Op.Stuck != "" }, w.act(from, spare), w.recoveryPass) {
+ w.mustHold(t)
+ }
+ w.resolveOnly()
+ if c := w.claim; to.Destroyed || c.Op.Stuck != "" || c.Op.Phase != "probe-failed" {
+ t.Fatalf("the resolve did not resume the recorded release (stopped %v): %s", to.Destroyed, w.state())
+ }
+ w.servingOn(t, nil)
+ if w.stats["operator stopped a target that cannot release"] != 0 || w.stats["release: replayed from the recorded positions"] == 0 {
+ t.Fatalf("the target was stopped, or its record not replayed: %v", w.stats)
+ }
+ w.finish(t)
+ w.mustHold(t)
+}
+
+// TestStoppedTargetKeepsItsLocalCleanup (fence-discharge-qualified,
+// operator-stop-unrecoverable-only; rev 10, Astra round 7 findings 1 and
+// 2): the failed target loses its database and files with its agent, so
+// its release is unrecoverable; the operator stops the box and the next
+// resolve declares it lost and replays. The box's volume would be deleted
+// on termination, but it was stopped, not terminated: its disk is kept,
+// so when the recovery completes its park-local is still owed (claim §7.3
+// D5, H19). The mutation of fence-discharge-qualified discharges it.
+func TestStoppedTargetKeepsItsLocalCleanup(t *testing.T) {
+ w := twoBoxWitness()
+ _, to := w.probeFailedTarget(t)
+ to.DeleteOnTermination = true
+ w.crash(to)
+ to.Files, to.DB, to.receipt = nil, nil, nil
+ if !w.reach(t, 3000, "serving after the operator's stop and replay", func() bool {
+ c := w.claim
+ return c.Op.Kind == "serving" && c.Op.Exec >= 0 && c.Op.Exec != to.ID
+ }, w.actAll(), w.recoveryPass, w.wakeExec, w.resolveOnly) {
+ w.mustHold(t)
+ }
+ if !to.Destroyed || to.Terminated || w.stats["operator stopped a target that cannot release"] == 0 {
+ t.Fatalf("the target was not stopped by the operator: %s", w.state())
+ }
+ if !w.owesLocal(w.claim, to) {
+ t.Fatalf("the stopped target's local cleanup was discharged: %s", w.state())
+ }
+ w.finish(t) // the operator's destroyed-local declaration, an explicit attestation, retires it
+ 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 17338b857..1407d22f6 100644
--- a/internal/sim/hostlife/regionha_test.go
+++ b/internal/sim/hostlife/regionha_test.go
@@ -1665,7 +1665,13 @@ func (w *world) fenceBox(n *claim, x *box) {
}
}
}
- qualified := x.DeleteOnTermination
+ // a fence exists only for a terminated box (TerminationWorker verifies
+ // terminated), and only a terminated box's volume evidence says
+ // anything: a stopped box keeps its disk, so its park-local chores
+ // stay owed whatever DeleteOnTermination says (claim §7.3 D5, H19;
+ // rev 10, Astra round 7). The operator's declared loss of a stopped
+ // box reaches this function too, and discharges nothing
+ qualified := x.Terminated && x.DeleteOnTermination
if !on("fence-discharge-qualified") {
qualified = true
}
@@ -1676,8 +1682,8 @@ func (w *world) fenceBox(n *claim, x *box) {
var keep []obligation
for _, o := range n.Obl {
if o.Kind == "park-local" && o.Box == x.ID {
- if !x.DeleteOnTermination {
- w.violate("INV-26: box %d's park-local chore %s discharged without qualifying volume evidence (§5.9, H19)", x.ID, o.ID)
+ if !x.Terminated || !x.DeleteOnTermination {
+ w.violate("INV-26: box %d's park-local chore %s discharged without qualifying volume evidence (§5.9, H19; terminated %v)", x.ID, o.ID, x.Terminated)
}
w.stats["fence: park-local chores discharged"]++
continue
@@ -1685,6 +1691,11 @@ func (w *world) fenceBox(n *claim, x *box) {
keep = append(keep, o)
}
n.Obl = keep
+ if !x.Terminated || !x.DeleteOnTermination {
+ // INV-26 (rev 10): a discharge recorded for the operation's
+ // leftovers is a discharge too, though no chore exists yet
+ w.violate("INV-26: box %d's local retirement discharged without qualifying volume evidence (§5.9, H19, claim §7.3 D5; terminated %v)", x.ID, x.Terminated)
+ }
n.Op.Discharged = addUniq(n.Op.Discharged, x.ID)
}
diff --git a/internal/sim/hostlife/rules_test.go b/internal/sim/hostlife/rules_test.go
index 12fd15926..a35e9995f 100644
--- a/internal/sim/hostlife/rules_test.go
+++ b/internal/sim/hostlife/rules_test.go
@@ -197,6 +197,7 @@ var allRules = []string{
"files-live-set-moves-parks", // finding F4 (rev 4), claim §6.2a: moves' parks (a push's whole-location park, a landing's install park, a rollback's return park) keep the files live set; the mutation archives it with the rest and the next failover can never pin the live files (INV-3)
"reloc-clear-after-cleanup", // 1b-next ruling 20 and rev 6 R4-5 (Finish clears the record only after a successful scoped cleanup): a failed cleanup keeps the controller record, which blocks executable updates (claim §11's witness); the mutation clears it and an update runs over the unfinished cleanup (INV-29)
"fence-converts-committed-landing", // finding F5 (rev 4; claim §11 "automatic target loss racing the record commit CAS"): a landing whose record committed and whose target is then terminated becomes a failover in the target's region; the mutation leaves it to the operator, and it never completes (INV-3)
+ "operator-stop-unrecoverable-only", // rev 10 (Astra round 7; plan ruling 13, no 1b-next code): the operator stops a live target that has not released only when its release is unrecoverable (no recorded flush, and the session's replicator or its files gone); otherwise the resolve resumes the release; the mutation stops every such target (TestOperatorResumesASlowRelease, TestOperatorResumesARecordedFlush)
"reloc-release-needs-flush", // rev 9 (Astra round 6; 1b-next rev 19 Task 7 Release, relocationFlushDB, ReleaseFlushFiles, ReleasePositions): a release needs the session's own replicator and the box's own files directory, or the positions it recorded for this stop; otherwise none, and the deadline makes the operation stuck; the mutation journals the remote position with Flushed false (TestReleaseRefusedAfterACrashBeforeTheFlush, TestReleaseReplaysTheRecordedFlush)
"reloc-fence-pending-blocks", // rev 8 (Astra round 5; 1b-next rev 19 Worker.Step returns w.replace(...) before its phase switch): while a relocation participant's fence is pending (a dead target, no spare, before its deadline) no regional phase transition runs; the participant's own release still does; the mutation goes on into the phase switch (TestPendingTargetFenceHoldsThePhase)
"reloc-name-before-pin", // rev 7 (Astra round 4 finding 1; 1b-next rev 19 Worker.pinning): a relocation at pinning with no target names one before it selects a pin, on every path; the mutation pins first, and a manifest that lands while no box is eligible is left out (a loss bound: TestConvertedMoveWaitsForATargetBeforeItsPin)