amadan

carlos / platform Public

sim: hostlife: a crash may take the disk, witnesses for evidence-whole-tree and timer-freeze, a nil guard in the clean close

The agent-crash fault loses the disk in one case in three while the host
is serving, so the random sweep reaches the writer-epoch hazard: a dead
writer's upload in flight across a replacement. Two rules the rev 7.8
sweep no longer caught at 3,000 seeds get deterministic witnesses: an
adopted legacy host with an escaped descendant whose move must take
evidence of the whole tree, and a registered timer whose refused
deliveries while the row is held must not advance the runner's
bookkeeping. idleStop no longer dereferences a database a stale step
destroyed.
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
claude 0d389d1b6fc2a733886cd554cf7eeecf60f09724 parent 15f2fa1
2 files changed, +57 −2
  • internal/sim/hostlife/background_test.go +18 −2
  • internal/sim/hostlife/witness_test.go +39 −0
diff --git a/internal/sim/hostlife/background_test.go b/internal/sim/hostlife/background_test.go
index c5f5555ca..d4504dc17 100644
--- a/internal/sim/hostlife/background_test.go
+++ b/internal/sim/hostlife/background_test.go
@@ -46,8 +46,10 @@ func (w *world) idleStop(b *box) {
}
b.Procs = keep
// the clean close (claim rev 6.6 §6.4a): drain, then closed.json
- b.DB.Closing = true
- w.closeStep(b)
+ if b.DB != nil {
+ b.DB.Closing = true
+ w.closeStep(b)
+ }
}
// wake: a request reaches this box's edge for the host.
@@ -343,6 +345,20 @@ func (w *world) fault() {
b.Procs = keep
b.forget()
w.logf("box %d agent crashed", b.ID)
+ // a crash that takes the disk with it (an instance replaced, a
+ // volume gone): the writer's uploads may still be in flight,
+ // which is the writer-epoch hazard (claim rev 6.6 §6.4a, R7-1)
+ if c := w.claim; w.fail["disk"] && c != nil && c.Holder != nil && c.Op.Kind == "serving" && c.Op.Exec == b.ID && b.DB != nil && w.rng.Intn(3) == 0 {
+ for i := range w.acks {
+ a := &w.acks[i]
+ if a.Box == b.ID && a.Inc == b.DB.Inc && !w.isDurable(a.W) {
+ a.Exempt = true
+ }
+ }
+ b.DB = nil
+ w.stats["disk-lost with the crash"]++
+ w.logf("box %d lost its disk with the crash", b.ID)
+ }
} else {
b.AgentDown = false
}
diff --git a/internal/sim/hostlife/witness_test.go b/internal/sim/hostlife/witness_test.go
index 5b52049c7..d38c2d0bc 100644
--- a/internal/sim/hostlife/witness_test.go
+++ b/internal/sim/hostlife/witness_test.go
@@ -125,6 +125,10 @@ var witnesses = []witness{
"a clean stop with an upload still in flight: closed.json is written only once the upload returned; written at once, the marker vouches for an upload that may still fail or land late (claim rev 6.6 §6.4a)", wCloseWaits},
{"newest-l0", "newest-l0", "newest level-0",
"the local position runs ahead of the uploads; two compactions and snapshot rotations later, retention below the previous snapshot would remove the newest uploaded level-0 file, which litestream never does (R7-3)", wNewestL0},
+ {"evidence-whole-tree", "evidence-whole-tree", "INV-1",
+ "an adopted legacy host runs a descendant outside the cgroup; the move's stop evidence must cover the whole tree, or the escaped descendant survives the cut and two boxes run the host (§6.1, J-D3)", wEvidenceWholeTree},
+ {"timer-freeze", "timer-freeze", "stuck",
+ "the source has a registered timer; the move stops and holds it; the runner's refused deliveries while held must not advance its bookkeeping, or a clean rollback's digest check finds the timers changed and the source is stuck (J-N14)", wTimerFreeze},
{"build-completion", "build-completion", "before its snapshot",
"a push's build with its snapshot PUT, then its anchor PUT, held, and the agent crashing in between: generation.json is published only once both are acknowledged; published from the intent it names artifacts that have not landed (R7-4)", wBuildCrashes},
}
@@ -1683,3 +1687,38 @@ func wBuildCrashes(t *testing.T, w *world) {
w.replicate(b)
w.finish(t)
}
+
+// wEvidenceWholeTree (§6.1): a legacy host adopted with a descendant that
+// escaped the cgroup; the move cuts.
+func wEvidenceWholeTree(t *testing.T, w *world) {
+ b0, b1 := w.boxes[0], w.boxes[1]
+ w.legacy(b0, 1)
+ w.tick(func() { w.reconcile(b0) }) // adoption
+ if w.claim == nil {
+ t.Fatalf("witness: not adopted")
+ }
+ w.reach(t, 400, "adoption settled", func() bool { return w.claim.oblFor("adopt") == 0 }, w.actAll(), w.recoveryPass)
+ if !hasMain(b0) {
+ w.recovered(t, b0, "running after adoption")
+ }
+ b0.Procs = append(b0.Procs, &proc{Main: false, Strict: false, Inc: 1, Box: b0.ID}) // an escaped descendant
+ w.moveTo(b1.Region)
+ w.finish(t)
+}
+
+// wTimerFreeze (J-N14): a timer registered on the source, a move that
+// holds the row, refused deliveries, then a clean rollback whose verify
+// compares the timer digest with the one recorded at the stop.
+func wTimerFreeze(t *testing.T, w *world) {
+ src, tgt := w.boxes[0], w.boxes[1]
+ w.serve(src, 1, app0)
+ w.nextW++
+ src.Timers = []int{w.nextW}
+ w.acks = append(w.acks, ack{W: w.nextW, Inc: 1, Box: src.ID, At: w.now, Kind: "timer"})
+ w.landProbed(t, src, tgt) // the source is stopped and its row held
+ for i := 0; i < 3; i++ {
+ w.runner(src) // deliveries refused while the row is held
+ }
+ w.rollback(w.claim, "settle check failed") // clean: the target wrote nothing
+ w.finish(t)
+}