amadan

carlos / platform Public

sim: the files home follows moves §5.1's authoritative region, so a park queued during a move keeps the live manifest in the source region until the flip

Joint round 1 review I1. filesHome is op.exec's region united with the
region moves §5.1's table names: the source region while moving (op.exec
none from stopped on), while landing until the target's probe is admitted
(holder.generation still op.SrcGen), while restoring (released included),
and for a whole relocation. Creating, deleting, parking and purging keep
none. New rule files-home-move-phases, whose mutation keeps op.exec's
region and a relocation's source only, with witness
wMoveStoppedKeepsLiveFiles: the source's restart inside a move queues the
origin's park-generation, the sibling runs it in stopped, the source is
terminated, and the converted failover pins the keyed manifest and serves;
under the mutation it is stuck for ever (INV-3).

M1: the files-live-region rule text matches the code (the source region
holds the whole files live set while a relocation runs). M2:
wLateManifestAfterMove also holds the changed file's object PUT, lands it
after the cleanup with the manifest, and requires both retired.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Paul Campbell pushed by claude dfab457ca04881cf6f22e01a5b832f9d1c1559a0 parent 55f03a6
4 files changed, +152 −34
  • internal/sim/hostlife/regionha_test.go +41 −12
  • internal/sim/hostlife/regionha_witness_test.go +107 −21
  • internal/sim/hostlife/rules_test.go +2 −1
  • internal/sim/hostlife/witness_test.go +2 −0
