carlos / platform Public

hostlife model: two faults the 100,000-seed baseline found on rev 7.13

A lost target's every session since the cut is declared (seed 33373): a
probe session that certified and a warm continuation that did not are
two sessions; the first's writes are durable only in the lost target's
region and no return lane carries them. Rev 7.12's box-wide exemption
hid the first behind the record for the last; the session-scoped match
exposed it. admissionRecord.LostMore carries the extra records.

A predecessor that is the live generation again is left uncovered at
publication, no chore (seed 41914): covered, as claim rev 6.14 item 5's
first bullet reads, nothing retires it once a later admission supersedes
it, since that admission's predecessor is the last record rather than
the generation it restored from; the source's republished marker covered
the target's record while the source's generation was live again, and the
generation was residue at the end. A reading for the claim.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>

claude 2 weeks ago 8cdc8bbbebb74ab9b7f1e48a13fce64c139b3ec3 parent a2dc9b2

2 files changed, +40 −2

internal/sim/hostlife/protocol_test.go +36 −2
internal/sim/hostlife/world_test.go +4 −0

diff --git a/internal/sim/hostlife/protocol_test.go b/internal/sim/hostlife/protocol_test.go

index d94625e30..73bffb8b0 100644

--- a/internal/sim/hostlife/protocol_test.go

+++ b/internal/sim/hostlife/protocol_test.go

@@ -974,8 +974,17 @@ func (w *world) publishGeneration(b *box, c *claim, observedOpID, observedPhase

}

switch {

case e.Predecessor.Gen == published:

- e.Covered = true // the predecessor is the live generation again

- w.stats["publish: predecessor live"]++

+ // the predecessor is the live generation again (a clean

+ // return's source generation, a republished lagging marker):

+ // left uncovered, no chore. Covered here, as claim rev 6.14

+ // item 5's first bullet reads, nothing would retire it once a

+ // later admission supersedes it, since that admission's

+ // predecessor is the last record, not the generation it

+ // restored from (seed 41914 / 100,000: the source's

+ // republished marker covered the target's record while the

+ // source's generation was live again, and the generation was

+ // residue at the end; a reading for the claim)

+ w.stats["publish: predecessor live, left uncovered"]++

continue

case e.PredRegion < 0:

e.Covered = true // it holds nothing anywhere and no writer can add to it

@@ -1604,6 +1613,7 @@ func (w *world) admitCommit(b *box, c *claim, a admitInput) bool {

}

h := c.Holder

var lost, lostSrc *writesLost

+ var lostTgt []*writesLost

var last *admissionRecord // the last admitted writer before this CAS, the predecessor's identity (claim rev 6.12, R11-4)

var entry admissionRecord

ok := w.cas(c, func(n *claim) bool {

@@ -1685,6 +1695,22 @@ func (w *world) admitCommit(b *box, c *claim, a admitInput) bool {

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 && b.ID == n.Op.Src && on("writes-lost") {

+ // every session the lost target was admitted into since the

+ // cut is declared (rev 7.13; seed 33373 / 100,000): a probe

+ // session that certified and a warm continuation that did

+ // not are two sessions, the first's writes are durable only in

+ // the lost target's region, and no return lane carries either

+ // (§7.10). Rev 7.12's box-wide exemption hid the first behind

+ // the record for the last

+ lostTgt = nil

+ for _, q := range n.Holder.Admissions {

+ if q.Box == n.Op.Tgt && q.Session > n.Op.CutSession && (lost == nil || q.Session != lost.Session) {

+ lostTgt = append(lostTgt, &writesLost{Box: q.Box, Gen: q.Gen, Session: q.Session, RemoteMaxTXID: a.RemoteMaxTXID})

+ }

+ e.LostMore = lostTgt

+ }

if n.Op.Kind == "restoring" && n.Op.LostAt != 0 && !n.Op.SrcCovered && !n.Op.Dirty && b.ID == n.Op.Src && h.Gen == n.Op.SrcGen && on("writes-lost") {

// the return is clean only because the target was declared

// lost; the seal in its region was the one holder of the

@@ -1749,6 +1775,14 @@ 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)

}

+ for _, x := range lostTgt {

+ n := w.exemptDeclared(b, x, h, a.NewGeneration, true)

+ w.stats["writes_lost declared"]++

+ w.stats["writes declared lost"] += n

+ w.stats["writes_lost: another session of a lost target"]++

+ w.lostAlert++

+ w.alert("box %d: writes_lost {box %d, generation %q, session %d, remote_max_txid %d}: %d acknowledged writes (a session of the lost target since the cut)", b.ID, x.Box, x.Gen, x.Session, x.RemoteMaxTXID, n)

+ }

if lostSrc != nil {

n := w.exemptDeclared(b, lostSrc, h, a.NewGeneration, false)

w.stats["writes_lost declared"]++

diff --git a/internal/sim/hostlife/world_test.go b/internal/sim/hostlife/world_test.go

index 0b10aa0a8..a62d0e6e5 100644

--- a/internal/sim/hostlife/world_test.go

+++ b/internal/sim/hostlife/world_test.go

@@ -669,6 +669,10 @@ 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

}

// pred is the predecessor an admission journals: the session, writer box,