amadan
sim: hostlife: the cold-restore oracle masks keys of writes declared lost
A write declared lost with a disk (an exempt acknowledgement) is required nowhere, but its upload may still land and a later restore may apply it: seed 68282 of 100,000 had such a write delete the oldest key, and the oracle compared the restored state with a replay that skipped the write. The comparison now masks the keys exempt writes touched; every other key must match. The diagnostic listing also used the rev 7.5 ltx/ prefix.
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
1 file changed,
+39
−2
internal/sim/hostlife/sim_test.go+39 −2
diff --git a/internal/sim/hostlife/sim_test.go b/internal/sim/hostlife/sim_test.go| index 7dc286030..912d1c6a0 100644 |
| --- a/internal/sim/hostlife/sim_test.go |
| +++ b/internal/sim/hostlife/sim_test.go |
| @@ -510,11 +510,48 @@ func (w *world) checkDurable(c *claim, when string) { |
| return |
| } |
| w.foreignWrites(db, c.Holder.Inc, "cold restore, "+when) |
| - if why, ok := statesEqual(w.expectState(c.Holder.Inc, db.TX), db.State); !ok { |
| - w.violate("INV-2 (cold restore, %s): the restored database differs from the acknowledged writes: %s (restored TXID %d; %s)", when, why, db.TX, w.ltxShape(e.Region, dataKey(c.Holder.Location, c.Holder.Gen, "ltx/"))) |
| + // a write declared lost with a disk (exempt) is not required anywhere, |
| + // but its upload may still land and the planner may still apply it, so |
| + // the keys such writes touched are indeterminate for this comparison; |
| + // every other key must match (rev 7.7: seed 68282, a delete of the |
| + // oldest key in an exempt write that landed after the cold restore) |
| + masked := w.exemptKeys(c.Holder.Inc) |
| + if why, ok := statesEqual(unmask(w.expectState(c.Holder.Inc, db.TX), masked), unmask(db.State, masked)); !ok { |
| + w.violate("INV-2 (cold restore, %s): the restored database differs from the acknowledged writes: %s (restored TXID %d; %s)", when, why, db.TX, w.ltxShape(e.Region, dataKey(c.Holder.Location, c.Holder.Gen, ""))) |
| } |
| } |
| +// exemptKeys are the keys touched by writes of inc that a disk loss |
| +// declared lost (exempt acknowledgements). |
| +func (w *world) exemptKeys(inc int) map[string]bool { |
| + out := map[string]bool{} |
| + for _, a := range w.acks { |
| + if a.Inc == inc && a.Exempt && a.Kind == "write" { |
| + t := w.txs[a.W] |
| + k := t.Key |
| + if k == "" { |
| + k = fmt.Sprintf("k%d", a.W) |
| + } |
| + out[k] = true |
| + } |
| + } |
| + return out |
| +} |
| + |
| +// unmask is state without the masked keys, for a comparison. |
| +func unmask(state map[string]int, masked map[string]bool) map[string]int { |
| + if len(masked) == 0 { |
| + return state |
| + } |
| + out := map[string]int{} |
| + for k, v := range state { |
| + if !masked[k] { |
| + out[k] = v |
| + } |
| + } |
| + return out |
| +} |
| + |
| // counting is the sweep's random source, counting its draws so the oracle |
| // purity check can show an oracle consumed none (R6-1). |
| type counting struct { |