amadan
sim: hostlife: the admitted writer's start is finished by its own agent loop; a prepared landing generation keeps the flip's stamp; a compaction with a full input is full; the return's lagging marker
Found by the first rev 7.10 baselines: an admitted writer waiting for its marker was resumed only by a wake (seed 5094 / 30,000), the probe's cold admission into the landing's prepared generation issued a second stamp and the probe was refused by its own record (seed 1117), a clean rollback's source saw the marker lag behind the generation the return named again (seed 9554), a prepared generation already opened was re-entered (seeds 43 and 87 / 300), a target that never restored a database returned a spurious dirty seal (seed 62 / 300), and a compaction of a warm admission's full first upload into a delta lost a deletion (seed 27371 / 30,000).
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
4 files changed,
+88
−10
internal/sim/hostlife/ltx_test.go+8 −0internal/sim/hostlife/moves_test.go+5 −0internal/sim/hostlife/protocol_test.go+44 −9internal/sim/hostlife/sim_test.go+31 −1
diff --git a/internal/sim/hostlife/ltx_test.go b/internal/sim/hostlife/ltx_test.go| index 461a01d4b..766d2245a 100644 |
| --- a/internal/sim/hostlife/ltx_test.go |
| +++ b/internal/sim/hostlife/ltx_test.go |
| @@ -513,6 +513,14 @@ func (w *world) compact(b *box) { |
| if max != 0 && !(v.B.Min <= max+1 && v.B.Max > max) { |
| return // non-contiguous inputs: litestream refuses to compact them |
| } |
| + if v.B.Full { |
| + // a full input anywhere makes the image complete from there: the |
| + // output carries every page and a key the full file lacked is |
| + // gone (rev 7.10: a warm admission's first upload is full, fact |
| + // R5-1c, so full files appear mid-generation; seed 27371 / |
| + // 30,000 compacted one into a delta and a deletion was lost) |
| + out.Full = true |
| + } |
| apply(out.Pages, v.B) |
| for k, val := range v.B.Pages { |
| if val == 0 { |
diff --git a/internal/sim/hostlife/moves_test.go b/internal/sim/hostlife/moves_test.go| index 93ca71fb7..66d3029b2 100644 |
| --- a/internal/sim/hostlife/moves_test.go |
| +++ b/internal/sim/hostlife/moves_test.go |
| @@ -172,6 +172,11 @@ func (w *world) role(b *box, c *claim) { |
| if c.Holder == nil { |
| return |
| } |
| + if b.open != nil { |
| + // an admitted writer finishing its start (rev 7.10 §7.14) |
| + w.resumeStart(b, c) |
| + return |
| + } |
| switch c.Op.Kind { |
| case "moving": |
| if b.ID == c.Op.Src { |
diff --git a/internal/sim/hostlife/protocol_test.go b/internal/sim/hostlife/protocol_test.go| index 6d18fb387..a1dc90e1c 100644 |
| --- a/internal/sim/hostlife/protocol_test.go |
| +++ b/internal/sim/hostlife/protocol_test.go |
| @@ -437,12 +437,14 @@ func (w *world) spawn(b *box, c *claim, want string, probe bool) bool { |
| } |
| if bg != h.Gen && on("start-check") { |
| switch { |
| - case h.WriterBox == b.ID && w.ancestorGen(loc, h.Gen, bg): |
| - // the marker lags behind this box's own admission: handled below. |
| - // Another box's lagging marker is the start check's refusal |
| - // (the generation clause, J2-R2-8): a stale box whose region |
| - // holds none of holder.generation's files is not the admitted |
| - // writer that died between its CAS and its marker |
| + case (h.WriterBox == b.ID || c.Op.Kind == "restoring" && b.ID == c.Op.Src) && w.ancestorGen(loc, h.Gen, bg): |
| + // the marker lags behind this box's own admission, or behind |
| + // the return that named the source's generation again: |
| + // handled below. Another box's lagging marker is the start |
| + // check's refusal (the generation clause, J2-R2-8): a stale |
| + // box whose region holds none of holder.generation's files is |
| + // not the admitted writer that died between its CAS and its |
| + // marker |
| case w.ancestorGen(loc, bg, h.Gen): |
| // the marker names a descendant: a clean rollback returned the |
| // claim to the source's generation and abandoned the target's; |
| @@ -464,7 +466,10 @@ func (w *world) spawn(b *box, c *claim, want string, probe bool) bool { |
| source, _ = w.parentGen(loc, source) |
| } |
| w.stats["abandoned empty generation skipped"]++ |
| - } else { |
| + } else if !w.republishMarker(b, loc, h.Gen) { |
| + // no earlier version names it: the admitted writer's marker |
| + // never landed; from the operation's build journal for its |
| + // prepared generation, else a fresh generation rooted at [1,1] |
| ver, key, tx := 0, "", 0 |
| if h.Gen == installGen(&c.Op) && c.Op.BaseKey != "" { |
| ver, key, tx = c.Op.BaseVer, c.Op.BaseKey, c.Op.BaseTX |
| @@ -512,7 +517,7 @@ func (w *world) spawn(b *box, c *claim, want string, probe bool) bool { |
| return false |
| } |
| db.Stamp = b.stampOf(h.Inc) |
| - w.logf("box %d restored %s: TXID %d at position %d (%s admission into %q)", b.ID, dataKey(loc, source, ""), db.TX, db.Pos, adm.Mode, adm.NewGeneration) |
| + w.logf("box %d restored %s: TXID %d at position %d, %d writes (%s admission into %q)", b.ID, dataKey(loc, source, ""), db.TX, db.Pos, len(db.Log), adm.Mode, adm.NewGeneration) |
| } |
| b.DB = db |
| if on("start-check") { |
| @@ -623,6 +628,25 @@ func (w *world) spawn(b *box, c *claim, want string, probe bool) bool { |
| return w.startProc(b, c, want, probe, adm.Mode) |
| } |
| +// resumeStart is the agent's own loop finishing an admitted writer's start |
| +// (rev 7.10 §7.14): the activator process holds the admission and waits |
| +// for the PUT it needs, without a wake. An admission the claim moved past |
| +// is abandoned. |
| +func (w *world) resumeStart(b *box, c *claim) { |
| + o := b.open |
| + if o == nil || c == nil || c.Holder == nil || hasMain(b) { |
| + return |
| + } |
| + if o.Gen != c.Holder.Gen || o.Session != c.Holder.Session { |
| + b.open = nil |
| + w.stats["open: abandoned"]++ |
| + return |
| + } |
| + if w.resumeOpen(b, c, o) { |
| + w.startProc(b, c, o.Want, false, o.Mode) |
| + } |
| +} |
| + |
| // startProc starts the host's processes on b for the admitted writer. |
| func (w *world) startProc(b *box, c *claim, want string, probe bool, mode string) bool { |
| h := c.Holder |
| @@ -902,6 +926,7 @@ func (w *world) resumeOpen(b *box, c *claim, o *openState) bool { |
| } |
| if !visible() { |
| w.stats["open: waits for the marker"]++ |
| + w.logf("box %d: admitted into %q, waiting for its marker", b.ID, db.Gen) |
| return false |
| } |
| } |
| @@ -998,7 +1023,17 @@ func (w *world) admitCommit(b *box, c *claim, a admitInput) bool { |
| if a.Mode == "cold" { |
| w.newGen(n.Holder.Location, h.Gen, a.NewGeneration) |
| n.Holder.Gen = a.NewGeneration |
| - n.Holder.Stamp = w.issueStamp(n, b.ID) // the installing CAS (claim rev 6.8 §6.4a, §6.4) |
| + if !(n.Op.Kind == "landing" && a.NewGeneration == installGen(&n.Op) && n.Holder.Stamp == n.Op.FlipGen) { |
| + // a new installation: a new stamp (the installing CAS, claim |
| + // rev 6.9 §6.4a, §6.4): a fresh generation, a push's prepared |
| + // generation, a dirty rollback's return generation (claim rev |
| + // 6.5: never the predecessor's stamp). The landing's prepared |
| + // generation is the installation the flip CAS already made |
| + // current with its stamp F, which the target's record |
| + // activated before the probe; another stamp here would refuse |
| + // the probe by its own record (seed 1117 / 30,000) |
| + n.Holder.Stamp = w.issueStamp(n, b.ID) |
| + } |
| e.Stamp = n.Holder.Stamp |
| if !a.PredecessorCertified && on("writes-lost") { |
| lost = &writesLost{Box: h.WriterBox, Gen: h.Gen, Session: h.Session, RemoteMaxTXID: a.RemoteMaxTXID} |
diff --git a/internal/sim/hostlife/sim_test.go b/internal/sim/hostlife/sim_test.go| index 79e42919f..f88f63bbc 100644 |
| --- a/internal/sim/hostlife/sim_test.go |
| +++ b/internal/sim/hostlife/sim_test.go |
| @@ -277,6 +277,9 @@ func (w *world) whyNotQuiescent() string { |
| if e := w.execBox(c); b != e && (b.Row != nil || len(b.Procs) > 0) { |
| out = append(out, fmt.Sprintf("box %d has a row or processes", b.ID)) |
| } |
| + if b.open != nil { |
| + out = append(out, fmt.Sprintf("box %d admitted into %q, start in progress at stage %s", b.ID, b.open.Gen, b.open.stage)) |
| + } |
| } |
| } |
| if r := w.residue(); len(r) > 0 { |
| @@ -324,6 +327,9 @@ func (w *world) atRest() bool { |
| if b != e && (b.Row != nil || len(b.Procs) > 0) { |
| return false |
| } |
| + if b.open != nil { |
| + return false // an admitted writer still finishing its start |
| + } |
| } |
| return true |
| } |
| @@ -577,8 +583,32 @@ func (w *world) checkDurable(c *claim, when string) { |
| // required write that is missing was caught above, and no key is ever |
| // masked; a later required write re-establishes its key's value |
| if why, ok := statesEqual(w.expectFrom(c.Holder.Inc, have), db.State); !ok { |
| - w.violate("INV-2 (cold restore, %s): the restored database differs from the replay of the writes it carries: %s (restored TXID %d; %s; %s)", when, why, db.TX, w.keyHistory(c.Holder.Inc, why, have), w.ltxShape(e.Region, dataKey(c.Holder.Location, c.Holder.Gen, ""))) |
| + w.violate("INV-2 (cold restore, %s): the restored database differs from the replay of the writes it carries: %s (restored TXID %d; %s; %s; %s)", when, why, db.TX, w.keyHistory(c.Holder.Inc, why, have), w.ltxShape(e.Region, dataKey(c.Holder.Location, c.Holder.Gen, "")), w.fileDetail(e.Region, dataKey(c.Holder.Location, c.Holder.Gen, ""), why)) |
| + } |
| +} |
| + |
| +// fileDetail lists, for diagnosis, each current file of the generation |
| +// with its kind, range, TXs and the page it holds for the key named in a |
| +// statesEqual message. |
| +func (w *world) fileDetail(r int, prefix, why string) string { |
| + key := "" |
| + if i := strings.Index(why, "key "); i >= 0 { |
| + rest := why[i+4:] |
| + if j := strings.Index(rest, " "); j > 0 { |
| + key = rest[:j] |
| + } |
| + } |
| + bk := w.buckets[r] |
| + var out []string |
| + for _, k := range bk.keys(prefix) { |
| + v := bk.current(k) |
| + if v == nil || v.B == nil || !isDataKey(k) { |
| + continue |
| + } |
| + val, ok := v.B.Pages[key] |
| + out = append(out, fmt.Sprintf("%s{full=%v txs=%v %s=%d/%v}", strings.TrimPrefix(k, prefix), v.B.Full, v.B.TXs, key, val, ok)) |
| } |
| + return "detail " + strings.Join(out, " ") |
| } |
| // keyHistory lists, for diagnosis, the acknowledged writes of inc that |