amadan
hostlife model: rev 7.14, joint round 13 and claim rev 6.22
Park state (R13-4, claim rev 6.15): remote chores carry a persisted park
scope {location, incarnation, evidence_at, limit}, bound in a CAS before
the first step or at the sweep's queuing CAS, so a retry after an agent
restart keeps the original evidence time; a free host's at-rest sweep is
a holderless parking op {kind: parking, intent.park_sweep: "v1"} with no
exec and no holder, whose last acknowledgement frees the claim again in
the same CAS (FreeAfterPark); on a serving host sweep chores carry
session:<n>; the create waits on the parking op; INV-20 in the create's
CAS. Rules persisted-park-scope and holderless-park; witnesses
wParkScopeSurvivesRestart and wFreeSweepVsCreate.
Coverage, completely (R13-2, claim rev 6.22 item 5): the publication
walk visits every entry in order, skipping covered ones, and requires an
entry to name the published generation; warm entries are born covered;
CoverParkedPredecessors(region, generations) covers only what the sweep
parks, at its queuing and acknowledgement CASes; INV-17 and the
whole-location coverage apply to every entry.
The run walk (R13-1, claim rev 6.22 §6.2a): a link in another region is
passed over, covered or not; a covered local link reached as a needed
baseline refuses the start and alerts; hasFiles reads current objects.
Rule covered-baseline-refused, witness wCoveredLocalBaseline;
TestInterruptedCleanReturn walks R -> T -> S and R2 -> R -> T -> S.
wOriginSwept names the refusal as its failure under the mutation.
additional_writes_lost (R13-3): the record field is renamed.
Rules: 104. Witnesses: 68.
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
6 files changed,
+526
−66
internal/sim/hostlife/console_test.go+27 −2internal/sim/hostlife/moves_test.go+35 −8internal/sim/hostlife/protocol_test.go+191 −49internal/sim/hostlife/rules_test.go+3 −0internal/sim/hostlife/witness_test.go+245 −2internal/sim/hostlife/world_test.go+25 −5
diff --git a/internal/sim/hostlife/console_test.go b/internal/sim/hostlife/console_test.go| index a0f9608f0..603e2f145 100644 |
| --- a/internal/sim/hostlife/console_test.go |
| +++ b/internal/sim/hostlife/console_test.go |
| @@ -208,6 +208,9 @@ func (w *world) createSteps(p *consolePlan) bool { |
| return false |
| } |
| c := w.claim |
| + if c != nil && c.Holder == nil && c.Op.Kind == "parking" && c.Op.ParkSweep != "" { |
| + return false // the holderless sweep blocks free's successor create until FreeAfterPark (claim rev 6.15 §6.2a) |
| + } |
| if c != nil && (c.Holder != nil || (c.Op.Kind != "" && c.Op.Kind != "serving")) || w.recPend != nil { |
| return abandon() |
| } |
| @@ -217,8 +220,8 @@ func (w *world) createSteps(p *consolePlan) bool { |
| // meanwhile changed it, and the 412 restarts the create |
| return restart() |
| } |
| - if c != nil && len(c.Obl) > 0 { |
| - return false // a pending chore, such as a sweep, finishes first (CC11) |
| + if c != nil && len(c.Obl) > 0 && on("holderless-park") { |
| + return false // a pending chore finishes first (CC11); since rev 7.14 a free host's sweep is the parking op above |
| } |
| if w.rec != nil { |
| // the record key is occupied: an orphan is removed by the |
| @@ -243,6 +246,12 @@ func (w *world) createSteps(p *consolePlan) bool { |
| } |
| w.serial++ |
| if !w.cas(c, func(n *claim) bool { |
| + if len(n.Obl) > 0 { |
| + // INV-20 (rev 7.14, R13-4): a create never claims a host while a |
| + // park of its namespace is outstanding; the holderless sweep's |
| + // op blocks it until FreeAfterPark |
| + w.violate("INV-20: create %s claimed the host while %d obligation(s) were outstanding (%s %s)", p.OpID, len(n.Obl), n.Obl[0].Kind, n.Obl[0].Prefix) |
| + } |
| n.Holder = &holder{Inc: p.Inc, App: p.App, Serial: w.serial, Location: locationFor(p.Inc, false), WriterBox: -1} // no writer yet |
| n.Op = opState{Kind: "creating", ID: p.OpID, Exec: -1, NewInc: p.Inc, NewApp: p.App, NewRegion: p.Region, ReqAt: w.now} |
| n.Regions, n.Boxes, n.Complete, n.Obl = []int{p.Region}, []int{b.ID}, true, nil |
| @@ -1050,6 +1059,22 @@ func (w *world) recoveryPass() { |
| } |
| } |
| case "deleting", "parking": |
| + if c.Holder == nil && c.Op.ParkSweep != "" { |
| + // a holderless sweep (claim rev 6.15 §6.2a) is the obligation |
| + // runners' to finish; the recovery pass only replays |
| + // FreeAfterPark for one whose chores are all acknowledged |
| + if c.oblFor(c.Op.ID) == 0 && w.now-c.Op.ReqAt >= 15 { |
| + id := c.Op.ID |
| + w.cas(c, func(n *claim) bool { |
| + if n.Holder != nil || n.Op.ID != id || n.oblFor(id) != 0 { |
| + return false |
| + } |
| + n.Op = opState{} |
| + return true |
| + }) |
| + } |
| + return |
| + } |
| if w.now-c.Op.ReqAt < 15 { |
| return |
| } |
diff --git a/internal/sim/hostlife/moves_test.go b/internal/sim/hostlife/moves_test.go| index 24e87c338..5217749d1 100644 |
| --- a/internal/sim/hostlife/moves_test.go |
| +++ b/internal/sim/hostlife/moves_test.go |
| @@ -1678,16 +1678,43 @@ func (w *world) sweep(b *box, c *claim) { |
| return |
| } |
| w.cas(c, func(n *claim) bool { |
| - if !(n.Op.Kind == "" || n.Op.Kind == "serving") { |
| - return false |
| + joining := n.Holder == nil && n.Op.Kind == "parking" && n.Op.ParkSweep != "" |
| + if !(n.Op.Kind == "" || n.Op.Kind == "serving" || joining) { |
| + return false // any other operation running suppresses new sweeps (claim rev 6.15 §6.2a) |
| + } |
| + // the chore's owner: on a serving host the session, as for |
| + // PublishGeneration; on a free host a holderless parking op, {kind: |
| + // parking, intent: {park_sweep: "v1"}}, no exec and no holder, the |
| + // only holderless claim that may carry obligations, so it blocks |
| + // free's successor create until its last acknowledgement frees the |
| + // claim again (FreeAfterPark; claim rev 6.15 §6.2a, R13-4). The |
| + // mutation of holderless-park queues rev 7.13's bare "sweep" chores |
| + // on the free claim. Another region's sweep while the op runs joins |
| + // it with its own chores (a reading, §19.4) |
| + op := "sweep" |
| + switch { |
| + case n.Holder != nil: |
| + op = fmt.Sprintf("session:%d", n.Holder.Session) |
| + case joining: |
| + op = n.Op.ID |
| + case on("holderless-park"): |
| + n.Op = opState{Kind: "parking", ID: w.newID("park"), ParkSweep: "v1", Exec: -1, ReqAt: w.now} |
| + op = n.Op.ID |
| + w.stats["holderless sweeps"]++ |
| + } |
| + inc := 0 |
| + if n.Holder != nil { |
| + inc = n.Holder.Inc |
| } |
| for _, p := range prefixes { |
| - n.Obl = append(n.Obl, obligation{ID: w.newID("ob"), Op: "sweep", Kind: "park-sweep", Region: b.Region, Box: -1, Prefix: p, Ret: "sweep"}) |
| - } |
| - // the sweep retires this region's dead generations wholesale: the |
| - // records whose predecessors it parks are covered here (rev 7.13; a |
| - // reading for the claim: item 6's composition applies to the sweep) |
| - w.coverSweptPredecessors(n, b.Region) |
| + // 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}}) |
| + } |
| + // CoverParkedPredecessors at the queuing CAS (claim rev 6.21 item 6): |
| + // the predecessors with a sweepable object, no others |
| + w.coverParkedPredecessors(n, b.Region, w.sweptPredecessors(n, b.Region, false)) |
| return true |
| }) |
| } |
diff --git a/internal/sim/hostlife/protocol_test.go b/internal/sim/hostlife/protocol_test.go| index 73bffb8b0..d8b6969d4 100644 |
| --- a/internal/sim/hostlife/protocol_test.go |
| +++ b/internal/sim/hostlife/protocol_test.go |
| @@ -491,13 +491,17 @@ func (w *world) spawn(b *box, c *claim, want string, probe bool) bool { |
| w.stats["start refused: unexplained empty generation"]++ |
| return false |
| } |
| - source = bg |
| - for _, g := range chain { |
| - if g != h.Gen && w.hasFiles(b, loc, g) { |
| - source = g |
| - break |
| - } |
| + // the recovery walk (claim rev 6.22 §6.2a, R13-1): newest |
| + // first over the run's links, a foreign link passed over, a |
| + // covered local one refused, the nearest local one holding an |
| + // object the baseline, else the marker's |
| + run, _ := w.unfinishedRun(c, bg) |
| + src, ok := w.runBaseline(b, c, run, bg) |
| + if !ok { |
| + return false |
| } |
| + source = src |
| + _ = chain |
| w.stats["abandoned empty generation skipped"]++ |
| } else if !w.republishMarker(b, loc, h.Gen) { |
| // no earlier version names it: the admitted writer's marker |
| @@ -960,6 +964,9 @@ 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) |
| + } |
| if n.Op.ID != observedOpID || phaseOf(&n.Op) != observedPhase { |
| return false // bound to the operation and phase it observed |
| } |
| @@ -967,9 +974,16 @@ func (w *world) publishGeneration(b *box, c *claim, observedOpID, observedPhase |
| if n.Op.Kind == "serving" || id == "" { |
| id = fmt.Sprintf("session:%d", session) |
| } |
| + // the walk is over the uncovered entries up to and including the |
| + // published one, warm records included (claim rev 6.21 item 5, as |
| + // E processes them; rev 7.13 skipped warm records): the publishing |
| + // session is the latest admitted, so no entry lies beyond it |
| for i := range n.Holder.Admissions { |
| e := &n.Holder.Admissions[i] |
| - if e.Mode != "cold" || e.Covered { |
| + if e.Session > session { |
| + break // beyond the published entry: the bound, never reached under the CAS's session check |
| + } |
| + if e.Covered { |
| continue |
| } |
| switch { |
| @@ -1024,11 +1038,11 @@ func (w *world) publishGeneration(b *box, c *claim, observedOpID, observedPhase |
| } |
| covered := 0 |
| for _, e := range n.Holder.Admissions { |
| - if e.Covered || e.Mode != "cold" { |
| + if e.Covered { |
| covered++ |
| } |
| } |
| - for covered > 8 && len(n.Holder.Admissions) > 1 && (n.Holder.Admissions[0].Covered || n.Holder.Admissions[0].Mode != "cold") { |
| + for covered > 8 && len(n.Holder.Admissions) > 1 && n.Holder.Admissions[0].Covered { |
| n.Holder.Admissions = n.Holder.Admissions[1:] |
| covered-- |
| } |
| @@ -1050,44 +1064,63 @@ func (w *world) coverRegionPredecessors(n *claim, region int, why string) { |
| } |
| for i := range n.Holder.Admissions { |
| e := &n.Holder.Admissions[i] |
| - if e.Mode == "cold" && !e.Covered && e.PredRegion == region && e.Predecessor.Gen != n.Holder.Gen { |
| + if !e.Covered && e.PredRegion == region && e.Predecessor.Gen != n.Holder.Gen { |
| e.Covered = true |
| w.stats["admissions covered at the "+why+" park"]++ |
| } |
| } |
| } |
| -// coverSweptPredecessors is the sweep's reading of item 6 (rev 7.13, a |
| -// claim question): the at-rest sweep parks a region's dead generations |
| -// wholesale, so the records whose predecessors it parks are covered in |
| -// its CASes, the one that queues the park-sweep (a predecessor with a |
| -// sweepable object) and the one that acknowledges it (a predecessor whose |
| -// objects it retired on the way). An empty predecessor, with nothing to |
| -// sweep, waits for its publication's chore. |
| -func (w *world) coverSweptPredecessors(n *claim, region int) { |
| - if n.Holder == nil || !on("cover-at-park") { |
| - return |
| +// sweptPredecessors is the generation set the at-rest sweep parks in a |
| +// region, read from the uncovered records whose predecessors are there: |
| +// at the queuing CAS, the predecessors with a sweepable object; at the |
| +// acknowledgement CAS (retired true), those whose objects it retired on |
| +// the way (had objects, has none). An empty predecessor, with nothing to |
| +// sweep, is in neither set and waits for its publication's chore. |
| +func (w *world) sweptPredecessors(n *claim, region int, retired bool) []string { |
| + if n.Holder == nil { |
| + return nil |
| } |
| bk := w.buckets[region] |
| loc := n.Holder.Location |
| - for i := range n.Holder.Admissions { |
| - e := &n.Holder.Admissions[i] |
| - if e.Mode != "cold" || e.Covered || e.PredRegion != region || e.Predecessor.Gen == n.Holder.Gen { |
| + var gens []string |
| + for _, e := range n.Holder.Admissions { |
| + if e.Covered || e.PredRegion != region || e.Predecessor.Gen == n.Holder.Gen || hasStr(gens, e.Predecessor.Gen) { |
| continue |
| } |
| - if w.hadFilesIn(region, loc, e.Predecessor.Gen) && !w.hasFilesIn(region, loc, e.Predecessor.Gen) { |
| - e.Covered = true // retired already: by this sweep or an earlier park |
| - w.stats["admissions covered at the sweep park"]++ |
| + if retired { |
| + if w.hadFilesIn(region, loc, e.Predecessor.Gen) && !w.hasFilesIn(region, loc, e.Predecessor.Gen) { |
| + gens = append(gens, e.Predecessor.Gen) |
| + } |
| continue |
| } |
| for _, k := range bk.keys(dataKey(loc, e.Predecessor.Gen, "")) { |
| if genOf(loc, k) == e.Predecessor.Gen && w.sweepable(n, region, k) { |
| - e.Covered = true |
| - w.stats["admissions covered at the sweep park"]++ |
| + gens = append(gens, e.Predecessor.Gen) |
| break |
| } |
| } |
| } |
| + return gens |
| +} |
| + |
| +// coverParkedPredecessors is claim rev 6.21's CoverParkedPredecessors(op, |
| +// phase, region, generations) (§6.4a item 6): the at-rest sweep covers |
| +// what it parks, selectively, in the CAS that queues its park-sweep and in |
| +// the one that acknowledges it; only the records whose predecessors are |
| +// among the generations it parks in the region are covered, never every |
| +// predecessor in the region. |
| +func (w *world) coverParkedPredecessors(n *claim, region int, gens []string) { |
| + if n.Holder == nil || !on("cover-at-park") { |
| + return |
| + } |
| + for i := range n.Holder.Admissions { |
| + e := &n.Holder.Admissions[i] |
| + if !e.Covered && e.PredRegion == region && e.Predecessor.Gen != n.Holder.Gen && hasStr(gens, e.Predecessor.Gen) { |
| + e.Covered = true |
| + w.stats["admissions covered at the sweep park"]++ |
| + } |
| + } |
| } |
| // hadFilesIn: the generation held an object in region r at some time: a |
| @@ -1128,12 +1161,38 @@ func hasObl(obl []obligation, id string) bool { |
| // certificate) in b's region; for the origin generation "", the objects |
| // directly under the location, not those of its g-<id>/ generations. |
| func (w *world) hasFiles(b *box, loc, gen string) bool { |
| - for _, k := range w.buckets[b.Region].keys(dataKey(loc, gen, "")) { |
| - if genOf(loc, k) == gen { |
| - return true |
| - } |
| - } |
| - return false |
| + return w.hasFilesIn(b.Region, loc, gen) |
| +} |
| + |
| +// runBaseline walks an unfinished run in b's region (claim rev 6.22 §6.2a, |
| +// R13-1): each record's predecessor is a link below it, newest first. A |
| +// link whose generation keeps its objects in another region is passed |
| +// over, covered or not (a clean return's fresh source admission after the |
| +// target's park was queued walks R, then the target's T in the other |
| +// region, then the source's S); a link in this region must be uncovered, |
| +// since a covered local generation is retired or being retired here, so |
| +// reaching one as a needed baseline refuses, with an alert. The baseline |
| +// is the newest link in this region that holds an object, else the |
| +// marker's generation (bg, the last link). The mutation of |
| +// covered-baseline-refused ignores the covered flag, as rev 7.13 did, and |
| +// selects by objects alone. |
| +func (w *world) runBaseline(b *box, c *claim, run []admissionRecord, bg string) (string, bool) { |
| + loc := c.Holder.Location |
| + for _, r := range run { |
| + link := r.Predecessor.Gen |
| + if r.PredRegion != b.Region { |
| + continue // another region's, or holding nothing anywhere: passed over |
| + } |
| + if r.Covered && on("covered-baseline-refused") { |
| + w.alert("box %d: generation %q, a baseline the restore of %q needs, is covered in this region (retired or being retired); the start is refused", b.ID, link, c.Holder.Gen) |
| + w.stats["start refused: covered local baseline"]++ |
| + return "", false |
| + } |
| + if w.hasFiles(b, loc, link) { |
| + return link, true |
| + } |
| + } |
| + return bg, true |
| } |
| func hasStr(xs []string, s string) bool { |
| @@ -1169,14 +1228,45 @@ func (w *world) restoreAsNext(e *box, c *claim) *localDB { |
| if !ok { |
| return w.restoreCalc(e.Region, h.Inc, loc, h.Gen) // unexplained: the restore refuses, as the start does |
| } |
| - for _, g := range chain { |
| - if g != h.Gen && w.hasFiles(e, loc, g) { |
| - return w.restoreWith(e.Region, h.Inc, loc, g, "", 0, 0) // a fresh generation rooted at [1, 1] |
| - } |
| + _ = chain |
| + run, _ := w.unfinishedRun(c, bg) |
| + src, fine := w.runBaseline(e, c, run, bg) |
| + if !fine { |
| + return nil // the start refuses: a covered local baseline (R13-1) |
| + } |
| + if src != bg { |
| + return w.restoreWith(e.Region, h.Inc, loc, src, "", 0, 0) // a fresh generation rooted at [1, 1] |
| } |
| return w.restoreCalc(e.Region, h.Inc, loc, bg) |
| } |
| +// unfinishedRun is unfinishedChain's records: the cold admissions of the |
| +// run, newest first, each one's predecessor the link below it; the last |
| +// record's predecessor is the marker's generation. |
| +func (w *world) unfinishedRun(c *claim, bg string) ([]admissionRecord, bool) { |
| + h := c.Holder |
| + if bg == h.Gen { |
| + return nil, true |
| + } |
| + gen := h.Gen |
| + var run []admissionRecord |
| + for i := len(c.Holder.Admissions) - 1; i >= 0; i-- { |
| + e := c.Holder.Admissions[i] |
| + if e.Gen != gen { |
| + return nil, false |
| + } |
| + if e.Mode != "cold" { |
| + continue |
| + } |
| + run = append(run, e) |
| + if e.Predecessor.Gen == bg { |
| + return run, true |
| + } |
| + gen = e.Predecessor.Gen |
| + } |
| + return nil, false |
| +} |
| + |
| // unfinishedChain explains a marker that lags holder.generation (claim rev |
| // 6.10, R10-2): the writers journal must show holder.generation to be the |
| // latest admission's, and every generation between it and the one the |
| @@ -1659,8 +1749,15 @@ func (w *world) admitCommit(b *box, c *claim, a admitInput) bool { |
| gen = n.Holder.Gen |
| } |
| e := admissionRecord{Session: n.Holder.Session, Box: b.ID, Gen: gen, Stamp: n.Holder.Stamp, Mode: a.Mode, Coverage: a.Coverage, Predecessor: p, Region: a.Region, PredRegion: a.PredecessorRegion} |
| - if a.Mode == "cold" && on("cover-at-park") { |
| - // born covered (rev 7.13, a reading for the claim's item 6): the |
| + if a.Mode != "cold" { |
| + // born covered (claim rev 6.22 item 5): a warm entry's predecessor |
| + // is its own generation, which nothing retires; the next cold |
| + // admission's record names it as predecessor and queues its chore |
| + e.Covered = true |
| + w.stats["admissions born covered: warm"]++ |
| + } |
| + if on("cover-at-park") { |
| + // born covered (claim rev 6.22 item 5, rev 7.13's reading): the |
| // claim already holds a whole-location park for the |
| // predecessor's region, so the predecessor is being retired there |
| // and this record needs no chore. A rollback's return is admitted |
| @@ -1709,7 +1806,7 @@ func (w *world) admitCommit(b *box, c *claim, a admitInput) bool { |
| lostTgt = append(lostTgt, &writesLost{Box: q.Box, Gen: q.Gen, Session: q.Session, RemoteMaxTXID: a.RemoteMaxTXID}) |
| } |
| } |
| - e.LostMore = lostTgt |
| + 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 |
| @@ -2039,21 +2136,54 @@ func (w *world) doObligation(b *box, c *claim, o obligation) { |
| } |
| } |
| // a replicator's PUT signed before that evidence can land up to |
| - // the horizon later: verify only after it (this model's finding) |
| + // the horizon later: verify only after it (this model's finding). |
| + // The evidence time is the chore's persisted park scope (claim |
| + // rev 6.15 §2, R13-4), bound in a CAS before the first step runs, |
| + // so a retry after an agent restart keeps the original time; the |
| + // mutation keeps rev 7.13's box-local map, which the restart |
| + // clears, and the horizon starts again from the restart's clock |
| + if o.Scope == nil && on("persisted-park-scope") { |
| + inc := 0 |
| + if c.Holder != nil { |
| + inc = c.Holder.Inc |
| + } |
| + scope := &parkScope{Location: o.Prefix, Inc: inc, EvidenceAt: w.now, Limit: horizonH} |
| + w.cas(c, func(n *claim) bool { |
| + for i := range n.Obl { |
| + if n.Obl[i].ID == o.ID && n.Obl[i].Scope == nil { |
| + n.Obl[i].Scope = scope |
| + return true |
| + } |
| + } |
| + return false |
| + }) |
| + w.stats["park scope bound"]++ |
| + return // the next step runs under the persisted scope |
| + } |
| if b.evidAt == nil { |
| b.evidAt = map[string]int{} |
| } |
| if _, ok := b.evidAt[o.ID]; !ok { |
| b.evidAt[o.ID] = w.now |
| } |
| - if on("quiet-before-ack") && b.evidAt[o.ID]+horizonH > quiet { |
| - quiet = b.evidAt[o.ID] + horizonH |
| + evidAt, limit := b.evidAt[o.ID], horizonH |
| + if o.Scope != nil { |
| + evidAt, limit = o.Scope.EvidenceAt, o.Scope.Limit |
| + } |
| + if on("quiet-before-ack") && evidAt+limit > quiet { |
| + quiet = evidAt + limit |
| } |
| } |
| 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 |
| + } |
| } |
| if o.Kind == "park-generation" { |
| // a dead generation within the live location (a cold recovery's |
| @@ -2068,15 +2198,18 @@ func (w *world) doObligation(b *box, c *claim, o obligation) { |
| return |
| } |
| } |
| - evid := 0 |
| + evid, limit := 0, horizonH |
| if b.evidAt != nil { |
| evid = b.evidAt[o.ID] |
| } |
| + if o.Scope != nil { |
| + evid, limit = o.Scope.EvidenceAt, o.Scope.Limit |
| + } |
| 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+horizonH > n.Quiet[o.Region] { |
| - n.Quiet[o.Region] = evid + horizonH // quiet_after survives free |
| + 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-superseded" && n.Holder != nil && o.Prefix == n.Holder.Location { |
| // INV-17 (rev 7.13, R12-3): the whole location in this region |
| @@ -2086,19 +2219,28 @@ func (w *world) doObligation(b *box, c *claim, o obligation) { |
| // would wait for a publication in this region that may never |
| // come, with a chore for a prefix already parked |
| for _, e := range n.Holder.Admissions { |
| - if e.Mode == "cold" && !e.Covered && e.PredRegion == o.Region && e.Predecessor.Gen != n.Holder.Gen { |
| + if !e.Covered && e.PredRegion == o.Region && e.Predecessor.Gen != n.Holder.Gen { |
| w.violate("INV-17: the whole-location park %s of region %d retired admission %d's predecessor %q, and the record is uncovered", o.ID, o.Region, e.Session, e.Predecessor.Gen) |
| break |
| } |
| } |
| } |
| if o.Kind == "park-sweep" && n.Holder != nil { |
| - w.coverSweptPredecessors(n, o.Region) // what the sweep retired on its way is covered as it finishes (rev 7.13 reading) |
| + // CoverParkedPredecessors at the acknowledgement (claim rev 6.21 |
| + // item 6): what the sweep retired on its way |
| + w.coverParkedPredecessors(n, o.Region, w.sweptPredecessors(n, o.Region, true)) |
| } |
| n.Obl = append(n.Obl[:i:i], n.Obl[i+1:]...) |
| if o.Ret == "legacy" && n.oblFor("adopt") == 0 { |
| n.Complete = true // every region has acknowledged |
| } |
| + if n.Holder == nil && n.Op.Kind == "parking" && n.Op.ParkSweep != "" && n.oblFor(n.Op.ID) == 0 { |
| + // FreeAfterPark (claim rev 6.15 §6.2a): the holderless |
| + // sweep's last acknowledgement frees the claim again in the |
| + // same CAS, keeping quiet_after |
| + n.Op = opState{} |
| + w.stats["free after park"]++ |
| + } |
| return true |
| } |
| } |
diff --git a/internal/sim/hostlife/rules_test.go b/internal/sim/hostlife/rules_test.go| index 8c9ff288a..f0026e033 100644 |
| --- a/internal/sim/hostlife/rules_test.go |
| +++ b/internal/sim/hostlife/rules_test.go |
| @@ -125,6 +125,9 @@ var allRules = []string{ |
| "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 |
diff --git a/internal/sim/hostlife/witness_test.go b/internal/sim/hostlife/witness_test.go| index 10346da3b..142a08091 100644 |
| --- a/internal/sim/hostlife/witness_test.go |
| +++ b/internal/sim/hostlife/witness_test.go |
| @@ -165,6 +165,12 @@ var witnesses = []witness{ |
| "the commit is interrupted between the record's flip and the claim's CAS: every actor pauses past the horizon; whoever follows the record later performs the one CAS, parks and coverage together (R12-3, interruption)", wCommitInterrupted}, |
| {"cover-at-park", "cover-at-park", "INV-17", |
| "the commit's CAS is followed again by another reader: the replay is refused, the park is queued once and the coverage stands (R12-3, replay)", wCommitReplayed}, |
| + {"persisted-park-scope", "persisted-park-scope", "INV-9", |
| + "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}, |
| + {"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", |
| + "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}, |
| {"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", |
| @@ -2410,13 +2416,250 @@ func wOriginSwept(t *testing.T, w *world) { |
| return |
| } |
| } |
| - w.recovered(t, b0, "woken after the sweep") |
| + // the recovery: under the mutation the swept origin is a covered local |
| + // baseline since rev 7.14 (claim rev 6.22 §6.2a), and the start refuses |
| + // with an alert rather than restoring nothing; either way the data is |
| + // unreachable, which is the failure the witness names |
| + 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-2 (witness): the recovery cannot start, its origin baseline was retired under the unfinished admission (%d starts refused as a covered local baseline)", w.stats["start refused: covered local baseline"]) |
| + } |
| + return |
| + } |
| w.checkLocal(w.claim, b0, b0.DB) |
| w.checkDurable(w.claim, "after the recovery") |
| w.finish(t) |
| } |
| -// ---------- rev 7.13 ---------- |
| +// ---------- rev 7.14 ---------- |
| + |
| +// wParkScopeSurvivesRestart (claim rev 6.15 §2, R13-4): a committed move's |
| +// source-region park binds its scope, with the evidence time, in the |
| +// claim; the region's agent restarts mid-park; the acknowledgement comes |
| +// at the original evidence time plus the horizon, not the restart's. |
| +func wParkScopeSurvivesRestart(t *testing.T, w *world) { |
| + src, tgt := w.boxes[0], w.boxes[1] |
| + w.serve(src, 1, app0) |
| + w.wake(src) |
| + w.appWrite(src) |
| + w.commitLanding(t, src, tgt) |
| + if len(w.violations) > 0 { |
| + return |
| + } |
| + t0 := w.now |
| + var id string |
| + for _, o := range w.claim.Obl { |
| + if o.Kind == "park-superseded" && o.Region == src.Region { |
| + id = o.ID |
| + } |
| + } |
| + if id == "" { |
| + t.Fatalf("witness: no park-superseded for the source region after the commit: %s", w.state()) |
| + } |
| + // the park runs for a while, then the source region's agent restarts |
| + for i := 0; i < 45; i++ { |
| + w.tick(w.act(src, tgt), w.runConsole, w.recoveryPass) |
| + if len(w.violations) > 0 { |
| + return |
| + } |
| + } |
| + if !hasObl(w.claim.Obl, id) { |
| + t.Fatalf("witness: the park %s acknowledged before the restart, at %d (commit at %d): the horizon did not hold", id, w.now, t0) |
| + } |
| + w.crash(src) // a new agent process: the box-local evidence map is gone |
| + w.reach(t, 400, "the source region's park acknowledged", func() bool { return !hasObl(w.claim.Obl, id) }, w.act(src, tgt), w.runConsole, w.recoveryPass) |
| + if len(w.violations) > 0 { |
| + return |
| + } |
| + if deadline := t0 + horizonH + 40; w.now > deadline { |
| + w.violate("INV-9 (witness): the park %s was acknowledged at %d, after %d, the commit's evidence plus the horizon and slack: the restart at %d started the horizon again", id, w.now, deadline, t0+45) |
| + return |
| + } |
| + w.finish(t) |
| +} |
| + |
| +// 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. |
| +// Without the op the create claims the host over the outstanding park |
| +// (INV-20). |
| +func wFreeSweepVsCreate(t *testing.T, w *world) { |
| + 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 { |
| + return |
| + } |
| + // a replica PUT accepted before the delete's park lands now |
| + k := ltxKey(loc, "", 0, 7, 7) |
| + w.buckets[b0.Region].objs[k] = append(w.buckets[b0.Region].objs[k], &version{ID: w.newVer(), B: &blob{Kind: "ltx", Level: 0, Min: 7, Max: 7, Inc: 1, Pages: map[string]int{}}}) |
| + // the create is requested at once; the sweep finds the residue on its |
| + // next pass |
| + w.nextInc++ |
| + w.console = append(w.console, &consolePlan{Kind: "create", Host: "h", App: app0, OpID: w.newID("cr"), Inc: w.nextInc, Region: 1}) |
| + w.reach(t, 800, "the create completed", func() bool { |
| + c := w.claim |
| + return len(w.violations) > 0 || c != nil && c.Holder != nil && c.Op.Kind == "serving" |
| + }, w.actAll(), w.runConsole, w.recoveryPass) |
| + if len(w.violations) > 0 { |
| + return |
| + } |
| + if w.stats["holderless sweeps"] == 0 && on("holderless-park") { |
| + t.Fatalf("witness: no holderless sweep ran before the create: %s", w.state()) |
| + } |
| + w.finish(t) |
| +} |
| + |
| +// wCoveredLocalBaseline (claim rev 6.22 §6.2a, R13-1): an unfinished run |
| +// whose link in this region is covered, its generation retired. The walk |
| +// must refuse the start and alert; reading objects alone, as rev 7.13 |
| +// did, it passes over the empty link and restores the marker's generation, |
| +// retired too, as an empty database (INV-2). |
| +func wCoveredLocalBaseline(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 |
| + // a cold admission into a fresh generation g1 that runs and publishes: |
| + // the serving session closes cleanly, its certificate is removed, the |
| + // next wake is cold |
| + 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)) |
| + w.wake(b0) |
| + g1 := w.claim.Holder.Gen |
| + if g1 == "" { |
| + t.Fatalf("witness: no cold admission after the certificate was removed: %s", w.state()) |
| + } |
| + w.reach(t, 200, "g1 published", func() bool { bg, _ := w.bucketGen(b0, loc); return bg == g1 }, w.act(b0)) |
| + w.idleStop(b0) |
| + w.reach(t, 200, "g1 closed", func() bool { return !hasMain(b0) && (b0.DB == nil || !b0.DB.Closing) }, w.act(b0)) |
| + // a second cold admission, g2, that dies before its first upload: the |
| + // marker still names g1, the run is g2 -> g1 |
| + delete(w.buckets[b0.Region].objs, closedKey(loc, g1, w.claim.Holder.Session)) |
| + 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 |
| + g2 := w.claim.Holder.Gen |
| + if g2 == g1 || g2 == "" { |
| + t.Fatalf("witness: no second cold admission: %s", w.state()) |
| + } |
| + // the constructed state: g2's record is covered and g1 is retired in |
| + // this region (an operator parked it, or a chore it should not have had) |
| + w.cas(w.claim, func(n *claim) bool { |
| + for i := range n.Holder.Admissions { |
| + if n.Holder.Admissions[i].Gen == g2 { |
| + n.Holder.Admissions[i].Covered = true |
| + } |
| + } |
| + return true |
| + }) |
| + bk := w.buckets[b0.Region] |
| + for _, k := range bk.keys(dataKey(loc, g1, "")) { |
| + if genOf(loc, k) == g1 { |
| + bk.objs[k] = nil // parked: the key keeps its entry with no version |
| + } |
| + } |
| + for i := 0; i < 80; i++ { |
| + w.tick(w.act(b0), w.recoveryPass, func() { w.wake(b0) }) |
| + if len(w.violations) > 0 || hasMain(b0) { |
| + break |
| + } |
| + } |
| + if hasMain(b0) { |
| + w.checkLocal(w.claim, b0, b0.DB) // started on nothing: INV-2 |
| + return |
| + } |
| + if w.stats["start refused: covered local baseline"] == 0 { |
| + t.Fatalf("witness: the host neither started nor refused a covered local baseline: %s", w.state()) |
| + } |
| +} |
| + |
| +// 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, |
| +// the target's generation, in the other region and covered under its park; |
| +// the walk passes T over and restores S; then one more interrupted |
| +// admission afterward, R2 -> R -> T -> S. |
| +func TestInterruptedCleanReturn(t *testing.T) { |
| + w := newWitness() |
| + defer func() { |
| + if t.Failed() { |
| + dump(t, w) |
| + } |
| + }() |
| + src, tgt := w.boxes[0], w.boxes[1] |
| + w.serve(src, 1, app0) |
| + w.wake(src) |
| + w.appWrite(src) |
| + w.replicate(src) |
| + w.landProbed(t, src, tgt) |
| + loc, gen0 := w.claim.Holder.Location, w.claim.Op.SrcGen |
| + w.rollback(w.claim, "settle check failed") // the target wrote nothing: a clean rollback |
| + crashes := 0 |
| + w.startHook = func(x *box) bool { |
| + if x != src || crashes >= 2 || w.claim.Op.Kind != "restoring" && w.claim.Op.Kind != "serving" { |
| + return false |
| + } |
| + crashes++ |
| + w.crash(x) // before the first upload: the fresh generation is empty |
| + return true |
| + } |
| + w.reach(t, 800, "the source's return admission crashed", func() bool { return crashes >= 1 }, w.act(src, tgt), w.recoveryPass, w.runConsole) |
| + if len(w.violations) > 0 { |
| + t.Fatalf("%s", w.violations[0]) |
| + } |
| + // the recovery: R is empty, T is the other region's, S holds the data |
| + w.recovered(t, src, "source recovered across the interrupted return") |
| + if w.stats["abandoned empty generation skipped"] < 1 { |
| + t.Fatalf("the recovery did not walk the run: %v", w.stats) |
| + } |
| + w.checkLocal(w.claim, src, src.DB) |
| + if len(w.violations) > 0 { |
| + t.Fatalf("%s", w.violations[0]) |
| + } |
| + // one more interrupted admission afterward: R2 -> R -> T -> S |
| + w.reach(t, 1500, "the rollback finished", func() bool { return w.claim.Op.Kind == "serving" }, w.act(src, tgt), w.recoveryPass, w.runConsole) |
| + if len(w.violations) > 0 { |
| + t.Fatalf("%s", w.violations[0]) |
| + } |
| + w.idleStop(src) |
| + w.reach(t, 200, "closed", func() bool { return !hasMain(src) }, w.act(src)) |
| + delete(w.buckets[src.Region].objs, closedKey(loc, w.claim.Holder.Gen, w.claim.Holder.Session)) |
| + w.wake(src) // cold, and the hook crashes it before its upload |
| + w.startHook = nil |
| + if crashes != 2 { |
| + t.Fatalf("the second admission did not crash (%d crashes): %s", crashes, w.state()) |
| + } |
| + w.recovered(t, src, "source recovered across two interrupted admissions") |
| + w.checkLocal(w.claim, src, src.DB) |
| + w.checkDurable(w.claim, "after the second recovery") |
| + if len(w.violations) > 0 { |
| + t.Fatalf("%s", w.violations[0]) |
| + } |
| + t.Logf("run walked twice from %q: %d empty generations skipped, %d starts refused", gen0, w.stats["abandoned empty generation skipped"], w.stats["start refused: covered local baseline"]) |
| + w.finish(t) |
| + if len(w.violations) > 0 { |
| + t.Fatalf("%s", w.violations[0]) |
| + } |
| +} |
| // wTwoSessionDeclaration (R12-1) is a constructed-state oracle test: the |
| // loss oracle's exemption, applied to acknowledgements of two sessions. |
diff --git a/internal/sim/hostlife/world_test.go b/internal/sim/hostlife/world_test.go| index a62d0e6e5..77b045435 100644 |
| --- a/internal/sim/hostlife/world_test.go |
| +++ b/internal/sim/hostlife/world_test.go |
| @@ -639,7 +639,20 @@ type obligation struct { |
| Box int |
| Prefix string |
| Ret string |
| - Quiet int // not before |
| + Quiet int // not before |
| + Scope *parkScope // the persisted park scope of a remote chore (claim rev 6.15 §2), bound before its first step runs |
| +} |
| + |
| +// parkScope is claim rev 6.15's park scope {location, incarnation, |
| +// evidence_at, request_limit_ns}, persisted in the chore when it is queued |
| +// or bound before its first step, so every retry, an agent restart's |
| +// 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) |
| } |
| // admissionRecord is one AdmitWriter (claim rev 6.8 §6.4a): the session it |
| @@ -669,10 +682,11 @@ type admissionRecord struct { |
| // false): those writes, acknowledged in the source's cut session, are |
| // declared too (seeds 16395 and 27191 / 30,000) |
| LostSrc *writesLost |
| - // LostMore (rev 7.13): 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) |
| - LostMore []*writesLost |
| + // AdditionalWritesLost (claim rev 6.21 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) |
| + AdditionalWritesLost []*writesLost |
| } |
| // pred is the predecessor an admission journals: the session, writer box, |
| @@ -726,6 +740,12 @@ type opState struct { |
| Phase string |
| Exec int // -1 none |
| Parts []int |
| + // ParkSweep is intent.park_sweep (claim rev 6.15 §6.2a): a free host's |
| + // at-rest sweep runs as a holderless parking op, {kind: parking, |
| + // intent: {park_sweep: "v1"}}, with no exec and no holder, carrying |
| + // only scoped remote chores; its last acknowledgement frees the claim |
| + // again in the same CAS (FreeAfterPark) |
| + ParkSweep string |
| // intent |
| Src, Tgt int |