amadan
sim: hostlife: claim rev 6.12, holder.admissions, PublishGeneration, Coverage, the origin's absent marker, the final recovery admission, a probe attempt's window (rev 7.12)
Joint round 11 (R11-1 to R11-5) and claim rev 6.12 (b202ea4e; E
34224a29). holder.Admissions ([]admissionRecord{session, box,
generation, predecessor, mode, coverage, covered, writes_lost}) replaces
op.journal.writers and survives every operation by living in the
holder, trimmed to eight covered records, never an uncovered one or the
current predecessor. An admission's predecessor is the last record
(session, box, generation), never the generation a clean return chose
for the restore; INV-16 checks it. Coverage "" | sealed | clean-return
replaces BaselineCoversPredecessor: only "" with no certificate records
writes_lost; a clean return with src_covered is covered unless its
target was declared lost. PublishGeneration(observedOpID, observedPhase,
observedSession, publishedGeneration, region, newID) is the only
retirement path, bound to the operation and phase, legal while serving
and inside operations, chores with op = op.id inside an operation and
session:<n> while serving; "" and @root are one origin.
R11-1: the sweep reads an absent generation.json as the origin, as the
residue oracle does, so an unfinished admission's chain protects an
adopted host's replica. R10-6: the final oracle runs the recovery
admission for real when the serving session is uncertified, judges by
what it declared, and counts an admission that could not run as an
unverified prospective declaration. A probe attempt's app restarts share
its readiness window (probeStartWindow): the fifth failure or the window
ends the attempt and the operation counts one budgeted try; a probe
never marks the host failed.
Rule clean-return-identity (96); witnesses wCleanReturnIdentity and
wOriginSwept (59). dirty-return's named failure is INV-2 local at the
final recovery.
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
7 files changed,
+364
−92
internal/sim/hostlife/console_test.go+2 −3internal/sim/hostlife/moves_test.go+17 −11internal/sim/hostlife/protocol_test.go+174 −37internal/sim/hostlife/rules_test.go+1 −0internal/sim/hostlife/sim_test.go+34 −17internal/sim/hostlife/witness_test.go+97 −2internal/sim/hostlife/world_test.go+39 −22
diff --git a/internal/sim/hostlife/console_test.go b/internal/sim/hostlife/console_test.go| index 0b6771276..533022cbe 100644 |
| --- a/internal/sim/hostlife/console_test.go |
| +++ b/internal/sim/hostlife/console_test.go |
| @@ -404,8 +404,7 @@ func (w *world) moveTo(r int) { |
| } |
| n.Op = opState{Kind: "moving", ID: id, Phase: "leases", Exec: src.ID, Parts: []int{src.ID, tgt.ID}, |
| Src: src.ID, Tgt: tgt.ID, SrcRegion: src.Region, TgtRegion: r, ReqAt: w.now, Auto: true, App: c.Holder.App, |
| - SrcGen: c.Holder.Gen, // the source's generation, which a clean rollback's return names again (rev 7.10) |
| - Writers: n.Op.Writers} // the writers journal is carried into every operation (rev 7.11 §5.1 step 9) |
| + SrcGen: c.Holder.Gen} // the source's generation, which a clean rollback's return names again (rev 7.10) |
| return true |
| }) { |
| w.logf("move %s inc %d from box %d to box %d", id, c.Holder.Inc, src.ID, tgt.ID) |
| @@ -433,7 +432,7 @@ func (w *world) userPush() { |
| if n.Op.Kind != "serving" { |
| return false |
| } |
| - n.Op = opState{Kind: "pushing", ID: id, Phase: "stopping", Exec: b.ID, Parts: []int{b.ID}, Src: b.ID, Tgt: b.ID, SrcRegion: b.Region, TgtRegion: b.Region, ReqAt: w.now, Writers: n.Op.Writers} |
| + n.Op = opState{Kind: "pushing", ID: id, Phase: "stopping", Exec: b.ID, Parts: []int{b.ID}, Src: b.ID, Tgt: b.ID, SrcRegion: b.Region, TgtRegion: b.Region, ReqAt: w.now} |
| return true |
| }) { |
| w.logf("push %s on box %d", id, b.ID) |
diff --git a/internal/sim/hostlife/moves_test.go b/internal/sim/hostlife/moves_test.go| index eefb687a4..a5d7131e5 100644 |
| --- a/internal/sim/hostlife/moves_test.go |
| +++ b/internal/sim/hostlife/moves_test.go |
| @@ -1203,12 +1203,10 @@ func (w *world) release(c *claim, execBox int) { |
| if !sameOp(n.Op.ID, op.ID) { |
| return false |
| } |
| - // the writers journal survives the release (rev 7.11): an admission |
| - // whose start is unfinished at the release stays explained, so its |
| - // predecessor stays live and the lagging marker is no alert (seed |
| - // 1052 / 30,000: an abort released over a source admitted a tick |
| - // earlier) |
| - n.Op = opState{Kind: "serving", Exec: execBox, Parts: []int{execBox}, Writers: n.Op.Writers} |
| + // holder.admissions survives the release by living in the holder |
| + // (claim rev 6.12): an admission whose start is unfinished at the |
| + // release stays explained (seed 1052 / 30,000) |
| + n.Op = opState{Kind: "serving", Exec: execBox, Parts: []int{execBox}} |
| return true |
| }) { |
| w.logf("released %s to serving on box %d", op.ID, execBox) |
| @@ -1638,7 +1636,7 @@ func sameStep(a, b *claim) bool { |
| if a.Holder != nil && a.Holder.WriterBox != b.Holder.WriterBox { |
| return false |
| } |
| - return len(x.Writers) == len(y.Writers) |
| + return a.Holder == nil || len(a.Holder.Admissions) == len(b.Holder.Admissions) |
| } |
| // sweep is claim rev 5's at-rest sweep (§6.2a, CC15): for a host with no |
| @@ -1753,14 +1751,22 @@ func (w *world) deadGeneration(c *claim, r int, k string) bool { |
| if !on("live-set-region") { |
| authoritative = true |
| } |
| - if v := w.buckets[r].current(genMarkerKey(h.Location)); authoritative && v != nil && v.B.Gen != h.Gen { |
| + // an absent marker is the origin generation "" (R11-1): an adopted |
| + // host's replica has no generation.json until its first cold admission |
| + // publishes one, and that admission's unfinished chain protects the |
| + // origin exactly as the residue oracle reads it |
| + mg := "" |
| + if v := w.buckets[r].current(genMarkerKey(h.Location)); v != nil { |
| + mg = v.B.Gen |
| + } |
| + if authoritative && mg != h.Gen { |
| // the marker disagrees with holder.generation. Normal while the |
| // latest admission is unfinished: the marker names its predecessor, |
| // and both generations are live (claim rev 6.10, R10-2). Any other |
| // disagreement: touch nothing under the location, and alert (§6.4) |
| - chain, ok := w.unfinishedChain(c, v.B.Gen) |
| + chain, ok := w.unfinishedChain(c, mg) |
| if ok && on("baseline-live") { |
| - for _, g := range append(chain, v.B.Gen) { |
| + for _, g := range append(chain, mg) { |
| if isDataKey(k) && genPrefixOf(k) == dataKey(h.Location, g, "") { |
| return false |
| } |
| @@ -1773,7 +1779,7 @@ func (w *world) deadGeneration(c *claim, r int, k string) bool { |
| } |
| } else if !w.markerAlerted[h.Location] { |
| w.markerAlerted[h.Location] = true |
| - w.alert("box in region %d: generation.json names %q, the claim %q, and no unfinished admission explains it; the location is left untouched", r, v.B.Gen, h.Gen) |
| + w.alert("box in region %d: generation.json names %q, the claim %q, and no unfinished admission explains it; the location is left untouched", r, mg, h.Gen) |
| return false |
| } else { |
| return false |
diff --git a/internal/sim/hostlife/protocol_test.go b/internal/sim/hostlife/protocol_test.go| index 7520c15e0..ea7f2a9de 100644 |
| --- a/internal/sim/hostlife/protocol_test.go |
| +++ b/internal/sim/hostlife/protocol_test.go |
| @@ -527,7 +527,7 @@ func (w *world) spawn(b *box, c *claim, want string, probe bool) bool { |
| } |
| } |
| lagDead = w.uncovered(b, c, loc, h.Gen, lagDead) |
| - if !w.queueGenerationRetire(b, c, h.Session, h.Gen, b.Region, lagDead) { |
| + if !w.publishGeneration(b, c, c.Op.ID, phaseOf(&c.Op), h.Session, h.Gen, b.Region, w.newID("ob"), lagDead) { |
| return false // the claim moved: next time |
| } |
| } |
| @@ -705,13 +705,36 @@ func (w *world) resumeOpen(b *box, c *claim, o *openState) bool { |
| continue |
| } |
| if !hasMain(b) { |
| + if o.startedAt == 0 { |
| + o.startedAt = w.now |
| + } |
| if !(b.Config == h.Inc && b.Live == h.App && b.LiveInc == h.Inc) { |
| + if o.Probe && w.now-o.startedAt >= probeStartWindow { |
| + // a probe attempt's readiness window has passed with the |
| + // environment never ready: the attempt fails (§7.7) |
| + b.open = nil |
| + b.startFails, b.nextStart = 0, 0 |
| + w.stats["probe attempt failed: environment"]++ |
| + w.probeAttemptFailed(b, cur) |
| + } |
| return false // the environment: wait, no failure counted |
| } |
| if !w.appStart(b, cur, o.Want, o.Probe, o.Mode) { |
| b.startFails++ |
| b.nextStart = w.now + startBackoff0<<(b.startFails-1) |
| w.stats["start failed"]++ |
| + if o.Probe && (b.startFails >= startAttemptsMax || w.now-o.startedAt >= probeStartWindow) { |
| + // a probe attempt's readiness window is the budget's 30 s |
| + // (§7.3, §7.7): the retry policy's restarts share it, and |
| + // when the fifth fails or the window passes the attempt |
| + // fails; the operation counts one of its budgeted tries, |
| + // and the host is not marked failed by a probe |
| + b.open = nil |
| + b.startFails, b.nextStart = 0, 0 |
| + w.stats["probe attempt failed: start"]++ |
| + w.probeAttemptFailed(b, cur) |
| + return false |
| + } |
| if b.startFails >= startAttemptsMax { |
| b.hostFailed, b.failedAt = true, w.now |
| b.open = nil // no session continues on a failed host; the operator's clearing leads to a fresh admission |
| @@ -845,7 +868,7 @@ func (w *world) resumeOpen(b *box, c *claim, o *openState) bool { |
| // landed but before it queued the chore left its own |
| // predecessor behind (seed 899 / 30,000) |
| dead := w.uncovered(b, cur, loc, o.Gen, append([]string(nil), o.Dead...)) |
| - if !w.queueGenerationRetire(b, cur, o.Session, o.Gen, b.Region, dead) { |
| + if !w.publishGeneration(b, cur, cur.Op.ID, phaseOf(&cur.Op), o.Session, o.Gen, b.Region, w.newID("ob"), dead) { |
| return false // the claim moved: next time |
| } |
| } |
| @@ -876,20 +899,47 @@ func (w *world) resumeOpen(b *box, c *claim, o *openState) bool { |
| // region, under the session's op id "session:<holder.session>". The |
| // mutation of baseline-live queues it at the admitting CAS instead, as |
| // rev 7.10 did, before the new generation has a root. |
| -func (w *world) queueGenerationRetire(b *box, c *claim, session int, published string, region int, dead []string) bool { |
| +// publishGeneration is claim rev 6.12's PublishGeneration(observedOpID, |
| +// observedPhase, observedSession, publishedGeneration, region): the one |
| +// CAS that retires generations, made after generation.json names the |
| +// published one, bound to the observed operation and phase like the |
| +// admission, legal while serving and inside any operation a writer runs |
| +// in (R11-5). It marks every admission entry up to the published |
| +// generation covered and queues one park-generation per dead generation, |
| +// deduplicated, with op = op.id inside an operation and "session:<n>" |
| +// while serving; only predecessors recorded in holder.admissions are ever |
| +// retired, and "" and "@root" are one origin (R11-2). Covered entries |
| +// beyond the last eight are trimmed. |
| +func (w *world) publishGeneration(b *box, c *claim, observedOpID, observedPhase string, session int, published string, region int, newID string, dead []string) bool { |
| return w.cas(c, func(n *claim) bool { |
| if n.Holder == nil || n.Holder.Session != session || n.Holder.Gen != published { |
| return false |
| } |
| - id := c.Op.ID |
| + if n.Op.ID != observedOpID || phaseOf(&n.Op) != observedPhase { |
| + return false // bound to the operation and phase it observed |
| + } |
| + id := n.Op.ID |
| if n.Op.Kind == "serving" || id == "" { |
| id = fmt.Sprintf("session:%d", session) |
| } |
| - for i := range n.Op.Writers { |
| - if e := &n.Op.Writers[i]; e.Mode == "cold" && e.Session <= session { |
| - e.Retired = true // its predecessor is parked or in this dead set |
| + for i := range n.Holder.Admissions { |
| + if e := &n.Holder.Admissions[i]; e.Mode == "cold" && e.Session <= session { |
| + e.Covered = true // its predecessor is parked or in this dead set |
| } |
| } |
| + var keep []admissionRecord |
| + covered := 0 |
| + for i := len(n.Holder.Admissions) - 1; i >= 0; i-- { |
| + e := n.Holder.Admissions[i] |
| + if e.Covered || e.Mode != "cold" { |
| + covered++ |
| + if covered > 8 { |
| + continue // trimmed (claim rev 6.12: at most the last eight covered entries) |
| + } |
| + } |
| + keep = append([]admissionRecord{e}, keep...) |
| + } |
| + n.Holder.Admissions = keep |
| next: |
| for _, retire := range dead { |
| if retire == published { |
| @@ -904,22 +954,35 @@ func (w *world) queueGenerationRetire(b *box, c *claim, session int, published s |
| continue next // already queued |
| } |
| } |
| - n.Obl = append(n.Obl, obligation{ID: w.newID("ob"), Op: id, Kind: "park-generation", Region: region, Box: -1, Prefix: n.Holder.Location, Ret: ret, Quiet: w.now + horizonH}) |
| + oid := newID |
| + if k := len(n.Obl); k > 0 && n.Obl[k-1].ID == oid || 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: region, Box: -1, Prefix: n.Holder.Location, Ret: ret, Quiet: w.now + horizonH}) |
| } |
| return true |
| }) |
| } |
| -// uncovered adds to dead the predecessor of every cold admission of the |
| -// operation's writers journal whose chores were never queued (its writer |
| -// died after its marker landed, before the chore CAS) and that still |
| +func hasObl(obl []obligation, id string) bool { |
| + for _, o := range obl { |
| + if o.ID == id { |
| + return true |
| + } |
| + } |
| + return false |
| +} |
| + |
| +// uncovered adds to dead the predecessor of every cold admission in |
| +// holder.admissions whose chores were never queued (its writer died after |
| +// its marker landed, before the PublishGeneration CAS) and that still |
| // holds objects (seeds 899 and 98677 / 100,000). Every entry is marked |
| // covered by the CAS that queues them. |
| func (w *world) uncovered(b *box, c *claim, loc, published string, dead []string) []string { |
| - for i := range c.Op.Writers { |
| - e := &c.Op.Writers[i] |
| - if e.Mode == "cold" && !e.Retired && e.Gen != published && e.Pred.Gen != published && !hasStr(dead, e.Pred.Gen) && w.hasFiles(b, loc, e.Pred.Gen) { |
| - dead = append(dead, e.Pred.Gen) |
| + for i := range c.Holder.Admissions { |
| + e := &c.Holder.Admissions[i] |
| + if e.Mode == "cold" && !e.Covered && e.Gen != published && e.Predecessor.Gen != published && !hasStr(dead, e.Predecessor.Gen) && w.hasFiles(b, loc, e.Predecessor.Gen) { |
| + dead = append(dead, e.Predecessor.Gen) |
| } |
| } |
| return dead |
| @@ -993,8 +1056,8 @@ func (w *world) unfinishedChain(c *claim, bg string) ([]string, bool) { |
| } |
| gen := h.Gen |
| var chain []string |
| - for i := len(c.Op.Writers) - 1; i >= 0; i-- { |
| - e := &c.Op.Writers[i] |
| + for i := len(c.Holder.Admissions) - 1; i >= 0; i-- { |
| + e := &c.Holder.Admissions[i] |
| if e.Gen != gen { |
| return nil, false // the journal does not explain holder.generation |
| } |
| @@ -1002,14 +1065,43 @@ func (w *world) unfinishedChain(c *claim, bg string) ([]string, bool) { |
| continue // a warm session of the same generation |
| } |
| chain = append(chain, gen) |
| - if e.Pred.Gen == bg { |
| + if e.Predecessor.Gen == bg { |
| return chain, true |
| } |
| - gen = e.Pred.Gen |
| + gen = e.Predecessor.Gen |
| } |
| return nil, false |
| } |
| +// probeAttemptFailed counts a failed probe attempt against the operation's |
| +// budget (§7.3, §7.7): a landing rolls back at probeTries, a revert or a |
| +// rollback's source is stuck at three times that; the next attempt, if |
| +// any, is a new cold admission into a fresh generation. |
| +func (w *world) probeAttemptFailed(b *box, c *claim) { |
| + id := c.Op.ID |
| + w.cas(c, func(n *claim) bool { |
| + if !sameOp(n.Op.ID, id) { |
| + return false |
| + } |
| + n.Op.ProbeTries++ |
| + switch n.Op.Kind { |
| + case "reverting": |
| + if n.Op.ProbeTries >= probeTries*3 { |
| + n.Op.RevPhase = "stuck" |
| + } |
| + case "restoring": |
| + if n.Op.ProbeTries >= probeTries*3 { |
| + n.Op.SrcPhase = "stuck" |
| + } |
| + } |
| + return true |
| + }) |
| + if cur := w.claim; cur != nil && sameOp(cur.Op.ID, id) && cur.Op.Kind == "landing" && cur.Op.ProbeTries >= probeTries { |
| + w.rollback(cur, "target would not start") |
| + } |
| + w.logf("box %d: probe attempt %d failed within its readiness window (%s/%s)", b.ID, w.claim.Op.ProbeTries, c.Op.Kind, id) |
| +} |
| + |
| // resumeStart is the agent's own loop finishing an admitted session's |
| // start (rev 7.11 §7.14): the activator process holds the admission and |
| // advances the stages without a wake, within the retry policy's backoff. |
| @@ -1223,10 +1315,14 @@ type admitInput struct { |
| // KeepStamp (claim rev 6.9.1): a cold admission keeps holder.stamp only |
| // when no writer was admitted since it was issued (stamp > session) |
| KeepStamp bool |
| - // BaselineCoversPredecessor (claim rev 6.9.1): the baseline is a seal |
| + // Coverage (claim rev 6.12) replaces rev 6.9.1's BaselineCoversPredecessor |
| // of the stopped predecessor, so nothing is lost and no writes_lost is |
| // recorded; the journal entry says baseline: sealed |
| - BaselineCoversPredecessor bool |
| + // "" (writes_lost unless certified), "sealed" (a from_db seal of the |
| + // stopped predecessor), "clean-return" (a clean rollback with |
| + // src_covered: the unchanged target and the source's complete replica |
| + // establish preservation, R11-4) |
| + Coverage string |
| } |
| // admitWriter decides the admission for a start on b under the claim it |
| @@ -1271,6 +1367,14 @@ func (w *world) admitWriter(b *box, c *claim, want string, probe bool) (admitInp |
| return a, true |
| } |
| a.Mode, a.NewGeneration = "cold", w.newID("rec") |
| + if c.Op.Kind == "restoring" && c.Op.DirtyKnown && !c.Op.Dirty && c.Op.LostAt == 0 && c.Op.SrcCovered && b.ID == c.Op.Src && h.Gen == c.Op.SrcGen && on("clean-return-identity") { |
| + // (a return made clean by a declared-lost target is not covered: |
| + // the target may have written, and its session is declared) |
| + // a clean rollback's return: the target wrote nothing and the |
| + // source's replica covered the stop, so the predecessor's writes |
| + // are preserved and nothing is declared (claim rev 6.12, R11-4) |
| + a.Coverage = "clean-return" |
| + } |
| return a, true |
| } |
| // the operation's prepared generation, opened for the first time; built |
| @@ -1285,16 +1389,20 @@ func (w *world) admitWriter(b *box, c *claim, want string, probe bool) (admitInp |
| if c.Op.Kind == "restoring" { |
| covers = c.Op.ReturnFromDB |
| } |
| - a.Mode, a.NewGeneration, a.BaselineCoversPredecessor = "cold", want, covers |
| + a.Mode, a.NewGeneration = "cold", want |
| + if covers { |
| + a.Coverage = "sealed" |
| + } |
| return a, true |
| } |
| -// lastWriter is the newest writers journal entry, or nil. |
| -func lastWriter(op *opState) *writerEntry { |
| - if len(op.Writers) == 0 { |
| +// lastAdmission is the newest entry of holder.admissions, or nil: the next |
| +// admission's predecessor (claim rev 6.12). |
| +func lastAdmission(h *holder) *admissionRecord { |
| + if h == nil || len(h.Admissions) == 0 { |
| return nil |
| } |
| - return &op.Writers[len(op.Writers)-1] |
| + return &h.Admissions[len(h.Admissions)-1] |
| } |
| // durableInLineage: W is durable in gen or one of its ancestors within loc. |
| @@ -1329,6 +1437,8 @@ func (w *world) admitCommit(b *box, c *claim, a admitInput) bool { |
| } |
| h := c.Holder |
| var lost, lostSrc *writesLost |
| + var last *admissionRecord // the last admitted writer before this CAS, the predecessor's identity (claim rev 6.12, R11-4) |
| + var entry admissionRecord |
| ok := w.cas(c, func(n *claim) bool { |
| if n.Holder == nil || n.Holder.Session != a.ObservedSession || n.Holder.Gen != a.ObservedGeneration { |
| return false |
| @@ -1349,14 +1459,29 @@ func (w *world) admitCommit(b *box, c *claim, a admitInput) bool { |
| if on("exec-writer") && n.Op.Exec != b.ID { |
| return false |
| } |
| + // the predecessor is the last writer in holder.admissions, with its |
| + // own session, box and generation; never the generation an |
| + // operation chose for the restore (claim rev 6.12, R11-4: a clean |
| + // return resets holder.generation to the source's, but the |
| + // predecessor is still the target's writer). The mutation takes |
| + // rev 7.11's holder fields and journals an identity that never |
| + // admitted a writer |
| + last = nil |
| + if l := lastAdmission(n.Holder); l != nil { |
| + cp := *l |
| + last = &cp |
| + } |
| + p := pred{Session: a.ObservedSession, Box: h.WriterBox, Gen: h.Gen, Stamp: h.Stamp} |
| + if last != nil && on("clean-return-identity") { |
| + p = pred{Session: last.Session, Box: last.Box, Gen: last.Gen, Stamp: last.Stamp} |
| + } |
| n.Holder.Session = w.nextGen() |
| n.Holder.WriterBox = b.ID |
| gen := a.NewGeneration |
| if a.Mode != "cold" { |
| gen = n.Holder.Gen |
| } |
| - e := writerEntry{Session: n.Holder.Session, Box: b.ID, Gen: gen, Stamp: n.Holder.Stamp, Mode: a.Mode, Baseline: "remote", |
| - Pred: pred{Session: a.ObservedSession, Box: h.WriterBox, Gen: h.Gen, Stamp: h.Stamp}} |
| + e := admissionRecord{Session: n.Holder.Session, Box: b.ID, Gen: gen, Stamp: n.Holder.Stamp, Mode: a.Mode, Coverage: a.Coverage, Predecessor: p} |
| if a.Mode == "cold" { |
| w.newGen(n.Holder.Location, h.Gen, a.NewGeneration) |
| n.Holder.Gen = a.NewGeneration |
| @@ -1371,10 +1496,11 @@ 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.BaselineCoversPredecessor { |
| - e.Baseline = "sealed" // nothing to declare: the seal holds every acknowledged write (claim rev 6.9.1) |
| - } else if !a.PredecessorCertified && on("writes-lost") { |
| - lost = &writesLost{Box: h.WriterBox, Gen: h.Gen, Session: h.Session, RemoteMaxTXID: a.RemoteMaxTXID} |
| + if a.Coverage == "" && !a.PredecessorCertified && 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 |
| + lost = &writesLost{Box: p.Box, Gen: p.Gen, Session: p.Session, RemoteMaxTXID: a.RemoteMaxTXID} |
| e.Lost = lost |
| } |
| 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") { |
| @@ -1383,9 +1509,9 @@ func (w *world) admitCommit(b *box, c *claim, a admitInput) bool { |
| // 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 _, p := range n.Op.Writers { |
| - if p.Box == n.Op.Src && p.Gen == n.Op.SrcGen { |
| - srcSession = p.Session |
| + for _, q := range n.Holder.Admissions { |
| + if q.Box == n.Op.Src && q.Gen == n.Op.SrcGen { |
| + srcSession = q.Session |
| } |
| } |
| lostSrc = &writesLost{Box: n.Op.Src, Gen: n.Op.SrcGen, Session: srcSession, RemoteMaxTXID: a.RemoteMaxTXID} |
| @@ -1395,7 +1521,7 @@ func (w *world) admitCommit(b *box, c *claim, a admitInput) bool { |
| // unfinished admission until generation.json names the new |
| // generation; the chore is queued then (claim rev 6.10, R10-2). |
| // The mutation of baseline-live queues it now, as rev 7.10 did |
| - if !on("baseline-live") && !a.BaselineCoversPredecessor { |
| + if !on("baseline-live") && a.Coverage != "sealed" { |
| ret := h.Gen |
| if ret == "" { |
| ret = "@root" |
| @@ -1403,7 +1529,8 @@ func (w *world) admitCommit(b *box, c *claim, a admitInput) bool { |
| 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.Op.Writers = append(n.Op.Writers, e) |
| + n.Holder.Admissions = append(n.Holder.Admissions, e) |
| + entry = e |
| return true |
| }) |
| if !ok { |
| @@ -1412,6 +1539,16 @@ func (w *world) admitCommit(b *box, c *claim, a admitInput) bool { |
| return false |
| } |
| w.stats["admissions: "+a.Mode]++ |
| + if last != nil && (entry.Predecessor.Session != last.Session || entry.Predecessor.Box != last.Box || entry.Predecessor.Gen != last.Gen) { |
| + // INV-16 (rev 7.12, R11-4): the journalled predecessor is the last |
| + // admitted writer; a tuple that never admitted a writer (the |
| + // target's session and box with the source's generation, after a |
| + // clean return) is a false record |
| + w.violate("INV-16: box %d journalled predecessor {session %d, box %d, generation %q}, but the last admitted writer was {session %d, box %d, generation %q}", b.ID, entry.Predecessor.Session, entry.Predecessor.Box, entry.Predecessor.Gen, last.Session, last.Box, last.Gen) |
| + } |
| + if a.Coverage != "" { |
| + w.stats["admissions covered: "+a.Coverage]++ |
| + } |
| switch w.claim.Op.Kind { |
| case "creating", "deleting", "parking", "purging", "placing": |
| // INV-13 (R9-4): no writer is admitted while the host is being |
diff --git a/internal/sim/hostlife/rules_test.go b/internal/sim/hostlife/rules_test.go| index 6db65b688..0d0faf225 100644 |
| --- a/internal/sim/hostlife/rules_test.go |
| +++ b/internal/sim/hostlife/rules_test.go |
| @@ -119,6 +119,7 @@ var allRules = []string{ |
| "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 |
| "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 1e8f88640..644977127 100644 |
| --- a/internal/sim/hostlife/sim_test.go |
| +++ b/internal/sim/hostlife/sim_test.go |
| @@ -455,8 +455,8 @@ func (w *world) owed(r int, k string) bool { |
| // pending chore's keys are (seeds 4159, 26817, 34163 / 100,000) |
| if h := c.Holder; h != nil && strings.HasPrefix(k, h.Location) { |
| g := genOf(h.Location, k) |
| - for i := range c.Op.Writers { |
| - if e := &c.Op.Writers[i]; e.Mode == "cold" && !e.Retired && e.Pred.Gen == g { |
| + for i := range c.Holder.Admissions { |
| + if e := &c.Holder.Admissions[i]; e.Mode == "cold" && !e.Covered && e.Predecessor.Gen == g { |
| return true |
| } |
| } |
| @@ -529,6 +529,34 @@ func (w *world) final() { |
| return |
| } |
| e := w.execBox(c) |
| + if !hasMain(e) && c.Op.Kind == "serving" && w.certificate(e, c) == nil { |
| + // the host is at rest after a session that did not certify: its |
| + // next wake is a cold admission that declares the acknowledged, |
| + // unuploaded writes (R10-6). Rev 7.11's oracle exempted them as a |
| + // prospective declaration, recording and alerting nothing; the |
| + // recovery admission is run for real now, then everything it |
| + // queued, and the writes are judged by what it declared |
| + w.stats["final: recovery admission run"]++ |
| + w.drive(400, func() bool { return hasMain(e) && e.open == nil }, func() { w.wake(e) }, w.actAll(), w.runConsole, w.recoveryPass, w.operator) |
| + if len(w.violations) > 0 { |
| + return |
| + } |
| + if !(hasMain(e) && e.open == nil) { |
| + w.stats["final: unverified prospective declaration"]++ |
| + w.logf("final: the recovery admission on box %d did not complete; its declaration is unverified", e.ID) |
| + } else { |
| + w.drive(calmSteps, w.quiescent, w.actAll(), w.runConsole, w.recoveryPass, w.operator) |
| + if len(w.violations) > 0 { |
| + return |
| + } |
| + if !w.quiescent() { |
| + w.violate("INV-3: no convergence after the final recovery admission: %s; %s%s", w.whyNotQuiescent(), w.state(), w.boxesState()) |
| + return |
| + } |
| + } |
| + c = w.claim |
| + e = w.execBox(c) |
| + } |
| if w.rec.Region != e.Region { |
| w.violate("claim/record: record region %d, claim serves from box %d in region %d", w.rec.Region, e.ID, e.Region) |
| } |
| @@ -549,26 +577,15 @@ func (w *world) final() { |
| defer w.pure("final oracle", before) |
| local := e.DB |
| if local == nil { |
| - local = w.restoreCalc(e.Region, c.Holder.Inc, c.Holder.Location, c.Holder.Gen) |
| - // the next admission would be cold if the session is uncertified, |
| - // and would declare the writer box's acknowledged, unuploaded |
| - // writes lost (R10-6: the faults exempt nothing themselves); the |
| - // oracle expects what that admission would serve |
| - if w.certificate(e, c) == nil { |
| - for i := range w.acks { |
| - x := &w.acks[i] |
| - if x.Box == c.Holder.WriterBox && x.Inc == c.Holder.Inc && x.Kind == "write" && !x.Exempt && !w.isDurable(x.W) { |
| - x.Exempt = true |
| - w.stats["final: writes the next admission would declare lost"]++ |
| - } |
| - } |
| - } |
| + local = w.restoreAsNext(e, c) |
| } |
| if local == nil { |
| w.violate("final: the serving box %d has no database and nothing to restore", e.ID) |
| return |
| } |
| - w.checkLocal(c, e, local) |
| + if w.stats["final: unverified prospective declaration"] == 0 || w.certificate(e, c) != nil { |
| + w.checkLocal(c, e, local) |
| + } |
| w.checkDurable(c, "final") |
| if w.lostAlert != w.stats["writes_lost declared"] { |
| w.violate("INV-14: %d writes_lost records, %d alerts delivered (R10-6)", w.stats["writes_lost declared"], w.lostAlert) |
diff --git a/internal/sim/hostlife/witness_test.go b/internal/sim/hostlife/witness_test.go| index 0673908ec..25e01bb76 100644 |
| --- a/internal/sim/hostlife/witness_test.go |
| +++ b/internal/sim/hostlife/witness_test.go |
| @@ -65,8 +65,8 @@ var witnesses = []witness{ |
| "a staging round completes after the landing's staging park acknowledged; retired at the seal rather than after the writers' horizon, the round is residue at the release (INV-10)", wStagingQuiet}, |
| {"claim-cas-opid", "claim-cas-opid,revalidate-before-effect", "store of app", |
| "redundant alone: a stalled source goroutine with the rollback's last read resumes after a purge claimed the host; revalidation stops it, and so does the op-id condition on its release CAS; with both gone the release overwrites the purge and the store is torn down under a serving host", wClaimCasOpID}, |
| - {"dirty-return", "dirty-return", "INV-15", |
| - "the target writes during its probe and replicates; the rollback is dirty and the return lane carries the write to the source; treated as clean, the source's admission declares a write lost that the host's remote holds and whose writer was never lost (INV-15, rev 7.11; rev 7.10 saw it as INV-2 on the serving database)", wDirtyReturn}, |
| + {"dirty-return", "dirty-return", "INV-2", |
| + "the target writes during its probe and replicates; the rollback is dirty and the return lane carries the write to the source; treated as clean with the source's replica covering the stop, the source's admission is covered clean-return, declares nothing, and the serving database lacks the target's write (INV-2 local at the final recovery, rev 7.12; rev 7.11 saw INV-15 at the declaration, rev 7.10 INV-2 on the serving database)", wDirtyReturn}, |
| {"commit-before-open", "commit-before-open", "INV-5", |
| "a public request reaches the target's edge while its probe runs; a row opened at the probe routes it before the commit (INV-5, R3-5)", wCommitBeforeOpen}, |
| {"exec-admission", "exec-admission,hold-op-open,start-check-claim-gen,exec-writer", "INV-1", |
| @@ -151,6 +151,10 @@ var witnesses = []witness{ |
| "a background worker acknowledges a write right after the app starts, and the box crashes before replication opens; admitted before the start, the acknowledgement is the session's and the next cold admission declares it; admitted after readiness (rev 7.10's order), it is in a database the next warm admission purges silently (claim rev 6.10, R10-1)", wAckBeforeAdmission}, |
| {"baseline-live", "baseline-live", "INV-2", |
| "a cold admission into a fresh generation; the box crashes before the first upload, so the generation is empty and the marker names the predecessor; the predecessor is the unfinished admission's baseline and stays live until the marker names the new generation; with the retire chore queued at the CAS, the predecessor is parked and the recovery restores nothing (claim rev 6.10, R10-2)", wBaselineParked}, |
| + {"clean-return-identity", "clean-return-identity", "INV-16", |
| + "a move's target is probed and writes nothing; the rollback is clean and the seal recorded src_covered; the source's re-admission journals the target's writer as its predecessor and coverage clean-return, declaring nothing; the mutation journals the target's session and box with the source's generation, a writer that never was, and declares a loss (claim rev 6.12, R11-4)", wCleanReturnIdentity}, |
| + {"baseline-live", "baseline-live", "INV-2", |
| + "an adopted host's origin replica holds durable writes and no generation.json; a cold admission into a fresh generation crashes before its first upload; the ordinary serving-time sweep runs before the recovery; with the absent marker read as the origin the chain protects it, and under the mutation the sweep parks the origin and the recovery restores nothing (R11-1)", wOriginSwept}, |
| {"seal-return", "seal-return", "INV-15", |
| "the source acknowledges a write whose upload is still in flight when the cut stops it: the seal carries the write, the source's replica does not; the landing is rolled back before its probe; the return must carry the seal, and treated as clean the source's cold admission declares the write lost while the landing's built generation holds it (rev 7.11 §7.8)", wSealReturn}, |
| {"close-evidence", "close-evidence", "certificate while", |
| @@ -2283,3 +2287,94 @@ func wSealReturn(t *testing.T, w *world) { |
| w.completeHeld(dataKey(loc, gen0, "")) |
| w.finish(t) |
| } |
| + |
| +// ---------- rev 7.12 ---------- |
| + |
| +// wCleanReturnIdentity (claim rev 6.12, R11-4): a clean rollback's return |
| +// and the identity the source's re-admission journals. |
| +func wCleanReturnIdentity(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.replicate(src) // the source's replica covers everything it acknowledged: src_covered at the seal |
| + w.landProbed(t, src, tgt) |
| + tl := lastAdmission(w.claim.Holder) |
| + if tl == nil || tl.Box != tgt.ID { |
| + t.Fatalf("witness: the target's probe is not the last admission: %s", w.state()) |
| + } |
| + tgtSession, tgtGen := tl.Session, tl.Gen |
| + if !w.claim.Op.SrcCovered { |
| + t.Fatalf("witness: the seal did not record src_covered: %s", w.state()) |
| + } |
| + w.rollback(w.claim, "settle check failed") // the target wrote nothing: a clean rollback |
| + before := w.stats["writes_lost declared"] |
| + w.reach(t, 800, "source re-admitted", func() bool { |
| + c := w.claim |
| + return len(w.violations) > 0 || c.Op.Kind == "serving" || c.Op.Kind == "restoring" && (c.Op.SrcPhase == "probed" || c.Op.SrcPhase == "opened") |
| + }, w.act(src, tgt), w.recoveryPass, w.runConsole) |
| + if len(w.violations) > 0 { |
| + return |
| + } |
| + e := lastAdmission(w.claim.Holder) |
| + if e == nil || e.Box != src.ID { |
| + t.Fatalf("witness: the source's re-admission is not the last admission: %s", w.state()) |
| + } |
| + if e.Predecessor.Session != tgtSession || e.Predecessor.Box != tgt.ID || e.Predecessor.Gen != tgtGen { |
| + w.violate("INV-16 (witness): the source journalled predecessor {session %d, box %d, generation %q}; the target's writer was {session %d, box %d, generation %q}", e.Predecessor.Session, e.Predecessor.Box, e.Predecessor.Gen, tgtSession, tgt.ID, tgtGen) |
| + return |
| + } |
| + if e.Coverage != "clean-return" || w.stats["writes_lost declared"] != before { |
| + w.violate("INV-16 (witness): a clean return with src_covered declared a loss (coverage %q, %d records)", e.Coverage, w.stats["writes_lost declared"]-before) |
| + return |
| + } |
| + w.finish(t) |
| +} |
| + |
| +// wOriginSwept (R11-1): origin, an unfinished admission, the ordinary |
| +// sweep, then the recovery. |
| +func wOriginSwept(t *testing.T, w *world) { |
| + b0 := w.boxes[0] |
| + w.legacy(b0, 1) |
| + w.tick(func() { w.reconcile(b0) }) // adoption |
| + if w.claim == nil { |
| + t.Fatalf("witness: not adopted") |
| + } |
| + w.reach(t, 400, "adoption settled", func() bool { return w.claim.oblFor("adopt") == 0 }, w.actAll(), w.recoveryPass) |
| + if len(w.violations) > 0 { |
| + return |
| + } |
| + // 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)) |
| + armed := true |
| + w.startHook = func(x *box) bool { |
| + if x != b0 || !armed { |
| + return false |
| + } |
| + armed = false |
| + w.crash(x) // before the first upload: the new generation is empty, the marker absent, the origin the baseline |
| + return true |
| + } |
| + w.wake(b0) // the first cold admission from the origin |
| + w.startHook = nil |
| + if g := w.claim.Holder.Gen; g == "" { |
| + t.Fatalf("witness: no cold admission happened: %s", w.state()) |
| + } |
| + // the ordinary sweep runs before any recovery: every box's obligation |
| + // runner, no wakes |
| + for i := 0; i < 3*horizonH; i++ { |
| + w.tick(func() { |
| + for _, b := range w.liveBoxes() { |
| + w.obligationRunner(b) |
| + } |
| + }) |
| + if len(w.violations) > 0 { |
| + return |
| + } |
| + } |
| + w.recovered(t, b0, "woken after the sweep") |
| + w.checkLocal(w.claim, b0, b0.DB) |
| + w.checkDurable(w.claim, "after the recovery") |
| + w.finish(t) |
| +} |
diff --git a/internal/sim/hostlife/world_test.go b/internal/sim/hostlife/world_test.go| index 8c287ba96..f561f61bd 100644 |
| --- a/internal/sim/hostlife/world_test.go |
| +++ b/internal/sim/hostlife/world_test.go |
| @@ -47,12 +47,17 @@ const ( |
| cutBudget = 320 // absolute cut deadline after admission |
| stagingTTL = 400 // staging-work lease TTL: longer than the cut budget, as in production |
| probeTries = 3 |
| - readyWait = 800 // abort a move whose readiness never comes |
| - maxSkew = 1 // a box clock is within this of true time |
| - maxPause = 3 // a typical pause between a check and the act (a VM freeze is longer) |
| - sigAge = 30 // S3's signature-age limit; H covers it plus the longest request |
| - beyondH = 20 // one long-tail request in this many completes after H (R2-1) |
| - retiredCap = 32 // retired_incarnations keeps this many (claim rev 6 §2) |
| + // 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 |
| + // the operation counts one of its budgeted tries (rev 7.12 §7.7) |
| + probeStartWindow = 30 |
| + readyWait = 800 // abort a move whose readiness never comes |
| + maxSkew = 1 // a box clock is within this of true time |
| + maxPause = 3 // a typical pause between a check and the act (a VM freeze is longer) |
| + sigAge = 30 // S3's signature-age limit; H covers it plus the longest request |
| + beyondH = 20 // one long-tail request in this many completes after H (R2-1) |
| + retiredCap = 32 // retired_incarnations keeps this many (claim rev 6 §2) |
| ) |
| // retire adds inc to retired_incarnations, dropping the oldest past the cap. |
| @@ -598,6 +603,14 @@ type holder struct { |
| // admission names as the current writer; it survives operation |
| // replacement, so a later cold admission's writes_lost names it (R9-2). |
| WriterBox int |
| + // Admissions is holder.admissions (claim rev 6.12): the record of writer |
| + // admissions whose chain is not yet finished or whose predecessors are |
| + // not yet queued for retirement, plus the last few covered ones; it |
| + // lives in the holder, so it survives every operation transition, |
| + // release and new operation. An admission's predecessor is always the |
| + // last entry here (session, box, generation), never the generation an |
| + // operation chose for a restore (R11-4) |
| + Admissions []admissionRecord |
| // Session is holder.session (claim rev 6.8 §6.4a, R8-1): the gen of the |
| // AdmitWriter CAS that admitted the current writer session. Every path |
| // that opens replication goes through that CAS, which moves the |
| @@ -623,18 +636,22 @@ type obligation struct { |
| Quiet int // not before |
| } |
| -// writerEntry is one AdmitWriter (claim rev 6.8 §6.4a): the session it |
| +// admissionRecord is one AdmitWriter (claim rev 6.8 §6.4a): the session it |
| // produced, the box and generation it admitted, the stamp, the mode (warm |
| // or cold), whether the writer has opened, and the predecessor it observed. |
| -type writerEntry struct { |
| +type admissionRecord struct { |
| Session, Box int |
| Gen string |
| Stamp int |
| Mode string // warm or cold (claim rev 6.9) |
| - Pred pred |
| + Predecessor pred |
| Lost *writesLost // a cold admission whose observed session had no certificate (claim rev 6.9, R9-2) |
| - Baseline string // remote, or sealed when a seal covers the stopped predecessor (claim rev 6.9.1, BaselineCoversPredecessor) |
| - Retired bool // this cold admission's predecessor has had its retire chore queued (by this writer's marker, or a successor's) |
| + // Coverage is the admission's coverage of its predecessor's writes |
| + // (claim rev 6.12): "" (uncovered: writes_lost unless certified), |
| + // "sealed" (a from_db seal), "clean-return" (a clean rollback with |
| + // src_covered). The entry always names it |
| + Coverage string |
| + Covered bool // this cold admission's predecessor has had its park-generation chore queued by a PublishGeneration (claim rev 6.12) |
| // 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 |
| @@ -670,6 +687,7 @@ type openState struct { |
| req *request |
| blob *blob // the first upload's or the anchor's bytes, captured once: a retry carries the same bytes (R10-7; seed 7574 / 30,000) |
| pendAt int // the pending writes the captured blob covers; later acknowledgements stay pending |
| + startedAt int // when the app stage first ran: a probe attempt's readiness window runs from here (rev 7.12 §7.7) |
| } |
| // writesLost is claim rev 6.9's writes_lost record: the writer whose |
| @@ -743,12 +761,9 @@ type opState struct { |
| RecVer int // a delete's or purge's intent: the record version it will DeleteIfMatch (claim §5.2 step 1, §5.3 step 4) |
| FlipGen int // the holder.stamp the flip CAS wrote: the landing's installation stamp (claim rev 6.5 §6.4) |
| SrcStamp int // the source installation's stamp before the flip, for the return to source (claim rev 6.5) |
| - // Writers is op.journal.writers (claim rev 6.9 §6.4a): one entry per |
| - // AdmitWriter CAS. It is the operation's, dropped with it; the writer's |
| - // box lives in holder.writer_box (R9-2). SrcGen is the source's |
| - // generation at the move's start, which a clean rollback's return CAS |
| - // names again (rev 7.10 §7.14). |
| - Writers []writerEntry |
| + // SrcGen is the source's generation at the cut (rev 7.10): a clean |
| + // rollback's return CAS names it again for the restore. Rev 7.11's |
| + // op.journal.writers moved to holder.admissions (claim rev 6.12) |
| SrcGen string |
| Committed bool |
| Opened bool |
| @@ -1033,11 +1048,13 @@ func (c *claim) clone() *claim { |
| } |
| n.Op.Parts = append([]int(nil), c.Op.Parts...) |
| n.Op.StopFiles = c.Op.StopFiles.clone() |
| - n.Op.Writers = append([]writerEntry(nil), c.Op.Writers...) |
| - for i := range n.Op.Writers { |
| - if l := n.Op.Writers[i].Lost; l != nil { |
| - cp := *l |
| - n.Op.Writers[i].Lost = &cp |
| + if c.Holder != nil { |
| + n.Holder.Admissions = append([]admissionRecord(nil), c.Holder.Admissions...) |
| + for i := range n.Holder.Admissions { |
| + if l := n.Holder.Admissions[i].Lost; l != nil { |
| + cp := *l |
| + n.Holder.Admissions[i].Lost = &cp |
| + } |
| } |
| } |
| n.Regions = append([]int(nil), c.Regions...) |