amadan
hostlife model: rev 7.15, joint round 14
R14-1: the start restores the generation the run walk selected as the oracle does: openState.SourcePin carries the restore mode (the marker's generation through generation.json, or a run generation rooted at [1, 1]); rule restore-selected-baseline, witness wIntermediateBaseline (R's first upload pending at its crash, an empty R2, R's upload landing). R14-2: one writes_lost plus additional_writes_lost, unique by (box, session): the source's cut session joins the list under its persisted identity (op.CutSession) and LostSrc is gone; one alert per declaration; INV-21 in admitCommit; rule unique-declarations, witnesses wNoDuplicateDeclarationEarly (the target destroyed before its first admission) and wNoDuplicateDeclarationLate (after its probe). R14-3: the park scope persists the request bound (RequestLimit), and the horizon after the evidence is sigAgeH + RequestLimit = horizonH; the sweep acknowledges only after its listing later than evidence_at + H. R14-4: a running holderless sweep admits another region's chores; TestJoinHolderlessSweep. R14-5: park-generation chores carry their scope from the publication, staging parks bind one before their first step (keeping the seal's quiet time); INV-22, no remote chore runs unscoped. Fidelity: the publication's precondition is that any entry names the generation (as E reads it); trimming is E's front-only rule over more than eight entries. Rules: 106. Witnesses: 71.
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
5 files changed,
+432
−118
internal/sim/hostlife/moves_test.go+5 −3internal/sim/hostlife/protocol_test.go+121 −62internal/sim/hostlife/rules_test.go+35 −33internal/sim/hostlife/witness_test.go+246 −0internal/sim/hostlife/world_test.go+25 −20
diff --git a/internal/sim/hostlife/moves_test.go b/internal/sim/hostlife/moves_test.go| index 5217749d1..754779310 100644 |
| --- a/internal/sim/hostlife/moves_test.go |
| +++ b/internal/sim/hostlife/moves_test.go |
| @@ -1656,8 +1656,9 @@ func sameStep(a, b *claim) bool { |
| // retirement event, under a park-sweep obligation it owns. The claim's |
| // wording leaves out `moves/<host>/`; `sweep-staging` (CC20) adds it. |
| func (w *world) sweep(b *box, c *claim) { |
| - if !on("straggler-sweep") || c == nil || !(c.Op.Kind == "" || c.Op.Kind == "serving") { |
| - return |
| + holderless := c != nil && c.Holder == nil && c.Op.Kind == "parking" && c.Op.ParkSweep != "" |
| + if !on("straggler-sweep") || c == nil || !(c.Op.Kind == "" || c.Op.Kind == "serving" || holderless) { |
| + return // a running holderless sweep admits another region's chores (R14-4); any other operation suppresses sweeps |
| } |
| for _, o := range c.Obl { |
| if o.Kind == "park-sweep" && o.Region == b.Region { |
| @@ -1697,6 +1698,7 @@ func (w *world) sweep(b *box, c *claim) { |
| op = fmt.Sprintf("session:%d", n.Holder.Session) |
| case joining: |
| op = n.Op.ID |
| + w.stats["sweep joined a running holderless op"]++ |
| case on("holderless-park"): |
| n.Op = opState{Kind: "parking", ID: w.newID("park"), ParkSweep: "v1", Exec: -1, ReqAt: w.now} |
| op = n.Op.ID |
| @@ -1710,7 +1712,7 @@ func (w *world) sweep(b *box, c *claim) { |
| // the scope is persisted at the queuing CAS (claim rev 6.15 §2): |
| // the sweeping box's complete listing is the evidence, taken now |
| n.Obl = append(n.Obl, obligation{ID: w.newID("ob"), Op: op, Kind: "park-sweep", Region: b.Region, Box: -1, Prefix: p, Ret: "sweep", |
| - Scope: &parkScope{Location: p, Inc: inc, EvidenceAt: w.now, Limit: horizonH}}) |
| + Scope: &parkScope{Location: p, Inc: inc, EvidenceAt: w.now, RequestLimit: requestLimitH}}) |
| } |
| // 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 d8b6969d4..1d5127371 100644 |
| --- a/internal/sim/hostlife/protocol_test.go |
| +++ b/internal/sim/hostlife/protocol_test.go |
| @@ -437,6 +437,7 @@ func (w *world) spawn(b *box, c *claim, want string, probe bool) bool { |
| // abandoned fresh one, left to the sweep, and the baseline is the |
| // generation the marker names, its parent, which holds the data |
| source := h.Gen |
| + pin := -1 // the marker's generation, through generation.json |
| prepared := adm.Mode == "cold" && adm.NewGeneration == want && want != h.Gen |
| if prepared { |
| // a cold admission into the operation's prepared generation: the |
| @@ -501,6 +502,14 @@ func (w *world) spawn(b *box, c *claim, want string, probe bool) bool { |
| return false |
| } |
| source = src |
| + if src != bg && on("restore-selected-baseline") { |
| + // a generation of the run that holds an object, selected |
| + // while the marker still names the run's baseline: restored |
| + // as the oracle restores it, rooted at [1, 1], never through |
| + // the marker (R14-1: rev 7.14 selected it and then refused it) |
| + pin = 0 |
| + w.stats["restore: run generation rooted"]++ |
| + } |
| _ = chain |
| w.stats["abandoned empty generation skipped"]++ |
| } else if !w.republishMarker(b, loc, h.Gen) { |
| @@ -544,7 +553,7 @@ func (w *world) spawn(b *box, c *claim, want string, probe bool) bool { |
| return false |
| } |
| nh := w.claim.Holder |
| - o := &openState{Gen: nh.Gen, Want: want, Session: nh.Session, Mode: adm.Mode, Prepared: prepared, Probe: probe, Source: source, RemoteMax: adm.RemoteMaxTXID, stage: "restore"} |
| + o := &openState{Gen: nh.Gen, Want: want, Session: nh.Session, Mode: adm.Mode, Prepared: prepared, Probe: probe, Source: source, SourcePin: pin, RemoteMax: adm.RemoteMaxTXID, stage: "restore"} |
| b.open = o |
| return w.resumeOpen(b, c, o) |
| } |
| @@ -661,7 +670,10 @@ func (w *world) resumeOpen(b *box, c *claim, o *openState) bool { |
| case o.Prepared: |
| db = w.restorePinned(b.Region, h.Inc, loc, o.Gen, cur.Op.BaseKey, cur.Op.BaseVer, cur.Op.BaseTX) |
| default: |
| - db = w.restoreCalc(b.Region, h.Inc, loc, o.Source) |
| + // the same selection semantics as the oracle's restoreAsNext |
| + // (R14-1): the marker's generation through generation.json, or |
| + // a run generation the walk selected, rooted at [1, 1] |
| + db = w.restoreWith(b.Region, h.Inc, loc, o.Source, "", 0, o.SourcePin) |
| if db != nil && o.Mode == "warm" && db.Pos < o.RemoteMax { |
| w.alert("box %d: the restore of %q reached position %d, the certificate says %d; the remote is incomplete", b.ID, o.Source, db.Pos, o.RemoteMax) |
| db = nil |
| @@ -964,8 +976,14 @@ func (w *world) publishGeneration(b *box, c *claim, observedOpID, observedPhase |
| if n.Holder == nil || n.Holder.Session != session || n.Holder.Gen != published { |
| return false |
| } |
| - if l := lastAdmission(n.Holder); l == nil || l.Gen != published { |
| - return false // an entry must name the published generation (claim rev 6.22 item 5) |
| + named := false |
| + for _, e := range n.Holder.Admissions { |
| + if e.Gen == published { |
| + named = true |
| + } |
| + } |
| + if !named { |
| + return false // an entry must name the published generation (claim rev 6.22 item 5; any entry, as E reads it) |
| } |
| if n.Op.ID != observedOpID || phaseOf(&n.Op) != observedPhase { |
| return false // bound to the operation and phase it observed |
| @@ -1034,17 +1052,16 @@ func (w *world) publishGeneration(b *box, c *claim, observedOpID, observedPhase |
| if hasObl(n.Obl, oid) { |
| oid = fmt.Sprintf("%s-%s", newID, ret) // one caller id, one chore per dead generation |
| } |
| - n.Obl = append(n.Obl, obligation{ID: oid, Op: id, Kind: "park-generation", Region: chore, Box: -1, Prefix: n.Holder.Location, Ret: ret, Quiet: w.now + horizonH}) |
| + // the chore's scope (claim rev 6.15 §2, R14-5): the publication is |
| + // the evidence that the predecessor is dead, taken now |
| + n.Obl = append(n.Obl, obligation{ID: oid, Op: id, Kind: "park-generation", Region: chore, Box: -1, Prefix: n.Holder.Location, Ret: ret, Quiet: w.now + horizonH, |
| + Scope: &parkScope{Location: n.Holder.Location, Inc: n.Holder.Inc, EvidenceAt: w.now, RequestLimit: requestLimitH}}) |
| } |
| - covered := 0 |
| - for _, e := range n.Holder.Admissions { |
| - if e.Covered { |
| - covered++ |
| - } |
| - } |
| - for covered > 8 && len(n.Holder.Admissions) > 1 && n.Holder.Admissions[0].Covered { |
| + // retention is E's (claim rev 6.14 item 8, R12-6): covered entries |
| + // are dropped from the front only while more than eight entries |
| + // remain; an uncovered head stops the trimming |
| + for len(n.Holder.Admissions) > 8 && n.Holder.Admissions[0].Covered { |
| n.Holder.Admissions = n.Holder.Admissions[1:] |
| - covered-- |
| } |
| return true |
| }) |
| @@ -1702,7 +1719,7 @@ func (w *world) admitCommit(b *box, c *claim, a admitInput) bool { |
| return true |
| } |
| h := c.Holder |
| - var lost, lostSrc *writesLost |
| + var lost *writesLost |
| var lostTgt []*writesLost |
| var last *admissionRecord // the last admitted writer before this CAS, the predecessor's identity (claim rev 6.12, R11-4) |
| var entry admissionRecord |
| @@ -1793,34 +1810,45 @@ func (w *world) admitCommit(b *box, c *claim, a admitInput) bool { |
| e.Lost = lost |
| } |
| if n.Op.Kind == "restoring" && n.Op.LostAt != 0 && b.ID == n.Op.Src && on("writes-lost") { |
| - // every session the lost target was admitted into since the |
| - // cut is declared (rev 7.13; seed 33373 / 100,000): a probe |
| - // session that certified and a warm continuation that did |
| - // not are two sessions, the first's writes are durable only in |
| - // the lost target's region, and no return lane carries either |
| - // (§7.10). Rev 7.12's box-wide exemption hid the first behind |
| - // the record for the last |
| + // additional_writes_lost (claim rev 6.22 item 2, R13-3, R14-2): |
| + // beside the ordinary writes_lost for the predecessor, every |
| + // session the lost target was admitted into since the cut (a |
| + // probe session that certified and a warm continuation that |
| + // did not are two; no return lane carries either's writes, |
| + // seed 33373 / 100,000), and the source's cut session when |
| + // src_covered is false (the seal in the lost region was the |
| + // one holder of its writes beyond the replica, §7.10; seeds |
| + // 16395 and 27191 / 30,000). The list and the ordinary record |
| + // are unique by (box, session): a target destroyed before its |
| + // first admission leaves the source's cut session as the |
| + // predecessor itself, declared once (R14-2; rev 7.14 declared |
| + // it twice through a separate field). The mutation of |
| + // unique-declarations is rev 7.14's separate path |
| lostTgt = nil |
| - for _, q := range n.Holder.Admissions { |
| - if q.Box == n.Op.Tgt && q.Session > n.Op.CutSession && (lost == nil || q.Session != lost.Session) { |
| - lostTgt = append(lostTgt, &writesLost{Box: q.Box, Gen: q.Gen, Session: q.Session, RemoteMaxTXID: a.RemoteMaxTXID}) |
| + add := func(x *writesLost) { |
| + if on("unique-declarations") { |
| + if lost != nil && lost.Box == x.Box && lost.Session == x.Session { |
| + return |
| + } |
| + for _, y := range lostTgt { |
| + if y.Box == x.Box && y.Session == x.Session { |
| + return |
| + } |
| + } |
| } |
| + lostTgt = append(lostTgt, x) |
| } |
| - e.AdditionalWritesLost = lostTgt |
| - } |
| - if n.Op.Kind == "restoring" && n.Op.LostAt != 0 && !n.Op.SrcCovered && !n.Op.Dirty && b.ID == n.Op.Src && h.Gen == n.Op.SrcGen && on("writes-lost") { |
| - // the return is clean only because the target was declared |
| - // lost; the seal in its region was the one holder of the |
| - // source's writes beyond its own replica, and no lane brings |
| - // them: the source's cut session is declared too (§7.10) |
| - srcSession := 0 |
| for _, q := range n.Holder.Admissions { |
| - if q.Box == n.Op.Src && q.Gen == n.Op.SrcGen { |
| - srcSession = q.Session |
| + if q.Box == n.Op.Tgt && q.Session > n.Op.CutSession { |
| + add(&writesLost{Box: q.Box, Gen: q.Gen, Session: q.Session, RemoteMaxTXID: a.RemoteMaxTXID}) |
| } |
| } |
| - lostSrc = &writesLost{Box: n.Op.Src, Gen: n.Op.SrcGen, Session: srcSession, RemoteMaxTXID: a.RemoteMaxTXID} |
| - e.LostSrc = lostSrc |
| + if !n.Op.SrcCovered && !n.Op.Dirty && h.Gen == n.Op.SrcGen { |
| + // the persisted cut-session identity, never a search by generation |
| + add(&writesLost{Box: n.Op.Src, Gen: n.Op.SrcGen, Session: n.Op.CutSession, RemoteMaxTXID: a.RemoteMaxTXID}) |
| + w.stats["writes_lost: source cut session behind a lost target"]++ |
| + } |
| + e.AdditionalWritesLost = lostTgt |
| } |
| // no retire chore here: the predecessor is the baseline of an |
| // unfinished admission until generation.json names the new |
| @@ -1831,7 +1859,8 @@ func (w *world) admitCommit(b *box, c *claim, a admitInput) bool { |
| if ret == "" { |
| ret = "@root" |
| } |
| - n.Obl = append(n.Obl, obligation{ID: w.newID("ob"), Op: fmt.Sprintf("session:%d", n.Holder.Session), Kind: "park-generation", Region: b.Region, Box: -1, Prefix: n.Holder.Location, Ret: ret, Quiet: w.now + horizonH}) |
| + n.Obl = append(n.Obl, obligation{ID: w.newID("ob"), Op: fmt.Sprintf("session:%d", n.Holder.Session), Kind: "park-generation", Region: b.Region, Box: -1, Prefix: n.Holder.Location, Ret: ret, Quiet: w.now + horizonH, |
| + Scope: &parkScope{Location: n.Holder.Location, Inc: n.Holder.Inc, EvidenceAt: w.now, RequestLimit: requestLimitH}}) |
| } |
| } |
| n.Holder.Admissions = append(n.Holder.Admissions, e) |
| @@ -1873,20 +1902,31 @@ func (w *world) admitCommit(b *box, c *claim, a admitInput) bool { |
| w.alert("box %d: writes_lost {box %d, generation %q, session %d, remote_max_txid %d}: %d acknowledged writes", b.ID, lost.Box, lost.Gen, lost.Session, lost.RemoteMaxTXID, n) |
| } |
| for _, x := range lostTgt { |
| + // one alert per declaration (claim rev 6.22 item 2) |
| n := w.exemptDeclared(b, x, h, a.NewGeneration, true) |
| w.stats["writes_lost declared"]++ |
| w.stats["writes declared lost"] += n |
| - w.stats["writes_lost: another session of a lost target"]++ |
| + if x.Box == w.claim.Op.Tgt { |
| + w.stats["writes_lost: another session of a lost target"]++ |
| + } |
| w.lostAlert++ |
| - w.alert("box %d: writes_lost {box %d, generation %q, session %d, remote_max_txid %d}: %d acknowledged writes (a session of the lost target since the cut)", b.ID, x.Box, x.Gen, x.Session, x.RemoteMaxTXID, n) |
| + w.alert("box %d: writes_lost {box %d, generation %q, session %d, remote_max_txid %d}: %d acknowledged writes (additional_writes_lost behind the lost target)", b.ID, x.Box, x.Gen, x.Session, x.RemoteMaxTXID, n) |
| } |
| - if lostSrc != nil { |
| - n := w.exemptDeclared(b, lostSrc, h, a.NewGeneration, false) |
| - w.stats["writes_lost declared"]++ |
| - w.stats["writes declared lost"] += n |
| - w.stats["writes_lost: source session behind a lost target"]++ |
| - w.lostAlert++ |
| - w.alert("box %d: writes_lost {box %d, generation %q, session %d, remote_max_txid %d}: %d acknowledged writes (the seal in the lost target's region held them)", b.ID, lostSrc.Box, lostSrc.Gen, lostSrc.Session, lostSrc.RemoteMaxTXID, n) |
| + 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 |
| + seen := map[[2]int]bool{} |
| + all := append([]*writesLost{}, lostTgt...) |
| + if lost != nil { |
| + all = append(all, lost) |
| + } |
| + for _, x := range all { |
| + k := [2]int{x.Box, x.Session} |
| + if seen[k] { |
| + 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 |
| + } |
| } |
| return true |
| } |
| @@ -2127,10 +2167,11 @@ func (w *world) doObligation(b *box, c *claim, o obligation) { |
| } |
| default: |
| quiet := o.Quiet |
| - if o.Kind == "park-replica" || o.Kind == "park-superseded" { |
| + 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 |
| - if c.Op.Exec != b.ID || c.Holder == nil { |
| + // host, when it is not the current executor (a whole-location |
| + // park; a staging park's quiet time is the seal's own) |
| + if (o.Kind == "park-replica" || o.Kind == "park-superseded") && (c.Op.Exec != b.ID || c.Holder == nil) { |
| if !w.evidence(b, o.Op) { |
| return |
| } |
| @@ -2147,7 +2188,7 @@ func (w *world) doObligation(b *box, c *claim, o obligation) { |
| if c.Holder != nil { |
| inc = c.Holder.Inc |
| } |
| - scope := &parkScope{Location: o.Prefix, Inc: inc, EvidenceAt: w.now, Limit: horizonH} |
| + scope := &parkScope{Location: o.Prefix, Inc: inc, EvidenceAt: w.now, RequestLimit: requestLimitH} |
| w.cas(c, func(n *claim) bool { |
| for i := range n.Obl { |
| if n.Obl[i].ID == o.ID && n.Obl[i].Scope == nil { |
| @@ -2166,23 +2207,41 @@ func (w *world) doObligation(b *box, c *claim, o obligation) { |
| if _, ok := b.evidAt[o.ID]; !ok { |
| b.evidAt[o.ID] = w.now |
| } |
| - evidAt, limit := b.evidAt[o.ID], horizonH |
| + // the horizon after the evidence is H, the signature-age |
| + // allowance plus the request bound (R14-3): the scope persists the |
| + // request bound, never the whole horizon |
| + evidAt, horizon := b.evidAt[o.ID], horizonH |
| if o.Scope != nil { |
| - evidAt, limit = o.Scope.EvidenceAt, o.Scope.Limit |
| + evidAt, horizon = o.Scope.EvidenceAt, sigAgeH+o.Scope.RequestLimit |
| } |
| - if on("quiet-before-ack") && evidAt+limit > quiet { |
| - quiet = evidAt + limit |
| + if on("quiet-before-ack") && o.Kind != "park-staging" && evidAt+horizon > quiet { |
| + quiet = evidAt + horizon // a staging park keeps the seal's quiet time (SealQuiet), bound by its own lease |
| } |
| } |
| + if o.Kind == "park-generation" && o.Scope != nil && on("quiet-before-ack") { |
| + // a dead generation's chore under its scope (R14-5): the |
| + // publication's evidence time plus H, never less than the |
| + // queued quiet time |
| + if q := o.Scope.EvidenceAt + sigAgeH + o.Scope.RequestLimit; q > quiet { |
| + quiet = q |
| + } |
| + } |
| + if o.Kind != "park-local" && o.Scope == nil && on("persisted-park-scope") { |
| + // INV-22 (rev 7.15, R14-5): every remote chore runs its steps under |
| + // a persisted scope, bound at its queuing or before its first step |
| + 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 o.Kind == "park-sweep" { |
| keep = func(k string) bool { return !w.sweepable(w.claim, b.Region, k) } |
| quiet = 0 |
| if o.Scope != nil && on("quiet-before-ack") { |
| - // the sweep's scope (claim rev 6.15 §6.2a): parked at once, and |
| - // acknowledged, with its straggler pass, only after the scope's |
| - // evidence time plus the request bound |
| - quiet = o.Scope.EvidenceAt + o.Scope.Limit |
| + // the sweep's scope (claim rev 6.15 §6.2a; platform-1e's answer |
| + // to rev 7.14 note 2): a park-sweep is a retirement event, parked |
| + // at once and acknowledged only after a verification listing |
| + // later than evidence_at + H, H the signature-age allowance plus |
| + // the request bound; the straggler pass is that listing |
| + quiet = o.Scope.EvidenceAt + sigAgeH + o.Scope.RequestLimit |
| } |
| } |
| if o.Kind == "park-generation" { |
| @@ -2198,18 +2257,18 @@ func (w *world) doObligation(b *box, c *claim, o obligation) { |
| return |
| } |
| } |
| - evid, limit := 0, horizonH |
| + evid, horizon := 0, horizonH |
| if b.evidAt != nil { |
| evid = b.evidAt[o.ID] |
| } |
| if o.Scope != nil { |
| - evid, limit = o.Scope.EvidenceAt, o.Scope.Limit |
| + evid, horizon = o.Scope.EvidenceAt, sigAgeH+o.Scope.RequestLimit |
| } |
| w.cas(c, func(n *claim) bool { |
| for i, x := range n.Obl { |
| if x.ID == o.ID { |
| - if (o.Kind == "park-replica" || o.Kind == "park-superseded") && on("quiet-before-ack") && o.Region >= 0 && evid+limit > n.Quiet[o.Region] { |
| - n.Quiet[o.Region] = evid + limit // quiet_after survives free |
| + if (o.Kind == "park-replica" || o.Kind == "park-superseded") && on("quiet-before-ack") && o.Region >= 0 && evid+horizon > n.Quiet[o.Region] { |
| + n.Quiet[o.Region] = evid + horizon // quiet_after survives free |
| } |
| if o.Kind == "park-superseded" && n.Holder != nil && o.Prefix == n.Holder.Location { |
| // INV-17 (rev 7.13, R12-3): the whole location in this region |
diff --git a/internal/sim/hostlife/rules_test.go b/internal/sim/hostlife/rules_test.go| index f0026e033..c84baa823 100644 |
| --- a/internal/sim/hostlife/rules_test.go |
| +++ b/internal/sim/hostlife/rules_test.go |
| @@ -107,37 +107,39 @@ var allRules = []string{ |
| "sweep-namespace", // claim rev 6 §6.2a (R3-4): the sweep discovers locations from the namespace; the mutation reads the capped retired_incarnations |
| "live-set-region", // claim rev 6.5 §6.2a (R4-3): the live set is {authoritative region, location, generation}; the mutation exempts matching keys in every region |
| // moves spec |
| - "seal-by-version", // J-N2: landing copies sealed versions |
| - "staging-quiet", // J-N2: staging retired after its writers' horizon |
| - "commit-before-open", // INV-5 |
| - "hold-op-open", // §5.2 conditional open |
| - "start-check", // INV-4: markers agree |
| - "start-check-claim-gen", // rev 6 §5.1 (R2-8): and name the generation the claim expects |
| - "generation-conditional", // rev 7.1 §5.1 (model 29): generation.json is written If-Match the marker it supersedes |
| - "markers-last", // R2-6 |
| - "revert-journal", // J-N11 |
| - "rollback-journal", // R2-3 |
| - "dirty-return", // INV-2 |
| - "seal-return", // rev 7.11 §7.8: a rollback whose source replica stops short of the stopped database returns the seal |
| - "clean-return-identity", // claim rev 6.12, R11-4: the predecessor is the last admitted writer, and a clean return with src_covered declares nothing |
| - "foreign-region-uncovered", // claim rev 6.14 item 5: a predecessor in another region stays uncovered, never queued into its region from here (R12-3) |
| - "cover-at-park", // claim rev 6.14 item 6: CoverRegionPredecessors inside the CAS that queues a region's whole-location park (R12-3) |
| - "session-scoped-loss", // rev 7.13 §14.2.3: a writes_lost record exempts the writes of the session it names, no other (R12-1) |
| - "probe-window", // rev 7.13 §7.7: a probe attempt's deadline is checked before the start and before readiness is accepted (R12-2) |
| - "absent-marker-origin", // rev 7.12 §6.4: the sweep reads an absent generation.json as the origin (R11-1), isolated from baseline-live |
| - "persisted-park-scope", // claim rev 6.15 §2: a remote chore's park scope is persisted, so a retry after an agent restart keeps the original evidence time (R13-4) |
| - "holderless-park", // claim rev 6.15 §6.2a: a free host's sweep is a holderless parking op that blocks the successor create until FreeAfterPark (R13-4) |
| - "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) |
| - "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 |
| - "timer-freeze", // J-N14 runner bookkeeping |
| - "timer-canonical", // J-N14 prune path |
| - "cut-deadline", // J-N15 |
| - "readiness-key", // T2 |
| - "source-readiness", // S1: the source can run the instance before the cut |
| - "readiness-quiet", // T12: the target region's quiet_after has passed |
| - "files-carried", // §8 (the kpmg outage) |
| - "config-before-probe", // L3 (the kpmg outage) |
| - "recovery-current-inputs", // rev 6 §7.7 (J2-R2-5): a recovery probe is not bound to the move's pinned inputs |
| + "seal-by-version", // J-N2: landing copies sealed versions |
| + "staging-quiet", // J-N2: staging retired after its writers' horizon |
| + "commit-before-open", // INV-5 |
| + "hold-op-open", // §5.2 conditional open |
| + "start-check", // INV-4: markers agree |
| + "start-check-claim-gen", // rev 6 §5.1 (R2-8): and name the generation the claim expects |
| + "generation-conditional", // rev 7.1 §5.1 (model 29): generation.json is written If-Match the marker it supersedes |
| + "markers-last", // R2-6 |
| + "revert-journal", // J-N11 |
| + "rollback-journal", // R2-3 |
| + "dirty-return", // INV-2 |
| + "seal-return", // rev 7.11 §7.8: a rollback whose source replica stops short of the stopped database returns the seal |
| + "clean-return-identity", // claim rev 6.12, R11-4: the predecessor is the last admitted writer, and a clean return with src_covered declares nothing |
| + "foreign-region-uncovered", // claim rev 6.14 item 5: a predecessor in another region stays uncovered, never queued into its region from here (R12-3) |
| + "cover-at-park", // claim rev 6.14 item 6: CoverRegionPredecessors inside the CAS that queues a region's whole-location park (R12-3) |
| + "session-scoped-loss", // rev 7.13 §14.2.3: a writes_lost record exempts the writes of the session it names, no other (R12-1) |
| + "probe-window", // rev 7.13 §7.7: a probe attempt's deadline is checked before the start and before readiness is accepted (R12-2) |
| + "absent-marker-origin", // rev 7.12 §6.4: the sweep reads an absent generation.json as the origin (R11-1), isolated from baseline-live |
| + "persisted-park-scope", // claim rev 6.15 §2: a remote chore's park scope is persisted, so a retry after an agent restart keeps the original evidence time (R13-4) |
| + "holderless-park", // claim rev 6.15 §6.2a: a free host's sweep is a holderless parking op that blocks the successor create until FreeAfterPark (R13-4) |
| + "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) |
| + "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 |
| + "timer-freeze", // J-N14 runner bookkeeping |
| + "timer-canonical", // J-N14 prune path |
| + "cut-deadline", // J-N15 |
| + "readiness-key", // T2 |
| + "source-readiness", // S1: the source can run the instance before the cut |
| + "readiness-quiet", // T12: the target region's quiet_after has passed |
| + "files-carried", // §8 (the kpmg outage) |
| + "config-before-probe", // L3 (the kpmg outage) |
| + "recovery-current-inputs", // rev 6 §7.7 (J2-R2-5): a recovery probe is not bound to the move's pinned inputs |
| } |
diff --git a/internal/sim/hostlife/witness_test.go b/internal/sim/hostlife/witness_test.go| index 142a08091..9bca1789d 100644 |
| --- a/internal/sim/hostlife/witness_test.go |
| +++ b/internal/sim/hostlife/witness_test.go |
| @@ -171,6 +171,12 @@ var witnesses = []witness{ |
| "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", |
| "an unfinished run whose link in this region is covered and whose generation was retired; the walk refuses the start and alerts; reading objects alone (rev 7.13) it passes over the empty link and restores the marker's retired generation as an empty database (claim rev 6.22 §6.2a, R13-1)", wCoveredLocalBaseline}, |
| + {"restore-selected-baseline", "restore-selected-baseline", "INV-3", |
| + "the marker names S; R issues its first upload and crashes while it is pending; an empty successor R2 is admitted and crashes before uploading; R's delayed upload lands; the next start selects R from R2 → R → S and must restore it rooted at [1, 1]; restoring through the marker, which names S, refuses it and the valid recovery stalls (R14-1)", wIntermediateBaseline}, |
| + {"unique-declarations", "unique-declarations", "INV-21", |
| + "the target is destroyed after the flip and before its first admission, src_covered is false and the source's cut session is uncertified; the return's admission must declare that session once; rev 7.14's separate source-cut path declared it twice, through writes_lost and again beside it (R14-2)", wNoDuplicateDeclarationEarly}, |
| + {"unique-declarations", "unique-declarations", "INV-21", |
| + "the same with the target lost after its probe was admitted: the predecessor is the target's probe session, the list carries the source's cut session once and no target session twice (R14-2)", wNoDuplicateDeclarationLate}, |
| {"probe-window", "probe-window", "INV-19", |
| "a landing probe's launch environment is ready exactly at the 30-step deadline; the deadline is checked before the start, so the attempt fails and a fresh admission follows; unchecked, the expired attempt starts, answers readiness and becomes the probed writer (R12-2)", wProbeWindowAt}, |
| {"seal-return", "seal-return", "INV-15", |
| @@ -2592,6 +2598,246 @@ func wCoveredLocalBaseline(t *testing.T, w *world) { |
| } |
| } |
| +// ---------- rev 7.15 ---------- |
| + |
| +// wIntermediateBaseline (R14-1): the run walk selects a generation of the |
| +// run that holds an object while the marker still names the run's |
| +// baseline; the start must restore what the walk selected, rooted at |
| +// [1, 1], as the oracle does. |
| +func wIntermediateBaseline(t *testing.T, w *world) { |
| + b0 := w.boxes[0] |
| + w.serve(b0, 1, app0) |
| + w.wake(b0) |
| + w.appWrite(b0) |
| + w.replicate(b0) |
| + loc := w.claim.Holder.Location |
| + w.idleStop(b0) |
| + w.reach(t, 200, "closed", func() bool { return !hasMain(b0) && (b0.DB == nil || !b0.DB.Closing) }, w.act(b0)) |
| + delete(w.buckets[b0.Region].objs, closedKey(loc, "", w.claim.Holder.Session)) |
| + // R: a cold admission whose first upload is held in flight |
| + w.hold = func(r *request) bool { |
| + g := genOf(loc, r.key) |
| + return r.kind == rPut && r.region == b0.Region && r.b != nil && r.b.Level == 0 && g != "" && g != "-" |
| + } |
| + w.wake(b0) |
| + gR := w.claim.Holder.Gen |
| + if gR == "" { |
| + t.Fatalf("witness: no cold admission R: %s", w.state()) |
| + } |
| + w.reach(t, 30, "R's first upload issued", func() bool { return b0.open != nil && b0.open.req != nil }, w.act(b0)) |
| + w.crash(b0) // R dies with its upload pending; the marker still names S |
| + w.hold = nil |
| + // R2: admitted over the empty R, dies before uploading |
| + armed := true |
| + w.startHook = func(x *box) bool { |
| + if x != b0 || !armed { |
| + return false |
| + } |
| + armed = false |
| + w.crash(x) |
| + return true |
| + } |
| + w.wake(b0) |
| + w.startHook = nil |
| + gR2 := w.claim.Holder.Gen |
| + if gR2 == gR || gR2 == "" { |
| + t.Fatalf("witness: no second cold admission R2: %s", w.state()) |
| + } |
| + // R's delayed upload lands: R holds an object, R2 none, the marker names S |
| + if w.completeHeld(dataKey(loc, gR, "")) == 0 { |
| + t.Fatalf("witness: R's upload was not held: %s", w.state()) |
| + } |
| + // the next start: R2 -> R -> S selects R |
| + if !w.drive(120, func() bool { return hasMain(b0) }, w.act(b0), w.recoveryPass, func() { w.wake(b0) }) { |
| + if len(w.violations) == 0 { |
| + w.violate("INV-3 (witness): the start cannot restore %q, the baseline the run walk selected, while the marker names %q (%d restores refused)", gR, "", w.stats["restore refused"]) |
| + } |
| + return |
| + } |
| + if w.stats["restore: run generation rooted"] == 0 { |
| + t.Fatalf("witness: the start did not restore the selected run generation: %v", w.stats) |
| + } |
| + w.checkLocal(w.claim, b0, b0.DB) |
| + w.checkDurable(w.claim, "after the recovery") |
| + w.finish(t) |
| +} |
| + |
| +// lostTargetReturn is the common opening of the R14-2 witnesses: the |
| +// source's level-0 uploads are held so src_covered is false and its cut |
| +// session is uncertified; the landing proceeds to the given point; the |
| +// target is destroyed and declared lost; the source's return is admitted. |
| +// It returns the source's return record. |
| +func (w *world) lostTargetReturn(t *testing.T, probed bool) *admissionRecord { |
| + src, tgt := w.boxes[0], w.boxes[1] |
| + w.serve(src, 1, app0) |
| + w.wake(src) |
| + loc, gen0 := w.claim.Holder.Location, w.claim.Holder.Gen |
| + w.hold = func(r *request) bool { |
| + return r.kind == rPut && r.region == src.Region && r.b != nil && r.b.Level == 0 && genOf(loc, r.key) == gen0 |
| + } |
| + w.appWrite(src) |
| + w.replicate(src) |
| + w.moveTo(tgt.Region) |
| + if probed { |
| + w.reach(t, 600, "landing probed", func() bool { |
| + c := w.claim |
| + return c.Op.Kind == "landing" && c.Op.LandPhase == "probed" && hasMain(tgt) |
| + }, w.act(src, tgt), w.recoveryPass) |
| + } else { |
| + w.reach(t, 600, "landing built, no admission yet", func() bool { |
| + c := w.claim |
| + return c.Op.Kind == "landing" && (c.Op.LandPhase == "local" || c.Op.LandPhase == "config" || c.Op.LandPhase == "probing") && tgt.open == nil |
| + }, w.act(src, tgt), w.recoveryPass) |
| + } |
| + if len(w.violations) > 0 { |
| + return nil |
| + } |
| + if w.claim.Op.SrcCovered { |
| + t.Fatalf("witness: the seal found the source's replica complete; the held upload was not held: %s", w.state()) |
| + } |
| + w.stop(tgt) // the cloud destroys the target |
| + w.reach(t, 400, "declared lost", func() bool { return contains(w.claim.Lost, tgt.ID) }, w.act(src), w.recoveryPass, w.operator) |
| + w.replaceDestroyed() |
| + w.reach(t, 800, "the source's return admitted", func() bool { |
| + c := w.claim |
| + if len(w.violations) > 0 || c.Op.Kind == "serving" { |
| + return true |
| + } |
| + l := lastAdmission(c.Holder) |
| + return c.Op.Kind == "restoring" && l != nil && l.Box == src.ID && l.Session > c.Op.CutSession |
| + }, w.act(src), w.recoveryPass, w.runConsole, w.operator) |
| + w.hold = nil |
| + w.completeHeld(dataKey(loc, gen0, "")) |
| + if len(w.violations) > 0 { |
| + return nil |
| + } |
| + l := lastAdmission(w.claim.Holder) |
| + if l == nil || l.Box != src.ID { |
| + t.Fatalf("witness: the source's return is not the last admission: %s", w.state()) |
| + } |
| + return l |
| +} |
| + |
| +// declarationsOf is a record's declarations, the ordinary one and the list. |
| +func declarationsOf(e *admissionRecord) []*writesLost { |
| + var out []*writesLost |
| + if e.Lost != nil { |
| + out = append(out, e.Lost) |
| + } |
| + return append(out, e.AdditionalWritesLost...) |
| +} |
| + |
| +// wNoDuplicateDeclarationEarly (R14-2): the target is destroyed before its |
| +// first admission, so the source's cut session is the predecessor itself; |
| +// it is declared once, as writes_lost, and never again in the list. |
| +func wNoDuplicateDeclarationEarly(t *testing.T, w *world) { |
| + e := w.lostTargetReturn(t, false) |
| + if e == nil { |
| + return |
| + } |
| + cut := w.claim.Op.CutSession |
| + n := 0 |
| + for _, x := range declarationsOf(e) { |
| + if x.Box == w.boxes[0].ID && x.Session == cut { |
| + n++ |
| + } |
| + } |
| + if n != 1 && len(w.violations) == 0 { |
| + w.violate("INV-21 (witness): the source's cut session %d was declared %d times by its return admission", cut, n) |
| + return |
| + } |
| + w.finish(t) |
| +} |
| + |
| +// wNoDuplicateDeclarationLate (R14-2): the target was admitted (its probe |
| +// session is the predecessor); the list carries the source's cut session |
| +// once and no target session twice. |
| +func wNoDuplicateDeclarationLate(t *testing.T, w *world) { |
| + e := w.lostTargetReturn(t, true) |
| + if e == nil { |
| + return |
| + } |
| + cut := w.claim.Op.CutSession |
| + seen := map[[2]int]int{} |
| + for _, x := range declarationsOf(e) { |
| + seen[[2]int{x.Box, x.Session}]++ |
| + } |
| + if seen[[2]int{w.boxes[0].ID, cut}] != 1 && len(w.violations) == 0 { |
| + w.violate("INV-21 (witness): the source's cut session %d was declared %d times behind the lost target", cut, seen[[2]int{w.boxes[0].ID, cut}]) |
| + return |
| + } |
| + for k, c := range seen { |
| + if c > 1 && len(w.violations) == 0 { |
| + w.violate("INV-21 (witness): {box %d, session %d} declared %d times", k[0], k[1], c) |
| + return |
| + } |
| + } |
| + if e.Predecessor.Box != w.boxes[1].ID { |
| + t.Fatalf("witness: the predecessor is not the target's probe session: %s", w.state()) |
| + } |
| + w.finish(t) |
| +} |
| + |
| +// TestJoinHolderlessSweep (R14-4) is the positive case of rev 7.14 note 1: |
| +// a deleted host keeps late residue in two regions; the first region's |
| +// sweep starts the holderless parking op and the second region's joins |
| +// it with its own scoped chores under the same op id. |
| +func TestJoinHolderlessSweep(t *testing.T) { |
| + w := newWitness() |
| + defer func() { |
| + if t.Failed() { |
| + dump(t, w) |
| + } |
| + }() |
| + b0 := w.boxes[0] |
| + w.serve(b0, 1, app0) |
| + w.wake(b0) |
| + w.appWrite(b0) |
| + loc := w.claim.Holder.Location |
| + 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 { |
| + t.Fatalf("%s", w.violations[0]) |
| + } |
| + for _, r := range []int{0, 1} { |
| + k := ltxKey(loc, "", 0, 7, 7) |
| + w.buckets[r].objs[k] = append(w.buckets[r].objs[k], &version{ID: w.newVer(), B: &blob{Kind: "ltx", Level: 0, Min: 7, Max: 7, Inc: 1, Pages: map[string]int{}}}) |
| + } |
| + // region 0's box sweeps first, then region 1's joins the running op |
| + joined := false |
| + w.tick(w.act(w.boxes[0])) |
| + if c := w.claim; c.Op.Kind != "parking" || c.Op.ParkSweep == "" { |
| + t.Fatalf("no holderless sweep started: %s", w.state()) |
| + } |
| + id := w.claim.Op.ID |
| + w.tick(w.act(w.boxes[1])) |
| + regions := map[int]bool{} |
| + for _, o := range w.claim.Obl { |
| + if o.Kind == "park-sweep" && o.Op == id { |
| + regions[o.Region] = true |
| + } |
| + } |
| + joined = regions[0] && regions[1] && w.claim.Op.ID == id |
| + if !joined { |
| + t.Fatalf("region 1 did not join op %s: %s", id, w.state()) |
| + } |
| + w.reach(t, 800, "freed after the park", func() bool { c := w.claim; return c != nil && c.Holder == nil && c.Op.Kind == "" && len(c.Obl) == 0 }, w.actAll(), w.recoveryPass) |
| + if len(w.violations) > 0 { |
| + t.Fatalf("%s", w.violations[0]) |
| + } |
| + if w.stats["holderless sweeps"] != 1 || w.stats["sweep joined a running holderless op"] < 1 || w.stats["free after park"] != 1 { |
| + t.Fatalf("one op, one join, one free expected: %v", w.stats) |
| + } |
| + t.Logf("op %s: regions %v joined, freed once", id, regions) |
| + w.finish(t) |
| + if len(w.violations) > 0 { |
| + t.Fatalf("%s", w.violations[0]) |
| + } |
| +} |
| + |
| // TestInterruptedCleanReturn (R13-1) is the positive case of claim rev |
| // 6.22's run walk across regions: a clean rollback's fresh source |
| // admission dies before its first upload, so the run is R -> T -> S with T, |
diff --git a/internal/sim/hostlife/world_test.go b/internal/sim/hostlife/world_test.go| index 77b045435..2f762fe31 100644 |
| --- a/internal/sim/hostlife/world_test.go |
| +++ b/internal/sim/hostlife/world_test.go |
| @@ -40,13 +40,19 @@ const ( |
| app1 = "B" |
| // Time is in model steps. |
| - horizonH = 60 // a request may complete up to H steps after issue |
| - execTTL = 40 // exec lease TTL |
| - execRenew = 15 // renew when this close to expiry |
| - lostMargin = 10 // declare-lost margin past expiry |
| - cutBudget = 320 // absolute cut deadline after admission |
| - stagingTTL = 400 // staging-work lease TTL: longer than the cut budget, as in production |
| - probeTries = 3 |
| + // H, the late-completion horizon (claim §6.2a): a request may complete |
| + // up to H steps after issue. It is the signature-age limit plus the |
| + // request bound, request_limit_ns (claim rev 6.15 §2); the park scope |
| + // persists the request bound and the horizon is computed from it (R14-3) |
| + horizonH = sigAgeH + requestLimitH |
| + sigAgeH = 45 // the signature-age allowance (the 15 minutes) |
| + requestLimitH = 15 // request_limit_ns: the longest request, added to the signature age |
| + execTTL = 40 // exec lease TTL |
| + execRenew = 15 // renew when this close to expiry |
| + lostMargin = 10 // declare-lost margin past expiry |
| + cutBudget = 320 // absolute cut deadline after admission |
| + stagingTTL = 400 // staging-work lease TTL: longer than the cut budget, as in production |
| + probeTries = 3 |
| // probeStartWindow is a probe attempt's readiness window in steps (the |
| // budget's 30 s, §7.3): the retry policy's app restarts within one |
| // admitted session share it, and when it passes the attempt fails and |
| @@ -649,10 +655,10 @@ type obligation struct { |
| // included, uses the same location, archive incarnation and original |
| // evidence time: a retry's own clock is never evidence (R13-4). |
| type parkScope struct { |
| - Location string |
| - Inc int |
| - EvidenceAt int |
| - Limit int // request_limit_ns: the bound H adds to the signature age (the model's horizonH) |
| + Location string |
| + Inc int |
| + EvidenceAt int |
| + RequestLimit int // request_limit_ns: the longest request, which H adds to the signature age; the acknowledgement waits EvidenceAt + sigAgeH + RequestLimit |
| } |
| // admissionRecord is one AdmitWriter (claim rev 6.8 §6.4a): the session it |
| @@ -676,16 +682,14 @@ type admissionRecord struct { |
| // anywhere (claim rev 6.14 §6.4a item 1: region, predecessor_region) |
| Region int |
| PredRegion int |
| - // LostSrc (rev 7.11): a rollback's source re-admitted from its own |
| - // generation after the target was declared lost while the seal was the |
| - // one holder of the source's writes beyond its replica (src_covered |
| - // false): those writes, acknowledged in the source's cut session, are |
| - // declared too (seeds 16395 and 27191 / 30,000) |
| - LostSrc *writesLost |
| - // AdditionalWritesLost (claim rev 6.21 item 2, additional_writes_lost): |
| + // AdditionalWritesLost (claim rev 6.22 item 2, additional_writes_lost): |
| // behind a declared-lost target, every other session the target was |
| - // admitted into since the cut, certified or not; no return lane |
| - // carries any of their writes (seed 33373 / 100,000) |
| + // admitted into since the cut, certified or not (no return lane carries |
| + // any of their writes, seed 33373 / 100,000), and the source's cut |
| + // session when src_covered is false (the seal in the lost region was |
| + // the one holder of its writes beyond the replica, seeds 16395 and |
| + // 27191 / 30,000; rev 7.11's LostSrc). With Lost, unique by (box, |
| + // session) (R14-2) |
| AdditionalWritesLost []*writesLost |
| } |
| @@ -709,6 +713,7 @@ type openState struct { |
| Prepared bool |
| Probe bool |
| Source string // the generation the restore reads |
| + SourcePin int // how: -1 the marker's generation (restoreCalc); 0 a generation the run walk selected, rooted at [1, 1] (R14-1) |
| RemoteMax int // the certificate's max_txid a warm restore must reach |
| DB *localDB |
| stage string // restore, app, first, marker, anchor, open |