amadan
sim: hostlife: claim rev 6 and the moves side of joint round 3 (rev 7.4)
Claim rev 6 (3ea3f90c), encoded:
- R3-2: orphan cleanup is a console plan with its observations in order
(record, then the claim fresh, then DeleteIfMatch) and pauses between
them; rule orphan-order reads the claim first. Record ETags are now
unique per write. The cleanup asserts it never deletes the record of
the claim's holder or creating incarnation.
- R3-3: the local retired marker is {incarnation, op}: it refuses a
writer at or before the fence's op, and a new installation of the
incarnation replaces it under the guard on a fresh claim read. Plans
carry the op sequence they validated under. Rule fence-by-installation;
the mutation is rev 5.2's whole-incarnation marker. The unmutated
round-trip witness (UK->US->UK) now serves on UK again, running.
- R3-4: the at-rest sweep discovers locations from the namespace;
retired_incarnations is capped at 32 and anti-reuse only. Rule
sweep-namespace; its witness runs 33 recreates and lands a held
replication PUT of incarnation 1.
Moves side of round 3:
- R3-1: restore is a chain, not a union: generation.json names the
snapshot's version id; LTX objects continue the chain only if their
history extends it; prefixes are skipped; a conflict refuses. The
install manifest records the snapshot's version (op.BaseVer).
- R3-5: the edge routes on the row: a public request reaching a landing
target before the commit is INV-5. commit-before-open has its own
violation and witness now.
- R3-7: budget_test.go states T11's arithmetic; the attempt count
depends on the admitted budget, and the test shows rev 7.3's formula
refused every default move.
- R2-5: a witness for recovery-current-inputs on a dirty rollback after
a bundle change.
- R3-6: mutate.sh fails on orchestration errors, requires one
well-formed verdict per mutation, and treats missing witness output
for a rule that has witnesses as an ERROR.
- Witness evidence: each witness names its failure; the gate runs every
witness in place, under every proper subset of its mutation set (must
hold) and under the whole set (must violate with the named failure).
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
11 files changed,
+695
−148
internal/sim/hostlife/background_test.go+14 −6internal/sim/hostlife/budget_test.go+69 −0internal/sim/hostlife/console_test.go+90 −22internal/sim/hostlife/expected-outcomes.txt+0 −1internal/sim/hostlife/moves_test.go+88 −28internal/sim/hostlife/mutate.sh+34 −4internal/sim/hostlife/protocol_test.go+65 −16internal/sim/hostlife/rules_test.go+3 −0internal/sim/hostlife/sim_test.go+1 −1internal/sim/hostlife/witness_test.go+268 −67internal/sim/hostlife/world_test.go+63 −3
diff --git a/internal/sim/hostlife/background_test.go b/internal/sim/hostlife/background_test.go| index 40fed13a1..120d2ced5 100644 |
| --- a/internal/sim/hostlife/background_test.go |
| +++ b/internal/sim/hostlife/background_test.go |
| @@ -58,7 +58,17 @@ func (w *world) idleStop(b *box) { |
| // wake: a request reaches this box's edge for the host. |
| func (w *world) wake(b *box) { |
| - if !w.agentUp(b) || b.Row == nil || b.Row.Status != "ready" || hasMain(b) { |
| + if !w.agentUp(b) || b.Row == nil || b.Row.Status != "ready" { |
| + return |
| + } |
| + // the edge routes on the row (edge.go:595): a ready row receives the |
| + // public request whether or not the instance already runs. INV-5: no |
| + // public delivery to a landing target before the commit (R3-5) |
| + if c := w.claim; c != nil && c.Op.Kind == "landing" && !c.Op.Committed && c.Op.Tgt == b.ID { |
| + w.violate("INV-5: a public request reached the landing target, box %d, before the commit of %s", b.ID, c.Op.ID) |
| + return |
| + } |
| + if hasMain(b) { |
| return |
| } |
| if b.Old { |
| @@ -196,9 +206,7 @@ func (w *world) reconcileClaimed(b *box, c *claim) { |
| } |
| if b.Row == nil && c.Op.Kind == "serving" { |
| b.Row = &row{Inc: h.Inc, App: h.App, Status: "ready"} |
| - if b.Retired != nil { |
| - delete(b.Retired, h.Inc) |
| - } |
| + delete(b.Fence, h.Inc) // the serving executor, on a fresh read: the fence is replaced |
| } |
| } else if b.Row != nil && !(on("participant-rows") && w.ownsLocalObligation(c, b)) { |
| w.retireRow(b) |
| @@ -225,7 +233,7 @@ func (w *world) passPlan(b *box, kind string) { |
| if kind == "config" && !b.HasKey { |
| return |
| } |
| - b.plans = append(b.plans, &plan{Kind: kind, Inc: b.Row.Inc, App: b.Row.App, Ver: w.cfgVer[b.Row.App], At: w.now + w.pauseLen()}) |
| + b.plans = append(b.plans, &plan{Kind: kind, Inc: b.Row.Inc, App: b.Row.App, Ver: w.cfgVer[b.Row.App], At: w.now + w.pauseLen(), Seq: w.nextID}) |
| } |
| // passExec runs one independent process's write. It needs the box running, |
| @@ -249,7 +257,7 @@ func (w *world) passExec(b *box) { |
| return |
| } |
| c := w.claim |
| - if c == nil || c.Holder == nil || c.Holder.Inc != p.Inc || b.Row == nil || b.Row.Inc != p.Inc || b.Retired[p.Inc] { |
| + if c == nil || c.Holder == nil || c.Holder.Inc != p.Inc || b.Row == nil || b.Row.Inc != p.Inc || w.fenced(b, p.Inc, p.Seq) { |
| return |
| } |
| if p.Kind == "config" && p.Ver != w.cfgVer[p.App] { |
diff --git a/internal/sim/hostlife/budget_test.go b/internal/sim/hostlife/budget_test.go| new file mode 100644 |
| index 000000000..7208e9c7c |
| --- /dev/null |
| +++ b/internal/sim/hostlife/budget_test.go |
| @@ -0,0 +1,69 @@ |
| +package hostlife |
| + |
| +import "testing" |
| + |
| +// The readiness arithmetic of moves spec §7.3 T11 (rev 7.4, R3-7), in |
| +// seconds. Rev 7.3's T11 required every one of three probe attempts, each |
| +// with its settle, to fit the window beside the fixed costs: 150 s of |
| +// probing alone, against a default window of 120 s, so no default move |
| +// was ever eligible. Rev 7.4 makes the permitted attempt count depend on |
| +// the admitted budget. |
| +type cutEstimate struct { |
| + Stop, Checkpoint, Mirror, Archive, Copy, Restore, Render, Open float64 |
| + Probe, Settle float64 // one attempt |
| +} |
| + |
| +const ( |
| + cutWindowDefault = 120.0 // the operator's default cut window |
| + probeAttemptsMax = 3 // §7.7: never more than three attempts |
| + probeSeconds = 30.0 |
| + settleSeconds = 20.0 |
| +) |
| + |
| +func (e cutEstimate) fixed() float64 { |
| + return e.Stop + e.Checkpoint + e.Mirror + e.Archive + e.Copy + e.Restore + e.Render + e.Open |
| +} |
| + |
| +// attemptsAdmitted is T11 as rev 7.4 states it: the attempts permitted are |
| +// what the window leaves after the fixed costs, at most three; the |
| +// instance is eligible when that is at least one, and the probe loop |
| +// (§7.7) runs at most that many. |
| +func (e cutEstimate) attemptsAdmitted(window float64) int { |
| + n := int((window - e.fixed()) / (e.Probe + e.Settle)) |
| + if n > probeAttemptsMax { |
| + n = probeAttemptsMax |
| + } |
| + if n < 0 { |
| + n = 0 |
| + } |
| + return n |
| +} |
| + |
| +// fitsRev73 is T11 as rev 7.3 stated it: three attempts, always. |
| +func (e cutEstimate) fitsRev73(window float64) bool { |
| + return e.fixed()+probeAttemptsMax*(e.Probe+e.Settle) <= window |
| +} |
| + |
| +func TestReadinessBudget(t *testing.T) { |
| + // a tiny instance: every fixed cost at the floor of its measured rate |
| + tiny := cutEstimate{Stop: 2, Checkpoint: 1, Mirror: 2, Archive: 2, Copy: 1, Restore: 1, Render: 1, Open: 5, Probe: probeSeconds, Settle: settleSeconds} |
| + if tiny.fitsRev73(cutWindowDefault) { |
| + t.Fatalf("rev 7.3's formula admits a tiny instance in the default window: R3-7 is stale") |
| + } |
| + if n := tiny.attemptsAdmitted(cutWindowDefault); n != 2 { |
| + t.Fatalf("rev 7.4's formula admits %d attempts for a tiny instance in %.0f s, want 2", n, cutWindowDefault) |
| + } |
| + // the boundary: fixed costs of 70 s leave exactly one attempt; 71 s none |
| + edge := cutEstimate{Stop: 70 - 5, Open: 5, Probe: probeSeconds, Settle: settleSeconds} |
| + if n := edge.attemptsAdmitted(cutWindowDefault); n != 1 { |
| + t.Fatalf("fixed costs of 70 s admit %d attempts, want 1", n) |
| + } |
| + edge.Stop++ |
| + if n := edge.attemptsAdmitted(cutWindowDefault); n != 0 { |
| + t.Fatalf("fixed costs of 71 s admit %d attempts, want 0 (refused)", n) |
| + } |
| + // a generous window never permits more than three |
| + if n := tiny.attemptsAdmitted(600); n != probeAttemptsMax { |
| + t.Fatalf("a 600 s window admits %d attempts, want %d", n, probeAttemptsMax) |
| + } |
| +} |
diff --git a/internal/sim/hostlife/console_test.go b/internal/sim/hostlife/console_test.go| index 78167bcb9..b2c701142 100644 |
| --- a/internal/sim/hostlife/console_test.go |
| +++ b/internal/sim/hostlife/console_test.go |
| @@ -18,6 +18,12 @@ type consolePlan struct { |
| Region int |
| Read bool // a create's registration re-read has passed |
| Stall int // the console is paused on this plan until then |
| + // an orphan cleanup's observations (claim rev 6 §5.1 step 5): the |
| + // record's ETag and incarnation, the claim read, and the verdict |
| + RecVer int |
| + RecInc int |
| + Snap *claim |
| + Orphan bool |
| // the claim's ETag as the create read it when it registered: its |
| // claim CAS is conditional on it (CC22) |
| SeenVer int |
| @@ -61,12 +67,12 @@ func (w *world) fixRecord() { |
| case "serving": |
| if b := w.execBox(c); b != nil && (w.rec.MoveID != "" || w.rec.Region != b.Region) { |
| w.rec.Region, w.rec.MoveID, w.rec.MoveState, w.rec.RollbackID = b.Region, "", "", "" |
| - w.rec.Ver++ |
| + w.rec.Ver = w.newVer() |
| } |
| case "moving": |
| if w.rec.MoveID == "" { |
| w.rec.MoveID, w.rec.MoveState = c.Op.ID, "" |
| - w.rec.Ver++ |
| + w.rec.Ver = w.newVer() |
| } |
| } |
| w.followRecord(c) |
| @@ -215,12 +221,15 @@ func (w *world) createSteps(p *consolePlan) bool { |
| return false // a pending chore, such as a sweep, finishes first (CC11) |
| } |
| if w.rec != nil { |
| - // the record key is occupied: an orphan is removed with |
| - // DeleteIfMatch and the create retries (CC17); anything else |
| + // the record key is occupied: an orphan is removed by the |
| + // cleanup of claim rev 6 §5.1 step 5, run by this console as |
| + // its own plan, and the create retries (CC17); anything else |
| // refuses the create |
| - if c != nil && w.orphan(c) && on("cancelled-creates") { |
| - w.logf("create %s: removing an orphan record inc %d", p.OpID, w.rec.Inc) |
| - w.rec = nil |
| + if c != nil && w.orphanOf(c, w.rec.Inc) && on("cancelled-creates") { |
| + if !w.hasPlan("orphan", "create") { |
| + w.logf("create %s: cleaning up an orphan record inc %d", p.OpID, w.rec.Inc) |
| + w.console = append(w.console, &consolePlan{Kind: "orphan", Host: "create"}) |
| + } |
| return false |
| } |
| return abandon() |
| @@ -259,7 +268,7 @@ func (w *world) createSteps(p *consolePlan) bool { |
| return abandon() |
| } |
| if w.rec == nil && w.recPend == nil { |
| - rec := &record{Inc: c.Holder.Inc, App: c.Holder.App, Region: c.Op.NewRegion} |
| + rec := &record{Ver: w.newVer(), Inc: c.Holder.Inc, App: c.Holder.App, Region: c.Op.NewRegion} |
| switch n := w.rng.Intn(10); { |
| case n < 7: |
| w.rec = rec |
| @@ -461,7 +470,7 @@ func (w *world) parkingObligations(n *claim, inc int) { |
| n.Obl = append(n.Obl, w.newObl(n, "park-local", -1, id, "", fmt.Sprint(inc), 0)) |
| } |
| } |
| - n.Retired = addUniq(n.Retired, inc) |
| + n.Retired = retire(n.Retired, inc) |
| } |
| // consoleStep runs the next step of one console plan, chosen at random: |
| @@ -491,10 +500,68 @@ func (w *world) runPlan(p *consolePlan) bool { |
| return w.deleteSteps(c) |
| case "purge": |
| return w.purgeSteps(p) |
| + case "orphan": |
| + return w.orphanSteps(p) |
| } |
| return true |
| } |
| +// hasPlan: a console plan of this kind, by this owner, is in flight. |
| +func (w *world) hasPlan(kind, owner string) bool { |
| + for _, p := range w.console { |
| + if p.Kind == kind && p.Host == owner { |
| + return true |
| + } |
| + } |
| + return false |
| +} |
| + |
| +// orphanSteps is the orphan cleanup of claim rev 6 §5.1 step 5 (R3-2) as |
| +// a console plan, so the console can pause between its observations and |
| +// its delete: read the record (ETag E, incarnation I); read the claim |
| +// fresh, afterwards; it is an orphan only if that claim names neither I |
| +// as holder nor a creating operation for I; DeleteIfMatch(E). The |
| +// mutation reads the claim first and the record second, and decides on |
| +// the stale claim: a successor that claimed and published in between is |
| +// then deleted. |
| +func (w *world) orphanSteps(p *consolePlan) bool { |
| + switch p.Step { |
| + case 0: |
| + if on("orphan-order") { |
| + if w.rec == nil { |
| + return true |
| + } |
| + p.RecVer, p.RecInc = w.rec.Ver, w.rec.Inc |
| + } else { |
| + p.Snap = w.claim.clone() |
| + } |
| + p.Step = 1 |
| + return false |
| + case 1: |
| + if on("orphan-order") { |
| + p.Orphan = w.orphanOf(w.claim, p.RecInc) // fresh, after the record |
| + } else { |
| + if w.rec == nil { |
| + return true |
| + } |
| + p.RecVer, p.RecInc = w.rec.Ver, w.rec.Inc |
| + p.Orphan = w.orphanOf(p.Snap, p.RecInc) |
| + } |
| + p.Step = 2 |
| + return false |
| + default: |
| + if !p.Orphan || w.rec == nil || w.rec.Ver != p.RecVer { |
| + return true // 412, or nothing to do |
| + } |
| + if c := w.claim; c != nil && (c.Holder != nil && c.Holder.Inc == w.rec.Inc || c.Op.Kind == "creating" && c.Op.NewInc == w.rec.Inc) { |
| + w.violate("claim/record: orphan cleanup deleted the record of incarnation %d, which the claim names", w.rec.Inc) |
| + } |
| + w.logf("orphan cleanup (%s): removed record inc %d", p.Host, w.rec.Inc) |
| + w.rec = nil |
| + return true |
| + } |
| +} |
| + |
| // deleteSteps: record DeleteIfMatch, then parking with obligations, then |
| // free once every obligation is acknowledged (claim §5.2). |
| func (w *world) deleteSteps(c *claim) bool { |
| @@ -891,11 +958,13 @@ func (w *world) recoveryPass() { |
| return |
| } |
| // a late record PUT from a cancelled create: an orphan, never admitted |
| - // (C1); DeleteIfMatch when cancelled_creates names its incarnation |
| - // (claim rev 4 §5.1, J2-R2-7) |
| - if w.rec != nil && on("cancelled-creates") && w.orphan(c) { |
| - w.logf("recovery: removing an orphan record inc %d", w.rec.Inc) |
| - w.rec = nil |
| + // (C1); removed by the ordered cleanup of claim rev 6 §5.1 step 5, as |
| + // a plan of this console (J2-R2-7, R3-2) |
| + if w.rec != nil && on("cancelled-creates") && w.orphanOf(c, w.rec.Inc) { |
| + if !w.hasPlan("orphan", "recovery") { |
| + w.logf("recovery: cleaning up an orphan record inc %d", w.rec.Inc) |
| + w.console = append(w.console, &consolePlan{Kind: "orphan", Host: "recovery"}) |
| + } |
| return |
| } |
| switch c.Op.Kind { |
| @@ -927,7 +996,7 @@ func (w *world) recoveryPass() { |
| } |
| n.Holder, n.Op = nil, opState{} |
| n.Regions, n.Boxes = nil, nil |
| - n.Retired = addUniq(n.Retired, inc) |
| + n.Retired = retire(n.Retired, inc) |
| n.Cancelled = append(n.Cancelled, cancelledCreate{Inc: inc, Until: w.now + 4*horizonH}) |
| return true |
| }) { |
| @@ -965,20 +1034,19 @@ func (w *world) recoveryPass() { |
| // orphan: claim rev 5 §5.1 (CC17). A record whose incarnation is retired, |
| // or is not the claim's holder, is an orphan at any time; rev 4's |
| // cancelled_creates window is the mutation. |
| -func (w *world) orphan(c *claim) bool { |
| - r := w.rec |
| - if r == nil || c == nil { |
| - return false |
| +func (w *world) orphanOf(c *claim, inc int) bool { |
| + if c == nil { |
| + return false // no claim at all: a legacy record, adopted (§9), never an orphan |
| } |
| - if c.Holder != nil && c.Holder.Inc == r.Inc { |
| + if c.Holder != nil && c.Holder.Inc == inc { |
| return false |
| } |
| - if c.Op.Kind == "creating" && c.Op.NewInc == r.Inc { |
| + if c.Op.Kind == "creating" && c.Op.NewInc == inc { |
| return false |
| } |
| if !on("orphan-no-deadline") { |
| for _, x := range c.Cancelled { |
| - if x.Inc == r.Inc && w.now <= x.Until { |
| + if x.Inc == inc && w.now <= x.Until { |
| return true |
| } |
| } |
diff --git a/internal/sim/hostlife/expected-outcomes.txt b/internal/sim/hostlife/expected-outcomes.txt| index 2c97a5e1c..6cc69ce95 100644 |
| --- a/internal/sim/hostlife/expected-outcomes.txt |
| +++ b/internal/sim/hostlife/expected-outcomes.txt |
| @@ -4,7 +4,6 @@ |
| # is caught (the expectation is stale). Spec §14.2.5 gives the |
| # combination that catches each, or why none does. |
| claim-cas-opid missed caught with revalidate-before-effect |
| -commit-before-open missed caught with dirty-return |
| config-before-probe missed liveness only: a target that cannot render config fails its probe and rolls back |
| readiness-key missed liveness only: T2 avoids a pointless cut |
| readiness-quiet missed unreachable under claim rev 4: acknowledgements wait out their own horizon and CC11 holds |
diff --git a/internal/sim/hostlife/moves_test.go b/internal/sim/hostlife/moves_test.go| index 11f1cfb90..0df9ad223 100644 |
| --- a/internal/sim/hostlife/moves_test.go |
| +++ b/internal/sim/hostlife/moves_test.go |
| @@ -86,7 +86,7 @@ func (w *world) role(b *box, c *claim) { |
| if b.DB != nil { |
| inc = b.DB.Inc |
| } |
| - if w.localPark(b, inc) { |
| + if w.localPark(b, inc, w.nextID) { // a quarantine retires every installation so far |
| b.Row = nil |
| } |
| } |
| @@ -176,7 +176,16 @@ func (w *world) snapshotBlobOf(b *box, c *claim, gen string) (*blob, *blob) { |
| db.Writes, db.SealKey = r.Writes, r.Key |
| } |
| if b.DB != nil { |
| - db.Writes = unionInts(db.Writes, b.DB.Writes) |
| + // the final checkpoint: the local database continues the replica's |
| + // history (R3-1); a local history that does not is never staged |
| + switch { |
| + case extends(b.DB.Writes, db.Writes): |
| + db.Writes = append([]int(nil), b.DB.Writes...) |
| + case extends(db.Writes, b.DB.Writes): |
| + default: |
| + w.logf("box %d snapshot: the local database does not continue the replica", b.ID) |
| + w.stats["snapshot refused: conflicting history"]++ |
| + } |
| if b.DB.Key != 0 { |
| db.SealKey = b.DB.Key |
| } |
| @@ -333,7 +342,7 @@ func (w *world) moveSource(b *box, c *claim) { |
| } |
| if w.rec != nil && w.rec.Inc == c.Holder.Inc && w.rec.MoveID == op.ID && w.rec.MoveState == "" && op.StopAt != 0 { |
| w.rec.Region, w.rec.MoveState = op.TgtRegion, "landing" |
| - w.rec.Ver++ |
| + w.rec.Ver = w.newVer() // every record write has a fresh ETag |
| w.logf("flip %s: record names region %d", op.ID, op.TgtRegion) |
| } |
| } |
| @@ -633,7 +642,7 @@ func (w *world) rollback(c *claim, why string) { |
| return |
| } |
| r.MoveState, r.Region, r.RollbackID, r.Reason = "rolling_back", op.SrcRegion, w.newID("rb"), why |
| - r.Ver++ |
| + r.Ver = w.newVer() |
| w.logf("rollback %s: %s", op.ID, why) |
| w.stats["why: "+why+" @"+op.LandPhase]++ |
| } |
| @@ -709,6 +718,16 @@ func (w *world) landTarget(b *box, c *claim) { |
| } |
| switch op.LandPhase { |
| case "checking": |
| + // a new installation of this incarnation here replaces the local |
| + // retired marker, under the guard, on a fresh read showing this |
| + // operation current and this box its target (claim rev 6 §6.4, |
| + // R3-3): a move back to a region the instance left |
| + if _, fenced := b.Fence[c.Holder.Inc]; fenced && on("fence-by-installation") { |
| + if fc, ok := w.readClaim(b); ok && fc.Op.ID == op.ID && fc.Op.Kind == "landing" && fc.Op.Tgt == b.ID { |
| + b.Fence[c.Holder.Inc] = w.opSeq(op.ID) - 1 |
| + w.logf("box %d: the fence for inc %d now admits %s", b.ID, c.Holder.Inc, op.ID) |
| + } |
| + } |
| w.cas(c, func(n *claim) bool { |
| n.Boxes = addUniq(n.Boxes, b.ID) |
| n.Op.LandPhase = "install-park" |
| @@ -748,10 +767,11 @@ func (w *world) landTarget(b *box, c *claim) { |
| // only ever add an object to this generation |
| v := w.issue(b.ID, &request{kind: rCopy, region: b.Region, key: dataKey(loc, op.ID, "base"), srcRegion: b.Region, srcKey: src.Key, srcVer: src.Ver}) |
| if v > 0 { |
| - w.cas(c, func(n *claim) bool { n.Op.LandPhase = "published"; return sameOp(n.Op.ID, op.ID) }) |
| + // the install manifest records the snapshot's version (R3-1) |
| + w.cas(c, func(n *claim) bool { n.Op.LandPhase, n.Op.BaseVer = "published", v; return sameOp(n.Op.ID, op.ID) }) |
| } |
| case "published": |
| - v := w.publishGen(b, loc, op.ID, c.Holder.Inc) |
| + v := w.publishGen(b, loc, op.ID, c.Holder.Inc, op.BaseVer) |
| if v > 0 { |
| w.cas(c, func(n *claim) bool { n.Op.LandPhase = "local"; return sameOp(n.Op.ID, op.ID) }) |
| } |
| @@ -831,7 +851,7 @@ func (w *world) landTarget(b *box, c *claim) { |
| r := w.rec |
| if r != nil && r.MoveID == op.ID && r.MoveState == "landing" && w.now <= op.CutDeadline { |
| r.MoveState = "committed" |
| - r.Ver++ |
| + r.Ver = w.newVer() |
| w.logf("commit %s: record committed", op.ID) |
| if w.now > op.CutAt+cutBudget { |
| w.violate("INV-9: %s committed at %d, cut at %d (budget %d)", op.ID, w.now, op.CutAt, cutBudget) |
| @@ -1084,10 +1104,10 @@ func (w *world) recoverSource(b *box, c *claim) { |
| case "install-copy": |
| v := w.issue(b.ID, &request{kind: rCopy, region: b.Region, key: dataKey(c.Holder.Location, op.RollbackID, "base"), srcRegion: b.Region, srcKey: op.ReturnDB.Key, srcVer: op.ReturnDB.Ver}) |
| if v > 0 { |
| - w.cas(c, func(n *claim) bool { n.Op.SrcPhase = "published"; return sameOp(n.Op.ID, op.ID) }) |
| + w.cas(c, func(n *claim) bool { n.Op.SrcPhase, n.Op.BaseVer = "published", v; return sameOp(n.Op.ID, op.ID) }) |
| } |
| case "published": |
| - v := w.publishGen(b, c.Holder.Location, op.RollbackID, c.Holder.Inc) |
| + v := w.publishGen(b, c.Holder.Location, op.RollbackID, c.Holder.Inc, op.BaseVer) |
| if v > 0 { |
| w.cas(c, func(n *claim) bool { n.Op.SrcPhase = "local"; return sameOp(n.Op.ID, op.ID) }) |
| } |
| @@ -1177,10 +1197,10 @@ func (w *world) pushStep(b *box, c *claim) { |
| } |
| v := w.issue(b.ID, &request{kind: rPut, region: b.Region, key: dataKey(loc, op.ID, "base"), b: &blob{Kind: "base", Inc: c.Holder.Inc, Gen: op.ID, Writes: op.PushWrites, SealKey: key}}) |
| if v > 0 { |
| - w.cas(c, func(n *claim) bool { n.Op.Phase = "published"; return sameOp(n.Op.ID, op.ID) }) |
| + w.cas(c, func(n *claim) bool { n.Op.Phase, n.Op.BaseVer = "published", v; return sameOp(n.Op.ID, op.ID) }) |
| } |
| case "published": |
| - v := w.publishGen(b, loc, op.ID, c.Holder.Inc) |
| + v := w.publishGen(b, loc, op.ID, c.Holder.Inc, op.BaseVer) |
| if v > 0 { |
| w.cas(c, func(n *claim) bool { n.Op.Phase = "restore"; return sameOp(n.Op.ID, op.ID) }) |
| } |
| @@ -1290,25 +1310,64 @@ func (w *world) sweepable(c *claim, r int, k string) bool { |
| return on("sweep-staging") // CC20 |
| } |
| h := c.Holder |
| - if h != nil && strings.HasPrefix(k, h.Location) { |
| - // a generation within the live location other than holder.generation |
| - if k == dataKey(h.Location, h.Gen, "base") || k == dataKey(h.Location, h.Gen, "ltx") { |
| - return false |
| - } |
| - if k == genMarkerKey(h.Location) { |
| - v := w.buckets[r].current(k) |
| - e := w.execBox(c) |
| - return v != nil && (v.B.Gen != h.Gen || e == nil || e.Region != r) |
| + if !on("sweep-namespace") { |
| + // claim rev 5's discovery: retired_incarnations (capped) and the |
| + // legacy flag. A location older than the cap is never listed |
| + if h != nil && strings.HasPrefix(k, h.Location) { |
| + return w.deadGeneration(c, r, k) |
| + } |
| + for _, inc := range c.Retired { |
| + if strings.HasPrefix(k, locationFor(inc, false)) { |
| + return true |
| + } |
| } |
| - return isDataKey(k) |
| + return w.legacyRetired(c) |
| } |
| - for _, inc := range c.Retired { |
| - if strings.HasPrefix(k, locationFor(inc, false)) { |
| - return true |
| + // claim rev 6 §6.2a (R3-4): locations come from the namespace itself. |
| + // Each child prefix of instances/<host>/ is an incarnation location, or |
| + // the legacy location (the host prefix, litestream's level layout): |
| + // residue unless it is holder.location, and within holder.location |
| + // residue unless it is holder.generation |
| + if h != nil && locationOf(k) == h.Location { |
| + return w.deadGeneration(c, r, k) |
| + } |
| + return true |
| +} |
| + |
| +// locationOf is the location a key under instances/<host>/ belongs to: |
| +// instances/<host>/<incarnation>/ for a child prefix, else the legacy |
| +// location instances/<host>/ (a level directory directly under the host). |
| +func locationOf(k string) string { |
| + p := "instances/" + host + "/" |
| + rest := strings.TrimPrefix(k, p) |
| + if i := strings.Index(rest, "/"); i > 0 { |
| + child := rest[:i] |
| + digits := len(child) > 0 |
| + for _, r := range child { |
| + if r < '0' || r > '9' { |
| + digits = false |
| + } |
| + } |
| + if digits { |
| + return p + child + "/" |
| } |
| } |
| - // a retired legacy incarnation's location is the bare namespace |
| - return w.legacyRetired(c) |
| + return p |
| +} |
| + |
| +// deadGeneration: within holder.location, a generation other than |
| +// holder.generation, or a marker that no longer names it. |
| +func (w *world) deadGeneration(c *claim, r int, k string) bool { |
| + h := c.Holder |
| + if k == dataKey(h.Location, h.Gen, "base") || k == dataKey(h.Location, h.Gen, "ltx") { |
| + return false |
| + } |
| + if k == genMarkerKey(h.Location) { |
| + v := w.buckets[r].current(k) |
| + e := w.execBox(c) |
| + return v != nil && (v.B.Gen != h.Gen || e == nil || e.Region != r) |
| + } |
| + return isDataKey(k) |
| } |
| // legacyRetired: the host once held a legacy incarnation, now retired, so |
| @@ -1327,8 +1386,9 @@ func (w *world) legacyRetired(c *claim) bool { |
| // (moves rev 7.1 §5.1, model 29). generation.json is a reused key, so an |
| // earlier publication that completes late would otherwise put an older |
| // generation back, and every wake would refuse. |
| -func (w *world) publishGen(b *box, loc, gen string, inc int) int { |
| - r := &request{kind: rPut, region: b.Region, key: genMarkerKey(loc), b: &blob{Kind: "gen", Gen: gen, Inc: inc}} |
| +func (w *world) publishGen(b *box, loc, gen string, inc int, base int) int { |
| + // the marker names the generation's snapshot by version id (R3-1) |
| + r := &request{kind: rPut, region: b.Region, key: genMarkerKey(loc), b: &blob{Kind: "gen", Gen: gen, Inc: inc, Base: base}} |
| if on("generation-conditional") { |
| r.ifSet = true |
| if cur := w.buckets[b.Region].current(r.key); cur != nil { |
diff --git a/internal/sim/hostlife/mutate.sh b/internal/sim/hostlife/mutate.sh| index 57a80bb71..c4ff0590c 100755 |
| --- a/internal/sim/hostlife/mutate.sh |
| +++ b/internal/sim/hostlife/mutate.sh |
| @@ -47,7 +47,7 @@ ROOT=$(git -C "$(dirname "$0")" rev-parse --show-toplevel) |
| PKG="$ROOT/internal/sim/hostlife" |
| SCRATCH=${HOSTLIFE_SCRATCH:-${TMPDIR:?}/hostlife-sim} |
| BIN=${HOSTLIFE_BIN:-$SCRATCH/hostlife.test} |
| -mkdir -p "$SCRATCH/logs" "$SCRATCH/verdicts" |
| +mkdir -p "$SCRATCH/logs" "$SCRATCH/verdicts" || { echo "cannot create $SCRATCH" >&2; exit 2; } |
| if [ ! -x "$BIN" ]; then |
| echo "no test binary at $BIN; build it with: go test -c -o $BIN ./internal/sim/hostlife/" >&2 |
| exit 2 |
| @@ -60,7 +60,10 @@ RULES="$*" |
| if [ -z "$RULES" ]; then |
| RULES=$(sed -n '/^var allRules/,/^}/p' "$PKG/rules_test.go" | grep -o '^\s*"[a-z0-9-]*"' | tr -d ' "\t') |
| fi |
| -rm -f "$SCRATCH"/verdicts/* |
| +# the rules that have witnesses (witness_test.go): a run of one of them |
| +# with no witness output is an ERROR, never "none" (R3-6) |
| +WRULES=$(grep -o '^\s*{"[a-z0-9-]*",' "$PKG/witness_test.go" | tr -d ' \t{",' | sort -u) |
| +rm -f "$SCRATCH"/verdicts/* || exit 2 |
| one() { |
| r=$1 |
| @@ -104,6 +107,14 @@ one() { |
| echo "ERROR $r: witness run rc=$wrc; see $wlog" | tee "$verdict" |
| return |
| fi |
| + if [ "$wit" = none ]; then |
| + for x in $(echo "$r" | tr ',' ' '); do |
| + if echo "$WRULES" | grep -qx "$x"; then |
| + echo "ERROR $r: $x has witnesses but the run produced no witness output; see $wlog" | tee "$verdict" |
| + return |
| + fi |
| + done |
| + fi |
| if [ -z "$sweep" ]; then |
| echo "ERROR $r: rc=$rc, no parsable sweep verdict; see $log" | tee "$verdict" |
| return |
| @@ -125,9 +136,28 @@ one() { |
| fi |
| } |
| export -f one |
| -export SEEDS PKG SCRATCH BIN |
| +export SEEDS PKG SCRATCH BIN WRULES |
| printf '%s\n' $RULES | xargs -P "${HOSTLIFE_PAR:-8}" -I{} bash -c 'one "$@"' _ {} |
| -bad=$(cat "$SCRATCH"/verdicts/* 2>/dev/null | grep -c "^ERROR\|^MISSED\|^STALE") |
| +xrc=$? |
| +if [ $xrc -ne 0 ]; then |
| + echo "sweep: orchestration failed (xargs rc=$xrc)" >&2 |
| + exit 2 |
| +fi |
| +# exactly one well-formed verdict per requested mutation (R3-6) |
| +want=$(printf '%s\n' $RULES | wc -l) |
| +have=$(ls "$SCRATCH"/verdicts 2>/dev/null | wc -l) |
| +if [ "$have" -ne "$want" ]; then |
| + echo "sweep: $want mutation(s) requested, $have verdict(s) written" >&2 |
| + exit 2 |
| +fi |
| +for r in $RULES; do |
| + v="$SCRATCH/verdicts/$(echo "$r" | tr ',' '+')" |
| + if ! grep -qE '^(CAUGHT|MISSED|EXPECTED-MISS|STALE|ERROR) ' "$v" 2>/dev/null; then |
| + echo "sweep: no well-formed verdict for $r" >&2 |
| + exit 2 |
| + fi |
| +done |
| +bad=$(cat "$SCRATCH"/verdicts/* | grep -c "^ERROR\|^MISSED\|^STALE") |
| if [ "$bad" -gt 0 ]; then |
| echo "sweep: $bad rule(s) ERROR, MISSED or STALE" >&2 |
| exit 1 |
diff --git a/internal/sim/hostlife/protocol_test.go b/internal/sim/hostlife/protocol_test.go| index 3ce546929..5b41f7687 100644 |
| --- a/internal/sim/hostlife/protocol_test.go |
| +++ b/internal/sim/hostlife/protocol_test.go |
| @@ -192,28 +192,75 @@ func (w *world) restore(b *box, inc int, loc, gen string) *localDB { |
| } |
| return db |
| } |
| + // the chain (rev 7.4 §5.1, R3-1): the generation's snapshot, named by |
| + // version id in generation.json, then the LTX objects of the |
| + // generation whose history extends what the chain holds, longest last. |
| + // A version whose history is a prefix of the chain is an older |
| + // checkpoint or a duplicate and is skipped; one that is neither is a |
| + // conflict, and the restore refuses rather than guess. Rev 7.3's model |
| + // took the union of every version's writes, which no restore can do. |
| + var history []int |
| found := false |
| - for _, k := range []string{dataKey(loc, gen, "base"), dataKey(loc, gen, "ltx")} { |
| - for _, v := range bk.objs[k] { |
| - if v.Marker { |
| - continue |
| - } |
| - found = true |
| - db.Writes = unionInts(db.Writes, v.B.Writes) |
| + if gen != "" { |
| + m := bk.current(genMarkerKey(loc)) |
| + if m == nil || m.B.Gen != gen { |
| + return nil // the marker does not name this generation: refuse |
| + } |
| + base := bk.byID(dataKey(loc, gen, "base"), m.B.Base) |
| + if base == nil || base.Marker { |
| + w.stats["restore refused: snapshot missing"]++ |
| + return nil |
| + } |
| + history = append([]int(nil), base.B.Writes...) |
| + db.Key = base.B.SealKey |
| + if base.B.Inc != 0 { |
| + db.Inc = base.B.Inc |
| + } |
| + found = true |
| + } |
| + for _, v := range bk.objs[dataKey(loc, gen, "ltx")] { |
| + if v.Marker { |
| + continue |
| + } |
| + found = true |
| + switch { |
| + case extends(v.B.Writes, history): |
| + history = append([]int(nil), v.B.Writes...) |
| if db.Key == 0 { |
| db.Key = v.B.SealKey |
| } |
| if v.B.Inc != 0 { |
| db.Inc = v.B.Inc |
| } |
| + case extends(history, v.B.Writes): |
| + // an older checkpoint, or a duplicate: skipped |
| + default: |
| + w.logf("box %d restore refused: %s version %d does not continue the chain", b.ID, dataKey(loc, gen, "ltx"), v.ID) |
| + w.stats["restore refused: conflicting history"]++ |
| + return nil |
| } |
| } |
| if !found && gen != "" { |
| return nil // an installed generation with nothing in it: refuse |
| } |
| + db.Writes = history |
| return db |
| } |
| +// fenced: the local retired marker refuses a writer for incarnation inc |
| +// carrying operation sequence seq (claim rev 6 §6.4, R3-3). The mutation |
| +// is rev 5.2's marker, which fences the whole incarnation for good. |
| +func (w *world) fenced(b *box, inc, seq int) bool { |
| + f, ok := b.Fence[inc] |
| + if !ok { |
| + return false |
| + } |
| + if !on("fence-by-installation") { |
| + return true |
| + } |
| + return seq <= f |
| +} |
| + |
| func unionInts(a, b []int) []int { |
| seen := map[int]bool{} |
| var out []int |
| @@ -354,8 +401,8 @@ func (w *world) admits(b *box, c *claim, probe string) bool { |
| if on("exec-admission") && c.Op.Exec != b.ID { |
| return false |
| } |
| - if b.Retired[c.Holder.Inc] { |
| - return false |
| + if w.fenced(b, c.Holder.Inc, w.opSeq(c.Op.ID)) { |
| + return false // retired here by this operation or a later one (claim rev 6 §6.4) |
| } |
| if w.isParticipant(c, b) && b.ExecUntil > 0 && w.localNow(b) > b.ExecUntil { |
| return false // self-fenced until the lease is renewed |
| @@ -502,13 +549,15 @@ func (w *world) parkDepth(b *box, prefix, dest string, quiet int, keep func(stri |
| // guard: a retired marker first, then each artifact renamed aside, one per |
| // call, so a crash can fall between any two (claim §6.3). It reports |
| // whether nothing is left. |
| -func (w *world) localPark(b *box, inc int) bool { |
| - if on("hostguard") && !b.Retired[inc] { |
| - if b.Retired == nil { |
| - b.Retired = map[int]bool{} |
| +func (w *world) localPark(b *box, inc int, seq int) bool { |
| + if on("hostguard") { |
| + if f, ok := b.Fence[inc]; !ok || f < seq { |
| + if b.Fence == nil { |
| + b.Fence = map[int]int{} |
| + } |
| + b.Fence[inc] = seq // {incarnation, op of the installation being retired} |
| + return false |
| } |
| - b.Retired[inc] = true |
| - return false |
| } |
| switch { |
| case b.DB != nil: |
| @@ -555,7 +604,7 @@ func (w *world) doObligation(b *box, c *claim, o obligation) { |
| if b.DB != nil && b.DB.Inc != 0 { |
| inc = b.DB.Inc |
| } |
| - if !w.localPark(b, inc) { |
| + if !w.localPark(b, inc, w.opSeq(o.Op)) { |
| return // the next artifact on a later step |
| } |
| if b.Row != nil && b.Row.HoldOp == o.Op || b.Row != nil && (c.Holder == nil || b.ID != c.Op.Exec) { |
diff --git a/internal/sim/hostlife/rules_test.go b/internal/sim/hostlife/rules_test.go| index d1eed185d..4071d38f5 100644 |
| --- a/internal/sim/hostlife/rules_test.go |
| +++ b/internal/sim/hostlife/rules_test.go |
| @@ -54,6 +54,7 @@ var allRules = []string{ |
| "park-skip-lock", // §6.2 step 2/J-N6 |
| "retirement-ids", // §6.2/J-D5/J-N7 |
| "hostguard", // §6.4/J-N8 |
| + "fence-by-installation", // claim rev 6 §6.4 (R3-3): the retired marker is {incarnation, op}; a new installation replaces it; the mutation fences the whole incarnation for good |
| "purge-reserve-first", // §5.3/J-N9 |
| "purge-adopts", // this model's finding: purge claims unclaimed legacy records first |
| "purge-journal", // this model's finding: the reservation is the purge's journal |
| @@ -65,6 +66,7 @@ var allRules = []string{ |
| "claim-never-deleted", // claim rev 5.2 C5a (CC22): a claim object is never deleted; a fence on an absent claim is released by writing free |
| "cancelled-creates", // claim rev 4 §5.1 (J2-R2-7): a late record PUT is removed |
| "orphan-no-deadline", // CC17: ... whenever it lands, not only before `until` |
| + "orphan-order", // claim rev 6 §5.1 step 5 (R3-2): read the record, then the claim fresh, then DeleteIfMatch; the mutation reads the claim first |
| "door-by-version", // §6.5/J-N10 |
| "door-reread", // claim rev 4 §6.5 (J2-R2-4): O2 refuses if the holder or op changed |
| "strict-spawn", // §6.1/J-D3 |
| @@ -80,6 +82,7 @@ var allRules = []string{ |
| "quiet-before-ack", // this model's finding (late writes after a park) |
| "straggler-sweep", // claim rev 5 §6.2a (CC15): the at-rest sweep |
| "sweep-staging", // CC20: the sweep also covers moves/<host>/ |
| + "sweep-namespace", // claim rev 6 §6.2a (R3-4): the sweep discovers locations from the namespace; the mutation reads the capped retired_incarnations |
| // moves spec |
| "seal-by-version", // J-N2: landing copies sealed versions |
| "staging-quiet", // J-N2: staging retired after its writers' horizon |
diff --git a/internal/sim/hostlife/sim_test.go b/internal/sim/hostlife/sim_test.go| index 32acfd089..557a99bc9 100644 |
| --- a/internal/sim/hostlife/sim_test.go |
| +++ b/internal/sim/hostlife/sim_test.go |
| @@ -53,7 +53,7 @@ func (w *world) legacyStart() { |
| b := w.regionBox(r) |
| w.nextInc++ |
| inc := w.nextInc |
| - w.rec = &record{Inc: inc, App: app0, Region: r} |
| + w.rec = &record{Ver: w.newVer(), Inc: inc, App: app0, Region: r} |
| w.legacyIncs[inc] = true |
| key := 7 |
| var writes []int |
diff --git a/internal/sim/hostlife/witness_test.go b/internal/sim/hostlife/witness_test.go| index 842abb56b..d2763de54 100644 |
| --- a/internal/sim/hostlife/witness_test.go |
| +++ b/internal/sim/hostlife/witness_test.go |
| @@ -39,110 +39,170 @@ func (quiet) Intn(n int) int { |
| type witness struct { |
| rule string // the rule it is for |
| needs string // the mutation set under which it must violate: the rule alone, or a combination the rule belongs to |
| + want string // the failure the scenario names: a substring of the first violation (R3 review) |
| note string // what it shows |
| run func(t *testing.T, w *world) |
| } |
| var witnesses = []witness{ |
| - {"generation-conditional", "generation-conditional", |
| + {"generation-conditional", "generation-conditional", "cannot start the host", |
| "an earlier push's generation.json PUT completes after a later push's; unconditional, it puts the old generation back and the serving box cannot start", wGenerationConditional}, |
| - {"lost-return-park", "lost-return-park", |
| + {"lost-return-park", "lost-return-park", "ended with residue", |
| "a target stopped after its first return PUT is declared lost; without the park the lane stays in the source region at the release (INV-10)", wLostReturnPark}, |
| - {"declare-lost-compute", "declare-lost-compute", |
| + {"declare-lost-compute", "declare-lost-compute", "INV-1", |
| "a frozen target's lease expires; declared lost on expiry alone, it resumes beside the recovered source (INV-1)", wDeclareLostCompute}, |
| - {"watchdog-independent", "declare-lost-compute,watchdog-independent", |
| + {"watchdog-independent", "declare-lost-compute,watchdog-independent", "INV-1", |
| "redundant alone: with compute fencing a paused agent cannot be declared lost; with expiry-based declare-lost, a watchdog inside the paused agent never fences, and the target runs beside the recovered source (INV-1)", wWatchdogIndependent}, |
| - {"lost-quarantine", "lost-quarantine", |
| + {"lost-quarantine", "lost-quarantine", "holds local state", |
| "a lost box starts again with its old disk; without the quarantine it keeps a database and files for a host served elsewhere (INV-10)", wLostQuarantine}, |
| - {"markers-last", "markers-last", |
| + {"markers-last", "markers-last", "acknowledged timer", |
| "the target's agent crashes between extracting the files and writing the marker; a marker written first vouches for timers that were never installed (INV-2)", wMarkersLast}, |
| - {"rollback-journal", "rollback-journal", |
| + {"rollback-journal", "rollback-journal", "cold restore", |
| "the source's agent restarts during a dirty rollback's probe; without the journal it restarts at `claimed`, parks the return generation it had replicated into, and a durable write is lost on cold restore (INV-2)", wRollbackJournal}, |
| - {"seal-by-version", "seal-by-version", |
| + {"seal-by-version", "seal-by-version", "cold restore", |
| "a pre-cut staging round completes after the seal; a landing that copies the current version installs the stale round and loses the writes made after it (INV-2)", wSealByVersion}, |
| - {"staging-quiet", "staging-quiet", |
| + {"staging-quiet", "staging-quiet", "ended with residue", |
| "a staging round completes after the landing's staging park acknowledged; retired at the seal rather than after the writers' horizon, the round is residue at the release (INV-10)", wStagingQuiet}, |
| - {"claim-cas-opid", "claim-cas-opid,revalidate-before-effect", |
| + {"claim-cas-opid", "claim-cas-opid,revalidate-before-effect", "store of app", |
| "redundant alone: a stalled source goroutine with the rollback's last read resumes after a purge claimed the host; revalidation stops it, and so does the op-id condition on its release CAS; with both gone the release overwrites the purge and the store is torn down under a serving host", wClaimCasOpID}, |
| - {"dirty-return", "dirty-return", |
| + {"dirty-return", "dirty-return", "INV-2 (local)", |
| "a target that wrote during its probe is rolled back; without the return its writes are lost (INV-2)", wDirtyReturn}, |
| - {"commit-before-open", "commit-before-open,dirty-return", |
| - "redundant alone in this model: a row opened before the commit admits nothing while the claim is uncommitted; the only violation the scenario can show is dirty-return's", wDirtyReturn}, |
| - {"exec-admission", "exec-admission,hold-op-open,start-check-claim-gen", |
| + {"commit-before-open", "commit-before-open", "INV-5", |
| + "a public request reaches the target's edge while its probe runs; a row opened at the probe routes it before the commit (INV-5, R3-5)", wCommitBeforeOpen}, |
| + {"exec-admission", "exec-admission,hold-op-open,start-check-claim-gen", "INV-1", |
| "one of three admission fences (J2-R2-8): a paused open from an earlier operation makes the old source ready after the commit; hold_op refuses the open, the exec check refuses the wake, the generation check refuses the start; with all three gone the source serves beside the target (INV-1)", wAdmissionTriple}, |
| - {"hold-op-open", "exec-admission,hold-op-open,start-check-claim-gen", "one of three admission fences (see exec-admission)", wAdmissionTriple}, |
| - {"start-check-claim-gen", "exec-admission,hold-op-open,start-check-claim-gen", "one of three admission fences (see exec-admission)", wAdmissionTriple}, |
| - {"start-check", "exec-admission,hold-op-open,start-check", "the whole start check in place of its generation clause (see exec-admission)", wAdmissionTriple}, |
| - {"strict-spawn", "strict-spawn,evidence-whole-tree", |
| + {"hold-op-open", "exec-admission,hold-op-open,start-check-claim-gen", "INV-1", "one of three admission fences (see exec-admission)", wAdmissionTriple}, |
| + {"start-check-claim-gen", "exec-admission,hold-op-open,start-check-claim-gen", "INV-1", "one of three admission fences (see exec-admission)", wAdmissionTriple}, |
| + {"start-check", "exec-admission,hold-op-open,start-check", "INV-1", "the whole start check in place of its generation clause (see exec-admission)", wAdmissionTriple}, |
| + {"strict-spawn", "strict-spawn,evidence-whole-tree", "INV-1", |
| "redundant alone: an escaped descendant is killed by the whole-tree cleanup; with evidence blind to escapees, a non-strict descendant survives the cut and writes beside the target (INV-1)", wStrictSpawn}, |
| - {"touched-incomplete", "touched-incomplete,legacy-discovery", |
| + {"touched-incomplete", "touched-incomplete,legacy-discovery", "freed with residue", |
| "redundant alone: discovery at adoption parks the other regions; without discovery, an incomplete touched set must park every region at delete, or a pre-release replica is residue after free (INV-10)", wTouchedIncomplete}, |
| - {"door-reread", "door-reread,location-per-incarnation", |
| + {"door-reread", "door-reread,location-per-incarnation", "door:", |
| "subsumed by C3a: a listing authorized for the old incarnation selects, after a recreate into the shared location, the new incarnation's object; O2 refuses it", wDoorReread}, |
| - {"door-by-version", "door-by-version,location-per-incarnation", |
| + {"door-by-version", "door-by-version,location-per-incarnation", "door:", |
| "subsumed by C3a: a handle signed before the delete opens, after a recreate into the shared location, the key's current object unless bound to the version it selected", wDoorByVersion}, |
| - {"registration-check", "registration-check,fence-etag", |
| + {"registration-check", "registration-check,fence-etag", "store of app", |
| "a cheap extra: a creator paused across a whole purge resumes; the fence and the ETag condition refuse it without the re-read; with the ETag condition gone the re-read is what stops it", wRegistrationCheck}, |
| - {"registration-check", "registration-check,purge-claim-fence", |
| + {"registration-check", "registration-check,purge-claim-fence", "store of app", |
| "the same, with the fence gone instead", wRegistrationCheck}, |
| -} |
| - |
| -// TestWitnesses runs every witness. With no mutation every witness must |
| -// hold. Under HOSTLIFE_MUTATE=m it runs the witnesses of the rules in m |
| -// and reports each as violated or held; a witness whose stated mutation |
| -// set is within m must violate, or the witness is broken and the test |
| -// fails. HOSTLIFE_WITNESS=rule runs one rule's witnesses with their trace. |
| + // rev 7.4 |
| + {"fence-by-installation", "fence-by-installation", "INV-3 (witness): instance back on box 0", |
| + "a round trip UK→US→UK (R3-3): the second landing replaces the retired marker UK wrote after the first move; a marker for the whole incarnation refuses the probe, the move back rolls back, and the instance never serves on UK again", wRoundTrip}, |
| + {"orphan-order", "orphan-order", "orphan cleanup deleted the record", |
| + "the cleanup reads the claim first and pauses; a create removes the orphan, claims and publishes; the cleanup reads that record, judges it by the stale claim and deletes it (R3-2)", wOrphanOrder}, |
| + {"sweep-namespace", "sweep-namespace", "residue never retired", |
| + "a replication PUT of incarnation 1 completes after 33 recreates dropped it from retired_incarnations; a sweep reading that list never finds it (R3-4)", wSweepNamespace}, |
| + {"recovery-current-inputs", "recovery-current-inputs", "stuck: source could not recover", |
| + "a bundle is published after admission and the target writes; the dirty recovery renders current inputs; gated on move.inputs it never passes its probe (R2-5, §7.8)", wRecoveryInputs}, |
| +} |
| + |
| +// TestWitnesses is the deterministic half of the mutation evidence. |
| +// |
| +// With no mutation (the gate) it proves every witness's claim in full: |
| +// the scenario holds with every rule in place, holds under every proper |
| +// subset of its stated mutation set (so a rule a combination names is |
| +// shown necessary, not assumed), and under the whole set violates the |
| +// failure the scenario names, not merely some invariant. |
| +// |
| +// Under HOSTLIFE_MUTATE=m (the harness) it runs the witnesses of the |
| +// rules in m and reports each as violated or held; a witness whose set is |
| +// within m must violate with its named failure, or the test fails (the |
| +// witness is broken, not the rule). HOSTLIFE_WITNESS=rule runs one rule's |
| +// witnesses with their trace. |
| func TestWitnesses(t *testing.T) { |
| - set := map[string]bool{} |
| - for _, m := range strings.Split(mutated, ",") { |
| - if m != "" { |
| - set[m] = true |
| + only := os.Getenv("HOSTLIFE_WITNESS") |
| + if mutated == "" { |
| + ran := 0 |
| + for _, x := range witnesses { |
| + if only != "" && x.rule != only { |
| + continue |
| + } |
| + ran++ |
| + check(t, x, "", false, only != "") |
| + for _, s := range properSubsets(x.needs) { |
| + check(t, x, s, false, only != "") |
| + } |
| + check(t, x, x.needs, true, only != "") |
| + } |
| + if only != "" && ran == 0 { |
| + t.Fatalf("no witness for rule %q", only) |
| } |
| + return |
| } |
| - only := os.Getenv("HOSTLIFE_WITNESS") |
| - ran := 0 |
| + set := mutationSet(mutated) |
| for _, x := range witnesses { |
| if only != "" && x.rule != only { |
| continue |
| } |
| - if mutated != "" && !set[x.rule] { |
| + if !set[x.rule] { |
| continue |
| } |
| - ran++ |
| - w := newWitness() |
| - x.run(t, w) |
| - violated := len(w.violations) > 0 |
| needs := true |
| for _, m := range strings.Split(x.needs, ",") { |
| if !set[m] { |
| needs = false |
| } |
| } |
| - tag := "held" |
| - if violated { |
| - tag = "violated: " + w.violations[0] |
| + check(t, x, mutated, needs, only != "") |
| + } |
| +} |
| + |
| +// check runs one witness under mutation m, reports it, and fails the |
| +// test if the outcome is not the stated one: held when no violation is |
| +// expected, the named failure when one is. |
| +func check(t *testing.T, x witness, m string, expectViolation bool, trace bool) { |
| + saved := mutated |
| + mutated = m |
| + defer func() { mutated = saved }() |
| + w := newWitness() |
| + x.run(t, w) |
| + violated := len(w.violations) > 0 |
| + tag := "held" |
| + if violated { |
| + tag = "violated: " + w.violations[0] |
| + } |
| + t.Logf("witness %s under %q (needs %q): %s", x.rule, m, x.needs, tag) |
| + switch { |
| + case expectViolation && !violated: |
| + t.Errorf("witness %s held under %q, which it must violate", x.rule, m) |
| + dump(t, w) |
| + case expectViolation && !strings.Contains(w.violations[0], x.want): |
| + t.Errorf("witness %s under %q violated, but not its named failure %q", x.rule, m, x.want) |
| + dump(t, w) |
| + case !expectViolation && violated: |
| + t.Errorf("witness %s violated under %q, where it must hold", x.rule, m) |
| + dump(t, w) |
| + } |
| + if trace { |
| + dump(t, w) |
| + } |
| +} |
| + |
| +func mutationSet(m string) map[string]bool { |
| + set := map[string]bool{} |
| + for _, x := range strings.Split(m, ",") { |
| + if x != "" { |
| + set[x] = true |
| } |
| - switch { |
| - case mutated == "": |
| - t.Logf("witness %s: %s", x.rule, tag) |
| - if violated { |
| - t.Errorf("witness %s violated with every rule in place", x.rule) |
| - dump(t, w) |
| - } |
| - default: |
| - t.Logf("witness %s under %q (needs %q): %s", x.rule, mutated, x.needs, tag) |
| - if needs && !violated { |
| - t.Errorf("witness %s held under %q, which it must violate", x.rule, mutated) |
| - dump(t, w) |
| + } |
| + return set |
| +} |
| + |
| +// properSubsets: every non-empty proper subset of a comma-separated set. |
| +func properSubsets(needs string) []string { |
| + xs := strings.Split(needs, ",") |
| + var out []string |
| + for mask := 1; mask < (1<<len(xs))-1; mask++ { |
| + var sub []string |
| + for i, x := range xs { |
| + if mask&(1<<i) != 0 { |
| + sub = append(sub, x) |
| } |
| } |
| - if only != "" { |
| - dump(t, w) |
| - } |
| - } |
| - if only != "" && ran == 0 { |
| - t.Fatalf("no witness for rule %q", only) |
| + out = append(out, strings.Join(sub, ",")) |
| } |
| + return out |
| } |
| func dump(t *testing.T, w *world) { |
| @@ -196,7 +256,7 @@ func (w *world) serve(b *box, inc int, app string) { |
| n.Op = opState{Kind: "serving", Exec: b.ID, Parts: []int{b.ID}} |
| n.Regions, n.Boxes, n.Complete, n.Obl = []int{b.Region}, []int{b.ID}, true, nil |
| w.claim = n |
| - w.rec = &record{Inc: inc, App: app, Region: b.Region} |
| + w.rec = &record{Ver: w.newVer(), Inc: inc, App: app, Region: b.Region} |
| b.Row = &row{Inc: inc, App: app, Status: "ready"} |
| b.DB = &localDB{Inc: inc, Loc: loc, Key: key, Writes: append([]int(nil), writes...)} |
| b.Files = &filesDir{Inc: inc, Key: key, Env: key, Done: true} |
| @@ -213,7 +273,7 @@ func (w *world) serve(b *box, inc int, app string) { |
| func (w *world) legacy(b *box, other int) { |
| w.nextInc++ |
| inc := w.nextInc |
| - w.rec = &record{Inc: inc, App: app0, Region: b.Region} |
| + w.rec = &record{Ver: w.newVer(), Inc: inc, App: app0, Region: b.Region} |
| w.legacyIncs[inc] = true |
| key := 7 |
| var writes []int |
| @@ -303,23 +363,45 @@ func (w *world) act(bs ...*box) func() { |
| } |
| } |
| -// actAll runs every live box, replacements included. |
| +// actAll runs every live box, replacements included: its worker, |
| +// obligation runner and reconcile, and the config-sync and adoption |
| +// passes a serving row needs before the host is at rest. |
| func (w *world) actAll() func() { |
| return func() { |
| for _, b := range w.liveBoxes() { |
| w.worker(b) |
| w.obligationRunner(b) |
| w.reconcile(b) |
| + if len(b.plans) == 0 { |
| + w.passPlan(b, "config") |
| + w.passPlan(b, "adopt") |
| + } |
| + w.passExec(b) |
| } |
| } |
| } |
| // runConsole runs one step of every console plan, in order: a |
| // deterministic consoleStep. |
| -func (w *world) runConsole() { |
| +func (w *world) runConsole() { w.runPlans(nil) } |
| + |
| +// runPlans runs one step of every console plan but skip. A plan may add |
| +// another (a create's orphan cleanup); the new one is kept for the next |
| +// step. |
| +func (w *world) runPlans(skip *consolePlan) { |
| + plans := append([]*consolePlan(nil), w.console...) |
| + done := map[*consolePlan]bool{} |
| + for _, p := range plans { |
| + if p == skip || p.Stall > w.now { |
| + continue |
| + } |
| + if w.runPlan(p) { |
| + done[p] = true |
| + } |
| + } |
| var keep []*consolePlan |
| for _, p := range w.console { |
| - if p.Stall > w.now || !w.runPlan(p) { |
| + if !done[p] { |
| keep = append(keep, p) |
| } |
| } |
| @@ -736,3 +818,122 @@ func wRegistrationCheck(t *testing.T, w *world) { |
| w.tick(func() { w.runPlan(p) }) // the creator resumes |
| } |
| } |
| + |
| +// ---------- rev 7.4 ---------- |
| + |
| +// wRoundTrip (claim rev 6 §6.4, R3-3): UK→US, then US→UK. The first |
| +// move's retirement wrote UK's local marker for the incarnation; the |
| +// second landing must replace it. Unmutated, the instance must serve on |
| +// UK again, running. |
| +func wRoundTrip(t *testing.T, w *world) { |
| + uk, us := w.boxes[0], w.boxes[1] |
| + w.serve(uk, 1, app0) |
| + w.moveTo(us.Region) |
| + w.reach(t, 1500, "serving on box 1 after the first move", func() bool { |
| + c := w.claim |
| + return c.Op.Kind == "serving" && c.Op.Exec == us.ID && w.rec != nil && w.rec.MoveID == "" && len(c.Obl) == 0 |
| + }, w.act(uk, us), w.recoveryPass) |
| + if _, fenced := uk.Fence[1]; !fenced { |
| + t.Fatalf("witness: box 0 wrote no retired marker: %s%s", w.state(), w.boxesState()) |
| + } |
| + w.moveTo(uk.Region) |
| + if w.claim.Op.Kind != "moving" { |
| + t.Fatalf("witness: the move back did not start: %s", w.state()) |
| + } |
| + w.reach(t, 1500, "instance back on box 0, running", func() bool { |
| + c := w.claim |
| + return c.Op.Kind == "serving" && c.Op.Exec == uk.ID && hasMain(uk) |
| + }, w.act(uk, us), w.recoveryPass, w.operator) |
| + w.finish(t) |
| +} |
| + |
| +// runOthers runs every console plan but skip, one step each, removing |
| +// the finished ones. |
| +func (w *world) runOthers(skip *consolePlan) func() { |
| + return func() { w.runPlans(skip) } |
| +} |
| + |
| +// wOrphanOrder (claim rev 6 §5.1 step 5, R3-2): a cancelled create's |
| +// record lands late; the recovery pass starts its cleanup and pauses |
| +// after its first observation; a create of the next incarnation removes |
| +// the orphan itself, claims and publishes; the paused cleanup resumes. |
| +func wOrphanOrder(t *testing.T, w *world) { |
| + w.claim = &claim{Ver: w.newVer(), Retired: []int{1}, Cancelled: []cancelledCreate{{Inc: 1, Until: w.now + 1000}}} |
| + w.nextInc = 1 |
| + w.rec = &record{Ver: w.newVer(), Inc: 1, App: app0, Region: 0} |
| + w.logf("witness: the record of cancelled incarnation 1 landed") |
| + w.recoveryPass() |
| + var p1 *consolePlan |
| + for _, p := range w.console { |
| + if p.Kind == "orphan" { |
| + p1 = p |
| + } |
| + } |
| + if p1 == nil { |
| + t.Fatalf("witness: the recovery pass started no cleanup: %s", w.state()) |
| + } |
| + w.tick(func() { w.runPlan(p1) }) // the first observation; then the console pauses |
| + cr := &consolePlan{Kind: "create", Host: "h", App: app0, OpID: w.newID("cr"), Inc: 2, Region: 0} |
| + w.console = append(w.console, cr) |
| + w.reach(t, 50, "incarnation 2 claimed and published", func() bool { |
| + return w.rec != nil && w.rec.Inc == 2 |
| + }, w.runOthers(p1)) |
| + w.tick(func() { w.runPlan(p1) }) // the paused cleanup resumes |
| + w.tick(func() { w.runPlan(p1) }) |
| + w.finish(t) |
| +} |
| + |
| +// wSweepNamespace (claim rev 6 §6.2a, R3-4): a replication PUT of |
| +// incarnation 1 is accepted and completes after 33 delete-and-recreate |
| +// cycles, by which time retired_incarnations no longer lists 1. |
| +func wSweepNamespace(t *testing.T, w *world) { |
| + b := w.boxes[0] |
| + w.serve(b, 1, app0) |
| + w.wake(b) |
| + if !hasMain(b) { |
| + t.Fatalf("witness: the host did not wake: %s", w.state()) |
| + } |
| + key := dataKey(w.claim.Holder.Location, "", "ltx") |
| + w.holdKey(key) |
| + w.replicate(b) |
| + w.hold = nil |
| + for inc := 2; inc <= retiredCap+2; inc++ { |
| + w.recreate(t, 0, inc) |
| + if len(w.violations) > 0 { |
| + return |
| + } |
| + } |
| + if contains(w.claim.Retired, 1) { |
| + t.Fatalf("witness: incarnation 1 is still in retired_incarnations after %d recreates", retiredCap+1) |
| + } |
| + if w.completeHeld(key) != 1 { |
| + t.Fatalf("witness: no held replication PUT") |
| + } |
| + w.finish(t) |
| +} |
| + |
| +// wCommitBeforeOpen (INV-5, R3-5): a public request reaches the target's |
| +// edge while its probe runs. The edge routes on the row. |
| +func wCommitBeforeOpen(t *testing.T, w *world) { |
| + src, tgt := w.boxes[0], w.boxes[1] |
| + w.serve(src, 1, app0) |
| + w.landProbed(t, src, tgt) |
| + w.wake(tgt) |
| + w.checkStep() |
| + w.finish(t) |
| +} |
| + |
| +// wRecoveryInputs (§7.8, R2-5): a config bundle is published after the |
| +// move was admitted; the target does real work and the rollback is |
| +// dirty; the source's recovery install must render current inputs, not |
| +// the inputs the move pinned. |
| +func wRecoveryInputs(t *testing.T, w *world) { |
| + src, tgt := w.boxes[0], w.boxes[1] |
| + w.serve(src, 1, app0) |
| + w.landProbed(t, src, tgt) |
| + w.cfgVer[app0]++ |
| + w.logf("witness: config bundle %s v%d published during the settle window", app0, w.cfgVer[app0]) |
| + w.appWrite(tgt) |
| + w.rollback(w.claim, "settle check failed") |
| + w.finish(t) |
| +} |
diff --git a/internal/sim/hostlife/world_test.go b/internal/sim/hostlife/world_test.go| index 0892dab88..a483ebcdf 100644 |
| --- a/internal/sim/hostlife/world_test.go |
| +++ b/internal/sim/hostlife/world_test.go |
| @@ -52,14 +52,40 @@ const ( |
| maxPause = 3 // a typical pause between a check and the act (a VM freeze is longer) |
| sigAge = 30 // S3's signature-age limit; H covers it plus the longest request |
| beyondH = 20 // one long-tail request in this many completes after H (R2-1) |
| + retiredCap = 32 // retired_incarnations keeps this many (claim rev 6 §2) |
| ) |
| +// retire adds inc to retired_incarnations, dropping the oldest past the cap. |
| +func retire(xs []int, inc int) []int { |
| + xs = addUniq(xs, inc) |
| + if len(xs) > retiredCap { |
| + xs = append([]int(nil), xs[len(xs)-retiredCap:]...) |
| + } |
| + return xs |
| +} |
| + |
| +// extends: history a is b with zero or more later transactions appended |
| +// (R3-1: a replica object continues the chain only if its history is an |
| +// extension of what the chain holds). |
| +func extends(a, b []int) bool { |
| + if len(a) < len(b) { |
| + return false |
| + } |
| + for i := range b { |
| + if a[i] != b[i] { |
| + return false |
| + } |
| + } |
| + return true |
| +} |
| + |
| // ---------- storage ---------- |
| type blob struct { |
| - Kind string // "ltx", "base", "files", "snap", "lock", "manifest", "lease", "report" |
| + Kind string // "ltx", "base", "files", "snap", "lock", "manifest", "lease", "report", "gen" |
| Inc int // incarnation tag; 0 = untagged legacy |
| Gen string // lineage that wrote it |
| + Base int // a "gen" marker: the version id of the generation's snapshot (R3-1) |
| Seq int |
| SealKey int // the instance.key the data is sealed with |
| Writes []int |
| @@ -284,8 +310,13 @@ type box struct { |
| History []int // delivered history (disposable) |
| Attempt int // runner bookkeeping |
| Procs []*proc |
| - Retired map[int]bool // retired-incarnation markers (hostguard) |
| - Parked int // count of locally parked artifacts |
| + // Fence is the local retired marker, per incarnation (claim rev 6 §6.4, |
| + // R3-3): {incarnation, op}. It refuses a writer for that incarnation |
| + // whose operation is at or before the fence's; a new installation of |
| + // the incarnation by a later operation replaces it under the guard. |
| + // The value is the sequence of the fence's op (opSeq). |
| + Fence map[int]int |
| + Parked int // count of locally parked artifacts |
| ExecUntil int // local exec-lease file (watchdog input); 0 none |
| // in-memory, lost on crash |
| @@ -311,6 +342,27 @@ type plan struct { |
| App string |
| Ver int // the config bundle version it selected |
| At int // it takes the guard no earlier than this |
| + // Seq is the operation identity the pass validated under (R2-3): the |
| + // sequence of the newest operation when it selected the row. The |
| + // host guard refuses it once the local fence is at or past it. |
| + Seq int |
| +} |
| + |
| +// opSeq orders operations: every op id the model mints carries the |
| +// global counter, so a later operation has a larger sequence. The serving |
| +// state has no op id and sorts as "now". Claim rev 6's marker names the |
| +// op id of the installation; the ordering it needs is this one. |
| +func (w *world) opSeq(id string) int { |
| + if id == "" || id == "sweep" || id == "adopt" { |
| + return w.nextID |
| + } |
| + n := 0 |
| + for _, r := range id { |
| + if r >= '0' && r <= '9' { |
| + n = n*10 + int(r-'0') |
| + } |
| + } |
| + return n |
| } |
| func (b *box) forget() { |
| @@ -407,6 +459,11 @@ type opState struct { |
| // 5.2 §5.3). Its release writes a free claim; the mutation of |
| // claim-never-deleted deletes the object instead |
| FencedAbsent bool |
| + // BaseVer is the version id of the generation's installed snapshot, |
| + // recorded by the install manifest and named by generation.json: the |
| + // immutable snapshot identity the restore starts from (rev 7.4 §5.1, |
| + // R3-1) |
| + BaseVer int |
| } |
| type digest struct { |
| @@ -425,6 +482,9 @@ type claim struct { |
| Complete bool |
| Obl []obligation |
| Lost []int |
| + // Retired is retired_incarnations: anti-reuse only, capped at |
| + // retiredCap entries (claim rev 6 §2, §6.2a). The sweep does not read |
| + // it; it discovers locations from the namespace (R3-4). |
| Retired []int |
| Quiet [nRegions]int |
| PurgeRes bool |