amadan
hostlife model: rev 7.17, joint round 16 and claim rev 6.24
R16-2: a park executes strictly within its scope's namespace. The sweep groups its residue by scope location (an incarnation's own, the legacy instances/<host> which excludes child incarnations, moves/<host>) and queues one chore per location with that scope and its archive incarnation; the archive destination names the incarnation; the runner confines every scoped chore's listing to its scope (a staging lane to its own lane, an instances scope never to moves/) and INV-23 checks every key a chore would archive for membership. The delete's park is scoped to the deleted incarnation's own location and the staging namespace, never the whole host prefix. Rule scope-membership (the mutation is rev 7.16's whole-prefix listing); witness wSweepScopeMembership. R16-3: the legacy identity is session 0 with generation "" (@root): adoption, the pre-release processes and their acknowledgements, and the witness fixtures carry it; INV-24 (every declaration names a box; session 0 only in the origin generation); a created incarnation's first admission declares nothing, its predecessor has no writer. TestLegacyLostTargetReturn: adopt, a move with src_covered false, a cold target admission, the target declared lost, the return declares the target's session and the source's cut session 0. R16-1: TestStagingSurvivesLegacyPark, sealed staging beside a legacy instance park. Born-covered narrowed to a park scoped exactly to holder.location or an unscoped park-replica (claim rev 6.24 item 5). Rules: 107. Witnesses: 73.
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
7 files changed,
+326
−33
internal/sim/hostlife/background_test.go+9 −5internal/sim/hostlife/console_test.go+10 −1internal/sim/hostlife/moves_test.go+21 −11internal/sim/hostlife/protocol_test.go+96 −6internal/sim/hostlife/rules_test.go+1 −0internal/sim/hostlife/sim_test.go+3 −3internal/sim/hostlife/witness_test.go+186 −7
diff --git a/internal/sim/hostlife/background_test.go b/internal/sim/hostlife/background_test.go| index bb5781ef5..642f71695 100644 |
| --- a/internal/sim/hostlife/background_test.go |
| +++ b/internal/sim/hostlife/background_test.go |
| @@ -167,11 +167,15 @@ func (w *world) adopt() bool { |
| if eb == nil { |
| return false |
| } |
| - // adoption writes holder.stamp (claim rev 6.5 §2); the session starts |
| - // with it, and the pre-release process on the executing box is its |
| - // writer (rev 7.11: the first cold admission's writes_lost names it; |
| - // seed 94288 / 100,000 named box 0 and left the legacy writes undeclared) |
| - n := &claim{Ver: 1, Holder: &holder{Inc: w.rec.Inc, App: w.rec.App, Legacy: true, Location: locationFor(w.rec.Inc, true), Stamp: 1, Session: 1, WriterBox: eb.ID}, |
| + // adoption writes holder.stamp (claim rev 6.5 §2). The pre-claim writer |
| + // is the legacy identity (claim rev 6.24, R16-3): session 0 with |
| + // generation "" (read as @root), the pre-release process on the |
| + // executing box its writer_box; the first cold admission's writes_lost |
| + // names it (seed 94288 / 100,000 named box 0 and left the legacy writes |
| + // undeclared), and a lost-target return declares it in |
| + // additional_writes_lost. Rev 7.13 to 7.16 gave it session 1, which hid |
| + // the session-zero case from E |
| + n := &claim{Ver: 1, Holder: &holder{Inc: w.rec.Inc, App: w.rec.App, Legacy: true, Location: locationFor(w.rec.Inc, true), Stamp: 1, Session: 0, WriterBox: eb.ID}, |
| Op: opState{Kind: "serving", Exec: eb.ID, Parts: []int{eb.ID}}, Regions: []int{w.rec.Region}, Boxes: []int{eb.ID}, Complete: false} |
| if w.stampBox == nil { |
| w.stampBox = map[int]int{} |
diff --git a/internal/sim/hostlife/console_test.go b/internal/sim/hostlife/console_test.go| index 48aeea4bc..89c0e50d7 100644 |
| --- a/internal/sim/hostlife/console_test.go |
| +++ b/internal/sim/hostlife/console_test.go |
| @@ -476,8 +476,17 @@ func (w *world) parkingObligations(n *claim, inc int) { |
| boxes = addUniq(boxes, b.ID) |
| } |
| } |
| + // the deleted incarnation's own location (the legacy instances/<host> |
| + // for a legacy host, which excludes child incarnations; claim rev |
| + // 6.24 §2) and the staging namespace, each its own chore; an older |
| + // incarnation's residue is the at-rest sweep's (R3-4). The mutation of |
| + // scope-membership parks the whole host prefix, as rev 7.16 did |
| + loc := "instances/" + host + "/" |
| + if n.Holder != nil && on("scope-membership") { |
| + loc = n.Holder.Location |
| + } |
| for _, r := range regions { |
| - for _, p := range []string{"instances/" + host + "/", "moves/" + host + "/"} { |
| + for _, p := range []string{loc, "moves/" + host + "/"} { |
| n.Obl = append(n.Obl, w.newObl(n, "park-replica", r, -1, p, fmt.Sprint(inc), 0)) |
| } |
| } |
diff --git a/internal/sim/hostlife/moves_test.go b/internal/sim/hostlife/moves_test.go| index c21e361ba..ed2a73a8e 100644 |
| --- a/internal/sim/hostlife/moves_test.go |
| +++ b/internal/sim/hostlife/moves_test.go |
| @@ -1666,12 +1666,26 @@ func (w *world) sweep(b *box, c *claim) { |
| } |
| } |
| bk := w.buckets[b.Region] |
| + // one chore per scope location holding residue (claim rev 6.24 §2, |
| + // R16-2): the sweepable keys are grouped by the location they belong |
| + // to, an incarnation's own, the legacy instances/<host> (a level |
| + // directory or generation directly under the host prefix, never a |
| + // child incarnation) or moves/<host>; each chore's scope names that |
| + // location and its archive incarnation. The mutation of |
| + // scope-membership queues rev 7.16's two chores, instances/<host> and |
| + // moves/<host>, over the whole prefixes |
| var prefixes []string |
| for _, p := range []string{"instances/" + host + "/", "moves/" + host + "/"} { |
| for _, k := range bk.keys(p) { |
| - if hasNonMarker(bk.objs[k]) && w.sweepable(c, b.Region, k) { |
| - prefixes = append(prefixes, p) |
| - break |
| + if !hasNonMarker(bk.objs[k]) || !w.sweepable(c, b.Region, k) { |
| + continue |
| + } |
| + loc := p |
| + if on("scope-membership") { |
| + loc = scopeOf(k) + "/" |
| + } |
| + if !hasStr(prefixes, loc) { |
| + prefixes = append(prefixes, loc) |
| } |
| } |
| } |
| @@ -1704,17 +1718,13 @@ func (w *world) sweep(b *box, c *claim) { |
| op = n.Op.ID |
| w.stats["holderless sweeps"]++ |
| } |
| - inc := 0 |
| - if n.Holder != nil { |
| - inc = n.Holder.Inc |
| - } else if len(n.Retired) > 0 { |
| - inc = n.Retired[len(n.Retired)-1] // a free host's sweep archives under the newest retired incarnation (claim rev 6.23 §2) |
| - } |
| for _, p := range prefixes { |
| // the scope is persisted at the queuing CAS (claim rev 6.23 §2): |
| // the sweeping box's complete listing is the evidence, taken now; |
| - // the location instances/<host> or moves/<host> |
| - n.Obl = append(n.Obl, w.scoped(obligation{ID: w.newID("ob"), Op: op, Kind: "park-sweep", Region: b.Region, Box: -1, Prefix: p, Ret: "sweep"}, w.now, inc)) |
| + // the location and its archive incarnation (the location's own, |
| + // the holder's for the legacy location or the staging sweep, the |
| + // newest retired on a free host; claim rev 6.24 §2) |
| + n.Obl = append(n.Obl, w.scoped(obligation{ID: w.newID("ob"), Op: op, Kind: "park-sweep", Region: b.Region, Box: -1, Prefix: p, Ret: "sweep"}, w.now, incOf(n, scopeLocation(p)))) |
| } |
| // CoverParkedPredecessors at the queuing CAS (claim rev 6.21 item 6): |
| // the predecessors with a sweepable object, no others |
diff --git a/internal/sim/hostlife/protocol_test.go b/internal/sim/hostlife/protocol_test.go| index f811d108b..b7986dd7d 100644 |
| --- a/internal/sim/hostlife/protocol_test.go |
| +++ b/internal/sim/hostlife/protocol_test.go |
| @@ -1781,7 +1781,12 @@ func (w *world) admitCommit(b *box, c *claim, a admitInput) bool { |
| // after the release queued the target region's park, and |
| // CoverRegionPredecessors in that CAS could not see this record |
| for _, o := range n.Obl { |
| - if o.Kind == "park-superseded" && o.Region == e.PredRegion && o.Prefix == n.Holder.Location { |
| + // narrowed (claim rev 6.24 item 5): a park scoped exactly to |
| + // holder.location, or an unscoped park-replica; a scoped park of |
| + // an old incarnation or of a staging prefix does not count |
| + exact := o.Kind == "park-superseded" && o.Prefix == n.Holder.Location && (o.Scope == nil || o.Scope.Location == scopeLocation(n.Holder.Location)) |
| + unscopedReplica := o.Kind == "park-replica" && o.Scope == nil |
| + if (exact || unscopedReplica) && o.Region == e.PredRegion { |
| e.Covered = true |
| w.stats["admissions born covered: whole-location park pending"]++ |
| break |
| @@ -1802,12 +1807,17 @@ func (w *world) admitCommit(b *box, c *claim, a admitInput) bool { |
| n.Holder.Stamp = w.issueStamp(n, b.ID) |
| } |
| e.Stamp = n.Holder.Stamp |
| - if a.Coverage == "" && !a.PredecessorCertified && on("writes-lost") { |
| + if a.Coverage == "" && !a.PredecessorCertified && p.Box >= 0 && on("writes-lost") { |
| // only an uncovered, uncertified predecessor is declared |
| // (claim rev 6.12): a sealed or clean-return coverage holds |
| - // every write it acknowledged |
| + // every write it acknowledged. A created incarnation's first |
| + // admission has no predecessor writer (holder.writer_box is |
| + // empty before the first writer, claim rev 6.24): nothing is |
| + // declared, since a declaration always names a box (INV-24) |
| lost = &writesLost{Box: p.Box, Gen: p.Gen, Session: p.Session, RemoteMaxTXID: a.RemoteMaxTXID} |
| e.Lost = lost |
| + } else if a.Coverage == "" && !a.PredecessorCertified && p.Box < 0 { |
| + w.stats["admission: no predecessor writer, nothing declared"]++ |
| } |
| if n.Op.Kind == "restoring" && n.Op.LostAt != 0 && b.ID == n.Op.Src && on("writes-lost") { |
| // additional_writes_lost (claim rev 6.22 item 2, R13-3, R14-2): |
| @@ -1913,7 +1923,10 @@ func (w *world) admitCommit(b *box, c *claim, a admitInput) bool { |
| } |
| if lost != nil || len(lostTgt) > 0 { |
| // INV-21 (rev 7.15, R14-2): the declarations of one admission are |
| - // unique by (box, session), the ordinary record and the list together |
| + // unique by (box, session), the ordinary record and the list together. |
| + // INV-24 (claim rev 6.24, R16-3): every declaration names a box; the |
| + // legacy identity, session 0, comes only with generation "" (@root), |
| + // the adopted host's pre-claim writer, and is valid in both fields |
| seen := map[[2]int]bool{} |
| all := append([]*writesLost{}, lostTgt...) |
| if lost != nil { |
| @@ -1925,6 +1938,12 @@ func (w *world) admitCommit(b *box, c *claim, a admitInput) bool { |
| w.violate("INV-21: box %d declared {box %d, session %d} twice in one admission (writes_lost and additional_writes_lost)", b.ID, x.Box, x.Session) |
| } |
| seen[k] = true |
| + if x.Box < 0 || x.Session == 0 && x.Gen != "" { |
| + w.violate("INV-24: box %d declared {box %d, generation %q, session %d}: a declaration names a box, and session 0 is the legacy identity in the origin generation only", b.ID, x.Box, x.Gen, x.Session) |
| + } |
| + if x.Session == 0 { |
| + w.stats["writes_lost: the legacy identity (session 0)"]++ |
| + } |
| } |
| } |
| return true |
| @@ -2171,6 +2190,25 @@ func (w *world) doObligation(b *box, c *claim, o obligation) { |
| // one of the grammar's four forms |
| w.violate("INV-23: chore %s (%s) carries a scope location %q outside the claim's grammar", o.ID, o.Kind, o.Scope.Location) |
| } |
| + // membership (claim rev 6.24 §2, R16-1, R16-2): a park executes |
| + // strictly within its scope's namespace. Every key the chore would |
| + // archive must be in scope (INV-23's second half, checked on the |
| + // manifest's sources), and under the rule the chore's listing is |
| + // confined to the scope: the legacy instances/<host> scope excludes |
| + // child incarnations, an instances scope never touches moves/, a |
| + // staging lane's scope only its own lane. The mutation of |
| + // scope-membership is rev 7.16's listing of the whole park prefix |
| + var member func(string) bool |
| + if o.Scope != nil && o.Kind != "park-local" { |
| + loc := o.Scope.Location |
| + member = func(k string) bool { return inScope(k, loc) } |
| + for _, k := range w.buckets[b.Region].keys(o.Prefix) { |
| + if !member(k) && hasNonMarker(w.buckets[b.Region].objs[k]) && (o.Kind != "park-sweep" || w.sweepable(w.claim, b.Region, k)) && !on("scope-membership") { |
| + w.violate("INV-23: chore %s (%s, scope %s, incarnation %d) would archive %s, outside its scope", o.ID, o.Kind, loc, o.Scope.Inc, k) |
| + break |
| + } |
| + } |
| + } |
| if o.Kind == "park-replica" || o.Kind == "park-superseded" || o.Kind == "park-staging" { |
| // the owner first proves the region's box runs nothing for the |
| // host, when it is not the current executor (a whole-location |
| @@ -2244,8 +2282,12 @@ func (w *world) doObligation(b *box, c *claim, o obligation) { |
| w.violate("INV-22: remote chore %s (%s %s) is about to run with no persisted park scope", o.ID, o.Kind, o.Prefix) |
| } |
| var keep func(string) bool |
| + if member != nil && on("scope-membership") { |
| + keep = func(k string) bool { return !member(k) } // confined to the scope |
| + } |
| if o.Kind == "park-sweep" { |
| - keep = func(k string) bool { return !w.sweepable(w.claim, b.Region, k) } |
| + inner := keep |
| + keep = func(k string) bool { return !w.sweepable(w.claim, b.Region, k) || inner != nil && inner(k) } |
| quiet = 0 |
| if o.Scope != nil && on("quiet-before-ack") { |
| // the sweep's scope (claim rev 6.23 §6.2a): a park-sweep is a |
| @@ -2263,7 +2305,8 @@ func (w *world) doObligation(b *box, c *claim, o obligation) { |
| if retire == "@root" { |
| retire = "" // the origin generation's sentinel (claim rev 6.10) |
| } |
| - keep = func(k string) bool { return genOf(o.Prefix, k) != retire } |
| + inner := keep |
| + keep = func(k string) bool { return genOf(o.Prefix, k) != retire || inner != nil && inner(k) } |
| } |
| if !w.parkStep(b, o.Prefix, o.Dest(), quiet, keep) { |
| return |
| @@ -2322,6 +2365,11 @@ func (w *world) doObligation(b *box, c *claim, o obligation) { |
| func (o obligation) Dest() string { |
| if o.Kind == "park-sweep" { |
| + if o.Scope != nil { |
| + // the archive names the scope's incarnation (claim rev 6.24 §2; |
| + // R16-2: rev 7.16's destination ignored it) |
| + return fmt.Sprintf("parked/sweep/%s/%d/%s/", host, o.Scope.Inc, o.ID) |
| + } |
| return fmt.Sprintf("parked/sweep/%s/%s/", host, o.ID) |
| } |
| if o.Kind == "park-replica" { |
| @@ -2351,6 +2399,48 @@ func (w *world) scoped(o obligation, evidenceAt, inc int) obligation { |
| // scopeLocation is the scope grammar's form of a park prefix. |
| func scopeLocation(prefix string) string { return strings.TrimSuffix(prefix, "/") } |
| +// scopeOf is the scope location a key belongs to (claim rev 6.24 §2): a |
| +// staging key's is moves/<host> (or its own lane, moves/<host>/<op id>, |
| +// which inScope tests by prefix); an instance key's is its incarnation |
| +// location, or the legacy instances/<host> for a level directory or |
| +// generation directly under the host prefix. A child incarnation never |
| +// belongs to the legacy scope, and nothing under moves/ belongs to an |
| +// instances scope. |
| +func scopeOf(k string) string { |
| + if strings.HasPrefix(k, "moves/"+host+"/") { |
| + return "moves/" + host |
| + } |
| + return scopeLocation(locationOf(k)) |
| +} |
| + |
| +// inScope: key k is within the scope location loc. |
| +func inScope(k, loc string) bool { |
| + if strings.HasPrefix(loc, "moves/"+host+"/") { |
| + return strings.HasPrefix(k, loc+"/") // one staging lane |
| + } |
| + return scopeOf(k) == loc |
| +} |
| + |
| +// incOf is the archive incarnation of a scope location (claim rev 6.24 |
| +// §2): an incarnation location's own; for the legacy location or the |
| +// staging sweep, the holder's incarnation, else the newest retired. |
| +func incOf(c *claim, loc string) int { |
| + if strings.HasPrefix(loc, "instances/"+host+"/") { |
| + n := 0 |
| + fmt.Sscanf(strings.TrimPrefix(loc, "instances/"+host+"/"), "%d", &n) |
| + if n > 0 { |
| + return n |
| + } |
| + } |
| + if c.Holder != nil { |
| + return c.Holder.Inc |
| + } |
| + if len(c.Retired) > 0 { |
| + return c.Retired[len(c.Retired)-1] |
| + } |
| + return 0 |
| +} |
| + |
| // scopeLocationRe is claim rev 6.23's grammar for a scope's location |
| // (the model's incarnation ids are decimal, the claim's 64 hex): exactly |
| // instances/<host>, instances/<host>/<incarnation>, moves/<host>/<op id> |
diff --git a/internal/sim/hostlife/rules_test.go b/internal/sim/hostlife/rules_test.go| index c84baa823..3efd01d9d 100644 |
| --- a/internal/sim/hostlife/rules_test.go |
| +++ b/internal/sim/hostlife/rules_test.go |
| @@ -130,6 +130,7 @@ var allRules = []string{ |
| "covered-baseline-refused", // claim rev 6.22 §6.2a: walking an unfinished run, a covered foreign link is passed over and a covered local generation reached as a needed baseline refuses the start (R13-1) |
| "restore-selected-baseline", // rev 7.15 §5.1: the start restores the generation the run walk selected, rooted at [1, 1], as the oracle does; not the marker's alone (R14-1) |
| "unique-declarations", // claim rev 6.22 item 2: writes_lost plus additional_writes_lost, unique by (box, session); the source's cut session joins the list and is never declared twice (R14-2) |
| + "scope-membership", // claim rev 6.24 §2: a park executes strictly within its scope's namespace; the legacy instances/<host> scope excludes child incarnations and an instances scope never touches moves/ (R16-1, R16-2) |
| "lost-return-park", // rev 7 §7.10 (model 27): declare-lost parks a return lane the lost target had begun (rev 7.2: a biased schedule stops the target mid-return) |
| "target-park", // R2-5/INV-10 |
| "abort-target-owner", // J-N13 |
diff --git a/internal/sim/hostlife/sim_test.go b/internal/sim/hostlife/sim_test.go| index c405e0cac..1cac18606 100644 |
| --- a/internal/sim/hostlife/sim_test.go |
| +++ b/internal/sim/hostlife/sim_test.go |
| @@ -88,7 +88,7 @@ func (w *world) legacyStart() { |
| b.DB = &localDB{Inc: inc, Loc: locationFor(inc, true), Key: key, State: map[string]int{}, Epoch: b.Epoch} |
| for i := 0; i < 3; i++ { |
| w.nextW++ |
| - w.acks = append(w.acks, ack{W: w.nextW, Inc: inc, Box: b.ID, Session: 1, Gen: "", At: 0, Kind: "write"}) // the pre-release writer: adoption's session 1 |
| + w.acks = append(w.acks, ack{W: w.nextW, Inc: inc, Box: b.ID, Session: 0, Gen: "", At: 0, Kind: "write"}) // the pre-release writer: the legacy identity, session 0 (claim rev 6.24) |
| w.writeInc[w.nextW] = inc |
| w.commit(b.DB, w.nextW) |
| } |
| @@ -107,8 +107,8 @@ func (w *world) legacyStart() { |
| other := (r + 1 + w.rng.Intn(nRegions-1)) % nRegions |
| w.buckets[other].objs[ltxKey(b.DB.Loc, "", 0, 1, 1)] = []*version{{ID: w.newVer(), B: part}} |
| if w.rng.Intn(2) == 0 { |
| - // the pre-release processes: adoption's session 1, the origin generation (rev 7.13; seed 44450 / 100,000 acknowledged under no session) |
| - b.Procs = []*proc{{Main: true, Strict: false, Inc: inc, Session: 1, Box: b.ID}, {Main: false, Strict: false, Inc: inc, Session: 1, Box: b.ID}} |
| + // the pre-release processes: the legacy identity, session 0 in the origin generation (claim rev 6.24; rev 7.13's seed 44450 found them acknowledging under no identity at all) |
| + b.Procs = []*proc{{Main: true, Strict: false, Inc: inc, Session: 0, Box: b.ID}, {Main: false, Strict: false, Inc: inc, Session: 0, Box: b.ID}} |
| } |
| if w.rng.Intn(2) == 0 { |
| // that earlier move also left the old box's local state behind: |
diff --git a/internal/sim/hostlife/witness_test.go b/internal/sim/hostlife/witness_test.go| index b6773cbae..3ff197598 100644 |
| --- a/internal/sim/hostlife/witness_test.go |
| +++ b/internal/sim/hostlife/witness_test.go |
| @@ -169,6 +169,8 @@ var witnesses = []witness{ |
| "a committed move's source-region park binds its scope, the original evidence time, in the claim; the region's agent restarts mid-park; with the box-local evidence map (rev 7.13) the horizon starts again from the restart and the acknowledgement comes late (claim rev 6.15 §2, R13-4)", wParkScopeSurvivesRestart}, |
| {"persisted-park-scope", "persisted-park-scope", "INV-9", |
| "a committed move's staging lane sealed at the cut: its persisted bound is the seal's, deadline seal + lease + H; the target region's cleanup first runs 40 steps after that deadline and its agent restarts as it begins; the acknowledgement must follow at once, since the persisted deadline has passed; bound at cleanup's own clock (rev 7.15) the chore waits a fresh horizon (claim rev 6.23 §2, R15-1)", wStagingScopeDeadline}, |
| + {"scope-membership", "scope-membership", "INV-23", |
| + "incarnation 2 serves after incarnation 1 was deleted; a late object lands under instances/<host>/1/g-old/; the sweep must queue a chore scoped to instances/<host>/1 with archive incarnation 1 and park within it; rev 7.16's sweep scoped the whole prefix as instances/<host> under incarnation 2 and archived the child incarnation's object from there (claim rev 6.24 §2, R16-2)", wSweepScopeMembership}, |
| {"holderless-park", "holderless-park", "INV-20", |
| "a deleted host's region keeps late residue; the free host's sweep runs as a holderless parking op and a create requested meanwhile waits for FreeAfterPark; with bare chores on the free claim (rev 7.13) the create claims the host over the outstanding park (claim rev 6.15 §6.2a, R13-4)", wFreeSweepVsCreate}, |
| {"covered-baseline-refused", "covered-baseline-refused", "INV-2", |
| @@ -416,11 +418,11 @@ func (w *world) legacy(b *box, other int) { |
| b.DB = &localDB{Inc: inc, Loc: locationFor(inc, true), Key: key, State: map[string]int{}, Epoch: b.Epoch} |
| for i := 0; i < 2; i++ { |
| w.nextW++ |
| - w.acks = append(w.acks, ack{W: w.nextW, Inc: inc, Box: b.ID, Session: 1, At: w.now, Kind: "write"}) // the pre-release writer: adoption's session 1 |
| + w.acks = append(w.acks, ack{W: w.nextW, Inc: inc, Box: b.ID, Session: 0, At: w.now, Kind: "write"}) // the pre-release writer: the legacy identity, session 0 (claim rev 6.24) |
| w.writeInc[w.nextW] = inc |
| w.commit(b.DB, w.nextW) |
| } |
| - b.DB.Session = 1 |
| + b.DB.Session = 0 |
| b.Files = &filesDir{Inc: inc, Key: key, Env: 1, Done: true} |
| b.Config, b.CfgVer, b.Live, b.LiveInc = inc, 1, app0, inc |
| full := w.deltaOf(b.DB, 0) |
| @@ -428,9 +430,11 @@ func (w *world) legacy(b *box, other int) { |
| k := ltxKey(b.DB.Loc, "", 0, 1, 1) |
| w.buckets[b.Region].objs[k] = []*version{{ID: w.newVer(), B: full}} |
| w.markDurable(k, full) |
| - // the pre-release writer closed cleanly on this box; adoption's stamp |
| - // and session are 1 |
| - w.buckets[b.Region].objs[closedKey(b.DB.Loc, "", 1)] = []*version{{ID: w.newVer(), B: &blob{Kind: "closed", Inc: inc, Stamp: 1, Seq: b.ID, Session: 1, TX: 1}}} |
| + // the pre-release writer closed cleanly on this box (a fixture for a |
| + // warm first wake; the real pre-release writer leaves no certificate, |
| + // so a real first wake is cold); adoption's stamp is 1 and the legacy |
| + // identity's session 0 (claim rev 6.24) |
| + w.buckets[b.Region].objs[closedKey(b.DB.Loc, "", 0)] = []*version{{ID: w.newVer(), B: &blob{Kind: "closed", Inc: inc, Stamp: 1, Seq: b.ID, Session: 0, TX: 1}}} |
| first := w.txs[b.DB.Log[0]] |
| part := &blob{Kind: "ltx", Level: 0, Min: 1, Max: 1, Inc: 0, SealKey: key, Pages: map[string]int{first.Key: first.Val}, TXs: []int{first.W}} |
| w.buckets[other].objs[ltxKey(b.DB.Loc, "", 0, 1, 1)] = []*version{{ID: w.newVer(), B: part}} |
| @@ -2271,7 +2275,7 @@ func wAnchorRetry(t *testing.T, w *world) { |
| k := snapKey(loc, "", 2) |
| w.buckets[b.Region].objs[k] = append(w.buckets[b.Region].objs[k], &version{ID: w.newVer(), B: snap}) |
| w.markDurable(k, snap) |
| - w.buckets[b.Region].objs[closedKey(loc, "", 1)][0].B.TX = 2 // the certificate names the snapshot's position |
| + w.buckets[b.Region].objs[closedKey(loc, "", w.claim.Holder.Session)][0].B.TX = 2 // the certificate names the snapshot's position (the serving fixture's session, not the legacy identity) |
| var original *request |
| w.hold = func(r *request) bool { |
| if r.kind == rPut && r.b != nil && r.b.Level == 0 && r.b.Min == 2 && r.b.Max == 2 && original == nil { |
| @@ -2397,7 +2401,7 @@ func wOriginSwept(t *testing.T, w *world) { |
| } |
| // the pre-release writer left no certificate (the helper's is for a |
| // warm first wake): the first wake is cold, from the origin |
| - delete(w.buckets[b0.Region].objs, closedKey(w.claim.Holder.Location, "", 1)) |
| + delete(w.buckets[b0.Region].objs, closedKey(w.claim.Holder.Location, "", 0)) |
| armed := true |
| w.startHook = func(x *box) bool { |
| if x != b0 || !armed { |
| @@ -2552,6 +2556,181 @@ func wStagingScopeDeadline(t *testing.T, w *world) { |
| w.finish(t) |
| } |
| +// ---------- rev 7.17 ---------- |
| + |
| +// recreated drives a delete of the serving host and a create of the next |
| +// incarnation in region r, and returns once it serves. |
| +func (w *world) recreated(t *testing.T, r int) { |
| + w.userDelete() |
| + w.reach(t, 800, "host deleted and free", func() bool { |
| + c := w.claim |
| + return c != nil && c.Holder == nil && c.Op.Kind == "" && len(c.Obl) == 0 && w.rec == nil |
| + }, w.actAll(), w.runConsole, w.recoveryPass) |
| + if len(w.violations) > 0 { |
| + return |
| + } |
| + w.nextInc++ |
| + w.console = append(w.console, &consolePlan{Kind: "create", Host: "h", App: app0, OpID: w.newID("cr"), Inc: w.nextInc, Region: r}) |
| + w.reach(t, 800, "the next incarnation serves", func() bool { |
| + c := w.claim |
| + return len(w.violations) > 0 || c != nil && c.Holder != nil && c.Op.Kind == "serving" && c.Holder.Inc == w.nextInc |
| + }, w.actAll(), w.runConsole, w.recoveryPass) |
| +} |
| + |
| +// wSweepScopeMembership (claim rev 6.24 §2, R16-2): the serving |
| +// incarnation's sweep finds a late object of a deleted incarnation; the |
| +// chore that parks it is scoped to that incarnation's own location and |
| +// archives under its incarnation, never under the serving one's legacy |
| +// scope. |
| +func wSweepScopeMembership(t *testing.T, w *world) { |
| + b0 := w.boxes[0] |
| + w.serve(b0, 1, app0) |
| + w.wake(b0) |
| + w.appWrite(b0) |
| + w.recreated(t, b0.Region) |
| + if len(w.violations) > 0 { |
| + return |
| + } |
| + if w.claim.Holder.Inc != 2 { |
| + t.Fatalf("witness: incarnation %d serves, want 2: %s", w.claim.Holder.Inc, w.state()) |
| + } |
| + // a late object of incarnation 1 lands under its own location |
| + old := locationFor(1, false) |
| + k := ltxKey(old, "old", 0, 3, 3) |
| + w.buckets[b0.Region].objs[k] = append(w.buckets[b0.Region].objs[k], &version{ID: w.newVer(), B: &blob{Kind: "ltx", Level: 0, Min: 3, Max: 3, Inc: 1, Pages: map[string]int{}}}) |
| + var scope *parkScope |
| + w.reach(t, 600, "the late object parked", func() bool { |
| + for _, o := range w.claim.Obl { |
| + if o.Kind == "park-sweep" && o.Region == b0.Region && o.Scope != nil && strings.HasPrefix(k, o.Prefix) { |
| + cp := *o.Scope |
| + scope = &cp |
| + } |
| + } |
| + return len(w.violations) > 0 || w.buckets[b0.Region].current(k) == nil |
| + }, w.actAll(), w.recoveryPass) |
| + if len(w.violations) > 0 { |
| + return |
| + } |
| + if scope == nil { |
| + t.Fatalf("witness: no scoped sweep chore covered %s: %s", k, w.state()) |
| + } |
| + if scope.Location != scopeLocation(old) || scope.Inc != 1 { |
| + w.violate("INV-23 (witness): the sweep parked %s under scope %s (incarnation %d); the object's own location is %s, incarnation 1", k, scope.Location, scope.Inc, scopeLocation(old)) |
| + return |
| + } |
| + w.finish(t) |
| +} |
| + |
| +// TestLegacyLostTargetReturn (claim rev 6.24, R16-3) is the legacy |
| +// identity through a lost-target return: an adopted host whose pre-claim |
| +// writer (session 0, generation "") left a write its replica never got; |
| +// no wake before the move, so the cut session is 0 and src_covered is |
| +// false; the target is admitted cold and declared lost; the source's |
| +// return declares the target's session and the source's cut session 0, in |
| +// additional_writes_lost, and INV-24 accepts the legacy identity. |
| +func TestLegacyLostTargetReturn(t *testing.T) { |
| + w := newWitness() |
| + defer func() { |
| + if t.Failed() { |
| + dump(t, w) |
| + } |
| + }() |
| + b0, b1 := w.boxes[0], w.boxes[1] |
| + w.legacy(b0, 1) |
| + w.tick(func() { w.reconcile(b0) }) // adoption |
| + if w.claim == nil || w.claim.Holder.Session != 0 { |
| + t.Fatalf("not adopted with the legacy identity: %s", w.state()) |
| + } |
| + w.reach(t, 400, "adoption settled", func() bool { return w.claim.oblFor("adopt") == 0 }, w.actAll(), w.recoveryPass) |
| + // the pre-claim writer's last write, acknowledged, never uploaded: the |
| + // origin's level-0 uploads are held, so the cut's flush cannot land it |
| + loc := w.claim.Holder.Location |
| + w.hold = func(r *request) bool { |
| + return r.kind == rPut && r.region == b0.Region && r.b != nil && r.b.Level == 0 && genOf(loc, r.key) == "" |
| + } |
| + w.nextW++ |
| + w.commit(b0.DB, w.nextW) |
| + w.acks = append(w.acks, ack{W: w.nextW, Inc: 1, Box: b0.ID, Session: 0, Gen: "", At: w.now, Kind: "write"}) |
| + w.writeInc[w.nextW] = 1 |
| + w.moveTo(b1.Region) |
| + w.reach(t, 600, "landing probed", func() bool { |
| + c := w.claim |
| + return len(w.violations) > 0 || c.Op.Kind == "landing" && c.Op.LandPhase == "probed" && hasMain(b1) |
| + }, w.act(b0, b1), w.recoveryPass) |
| + if len(w.violations) > 0 { |
| + t.Fatalf("%s", w.violations[0]) |
| + } |
| + if w.claim.Op.SrcCovered || w.claim.Op.CutSession != 0 { |
| + t.Fatalf("the cut must be session 0 with src_covered false: covered=%v cut=%d", w.claim.Op.SrcCovered, w.claim.Op.CutSession) |
| + } |
| + tgtSession := lastAdmission(w.claim.Holder).Session |
| + w.stop(b1) |
| + w.reach(t, 400, "declared lost", func() bool { return contains(w.claim.Lost, b1.ID) }, w.act(b0), w.recoveryPass, w.operator) |
| + w.replaceDestroyed() |
| + w.reach(t, 800, "the source's return admitted", func() bool { |
| + c := w.claim |
| + l := lastAdmission(c.Holder) |
| + return len(w.violations) > 0 || c.Op.Kind == "serving" || c.Op.Kind == "restoring" && l != nil && l.Box == b0.ID && l.Session > tgtSession |
| + }, w.act(b0), w.recoveryPass, w.runConsole, w.operator) |
| + w.hold = nil |
| + w.completeHeld(dataKey(loc, "", "")) |
| + if len(w.violations) > 0 { |
| + t.Fatalf("%s", w.violations[0]) |
| + } |
| + e := lastAdmission(w.claim.Holder) |
| + seen := map[[2]int]int{} |
| + for _, x := range declarationsOf(e) { |
| + seen[[2]int{x.Box, x.Session}]++ |
| + } |
| + if seen[[2]int{b1.ID, tgtSession}] != 1 || seen[[2]int{b0.ID, 0}] != 1 { |
| + t.Fatalf("the return must declare the target's session %d and the source's cut session 0 once each: %v (record %+v)", tgtSession, seen, *e) |
| + } |
| + t.Logf("declared %v at %s; legacy declarations %d", seen, loc, w.stats["writes_lost: the legacy identity (session 0)"]) |
| + w.finish(t) |
| + if len(w.violations) > 0 { |
| + t.Fatalf("%s", w.violations[0]) |
| + } |
| +} |
| + |
| +// TestStagingSurvivesLegacyPark (claim rev 6.24 §2, R16-1): a legacy host's |
| +// earlier stay in the target region is parked by the landing's install |
| +// phase while the move's sealed staging sits beside it under moves/; the |
| +// park is scoped to the legacy instance location and the staging survives |
| +// for the build. |
| +func TestStagingSurvivesLegacyPark(t *testing.T) { |
| + w := newWitness() |
| + defer func() { |
| + if t.Failed() { |
| + dump(t, w) |
| + } |
| + }() |
| + b0, b1 := w.boxes[0], w.boxes[1] |
| + w.legacy(b0, 1) // the fixture leaves an earlier stay's replica part in region 1 |
| + w.tick(func() { w.reconcile(b0) }) |
| + w.reach(t, 400, "adoption settled", func() bool { return w.claim.oblFor("adopt") == 0 }, w.actAll(), w.recoveryPass) |
| + w.recovered(t, b0, "running after adoption") |
| + w.appWrite(b0) |
| + w.moveTo(b1.Region) |
| + w.reach(t, 600, "landing probed", func() bool { |
| + c := w.claim |
| + return len(w.violations) > 0 || c.Op.Kind == "landing" && c.Op.LandPhase == "probed" && hasMain(b1) |
| + }, w.act(b0, b1), w.recoveryPass) |
| + if len(w.violations) > 0 { |
| + t.Fatalf("%s", w.violations[0]) |
| + } |
| + op := w.claim.Op |
| + for _, r := range []ref{op.SealDB, op.SealFiles} { |
| + if w.buckets[r.Region].byID(r.Key, r.Ver) == nil || w.buckets[r.Region].current(r.Key) == nil { |
| + t.Fatalf("the sealed staging %s@%d is gone from region %d after the install park", r.Key, r.Ver, r.Region) |
| + } |
| + } |
| + t.Logf("staging %s and %s survived the legacy instance park; landing probed", op.SealDB.Key, op.SealFiles.Key) |
| + w.finish(t) |
| + if len(w.violations) > 0 { |
| + t.Fatalf("%s", w.violations[0]) |
| + } |
| +} |
| + |
| // wFreeSweepVsCreate (claim rev 6.15 §6.2a, R13-4): a deleted host's |
| // region keeps late residue; the free host's sweep runs as a holderless |
| // parking op, and a create requested meanwhile waits for FreeAfterPark. |