amadan
sim: the files live set is region-qualified, so a manifest PUT that lands in a former region after a move's cleanup is retired by the sweep there
Joint round 1 finding 1. filesLive, filesLiveSet and objectReferenced take the key's region. A files key is live only in the files home: the authoritative region (op.exec's box, as deadGeneration reads it) and, while a relocation runs, its source region, where the pin is selected and P is built. The chain's newest manifest is read only in the key's own region, and a box's files directory protects only its own region's object. The source region stays home for the whole relocation, not only for the pin and P: under the narrower reading two-box seed 1215 fails (INV-3), as a park-generation archives the live manifest while a failover's op.exec is none, and the pin then finds no keyed manifest. New rule files-live-region (region HA block) with witness wLateManifestAfterMove: the source's manifest PUT is held across a move to region 1 and region 0's cleanup, then lands; the sweep retires it, and under the mutation (the region-blind set) it is residue for ever (INV-10). The live-set-region mutation also reads the files live set region-blind, as before. One-box COUNTERS and traces are unchanged.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
7 files changed,
+134
−25
internal/sim/hostlife/moves_test.go+1 −1internal/sim/hostlife/protocol_test.go+1 −1internal/sim/hostlife/regionha_test.go+77 −22internal/sim/hostlife/regionha_witness_test.go+49 −0internal/sim/hostlife/rules_test.go+2 −0internal/sim/hostlife/sim_test.go+1 −1internal/sim/hostlife/witness_test.go+3 −0
diff --git a/internal/sim/hostlife/moves_test.go b/internal/sim/hostlife/moves_test.go| index 3b434c9d7..c99a25ee8 100644 |
| --- a/internal/sim/hostlife/moves_test.go |
| +++ b/internal/sim/hostlife/moves_test.go |
| @@ -1921,7 +1921,7 @@ func locationOf(k string) string { |
| // in every region. |
| func (w *world) deadGeneration(c *claim, r int, k string) bool { |
| h := c.Holder |
| - if w.filesLive(c, k) { |
| + if w.filesLive(c, r, k) { |
| return false |
| } |
| e := w.execBox(c) |
diff --git a/internal/sim/hostlife/protocol_test.go b/internal/sim/hostlife/protocol_test.go| index f01ff161e..4c9ece1e0 100644 |
| --- a/internal/sim/hostlife/protocol_test.go |
| +++ b/internal/sim/hostlife/protocol_test.go |
| @@ -2391,7 +2391,7 @@ func (w *world) doObligation(b *box, c *claim, o obligation) { |
| if genOf(o.Prefix, k) != retire || inner != nil && inner(k) { |
| return true |
| } |
| - if w.filesLive(w.claim, k) { |
| + if w.filesLive(w.claim, b.Region, k) { |
| w.markSweepOwed(b.Region, k) |
| return true |
| } |
diff --git a/internal/sim/hostlife/regionha_test.go b/internal/sim/hostlife/regionha_test.go| index 2d325bb8f..0b221f322 100644 |
| --- a/internal/sim/hostlife/regionha_test.go |
| +++ b/internal/sim/hostlife/regionha_test.go |
| @@ -2081,26 +2081,60 @@ func (w *world) lastLandedManifest(r int, loc, gen string) *blob { |
| // generation, the one a running relocation's pin names, and the newest |
| // landed manifest of the admitted chain (the live manifest, which an |
| // unchanged file keeps referencing generations after it was published) |
| -// is never archived by a park-generation or read as residue. The |
| -// mutation of files-live-set protects nothing, so a park-generation of an |
| -// older generation archives the live or the pinned manifest. |
| -func (w *world) filesLive(c *claim, k string) bool { |
| - return on("files-live-set") && w.filesLiveSet(c, k) |
| +// is never archived by a park-generation or read as residue. It is |
| +// region-qualified (rule files-live-region; joint round 1 finding 1): k |
| +// is the key in region r's bucket. The mutation of files-live-set |
| +// protects nothing, so a park-generation of an older generation archives |
| +// the live or the pinned manifest. |
| +func (w *world) filesLive(c *claim, r int, k string) bool { |
| + return on("files-live-set") && w.filesLiveIn(c, r, k, on("files-live-region") && on("live-set-region")) |
| +} |
| + |
| +// filesLiveSet is the files live set itself, region-qualified, which the |
| +// residue oracle reads whatever is mutated. |
| +func (w *world) filesLiveSet(c *claim, r int, k string) bool { |
| + return w.filesLiveIn(c, r, k, true) |
| +} |
| + |
| +// filesHome: does region r hold the files live set? Only the |
| +// authoritative region does: the region of the holder's current |
| +// installation, op.exec's box, as deadGeneration reads it (claim rev 6.5 |
| +// §6.2a, R4-3); and while a relocation runs, its source region, where the |
| +// pin is selected and read (pinnedManifest reads op.SrcRegion) and P is |
| +// built. A relocation never leaves its source region, so this differs |
| +// from op.exec's region only while op.exec is none (a failover's pinning, |
| +// a replay): the chain's newest manifest there is the pin's candidate, |
| +// and a park-generation that archived it then would leave the pin |
| +// without the host's files (two-box seed 1215 under the narrower |
| +// reading: stuck for ever, INV-3). |
| +func (w *world) filesHome(c *claim, r int) bool { |
| + if c.Op.Kind == "relocating" && r == c.Op.SrcRegion { |
| + return true |
| + } |
| + e := w.execBox(c) |
| + return e != nil && e.Region == r |
| } |
| -// filesLiveSet is the files live set itself, which the residue oracle |
| -// reads whatever is mutated. |
| -func (w *world) filesLiveSet(c *claim, k string) bool { |
| +// 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): |
| +// the newest manifest of the chain in any region is live in every region, |
| +// so a manifest PUT that lands in a former region after a move's cleanup |
| +// protects itself there for ever. |
| +func (w *world) filesLiveIn(c *claim, r int, k string, regional bool) bool { |
| if c == nil || c.Holder == nil || !isFilesKey(k) { |
| return false |
| } |
| if !isManifestKey(k) { |
| - return w.objectReferenced(c, k) |
| + return w.objectReferenced(c, r, k, regional) |
| } |
| loc := c.Holder.Location |
| if !strings.HasPrefix(k, loc) { |
| return false |
| } |
| + if regional && !w.filesHome(c, r) { |
| + return false |
| + } |
| g := genOf(loc, k) |
| if g == c.Holder.Gen { |
| return true |
| @@ -2113,14 +2147,27 @@ func (w *world) filesLiveSet(c *claim, k string) bool { |
| return true |
| } |
| } |
| - for r := 0; r < nRegions; r++ { |
| - if mk, _, _, _, _ := w.newestManifest(r, loc, c.Holder.Gen); mk == k { |
| + for _, x := range w.filesRegions(r, regional) { |
| + if mk, _, _, _, _ := w.newestManifest(x, loc, c.Holder.Gen); mk == k { |
| return true |
| } |
| } |
| return false |
| } |
| +// filesRegions is where the live set's newest manifest is read for a key |
| +// of region r: region r alone; the region-blind set reads every region. |
| +func (w *world) filesRegions(r int, regional bool) []int { |
| + if regional { |
| + return []int{r} |
| + } |
| + all := make([]int, nRegions) |
| + for i := range all { |
| + all[i] = i |
| + } |
| + return all |
| +} |
| + |
| // pinnedManifest is the manifest the local install applies: the exact |
| // version the pin names (rule files-pin-exact; the model's versioned |
| // bucket reads it by version id, where the real store, which has none, |
| @@ -2269,18 +2316,26 @@ func observedAt(x *box) int { |
| return x.FenceObservedAt |
| } |
| -// objectReferenced: a live manifest (the chain's newest in any region, |
| -// the pinned one, holder.generation's or P's) names the object, or a |
| -// live box's files directory does (its next manifest will): the files |
| -// live set is every object the live manifests reference (claim §6.2a). |
| -func (w *world) objectReferenced(c *claim, k string) bool { |
| +// objectReferenced: a live manifest (the chain's newest, the pinned one, |
| +// holder.generation's or P's) names the object, or a live box's files |
| +// directory does (its next manifest will): the files live set is every |
| +// object the live manifests reference (claim §6.2a). Region-qualified as |
| +// the manifests are: k is the key in region r's bucket, region r must be |
| +// the files home (filesHome), only region r's manifests are read, and a |
| +// box's directory names k only when it names region r's object. The |
| +// region-blind set (regional false) reads every region's manifests and |
| +// every box's directory, for a key of any region. |
| +func (w *world) objectReferenced(c *claim, r int, k string, regional bool) bool { |
| loc := c.Holder.Location |
| names := func(m *blob) bool { return m != nil && m.Files != nil && m.Files.Obj == k } |
| - for r := 0; r < nRegions; r++ { |
| - if _, _, _, _, m := w.newestManifest(r, loc, c.Holder.Gen); names(m) { |
| + if regional && !w.filesHome(c, r) { |
| + return false |
| + } |
| + for _, x := range w.filesRegions(r, regional) { |
| + if _, _, _, _, m := w.newestManifest(x, loc, c.Holder.Gen); names(m) { |
| return true |
| } |
| - bk := w.buckets[r] |
| + bk := w.buckets[x] |
| for _, g := range []string{c.Holder.Gen, c.Op.Prepared} { |
| if g == "" && g != c.Holder.Gen { |
| continue |
| @@ -2292,13 +2347,13 @@ func (w *world) objectReferenced(c *claim, k string) bool { |
| } |
| } |
| } |
| - if c.Op.Kind == "relocating" && c.Op.Pin != nil && c.Op.Pin.ManKey != "" { |
| + if c.Op.Kind == "relocating" && c.Op.Pin != nil && c.Op.Pin.ManKey != "" && (!regional || r == c.Op.SrcRegion) { |
| if names(w.pinnedManifestOf(c.Op.SrcRegion, c.Op.Pin)) { |
| return true |
| } |
| } |
| for _, b := range w.liveBoxes() { |
| - if b.Files != nil && b.Files.Obj == k { |
| + if b.Files != nil && b.Files.Obj == k && (!regional || b.Files.ObjRegion == r) { |
| return true |
| } |
| } |
| @@ -2316,7 +2371,7 @@ func (w *world) keepFilesLive(r int, keep func(string) bool) func(string) bool { |
| if keep(k) { |
| return true |
| } |
| - if on("files-live-set-moves-parks") && w.filesLive(w.claim, k) { |
| + if on("files-live-set-moves-parks") && w.filesLive(w.claim, r, k) { |
| w.markSweepOwed(r, k) |
| return true |
| } |
diff --git a/internal/sim/hostlife/regionha_witness_test.go b/internal/sim/hostlife/regionha_witness_test.go| index 15b0c012e..2ab4c0500 100644 |
| --- a/internal/sim/hostlife/regionha_witness_test.go |
| +++ b/internal/sim/hostlife/regionha_witness_test.go |
| @@ -966,6 +966,55 @@ func wPushKeepsLiveFiles(t *testing.T, w *world) { |
| w.finish(t) |
| } |
| +// wLateManifestAfterMove (files-live-region; joint round 1 finding 1, |
| +// claim §6.2a): the source in region 0 publishes a manifest whose PUT |
| +// the witness holds; the host moves to region 1, which admits a |
| +// generation whose chain (genParent) leads back to the source's; the |
| +// source region is cleaned up, and only then does the held PUT land in |
| +// region 0. Region 0 is no longer authoritative, so the late manifest is |
| +// residue there, and the at-rest sweep retires it. Read without its |
| +// region, the files live set finds it as the chain's newest manifest in |
| +// region 0, it protects itself, and the sweep never retires it (INV-10). |
| +func wLateManifestAfterMove(t *testing.T, w *world) { |
| + w.twoBox() |
| + src := w.boxes[0] |
| + w.serve(src, 1, app0) |
| + w.running(t, src) |
| + w.published(t, src) |
| + loc := w.claim.Holder.Location |
| + w.timerOn(src) // a changed state: the publisher's next manifest |
| + w.holdKey(loc + "files/") |
| + w.publishFiles(src) |
| + w.hold = nil |
| + held := 0 |
| + for _, r := range w.pending { |
| + if r.region == src.Region && isManifestKey(r.key) && r.doneAt == 1<<30 { |
| + held++ |
| + } |
| + } |
| + if held != 1 { |
| + t.Fatalf("witness: held manifest PUTs: %d, want 1: %s", held, w.state()) |
| + } |
| + w.moveTo(1) |
| + if w.claim.Op.Kind != "moving" { |
| + t.Fatalf("witness: the move did not start: %s", w.state()) |
| + } |
| + if !w.servingOn(t, nil) { |
| + return |
| + } |
| + if e := w.execBox(w.claim); e == nil || e.Region != 1 { |
| + w.violate("witness: the move did not land in region 1: %s", w.state()) |
| + return |
| + } |
| + if !w.reach(t, 1200, "the source region cleaned up", func() bool { return len(w.claim.Obl) == 0 }, w.actAll(), w.recoveryPass) { |
| + return |
| + } |
| + if n := w.completeHeld(loc + "files/"); n != 1 { |
| + t.Fatalf("witness: held manifest PUTs completed: %d, want 1", n) |
| + } |
| + 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 |
diff --git a/internal/sim/hostlife/rules_test.go b/internal/sim/hostlife/rules_test.go| index d1c5f5b8c..374241436 100644 |
| --- a/internal/sim/hostlife/rules_test.go |
| +++ b/internal/sim/hostlife/rules_test.go |
| @@ -206,4 +206,6 @@ var allRules = []string{ |
| "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) |
| "reloc-name-drops-move-target", // final review Important 1 (1b-next 151261fe, NameTarget; moves §7.10, region HA §5.8): naming a converted move's same-region target takes the move's own target (move_target_box, in the other region) off the participants in the same CAS; the mutation keeps it on the barrier, and a stopped move target holds the relocation at pinning for ever (liveness, expected miss; TestConvertedMoveDropsTheMoveTargetFromTheBarrier) |
| "park-evidence-every-box", // final review Important 2 (cf566b41; hostops RetirementEvidence.VerifyObligation, collectEvidence over the inventory; claim §6.2a): in a two-box region a park-replica or park-superseded run by a box that is not the executor waits for every live box of the region not on lost to publish its stop evidence for the operation; the mutation parks on the owner's evidence alone, and the sibling writer's replicator ships into the parked region (INV-10, seed 819; witness) |
| + // Astra's joint round 1 on the two-box model |
| + "files-live-region", // joint round 1 finding 1, claim §6.2a (the live set is {authoritative region, location, generation}; region HA §5.6, L13): the files live set is region-qualified: holder.generation's manifests, the chain's newest and the objects they name are live only in the authoritative region, a relocation's pin and P also in its source region, and the newest manifest is read only there; the mutation reads the chain's newest manifest in every region, so a manifest PUT landing in the former region after a move's cleanup protects itself and the sweep never retires it (INV-10; witness) |
| } |
diff --git a/internal/sim/hostlife/sim_test.go b/internal/sim/hostlife/sim_test.go| index f99260ce4..397473f60 100644 |
| --- a/internal/sim/hostlife/sim_test.go |
| +++ b/internal/sim/hostlife/sim_test.go |
| @@ -455,7 +455,7 @@ func (w *world) residueOf(exceptStragglers bool) []string { |
| bk := w.buckets[r] |
| for _, p := range []string{"instances/" + host + "/", "moves/" + host + "/"} { |
| for _, k := range bk.keys(p) { |
| - if strings.HasSuffix(k, "lock.json") || (r == serving && (live[k] || isDataKey(k) && live[genPrefixOf(k)] || isClosedKey(k) && live[k[:strings.LastIndex(k, "closed/")+7]] || w.filesLiveSet(c, k))) { |
| + if strings.HasSuffix(k, "lock.json") || (r == serving && (live[k] || isDataKey(k) && live[genPrefixOf(k)] || isClosedKey(k) && live[k[:strings.LastIndex(k, "closed/")+7]] || w.filesLiveSet(c, r, k))) { |
| continue |
| } |
| if exceptStragglers && w.owed(r, k) { |
diff --git a/internal/sim/hostlife/witness_test.go b/internal/sim/hostlife/witness_test.go| index 4cb78f896..6d0f7d116 100644 |
| --- a/internal/sim/hostlife/witness_test.go |
| +++ b/internal/sim/hostlife/witness_test.go |
| @@ -261,6 +261,9 @@ var witnesses = []witness{ |
| // the final review's fixes |
| {"park-evidence-every-box", "park-evidence-every-box", "freed with residue", |
| "two-box seed 819: a delete's regional park-replica is run by the writer's sibling while the writer's replicator still runs; with the rule it waits for the writer's own stop evidence, without it the region is parked and the writer's next shipment is residue when the host is freed (INV-10)", wParkEvidenceEveryBox}, |
| + // 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}, |
| } |
| // TestWitnesses is the deterministic half of the mutation evidence. |