carlos / platform Public

sim: hostlife: a crash that takes the disk takes every process with it

Seed 50672 of 100,000: a nested descendant survived the crash-with-disk
fault and acknowledged writes into no database, which the oracle rightly
reported as lost. Nothing survives a lost volume. The local INV-2 message
now carries the key's write history, like the cold-restore one.

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

claude 3 weeks ago 734a7f5baab51c85bb8861423b883aacc415394a parent 0d389d1

2 files changed, +6 −1

internal/sim/hostlife/background_test.go +1 −0
internal/sim/hostlife/sim_test.go +5 −1

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

index d4504dc17..dae4d547a 100644

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

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

@@ -356,6 +356,7 @@ func (w *world) fault() {

}

b.DB = nil

+ b.Procs = nil // nothing survives the disk: a descendant with no database would acknowledge writes into nowhere

w.stats["disk-lost with the crash"]++

w.logf("box %d lost its disk with the crash", b.ID)

}

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

index 48158cc77..6e921e98d 100644

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

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

@@ -669,7 +669,11 @@ func (w *world) foreignWrites(db *localDB, inc int, how string) {

// acknowledged timer is delivered or still registered.

func (w *world) checkLocal(c *claim, e *box, db *localDB) {

if why, ok := statesEqual(w.expectState(c.Holder.Inc, -1), db.State); !ok {

- w.violate("INV-2 (local): the serving database differs from the acknowledged writes: %s", why)

+ have := map[int]bool{}

+ for _, x := range db.Log {

+ have[x] = true

+ }

+ w.violate("INV-2 (local): the serving database differs from the acknowledged writes: %s (%s)", why, w.keyHistory(c.Holder.Inc, why, have))

return

}

timers := map[int]bool{}