amadan
sim: the source region keeps the files live set until the move commits, and INV-30 checks every servable region's next pin survives
Astra joint round 2 (J1). filesHome's landing branch keeps the source region home until the claim follows the commit (op.Committed), not only until the target's probe is admitted: admission commits nothing, and until the record's commit a clean rollback names op.SrcGen again in the source region. New witness wRollbackKeepsSourceFiles (files-home-move-phases): the source's restart queues the origin's park-generation, the sibling runs it after the target's probe is admitted and before the commit, the landing misses its cut deadline and rolls back cleanly, the publisher has nothing to republish, and the source's failover pins the keyed manifest and serves; at dfab457c's landing rule INV-30 fires at t=125, and under the mutation it is caught the same way. INV-30 (checkFilesPreserved), written apart from filesHome: in every region where the host could still be served next (op.exec's; a relocation's, move's or rollback's source; a landing's source until the record commits) the manifest its next install would pin, and the object it names, survive in its bucket unless a newer manifest landed. It runs only in the two-box shape. The files-live-set, files-live-set-moves-parks and files-home-move-phases witnesses now name INV-30, matched with a digit boundary so INV-3 no longer matches INV-30; TestFilesWitnessesStuckWithoutINV30 keeps their INV-3 liveness outcome with INV-30 off.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
5 files changed,
+257
−10
internal/sim/hostlife/regionha_test.go+100 −6internal/sim/hostlife/regionha_witness_test.go+121 −0internal/sim/hostlife/sim_test.go+3 −0internal/sim/hostlife/witness_test.go+27 −4internal/sim/hostlife/world_test.go+6 −0
diff --git a/internal/sim/hostlife/regionha_test.go b/internal/sim/hostlife/regionha_test.go| index 91aa837db..bb4644a2a 100644 |
| --- a/internal/sim/hostlife/regionha_test.go |
| +++ b/internal/sim/hostlife/regionha_test.go |
| @@ -2111,9 +2111,19 @@ func (w *world) filesLiveSet(c *claim, r int, k string) bool { |
| // reading, INV-3); |
| // - moving (before the flip, every phase, op.exec none from stopped on): |
| // the source's region; |
| -// - landing: the source's region until the target's probe is admitted |
| -// (holder.generation is still op.SrcGen), and the target's region, |
| -// op.exec's, throughout; |
| +// - landing: the target's region, op.exec's, throughout; and the |
| +// source's region until the claim follows the move's commit |
| +// (op.Committed, followRecord's "committed" case), not only until the |
| +// target's probe is admitted as §5.1's row for holder.generation |
| +// reads: the probe's admission commits nothing, and until the commit |
| +// a clean rollback names op.SrcGen again in the source region |
| +// (moves_test.go's return CAS, Holder.Gen = op.SrcGen), whose next |
| +// failover pins the source's chain there (Astra joint round 2). The |
| +// record's commit (landTarget's MoveState = "committed", the CAS on |
| +// the field rollback also takes) rules the rollback out; the claim |
| +// follows it in the CAS that queues the source region's |
| +// whole-location park-superseded, so the source stays home until |
| +// that park owns it; |
| // - restoring, every phase, released with op.exec none included: the |
| // source's region (a clean return names op.SrcGen again there; a |
| // dirty return's target region is retired by the release's |
| @@ -2123,8 +2133,8 @@ func (w *world) filesLiveSet(c *claim, r int, k string) bool { |
| // |
| // The mutation of files-home-move-phases keeps op.exec's region and a |
| // relocation's source only, so from a move's stopped phase to the |
| -// target's probe, and in a rollback's released phase, a park-generation |
| -// queued during the move archives the live manifest in the source region. |
| +// commit, and in a rollback's released phase, a park-generation queued |
| +// during the move archives the live manifest in the source region. |
| func (w *world) filesHome(c *claim, r int) bool { |
| if e := w.execBox(c); e != nil && e.Region == r { |
| return true |
| @@ -2139,11 +2149,95 @@ func (w *world) filesHome(c *claim, r int) bool { |
| case "moving", "restoring": |
| return true |
| case "landing": |
| - return c.Holder.Gen == c.Op.SrcGen |
| + return !c.Op.Committed |
| } |
| return false |
| } |
| +// pinWatch is what INV-30 remembers of one region: the manifest version |
| +// its next install would pin, and the object that manifest names when |
| +// the object was current in the region's bucket. |
| +type pinWatch struct { |
| + inc int |
| + loc string |
| + key string |
| + ver, base int |
| + obj string |
| +} |
| + |
| +// servableRegions are the regions where the host could still be served |
| +// next (INV-30's own reading of claim §6.2a and moves §5.1, written |
| +// apart from filesHome so that it can catch filesHome): op.exec's |
| +// region; a relocation's source region (it never leaves it); a move's |
| +// source region before the flip; a landing's source region until the |
| +// record commits (landTarget's MoveState = "committed", the CAS on the |
| +// field a rollback also takes: until then a clean rollback names |
| +// op.SrcGen again there); a rollback's source region. Creating, |
| +// deleting, parking and purging have no executor and name none. |
| +func (w *world) servableRegions(c *claim) []int { |
| + if c == nil || c.Holder == nil { |
| + return nil |
| + } |
| + var out []int |
| + if e := w.execBox(c); e != nil { |
| + out = append(out, e.Region) |
| + } |
| + src := false |
| + switch c.Op.Kind { |
| + case "relocating", "moving", "restoring": |
| + src = true |
| + case "landing": |
| + src = !c.Op.Committed && !(w.rec != nil && w.rec.MoveID == c.Op.ID && w.rec.MoveState == "committed") |
| + } |
| + if src && (len(out) == 0 || out[0] != c.Op.SrcRegion) { |
| + out = append(out, c.Op.SrcRegion) |
| + } |
| + return out |
| +} |
| + |
| +// checkFilesPreserved is INV-30 (joint round 2; claim §6.2a "Files in the |
| +// live set", moves §5.1): in every region where the host could still be |
| +// served next, the manifest that region's next install would pin (the |
| +// newest landed manifest of the admitted chain there, newestManifest, |
| +// which the failover's pin takes) and the object it names survive: once |
| +// seen, the version is never archived or deleted while the region can |
| +// still serve, unless a newer manifest has landed in its place. It reads |
| +// the bucket each step and remembers the last step's choice, so an |
| +// archive is seen as it happens, before any later read of the bucket |
| +// takes the shortened chain for the truth (the fence's timerCarried and |
| +// INV-28 read the bucket after the archive; a failover's stuck pin is |
| +// INV-3 only much later, and only if a failover happens). |
| +func (w *world) checkFilesPreserved() { |
| + c := w.claim |
| + next := map[int]pinWatch{} |
| + for _, r := range w.servableRegions(c) { |
| + loc := c.Holder.Location |
| + bk := w.buckets[r] |
| + mk, mv, _, _, m := w.newestManifest(r, loc, c.Holder.Gen) |
| + if p, ok := w.pinWatch[r]; ok && p.inc == c.Holder.Inc && p.loc == loc { |
| + gone := bk.current(p.key) == nil || bk.byID(p.key, p.ver) == nil |
| + superseded := m != nil && m.Base > p.base |
| + if gone && !superseded { |
| + w.violate("INV-30: region %d could still serve inc %d (%s %s), and the manifest its next install would pin, %s@%d, is gone from its bucket (now %q)", r, c.Holder.Inc, c.Op.Kind, c.Op.ID, p.key, p.ver, mk) |
| + return |
| + } |
| + if !gone && mk == p.key && p.obj != "" && bk.current(p.obj) == nil { |
| + w.violate("INV-30: region %d could still serve inc %d (%s %s), and the object %s its pinned manifest %s names is gone from its bucket", r, c.Holder.Inc, c.Op.Kind, c.Op.ID, p.obj, p.key) |
| + return |
| + } |
| + } |
| + if m == nil { |
| + continue |
| + } |
| + pw := pinWatch{inc: c.Holder.Inc, loc: loc, key: mk, ver: mv, base: m.Base} |
| + if m.Files != nil && m.Files.Obj != "" && bk.current(m.Files.Obj) != nil { |
| + pw.obj = m.Files.Obj |
| + } |
| + next[r] = pw |
| + } |
| + w.pinWatch = next |
| +} |
| + |
| // filesLiveIn is the files live set of region r. regional false is the |
| // region-blind set the rule files-live-region replaced (and every region |
| // authoritative, as live-set-region's mutation reads the whole live set): |
diff --git a/internal/sim/hostlife/regionha_witness_test.go b/internal/sim/hostlife/regionha_witness_test.go| index d4fb5abaf..118dab54f 100644 |
| --- a/internal/sim/hostlife/regionha_witness_test.go |
| +++ b/internal/sim/hostlife/regionha_witness_test.go |
| @@ -1101,6 +1101,93 @@ func wMoveStoppedKeepsLiveFiles(t *testing.T, w *world) { |
| w.finish(t) |
| } |
| +// wRollbackKeepsSourceFiles (files-home-move-phases; Astra joint round |
| +// 2): the stopped-move witness's setup, the source's restart inside a move |
| +// to region 1 queuing the origin's park-generation in region 0 while the |
| +// origin holds the keyed manifest, but the park waits until the move has |
| +// flipped and the target's probe is admitted (holder.generation is the |
| +// target's), before the commit. The sibling runs it then. The landing |
| +// misses its cut deadline and rolls back cleanly: the return names the |
| +// source's generation again in region 0, and the source serves there with |
| +// its files unchanged, so the publisher has nothing to republish. The |
| +// source is then terminated. Until the commit a rollback is possible, so |
| +// region 0 stayed the files home and the failover there pins the keyed |
| +// manifest and serves; with region 0 home only until the probe's |
| +// admission (dfab457c) or never (the mutation) the park archived it, and |
| +// the failover finds no manifest carrying instance.key: stuck for ever |
| +// (INV-3). |
| +func wRollbackKeepsSourceFiles(t *testing.T, w *world) { |
| + w.twoBox() |
| + src, sib := w.boxes[0], w.boxes[3] |
| + w.serve(src, 1, app0) |
| + w.running(t, src) |
| + w.published(t, src) |
| + loc := w.claim.Holder.Location |
| + published := w.stats["files manifests published"] |
| + if _, _, _, _, m := w.newestManifest(0, loc, w.claim.Holder.Gen); !manifestHasKey(m) { |
| + t.Fatalf("witness: the origin's manifest carries no instance.key: %s", w.state()) |
| + } |
| + w.moveTo(1) |
| + if w.claim.Op.Kind != "moving" { |
| + t.Fatalf("witness: the move did not start: %s", w.state()) |
| + } |
| + tgt := w.boxByID(w.claim.Op.Tgt) |
| + w.crash(src) |
| + parkQueued := func() bool { |
| + for _, o := range w.claim.Obl { |
| + if o.Kind == "park-generation" && o.Region == src.Region && o.Ret == "@root" { |
| + return true |
| + } |
| + } |
| + return false |
| + } |
| + if !w.reach(t, 200, "a fresh generation inside the move and the origin's park-generation queued", func() bool { |
| + return w.claim.Holder.Gen != "" && parkQueued() |
| + }, func() { w.worker(src); w.reconcile(src); w.wake(src) }) { |
| + return |
| + } |
| + srcGen := w.claim.Holder.Gen |
| + if !w.reach(t, 400, "the target's probe admitted, before the commit", func() bool { |
| + c := w.claim |
| + return c.Op.Kind == "landing" && !c.Op.Committed && c.Holder.Gen != srcGen && w.rec.MoveState == "landing" |
| + }, func() { w.worker(src); w.reconcile(src); w.worker(tgt); w.reconcile(tgt); w.runConsole() }) { |
| + return |
| + } |
| + if !w.reach(t, 400, "the sibling ran the origin's park-generation before the commit", func() bool { return !parkQueued() }, w.act(sib)) { |
| + return |
| + } |
| + if c := w.claim; c.Op.Kind != "landing" || c.Op.Committed { |
| + t.Fatalf("witness: the landing committed before the park: %s", w.state()) |
| + } |
| + // the target's agent stalls past the cut deadline; it rolls back when it |
| + // next acts, having written nothing |
| + deadline := w.claim.Op.CutDeadline |
| + w.drive(deadline+1-w.now, never, w.act(sib)) |
| + if !w.reach(t, 1500, "the clean return serving on the source", func() bool { |
| + c := w.claim |
| + return c.Op.Kind == "serving" && c.Op.Exec == src.ID // the return named srcGen; the re-admission moved to a fresh generation from it |
| + }, w.actAll(), w.recoveryPass, w.runConsole, func() { w.wake(src) }) { |
| + return |
| + } |
| + if w.stats["rollback-clean"] == 0 { |
| + t.Fatalf("witness: the rollback was not clean: %s", w.state()) |
| + } |
| + w.drive(20, never, w.act(src)) |
| + w.completeDue(true) |
| + if n := w.stats["files manifests published"]; n != published { |
| + t.Fatalf("witness: the publisher republished (%d manifests, %d before the move): the files are unchanged", n, published) |
| + } |
| + if _, _, _, _, m := w.newestManifest(src.Region, loc, w.claim.Holder.Gen); m == nil && on("files-home-move-phases") { |
| + t.Fatalf("witness: no manifest in the source region after the return: %s", w.state()) |
| + } |
| + w.terminate(src) |
| + w.reach(t, 3000, "serving again after the source's failover", func() bool { |
| + c := w.claim |
| + return c.Op.Kind == "serving" && c.Op.Exec >= 0 && c.Op.Exec != src.ID |
| + }, w.actAll(), w.recoveryPass, w.operator, w.wakeExec) |
| + w.finish(t) |
| +} |
| + |
| // wParkEvidenceEveryBox (park-evidence-every-box; final review Important |
| // 2, the shape of two-box seed 819): the host serves on box 0 with an |
| // acknowledged write its replicator has not shipped, and a delete |
| @@ -1137,3 +1224,37 @@ func wParkEvidenceEveryBox(t *testing.T, w *world) { |
| w.replicate(writer) |
| w.finish(t) |
| } |
| + |
| +// TestFilesWitnessesStuckWithoutINV30 keeps the liveness half of the files |
| +// witnesses (joint round 2). INV-30 now catches each of their mutations |
| +// at the archive, so TestWitnesses names INV-30; with INV-30 off, the |
| +// same scenario under the same mutation must still end in the failure it |
| +// was written for, the failover that can never pin the host's files |
| +// (INV-3), and must hold with the rule in place. |
| +func TestFilesWitnessesStuckWithoutINV30(t *testing.T) { |
| + saved := mutated |
| + defer func() { mutated = saved }() |
| + n := 0 |
| + for _, x := range witnesses { |
| + if x.want != "INV-30" { |
| + continue |
| + } |
| + n++ |
| + for _, m := range []string{"", x.needs} { |
| + mutated = m |
| + w := newWitness() |
| + w.noPinWatch = true |
| + x.run(t, w) |
| + switch { |
| + case m == "" && len(w.violations) > 0: |
| + t.Errorf("witness %s (INV-30 off) violated with its rule in place: %s", x.rule, w.violations[0]) |
| + case m != "" && (len(w.violations) == 0 || !namedFailure(w.violations[0], "INV-3")): |
| + dump(t, w) |
| + t.Errorf("witness %s under %q with INV-30 off: want INV-3, got %v", x.rule, m, w.violations) |
| + } |
| + } |
| + } |
| + if n != 4 { |
| + t.Fatalf("files witnesses naming INV-30: %d, want 4 (files-live-set, files-live-set-moves-parks, files-home-move-phases twice)", n) |
| + } |
| +} |
diff --git a/internal/sim/hostlife/sim_test.go b/internal/sim/hostlife/sim_test.go| index 397473f60..d7cc3fe6c 100644 |
| --- a/internal/sim/hostlife/sim_test.go |
| +++ b/internal/sim/hostlife/sim_test.go |
| @@ -406,6 +406,9 @@ func (w *world) checkStep() { |
| w.violate("INV-27: relocation %s names box %d as op.exec, which is unenrolled or lost", c.Op.ID, c.Op.Exec) |
| } |
| } |
| + if w.perRegion > 1 && !w.noPinWatch { |
| + w.checkFilesPreserved() // INV-30 (joint round 2): only the two-box shape has files keys |
| + } |
| } |
| func (w *world) boxesState() string { |
diff --git a/internal/sim/hostlife/witness_test.go b/internal/sim/hostlife/witness_test.go| index b1716e894..824c6fa84 100644 |
| --- a/internal/sim/hostlife/witness_test.go |
| +++ b/internal/sim/hostlife/witness_test.go |
| @@ -218,7 +218,7 @@ var witnesses = []witness{ |
| "the executor registers a timer whose manifest never lands and is terminated; the fence drops the timer silently", wFenceDeclaresTimers}, |
| {"reloc-enrolled-only", "reloc-enrolled-only", "INV-27", |
| "the only other box of the region holds no key and a replacement has launched unenrolled; the failover names the unenrolled reference", wRelocEnrolledOnly}, |
| - {"files-live-set", "files-live-set", "INV-3", |
| + {"files-live-set", "files-live-set", "INV-30", |
| "the chain's live manifest is the origin generation's, which a cold admission superseded without publishing (nothing changed: 1b-next rev 12's unchanged file); the origin's park-generation archives it, and the failover finds no manifest carrying instance.key: stuck, never served (rev 3: 1b-next ruling 25 makes the loss fail safe; with files-pin-needs-key also gone it is INV-4)", wFilesLiveSet}, |
| {"reloc-pin-claim-gen", "reloc-pin-claim-gen", "INV-3", |
| "a pinner observed the first round after the source's release and stalled; after the target wrote into P and died, its stale selection of generation_from is journaled for the nested pinning, and the build waits forever for objects generation_from's own park retired", wRelocPinClaimGen}, |
| @@ -250,7 +250,7 @@ var witnesses = []witness{ |
| "claim §11: the former source's scoped cleanup fails after the drain; its controller record stays and root refuses an executable update until the cleanup succeeds; without the rule the update runs over the unfinished cleanup", wClearAfterCleanup}, |
| {"fence-converts-committed-landing", "fence-converts-committed-landing", "INV-3", |
| "claim §11, F5: the record commits a landing and its target dies before the claim follows; the fence makes it a failover in the target's region, or nothing ever finishes it", wCommittedLandingTargetLost}, |
| - {"files-live-set-moves-parks", "files-live-set-moves-parks", "INV-3", |
| + {"files-live-set-moves-parks", "files-live-set-moves-parks", "INV-30", |
| "F4: a push parks the whole location; the files live set survives, so the later failover pins the live object, or can never pin the host's files", wPushKeepsLiveFiles}, |
| {"files-pin-needs-key", "files-pin-needs-key", "INV-4", |
| "L21, explicit: the pre-start manifest copy landed without instance.key, the app minted the key after starting and replicated rows sealed with it, and the box died before the keyed manifest landed; with the rule recovery is stuck and installs nothing, without it the keyless pin installs a fresh key over the sealed rows", wL21Window}, |
| @@ -264,8 +264,10 @@ var witnesses = []witness{ |
| // joint round 1 |
| {"files-live-region", "files-live-region", "residue never retired", |
| "joint round 1 finding 1: the source's manifest PUT is held while the host moves to region 1 and region 0 is cleaned up, then lands in region 0; the files live set is region-qualified, so the at-rest sweep retires it there; read in every region, the chain's newest manifest protects itself and is never retired (INV-10)", wLateManifestAfterMove}, |
| - {"files-home-move-phases", "files-home-move-phases", "INV-3", |
| + {"files-home-move-phases", "files-home-move-phases", "INV-30", |
| "joint round 1 review I1: a park-generation the source's restart queues during a move runs in the move's stopped phase, op.exec none; region 0 is still authoritative (moves §5.1), so the live manifest survives and the failover the source's termination converts the move into pins it and serves; with the files home read from op.exec alone it is archived and the failover is stuck for ever (INV-3)", wMoveStoppedKeepsLiveFiles}, |
| + {"files-home-move-phases", "files-home-move-phases", "INV-30", |
| + "Astra joint round 2: the same park waits until the target's probe is admitted, runs before the commit, and the landing rolls back cleanly; the source region stays the files home until the commit, so the source's failover after the return pins the keyed manifest and serves; home only until the probe's admission, or never, it is archived and the failover is stuck for ever (INV-3)", wRollbackKeepsSourceFiles}, |
| } |
| // TestWitnesses is the deterministic half of the mutation evidence. |
| @@ -362,7 +364,7 @@ func check(t *testing.T, x witness, m string, expectViolation bool, trace bool) |
| case expectViolation && !violated: |
| t.Errorf("witness %s held under %q, which it must violate", x.rule, m) |
| dump(t, w) |
| - case expectViolation && !strings.Contains(w.violations[0], x.want): |
| + case expectViolation && !namedFailure(w.violations[0], x.want): |
| t.Errorf("witness %s under %q violated, but not its named failure %q", x.rule, m, x.want) |
| dump(t, w) |
| case !expectViolation && violated: |
| @@ -374,6 +376,27 @@ func check(t *testing.T, x witness, m string, expectViolation bool, trace bool) |
| } |
| } |
| +// namedFailure: the violation names the witness's failure. want is one |
| +// failure or several separated by "|" (any of them); a failure that ends |
| +// in a digit must not run on into another (INV-3 is not INV-30). |
| +func namedFailure(v, want string) bool { |
| + for _, f := range strings.Split(want, "|") { |
| + for i := 0; ; { |
| + j := strings.Index(v[i:], f) |
| + if j < 0 { |
| + break |
| + } |
| + end := i + j + len(f) |
| + last := f[len(f)-1] |
| + if !(last >= '0' && last <= '9') || end == len(v) || v[end] < '0' || v[end] > '9' { |
| + return true |
| + } |
| + i = i + j + 1 |
| + } |
| + } |
| + return false |
| +} |
| + |
| func mutationSet(m string) map[string]bool { |
| set := map[string]bool{} |
| for _, x := range strings.Split(m, ",") { |
diff --git a/internal/sim/hostlife/world_test.go b/internal/sim/hostlife/world_test.go| index 0049356e7..7acb5fe1f 100644 |
| --- a/internal/sim/hostlife/world_test.go |
| +++ b/internal/sim/hostlife/world_test.go |
| @@ -1090,6 +1090,12 @@ type intner interface{ Intn(n int) int } |
| type world struct { |
| perRegion int // boxes per region at the start (region HA L18): 1, today's model, or 2 |
| issued int // files manifests issued, in order: INV-28's ground truth (blob.Base) |
| + // pinWatch is INV-30's memory: per region that could still serve, the |
| + // manifest its next install would pin, as the oracle saw it last step |
| + pinWatch map[int]pinWatch |
| + // noPinWatch turns INV-30 off: TestFilesWitnessesStuckWithoutINV30's |
| + // liveness runs only |
| + noPinWatch bool |
| // oneBoxRegion: a witness's region kept at one box by its group in the |
| // two-box shape (H5's minimum is per region) |
| oneBoxRegion [nRegions]bool |