carlos / platform Public

sim: hostlife: an abandoned cold admission is parked by the next op.exec; a writer inside an operation certifies its close; diagnostics

Found by the 100,000-seed baseline of rev 7.9's first model: a lost
target's unfinished cold admission inside the landing blocked the
source's rollback probe for good (seed 58795), and every clean close
outside serving was dropped, so a rollback's reopened source was admitted
cold at every wake and the rollback never released (seed 84087). The
close is dropped only for a push, a move's cut, a delete or a purge (the
first correction let a push's writer certify into the superseded
generation, seed 4493 / 30,000). Logs for a refused admission, a failed
rollback probe, a skipped obligation run and each park-local step.
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
claude agent, operated by paul@keymail.dev dfc352ef36d5fc41c594a19d5eccb209753d1ea2 parent 866c588
4 files changed, +56 −5
  • internal/sim/hostlife/ltx_test.go +17 −4
  • internal/sim/hostlife/moves_test.go +27 −0
  • internal/sim/hostlife/protocol_test.go +10 −1
  • internal/sim/hostlife/world_test.go +2 −0
diff --git a/internal/sim/hostlife/ltx_test.go b/internal/sim/hostlife/ltx_test.go
index 68065a9a4..4bcd5f384 100644
--- a/internal/sim/hostlife/ltx_test.go
+++ b/internal/sim/hostlife/ltx_test.go
@@ -346,10 +346,23 @@ func (w *world) closeStep(b *box) {
if db == nil || !db.Closing || hasMain(b) {
return
}
- // the marker is the live generation's: once an operation has taken the
- // writer over (a push, a move, a delete), or the claim has moved on,
- // the generation is dead or being replaced and the close is dropped
- if c := w.claim; c == nil || c.Holder == nil || c.Op.Kind != "serving" || c.Op.Exec != b.ID || c.Holder.Gen != db.Gen || c.Holder.Inc != db.Inc {
+ // the certificate is the live generation's: once an operation has
+ // taken the writer over (a push, a move, a delete), or the claim has
+ // moved on, the generation is dead or being replaced and the close is
+ // dropped. A writer running inside an operation (a landing's probe or
+ // its committed target, a rollback's reopened source, a push's probe)
+ // certifies like any other (claim rev 6.8 §6.4a; seed 84087 / 100,000:
+ // rev 7.9's first build dropped every close outside serving, so a
+ // rollback's source was admitted cold at every wake and the rollback
+ // never released)
+ c := w.claim
+ inside := c != nil && (c.Op.Kind == "serving" || c.Op.Kind == "landing" || c.Op.Kind == "restoring" || c.Op.Kind == "reverting")
+ if c == nil || c.Holder == nil || !inside || c.Op.Exec != b.ID || c.Holder.Inc != db.Inc || (db.Gen != c.Holder.Gen && db.Gen != w.opGen(&c.Op)) {
+ // a push, a move's cut, a delete or a purge is taking this writer
+ // over: its generation is being replaced or parked, and a
+ // certificate written into it now would outlive the park (seed
+ // 4493 / 30,000: a certificate landed in a generation a push had
+ // superseded)
db.Closing, db.CloseReq = false, nil
return
}
diff --git a/internal/sim/hostlife/moves_test.go b/internal/sim/hostlife/moves_test.go
index 34afc0581..e79640d55 100644
--- a/internal/sim/hostlife/moves_test.go
+++ b/internal/sim/hostlife/moves_test.go
@@ -21,10 +21,16 @@ func (w *world) workerMode(b *box, obl bool) {
}
c, ok := w.readClaim(b)
if !ok {
+ if obl && w.claim != nil && len(w.claim.Obl) > 0 && w.calm {
+ w.logf("box %d: obligation run skipped, the agent cannot read the claim (down=%v paused=%v frozen=%v partitioned=%v destroyed=%v)", b.ID, b.AgentDown, b.AgentPaused, b.Frozen, b.Partitioned, b.Destroyed)
+ }
return
}
if obl {
if c == nil || (contains(c.Lost, b.ID) && on("lost-quarantine")) {
+ if c != nil && w.calm {
+ w.logf("box %d: obligation run refused, the box is declared lost", b.ID)
+ }
return
}
for _, o := range c.Obl {
@@ -166,6 +172,26 @@ func (w *world) role(b *box, c *claim) {
if c.Holder == nil {
return
}
+ if r := c.Op.Rec; r != nil && r.Box != c.Op.Exec && (c.Op.Exec == b.ID || c.Op.Exec == -1 && w.isParticipant(c, b)) {
+ // the admitting box lost op.exec before its build finished (a
+ // rollback's release of the target, a declared loss): its cold
+ // admission is abandoned by whoever holds op.exec next, and the
+ // generation it was building is parked as a chore (seed 58795 /
+ // 100,000: the source's rollback probe could not be admitted behind
+ // the lost target's build)
+ if w.cas(c, func(n *claim) bool {
+ if n.Op.Rec == nil || n.Op.Rec.Gen != r.Gen || n.Op.Rec.Box == n.Op.Exec {
+ return false
+ }
+ n.Obl = append(n.Obl, w.newObl(n, "park-generation", r.Region, -1, c.Holder.Location, r.Gen, w.now+horizonH))
+ n.Op.Rec = nil
+ return true
+ }) {
+ w.logf("box %d: cold admission %s of box %d abandoned, its exec is gone (op %s/%s exec %d)", b.ID, r.Gen, r.Box, c.Op.Kind, c.Op.ID, c.Op.Exec)
+ w.stats["cold admissions abandoned"]++
+ }
+ return
+ }
if c.Op.Rec != nil && c.Op.Rec.Box == b.ID {
// a cold admission's build runs under the operation, by the box it
// admitted, before the operation's own step (claim rev 6.8 §6.4a, R8-2)
@@ -1326,6 +1352,7 @@ func (w *world) recoverSource(b *box, c *claim) {
w.cas(c, func(n *claim) bool { n.Op.SrcPhase = "probed"; return sameOp(n.Op.ID, op.ID) })
return
}
+ w.logf("box %d: the rollback's probe did not start (try %d, generation %q, db=%v)", b.ID, op.ProbeTries+1, want, b.DB != nil)
w.cas(c, func(n *claim) bool {
n.Op.ProbeTries++
if n.Op.ProbeTries >= probeTries*3 {
diff --git a/internal/sim/hostlife/protocol_test.go b/internal/sim/hostlife/protocol_test.go
index 7e6b8b1ed..49f0a1294 100644
--- a/internal/sim/hostlife/protocol_test.go
+++ b/internal/sim/hostlife/protocol_test.go
@@ -386,6 +386,7 @@ func (w *world) spawn(b *box, c *claim, want string, probe bool) bool {
w.closeStep(b)
if b.DB.Closing {
w.stats["wake waited for a clean close"]++
+ w.logf("box %d: start waits for the previous session's clean close", b.ID)
return false
}
}
@@ -597,6 +598,7 @@ func (w *world) admitWriter(b *box, c *claim, gen string, probe bool) string {
h := c.Holder
if on("exec-writer") && c.Op.Exec != b.ID {
w.stats["admission refused: not op.exec"]++
+ w.logf("box %d: admission refused, op.exec is %d (%s/%s)", b.ID, c.Op.Exec, c.Op.Kind, c.Op.ID)
return ""
}
if !on("admit-everywhere") && c.Op.Kind != "serving" {
@@ -626,7 +628,7 @@ func (w *world) admitWriter(b *box, c *claim, gen string, probe bool) string {
n.Holder.Session = w.nextGen()
p := pred{Session: h.Session, Box: w.predBox(c), Gen: gen, Stamp: h.Stamp}
n.Op.Writers = append(n.Op.Writers, writerEntry{Session: n.Holder.Session, Box: b.ID, Gen: id, Mode: "cold", Pred: p})
- n.Op.Rec = &recState{Gen: id, Base: gen, Session: n.Holder.Session, Box: b.ID, Phase: "build", Pred: p}
+ n.Op.Rec = &recState{Gen: id, Base: gen, Session: n.Holder.Session, Box: b.ID, Region: b.Region, Phase: "build", Pred: p}
w.newGen(n.Holder.Location, gen, id)
if gen == n.Holder.Gen {
n.Holder.Gen = id // the claim's generation moves with the writer it admits
@@ -672,6 +674,8 @@ func (w *world) admitCommit(b *box, c *claim, gen, mode string) bool {
})
if ok {
w.stats["admissions: "+mode]++
+ } else {
+ w.logf("box %d: %s admission CAS refused (session %d, op %s/%s exec %d)", b.ID, mode, h.Session, c.Op.Kind, c.Op.ID, c.Op.Exec)
}
return ok
}
@@ -1010,6 +1014,7 @@ func (w *world) doObligation(b *box, c *claim, o obligation) {
switch o.Kind {
case "park-local":
if !w.evidence(b, o.Op) {
+ w.logf("box %d: park-local %s waits for stop evidence", b.ID, o.ID)
return
}
inc := 0
@@ -1020,8 +1025,12 @@ func (w *world) doObligation(b *box, c *claim, o obligation) {
inc = b.DB.Inc
}
if !w.localPark(b, inc) {
+ if w.calm {
+ w.logf("box %d: park-local %s parked an artifact of inc %d (stamp %d, db=%v files=%v cfg=%d live=%q)", b.ID, o.ID, inc, b.stampOf(inc), b.DB != nil, b.Files != nil, b.Config, b.Live)
+ }
return // the next artifact on a later step
}
+ w.logf("box %d: park-local %s done", b.ID, o.ID)
if b.Row != nil && b.Row.HoldOp == o.Op || b.Row != nil && (c.Holder == nil || b.ID != c.Op.Exec) {
b.Row = nil
}
diff --git a/internal/sim/hostlife/world_test.go b/internal/sim/hostlife/world_test.go
index 5853375d5..d321f3ad9 100644
--- a/internal/sim/hostlife/world_test.go
+++ b/internal/sim/hostlife/world_test.go
@@ -614,6 +614,8 @@ type pred struct {
// session and box admitted, the phase, the predecessor, and the snapshot
// identity once written.
type recState struct {
+ Region int // the admitting box's region, where the generation under construction lives
+
Gen, Base string
Session, Box int
Phase string