diff --git a/internal/sim/hostlife/regionha_test.go b/internal/sim/hostlife/regionha_test.go
index 0b221f322..91aa837db 100644
--- a/internal/sim/hostlife/regionha_test.go
+++ b/internal/sim/hostlife/regionha_test.go
@@ -2097,22 +2097,51 @@ func (w *world) filesLiveSet(c *claim, r int, k string) bool {
}
// 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).
+// authoritative region does (claim rev 6.5 §6.2a, R4-3): the region of
+// the holder's current installation, as the moves spec's §5.1 table
+// ("The authoritative region", the claim state by claim state table)
+// names it, united with op.exec's region, whose box runs moves' own parks
+// (F4's keepFilesLive):
+//
+// - serving, pushing, reverting: op.exec's region;
+// - relocating: its source region, for the whole operation (a
+// relocation never leaves it; while op.exec is none, at a failover's
+// pinning or a replay, the chain's newest manifest there is the pin's
+// candidate: two-box seed 1215, stuck for ever under a narrower
+// 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;
+// - 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
+// whole-location park, which never consults the files live set);
+// - creating, deleting, parking, purging, free: none (op.exec is none
+// in each, and no case below names them).
+//
+// 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.
func (w *world) filesHome(c *claim, r int) bool {
+ if e := w.execBox(c); e != nil && e.Region == r {
+ return true
+ }
if c.Op.Kind == "relocating" && r == c.Op.SrcRegion {
return true
}
- e := w.execBox(c)
- return e != nil && e.Region == r
+ if !on("files-home-move-phases") || r != c.Op.SrcRegion {
+ return false
+ }
+ switch c.Op.Kind {
+ case "moving", "restoring":
+ return true
+ case "landing":
+ return c.Holder.Gen == c.Op.SrcGen
+ }
+ return false
}
// filesLiveIn is the files live set of region r. regional false is the
diff --git a/internal/sim/hostlife/regionha_witness_test.go b/internal/sim/hostlife/regionha_witness_test.go
index 2ab4c0500..d4fb5abaf 100644
--- a/internal/sim/hostlife/regionha_witness_test.go
+++ b/internal/sim/hostlife/regionha_witness_test.go
@@ -1,6 +1,9 @@
package hostlife
-import "testing"
+import (
+ "strings"
+ "testing"
+)
// twoBoxWitness is newWitness with a second enrolled box in every region.
func twoBoxWitness() *world {
@@ -967,14 +970,17 @@ func wPushKeepsLiveFiles(t *testing.T, w *world) {
}
// 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).
+// claim §6.2a): the source in region 0 changes a file; the first PUT of
+// its new object is held, the publisher's retry lands, and the manifest
+// naming that object is held too. 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 do both held
+// PUTs land in region 0. Region 0 is no longer authoritative, so the late
+// manifest and the late object are residue there, and the at-rest sweep
+// retires both. Read without its region, the files live set finds the
+// late manifest as the chain's newest in region 0 and the object as the
+// one it names; they protect each other, and the sweep never retires
+// them (INV-10).
func wLateManifestAfterMove(t *testing.T, w *world) {
w.twoBox()
src := w.boxes[0]
@@ -982,18 +988,37 @@ func wLateManifestAfterMove(t *testing.T, w *world) {
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++
+ src.Files.Env++ // a changed file: its object first, then the manifest naming it
+ obj := objectKey(loc, w.claim.Holder.Gen, src.Files)
+ objHeld := false
+ w.hold = func(r *request) bool {
+ if r.key == obj && !objHeld {
+ objHeld = true // the object's first PUT; the publisher's retry lands
+ return true
+ }
+ return r.region == src.Region && isManifestKey(r.key) && strings.HasPrefix(r.key, loc)
+ }
+ held := func() (objs, mans int) {
+ for _, r := range w.pending {
+ if r.region == src.Region && r.doneAt == 1<<30 {
+ if r.key == obj {
+ objs++
+ } else if isManifestKey(r.key) {
+ mans++
+ }
+ }
}
+ return objs, mans
}
- if held != 1 {
- t.Fatalf("witness: held manifest PUTs: %d, want 1: %s", held, w.state())
+ if !w.reach(t, 3*uploadTimeout, "the object's first PUT and the manifest naming it held", func() bool {
+ o, m := held()
+ return o == 1 && m == 1
+ }) {
+ return
+ }
+ w.hold = nil
+ if src.Files.Obj != obj {
+ t.Fatalf("witness: the held manifest does not name the held object %s: %+v", obj, src.Files)
}
w.moveTo(1)
if w.claim.Op.Kind != "moving" {
@@ -1009,9 +1034,70 @@ func wLateManifestAfterMove(t *testing.T, w *world) {
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)
+ if n := w.completeHeld(loc + "files/"); n != 2 {
+ t.Fatalf("witness: held object and manifest PUTs completed: %d, want 2", n)
+ }
+ w.finish(t)
+}
+
+// wMoveStoppedKeepsLiveFiles (files-home-move-phases; joint round 1
+// review I1, moves §5.1's authoritative-region table): the source in
+// region 0 serves with a keyed manifest in the origin generation. A move
+// to region 1 starts, and the source's agent restarts inside it: its cold
+// admission into a fresh generation publishes the marker, which queues
+// the origin's park-generation in region 0 (PublishGeneration, legal
+// inside an operation a writer runs in), and publishes no manifest of its
+// own (nothing changed), so the origin's manifest stays the chain's
+// newest. The source stops (op.exec none) and only then does the
+// sibling, box 3, run the park-generation. The source is terminated and
+// the fence converts the move to a failover in region 0. Region 0 is the
+// authoritative region before the flip, so the files live set kept the
+// manifest and the failover pins it and serves; with the files home read
+// from op.exec alone it was archived, and the failover finds no manifest
+// carrying instance.key: stuck for ever (INV-3).
+func wMoveStoppedKeepsLiveFiles(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
+ 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
+ }
+ if !w.reach(t, 400, "the source stopped", func() bool {
+ c := w.claim
+ return c.Op.Kind == "moving" && c.Op.Exec == -1
+ }, func() { w.worker(src); w.reconcile(src); w.worker(tgt); w.reconcile(tgt) }) {
+ return
}
+ if !w.reach(t, 400, "the sibling ran the origin's park-generation while the move was stopped", func() bool { return !parkQueued() }, w.act(sib)) {
+ return
+ }
+ if c := w.claim; c.Op.Kind != "moving" {
+ t.Fatalf("witness: the move left its pre-flip phases before the park: %s", w.state())
+ }
+ w.terminate(src)
+ w.servingOn(t, nil)
w.finish(t)
}
diff --git a/internal/sim/hostlife/rules_test.go b/internal/sim/hostlife/rules_test.go
index 374241436..439cf4cbc 100644
--- a/internal/sim/hostlife/rules_test.go
+++ b/internal/sim/hostlife/rules_test.go
@@ -207,5 +207,6 @@ var allRules = []string{
"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)
+ "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 pin's, P's, the chain's newest and the objects they or a box's files directory name are live only in the files home (filesHome: the authoritative region, and while a relocation runs its source region holds the whole files live set), and the newest manifest is read only in the key's own region; the mutation reads every region, so a manifest PUT landing in the former region after a move's cleanup protects itself and the object it names, and the sweep never retires them (INV-10; witness)
+ "files-home-move-phases", // joint round 1 review I1, claim §6.2a and moves §5.1's authoritative-region table: the files home also holds the source region while moving (op.exec none from stopped on), while landing until the target's probe is admitted, and while restoring (released included); the mutation keeps op.exec's region and a relocation's source only, so a park-generation queued during the move archives the live manifest in stopped and the converted failover pins no keyed manifest (INV-3; witness)
}
diff --git a/internal/sim/hostlife/witness_test.go b/internal/sim/hostlife/witness_test.go
index 6d0f7d116..b1716e894 100644
--- a/internal/sim/hostlife/witness_test.go
+++ b/internal/sim/hostlife/witness_test.go
@@ -264,6 +264,8 @@ 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",
+ "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},
}
// TestWitnesses is the deterministic half of the mutation evidence.