amadan

carlos / platform Public

sim: hostlife: a clean return behind a declared-lost target declares the source's cut session too

Found by the rev 7.11 30,000-seed baseline (seeds 16395 and 27191): the
target was declared lost, the console's release made the return clean,
and the seal in the lost target's region was the one holder of the
writes the source acknowledged in its cut session beyond its own
replica (src_covered false). The source's re-admission from its own
generation declared only the target's session; the source's writes went
undeclared and the serving database differed from the acknowledged
writes. The admission now records a second writes_lost for the source's
cut session (journal entry LostSrc), declares those writes and alerts.
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
claude d076b65683ec886a114677a387fcf24e3ad375fc parent d1c7b83
2 files changed, +36 −1
  • internal/sim/hostlife/protocol_test.go +30 −1
  • internal/sim/hostlife/world_test.go +6 −0
diff --git a/internal/sim/hostlife/protocol_test.go b/internal/sim/hostlife/protocol_test.go
index 68f14c928..7520c15e0 100644
--- a/internal/sim/hostlife/protocol_test.go
+++ b/internal/sim/hostlife/protocol_test.go
@@ -1328,7 +1328,7 @@ func (w *world) admitCommit(b *box, c *claim, a admitInput) bool {
return true
}
h := c.Holder
- var lost *writesLost
+ var lost, lostSrc *writesLost
ok := w.cas(c, func(n *claim) bool {
if n.Holder == nil || n.Holder.Session != a.ObservedSession || n.Holder.Gen != a.ObservedGeneration {
return false
@@ -1377,6 +1377,20 @@ func (w *world) admitCommit(b *box, c *claim, a admitInput) bool {
lost = &writesLost{Box: h.WriterBox, Gen: h.Gen, Session: h.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") {
+ // the return is clean only because the target was declared
+ // lost; the seal in its region was the one holder of the
+ // source's writes beyond its own replica, and no lane brings
+ // them: the source's cut session is declared too (§7.10)
+ srcSession := 0
+ for _, p := range n.Op.Writers {
+ if p.Box == n.Op.Src && p.Gen == n.Op.SrcGen {
+ srcSession = p.Session
+ }
+ }
+ lostSrc = &writesLost{Box: n.Op.Src, Gen: n.Op.SrcGen, Session: srcSession, RemoteMaxTXID: a.RemoteMaxTXID}
+ e.LostSrc = lostSrc
+ }
// no retire chore here: the predecessor is the baseline of an
// unfinished admission until generation.json names the new
// generation; the chore is queued then (claim rev 6.10, R10-2).
@@ -1437,6 +1451,21 @@ func (w *world) admitCommit(b *box, c *claim, a admitInput) bool {
w.lostAlert++
w.alert("box %d: writes_lost {box %d, generation %q, session %d, remote_max_txid %d}: %d acknowledged writes", b.ID, lost.Box, lost.Gen, lost.Session, lost.RemoteMaxTXID, n)
}
+ if lostSrc != nil {
+ n := 0
+ for i := range w.acks {
+ x := &w.acks[i]
+ if x.Box == lostSrc.Box && x.Inc == h.Inc && x.Kind == "write" && !x.Exempt && !w.durableInLineage(h.Location, a.NewGeneration, x.W) {
+ x.Exempt = true
+ n++
+ }
+ }
+ w.stats["writes_lost declared"]++
+ w.stats["writes declared lost"] += n
+ w.stats["writes_lost: source session behind a lost target"]++
+ w.lostAlert++
+ w.alert("box %d: writes_lost {box %d, generation %q, session %d, remote_max_txid %d}: %d acknowledged writes (the seal in the lost target's region held them)", b.ID, lostSrc.Box, lostSrc.Gen, lostSrc.Session, lostSrc.RemoteMaxTXID, n)
+ }
return true
}
diff --git a/internal/sim/hostlife/world_test.go b/internal/sim/hostlife/world_test.go
index 59e8415d4..8c287ba96 100644
--- a/internal/sim/hostlife/world_test.go
+++ b/internal/sim/hostlife/world_test.go
@@ -635,6 +635,12 @@ type writerEntry struct {
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)
+ // LostSrc (rev 7.11): a rollback's source re-admitted from its own
+ // generation after the target was declared lost while the seal was the
+ // one holder of the source's writes beyond its replica (src_covered
+ // false): those writes, acknowledged in the source's cut session, are
+ // declared too (seeds 16395 and 27191 / 30,000)
+ LostSrc *writesLost
}
// pred is the predecessor an admission journals: the session, writer box,