amadan

carlos / platform Public

sim: hostlife: clean-return coverage speaks for two sessions; per-region coverage in PublishGeneration; a probe's failing restore ends its attempt

Found by the rev 7.12 100,000-seed baseline. A clean-return coverage was
applied to a later session of the recovered source, whose uncertified
death then went undeclared (seed 95491): the coverage speaks for the
target's probe session and the source's cut session (op.CutSession)
only. A move's source generation, reached by the target's publication
through the chain, was marked covered by a chore in the target's region
that parked nothing, and the source's region never retired it (seeds
33646, 40148): a record is covered only when its predecessor's chore was
queued where the predecessor's objects are, or it holds none anywhere,
and no chore is queued for a generation absent from the publishing
region; a first fix that queued chores into the other regions parked the
source's own generation under a rollback (seeds 1036, 1296 / 3,000) and
was withdrawn. A probe whose restore cannot proceed within its window
fails the attempt like one whose app will not start.
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
claude 18d977ae940a76c8a43660e8eb8885846b925dc9 parent b6ed9f6
3 files changed, +66 −9
  • internal/sim/hostlife/moves_test.go +1 −0
  • internal/sim/hostlife/protocol_test.go +61 −9
  • internal/sim/hostlife/world_test.go +4 −0
diff --git a/internal/sim/hostlife/moves_test.go b/internal/sim/hostlife/moves_test.go
index a5d7131e5..cba286fdc 100644
--- a/internal/sim/hostlife/moves_test.go
+++ b/internal/sim/hostlife/moves_test.go
@@ -438,6 +438,7 @@ func (w *world) moveSource(b *box, c *claim) {
return false
}
n.Op.Phase, n.Op.StopAt, n.Op.StopDigest, n.Op.StopFiles = "stopped", w.now, d, files
+ n.Op.CutSession = n.Holder.Session // the session src_covered speaks for (rev 7.12)
n.Op.Repl, n.Op.Next = repl, next
n.Op.Exec = -1 // K3: the source gives up execution, citing its evidence
return true
diff --git a/internal/sim/hostlife/protocol_test.go b/internal/sim/hostlife/protocol_test.go
index ea7f2a9de..8c9cc3713 100644
--- a/internal/sim/hostlife/protocol_test.go
+++ b/internal/sim/hostlife/protocol_test.go
@@ -675,6 +675,16 @@ func (w *world) resumeOpen(b *box, c *claim, o *openState) bool {
if db == nil {
w.stats["restore refused"]++
w.logf("box %d: nothing to restore for a %s admission from %q", b.ID, o.Mode, o.Source)
+ if o.startedAt == 0 {
+ o.startedAt = w.now
+ }
+ if o.Probe && w.now-o.startedAt >= probeStartWindow {
+ // a probe attempt whose restore cannot proceed within its
+ // window fails like one whose app will not start (§7.7)
+ b.open = nil
+ w.stats["probe attempt failed: restore"]++
+ w.probeAttemptFailed(b, cur)
+ }
return false
}
w.logf("box %d restored %s: TXID %d at position %d, %d writes (%s admission into %q)", b.ID, dataKey(loc, o.Source, ""), db.TX, db.Pos, len(db.Log), o.Mode, o.Gen)
@@ -923,8 +933,19 @@ func (w *world) publishGeneration(b *box, c *claim, observedOpID, observedPhase
id = fmt.Sprintf("session:%d", session)
}
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
+ e := &n.Holder.Admissions[i]
+ if e.Mode != "cold" || e.Session > session || e.Covered {
+ continue
+ }
+ // covered: its predecessor is in this dead set (a chore in this
+ // region), or is the published generation, or holds no object in
+ // any region. A predecessor whose files live in another region
+ // (a move's source generation, seen by the target's publication)
+ // stays uncovered for that region's next PublishGeneration: a
+ // chore queued there from here would park a generation the
+ // rollback may still need (seeds 33646, 40148, 1296 / rev 7.12)
+ if e.Predecessor.Gen == published || !w.hasFilesAnywhere(n.Holder.Location, e.Predecessor.Gen) || hasStr(dead, e.Predecessor.Gen) && w.hasFilesIn(region, n.Holder.Location, e.Predecessor.Gen) {
+ e.Covered = true
}
}
var keep []admissionRecord
@@ -940,22 +961,25 @@ func (w *world) publishGeneration(b *box, c *claim, observedOpID, observedPhase
keep = append([]admissionRecord{e}, keep...)
}
n.Holder.Admissions = keep
- next:
for _, retire := range dead {
- if retire == published {
- continue
+ if retire == published || !w.hasFilesIn(region, n.Holder.Location, retire) {
+ continue // nothing of it here: an empty generation, or one whose objects are another region's
}
ret := retire
if ret == "" {
ret = "@root" // the sentinel for the origin generation (claim rev 6.10)
}
+ queued := false
for _, o := range n.Obl {
if o.Kind == "park-generation" && o.Region == region && o.Ret == ret && o.Prefix == n.Holder.Location {
- continue next // already queued
+ queued = true // already queued
}
}
+ if queued {
+ continue
+ }
oid := newID
- if k := len(n.Obl); k > 0 && n.Obl[k-1].ID == oid || hasObl(n.Obl, oid) {
+ 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: region, Box: -1, Prefix: n.Holder.Location, Ret: ret, Quiet: w.now + horizonH})
@@ -964,6 +988,28 @@ func (w *world) publishGeneration(b *box, c *claim, observedOpID, observedPhase
})
}
+// hasFilesIn is hasFiles for a region.
+func (w *world) hasFilesIn(r int, loc, gen string) bool {
+ for _, k := range w.buckets[r].keys(dataKey(loc, gen, "")) {
+ if genOf(loc, k) == gen {
+ return true
+ }
+ }
+ return false
+}
+
+// hasFilesAnywhere: the generation holds an object in some region.
+func (w *world) hasFilesAnywhere(loc, gen string) bool {
+ for r := range w.buckets {
+ for _, k := range w.buckets[r].keys(dataKey(loc, gen, "")) {
+ if genOf(loc, k) == gen {
+ return true
+ }
+ }
+ }
+ return false
+}
+
func hasObl(obl []obligation, id string) bool {
for _, o := range obl {
if o.ID == id {
@@ -1357,6 +1403,7 @@ func (w *world) admitWriter(b *box, c *claim, want string, probe bool) (admitInp
bk := w.buckets[b.Region]
a.RemoteMaxTXID = w.remoteMax(bk, dataKey(h.Location, h.Gen, ""))
a.PredecessorCertified = w.certificate(b, c) != nil
+
if want == "" || want == h.Gen || w.ancestorGen(h.Location, h.Gen, want) {
// holder.generation, or an operation's prepared generation that a
// writer already opened (it is holder.generation or an ancestor of
@@ -1367,9 +1414,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") {
+ if l := lastAdmission(h); 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 &&
+ l != nil && (l.Box == c.Op.Tgt || l.Session == c.Op.CutSession) && 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)
+ // the target may have written, and its session is declared; and
+ // only the target's probe session or the source's own cut
+ // session is covered by the seal's src_covered: a later session
+ // of the recovered source that dies uncertified is declared as
+ // any other, seed 95491 / 100,000)
// 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)
diff --git a/internal/sim/hostlife/world_test.go b/internal/sim/hostlife/world_test.go
index f561f61bd..fdea52508 100644
--- a/internal/sim/hostlife/world_test.go
+++ b/internal/sim/hostlife/world_test.go
@@ -743,6 +743,10 @@ type opState struct {
// rollback may restore the source from it; otherwise the seal holds
// writes the replica does not, and the return carries the seal
SrcCovered bool
+ // CutSession (rev 7.12) is holder.session at the cut's stop: the
+ // source's session whose writes src_covered speaks for; a clean return's
+ // coverage applies to it and to the target's probe session only
+ CutSession int
// SealFromDB (rev 7.11): the seal was built from the stopped database
// itself, every page of it, so it covers every write the predecessor
// acknowledged; false when the disk was gone and the seal is the