carlos / platform Public

sim: hostlife: a clean close is refused while an escapee runs or when its certificate PUT is not acknowledged; a resumed step carries the stamp active now; strict-spawn caught alone

Found by the second rev 7.10 100,000-seed baseline: a close waiting for an
escaped descendant, and one waiting for a certificate PUT late by three
horizons, held a revert's probe until it stuck (seed 97950); a stalled
probe step carried the stamp active at its read, before a cold admission's
installing CAS, and the box's record refused its own probe (seed 67671).
The strict-spawn mutation is caught alone by the sweep now (a descendant
surviving the idle stop acknowledges writes the purge then loses), so its
expected-miss line goes.

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

claude 2 weeks ago 572066eced619a1eb711d97b05ee64533d0a6f76 parent 5b7cf1d

3 files changed, +37 −6

internal/sim/hostlife/expected-outcomes.txt +0 −1
internal/sim/hostlife/ltx_test.go +29 −4
internal/sim/hostlife/moves_test.go +8 −1

diff --git a/internal/sim/hostlife/expected-outcomes.txt b/internal/sim/hostlife/expected-outcomes.txt

index cfb23c5e5..5bbbdea22 100644

--- a/internal/sim/hostlife/expected-outcomes.txt

+++ b/internal/sim/hostlife/expected-outcomes.txt

@@ -12,7 +12,6 @@ exec-admission missed one of four admission fences (claim rev 6.8.1 adds exec-wr

hold-op-open missed one of four admission fences; caught with exec-admission, start-check-claim-gen and exec-writer

start-check-claim-gen missed one of four admission fences; caught with exec-admission, hold-op-open and exec-writer

start-check missed subsumed since rev 7.10: a box restores only its own region's remote of holder.generation, so with the whole start check gone the stale source of a cross-region move finds nothing to restore and cannot start beside the target; the witness is retired, the generation clause (start-check-claim-gen) keeps its witness

-strict-spawn missed caught with evidence-whole-tree

touched-incomplete missed caught with legacy-discovery

door-reread missed subsumed by C3a and, since rev 7.8, by writer epochs (claim rev 6.6): a recreated incarnation writes into a fresh generation the listing never selects; its witness is retired

door-by-version missed subsumed by C3a and, since rev 7.8, by writer epochs (claim rev 6.6): a recreated incarnation writes into a fresh generation the listing never selects; its witness is retired

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

index 766d2245a..0c486368e 100644

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

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

@@ -362,11 +362,21 @@ func (db *localDB) settled(now int) bool {

// stops.

func (w *world) closeStep(b *box) {

db := b.DB

- if db == nil || !db.Closing || len(b.Procs) > 0 {

+ if db == nil || !db.Closing || hasMain(b) {

+ return

+ }

+ if len(b.Procs) > 0 {

// nothing of the host may run when the session certifies: a

- // descendant that outlived the main process can still acknowledge

- // writes the certificate would not cover, which the next admission's

- // purge would lose silently (rev 7.10; seed 17 / 300)

+ // descendant that outlived the unit stop (an escapee outside the

+ // cgroup) can still acknowledge writes the certificate would not

+ // cover, which the next admission's purge would lose silently (rev

+ // 7.10; seed 17 / 300). The close is refused, not delayed: the

+ // session stays uncertified, the next wake is cold and declares

+ // (seed 97950 / 100,000: a close that waited for an escapee held

+ // the revert's probe until it stuck)

+ db.Closing, db.CloseReq = false, nil

+ w.stats["clean close refused: a process still runs"]++

+ w.logf("box %d: clean close refused, a descendant of the host still runs", b.ID)

return

}

// the certificate is the live generation's: once an operation has

@@ -396,7 +406,11 @@ func (w *world) closeStep(b *box) {

// is unknown for good, so this session never certifies

db.Closing = false

w.stats["clean close refused: uncertain"]++

+ w.logf("box %d: clean close refused, the session is uncertain", b.ID)

+ return

}

+ inflight := db.InFlight != nil && !db.InFlight.done

+ w.logf("box %d: clean close waits (queue %d, upload in flight %v, %d requests tracked)", b.ID, len(db.Queue), inflight, len(db.Issued))

return

}

if db.CloseReq == nil {

@@ -407,6 +421,17 @@ func (w *world) closeStep(b *box) {

}

if db.CloseReq.done {

db.Closing, db.CloseReq = false, nil

+ } else if w.now-db.CloseReq.at >= uploadTimeout {

+ // the certificate PUT itself was not acknowledged within the

+ // client's wait: the close ends without a certificate the box can

+ // rely on; the PUT may still land, and a later wake that finds it

+ // may continue warm, since its content is right (the drain was

+ // complete); meanwhile the next wake is cold (seed 97950 / 100,000:

+ // a certificate PUT late by three horizons held the revert's probe

+ // until it stuck)

+ db.Closing, db.CloseReq = false, nil

+ w.stats["clean close: certificate not acknowledged"]++

+ w.logf("box %d: the certificate PUT was not acknowledged; the close ends uncertified", b.ID)

}

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

index 66d3029b2..5cc2902b4 100644

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

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

@@ -135,7 +135,14 @@ func (w *world) resumeStale(b *box, old *claim) {

if on("revalidate-before-effect") && !sameStep(old, c) {

return

}

- w.role(b, old.clone())

+ // the revalidation re-reads the box's own record as well: the stamp the

+ // resumed step carries is the one active now (claim rev 6.5 §6.4; seed

+ // 67671 / 100,000: a stalled probe step carried the stamp active at its

+ // read, before a cold admission's installing CAS, and the box's record

+ // refused its own probe)

+ old = old.clone()

+ old.readStamp = c.readStamp

+ w.role(b, old)

}

// role is the worker's exec-lease renewal, quarantine and operation role,