amadan
sim: hostlife on claim rev 5, with a biased delete-and-recreate schedule
Claim rev 5 (4a458a9c) re-encoded: the at-rest sweep as claim §6.2a states it, under a park-sweep obligation the sweeping box owns (CC15); registrations renewed by their console and drained only when expired and unclaimed (CC16); orphan records at any time, removed by the pass or by a create that finds its key occupied (CC17); holder.generation (CC18); signatures taken at the deadline check, with an SDK retry that would re-sign (CC19). Two rules the strict model needed beyond rev 5: sweep-staging (CC20: the sweep must also cover moves/<host>/) and registration-check (CC21: a create checks its registration right before its claim CAS). The biased schedule (half the seeds): a host is recreated at once where it last served; the old executor's last replication PUT completes at its worst moment, after the recreate; door listings stall until the location's object belongs to another incarnation. location-per-incarnation (C3a) is now caught alone, and both door rules with it.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
8 files changed,
+241
−106
internal/sim/hostlife/background_test.go+3 −0internal/sim/hostlife/console_test.go+87 −25internal/sim/hostlife/expected-outcomes.txt+2 −3internal/sim/hostlife/moves_test.go+72 −38internal/sim/hostlife/protocol_test.go+9 −1internal/sim/hostlife/rules_test.go+4 −1internal/sim/hostlife/sim_test.go+3 −2internal/sim/hostlife/world_test.go+61 −36
diff --git a/internal/sim/hostlife/background_test.go b/internal/sim/hostlife/background_test.go| index e3c28c213..40fed13a1 100644 |
| --- a/internal/sim/hostlife/background_test.go |
| +++ b/internal/sim/hostlife/background_test.go |
| @@ -306,6 +306,9 @@ func (w *world) fault() { |
| if len(w.pending) > 0 && w.rng.Intn(3) == 0 { |
| i := w.rng.Intn(len(w.pending)) |
| r := w.pending[i] |
| + if r.beyond && w.fail["recreate"] { |
| + return // the biased schedule keeps it for its worst moment |
| + } |
| w.pending = append(w.pending[:i:i], w.pending[i+1:]...) |
| w.complete(r) |
| return |
diff --git a/internal/sim/hostlife/console_test.go b/internal/sim/hostlife/console_test.go| index 1a403c781..5a37078bc 100644 |
| --- a/internal/sim/hostlife/console_test.go |
| +++ b/internal/sim/hostlife/console_test.go |
| @@ -28,7 +28,8 @@ type doorPlan struct { |
| Key string |
| Ver int |
| Signed bool |
| - Until int // a stalled step may resume until then (one in four stall long) |
| + Adv bool // the biased schedule stalls this one until its worst moment |
| + Until int // a stalled step may resume until then (one in four stall long) |
| } |
| func (w *world) execBox(c *claim) *box { |
| @@ -114,6 +115,11 @@ func (w *world) createSteps(p *consolePlan) bool { |
| delete(ad.Reg, p.OpID) |
| return true |
| } |
| + if e, ok := ad.Reg[p.OpID]; ok && p.Step > 0 { |
| + // the creating console renews its registration lease (CC16) |
| + e.Until = w.now + 60 |
| + ad.Reg[p.OpID] = e |
| + } |
| switch p.Step { |
| case 0: |
| // app admission (claim rev 4 §5.1 step 0): register while open. |
| @@ -132,8 +138,8 @@ func (w *world) createSteps(p *consolePlan) bool { |
| p.Step = 1 |
| return false |
| case 1: |
| - if e, ok := ad.Reg[p.OpID]; on("admission-registration") && on("registration-recovery") && (!ok || w.now > e.Until-maxPause) { |
| - return abandon() // the registration lease ended before the claim CAS |
| + if _, ok := ad.Reg[p.OpID]; on("admission-registration") && on("registration-check") && !ok { |
| + return abandon() // CC21: the registration is gone; the claim CAS must not follow |
| } |
| if p.Host == "h2" { |
| if w.h2.Kind != "" { |
| @@ -145,7 +151,21 @@ func (w *world) createSteps(p *consolePlan) bool { |
| return false |
| } |
| c := w.claim |
| - if c != nil && (c.Holder != nil || (c.Op.Kind != "" && c.Op.Kind != "serving")) || w.rec != nil || w.recPend != nil { |
| + if c != nil && (c.Holder != nil || (c.Op.Kind != "" && c.Op.Kind != "serving")) || w.recPend != nil { |
| + return abandon() |
| + } |
| + if c != nil && len(c.Obl) > 0 { |
| + 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 |
| + // 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 |
| + return false |
| + } |
| return abandon() |
| } |
| b := w.regionBox(p.Region) |
| @@ -245,6 +265,19 @@ func (w *world) userDelete() { |
| return |
| } |
| id := w.newID("del") |
| + if e := w.execBox(c); e != nil { |
| + w.lastRegion = e.Region |
| + } |
| + if w.fail["recreate"] && c.Op.Kind == "serving" { |
| + w.doorAuthorize() // a door listing that will race the delete and a recreate |
| + if e := w.execBox(c); e != nil && e.DB != nil && hasMain(e) && w.rng.Intn(2) == 0 { |
| + // the replicator's last PUT before the delete's stop evidence: |
| + // accepted, then completing after the host is recreated |
| + bl := &blob{Kind: "ltx", Inc: e.DB.Inc, Gen: e.DB.Gen, Writes: append([]int(nil), e.DB.Writes...), SealKey: e.DB.Key} |
| + w.pending = append(w.pending, &request{kind: rPut, region: e.Region, key: dataKey(e.DB.Loc, e.DB.Gen, "ltx"), b: bl, |
| + doneAt: w.now + 40*horizonH, beyond: true, by: fmt.Sprintf("box:%d", e.ID)}) |
| + } |
| + } |
| if w.cas(c, func(n *claim) bool { |
| n.Op = opState{Kind: "deleting", ID: id, Exec: -1, ReqAt: w.now} |
| return true |
| @@ -438,6 +471,12 @@ func (w *world) free(c *claim) { |
| w.violate("INV-10: the host was freed with residue %v", r) |
| } |
| w.stats["freed"]++ |
| + if w.fail["recreate"] && w.rng.Intn(2) == 0 && !w.calm { |
| + // the biased schedule: recreate the host at once, where it last |
| + // served, while the old incarnation's requests are in flight |
| + w.nextInc++ |
| + w.console = append(w.console, &consolePlan{Kind: "create", Host: "h", App: app, OpID: w.newID("cr"), Inc: w.nextInc, Region: w.lastRegion}) |
| + } |
| if w.purgeRes[app] && !on("purge-journal") { |
| w.purgeRes[app] = false // freeing the host drops the reservation |
| } |
| @@ -596,8 +635,15 @@ func (w *world) doorAuthorize() { |
| if b == nil { |
| return |
| } |
| - w.doorReads = append(w.doorReads, &doorPlan{Region: b.Region, Loc: c.Holder.Location, Gen: c.Holder.Gen, Inc: c.Holder.Inc, OpID: c.Op.ID, |
| - Key: dataKey(c.Holder.Location, c.Holder.Gen, "ltx"), Until: w.now + 1 + w.pauseLen()}) |
| + d := &doorPlan{Region: b.Region, Loc: c.Holder.Location, Gen: c.Holder.Gen, Inc: c.Holder.Inc, OpID: c.Op.ID, |
| + Key: dataKey(c.Holder.Location, c.Holder.Gen, "ltx"), Until: w.now + 1 + w.pauseLen()} |
| + if w.fail["recreate"] && w.rng.Intn(2) == 0 { |
| + d.Adv = true |
| + if w.rng.Intn(2) == 0 { |
| + d.Until = w.now + 40*horizonH // stalls before selecting |
| + } |
| + } |
| + w.doorReads = append(w.doorReads, d) |
| } |
| // doorOpen advances one stalled listing or file request. A stalled step |
| @@ -610,7 +656,9 @@ func (w *world) doorOpen() { |
| i := w.rng.Intn(len(w.doorReads)) |
| worst := -1 |
| for j, d := range w.doorReads { |
| - if c := w.claim; c == nil || c.Holder == nil || c.Holder.Inc != d.Inc { |
| + // its worst moment: the object its key names now belongs to |
| + // another incarnation |
| + if cur := w.buckets[d.Region].current(d.Key); cur != nil && !cur.Marker && cur.B.Inc != 0 && cur.B.Inc != d.Inc { |
| worst = j |
| break |
| } |
| @@ -639,6 +687,9 @@ func (w *world) doorOpen() { |
| return |
| } |
| d.Signed, d.Until = true, w.now+1+w.pauseLen() |
| + if d.Adv { |
| + d.Until = w.now + 40*horizonH // stalls between signing and the open |
| + } |
| return |
| } |
| w.doorReads = append(w.doorReads[:i:i], w.doorReads[i+1:]...) |
| @@ -677,24 +728,10 @@ func (w *world) recoveryPass() { |
| // 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 && (c.Holder == nil || c.Holder.Inc != w.rec.Inc) && c.Op.Kind != "creating" && on("cancelled-creates") { |
| - orphan := false |
| - for _, x := range c.Cancelled { |
| - if x.Inc == w.rec.Inc && w.now <= x.Until { |
| - orphan = true |
| - } |
| - } |
| - // CC17: a record PUT has no completion bound either (C3a's |
| - // lesson), so `until` cannot close the window. A record whose |
| - // incarnation is retired is an orphan whenever it lands. |
| - if on("orphan-no-deadline") && contains(c.Retired, w.rec.Inc) { |
| - orphan = true |
| - } |
| - if orphan { |
| - w.logf("recovery: removing a cancelled create's late record inc %d", w.rec.Inc) |
| - w.rec = nil |
| - return |
| - } |
| + 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 |
| + return |
| } |
| switch c.Op.Kind { |
| case "creating": |
| @@ -757,6 +794,31 @@ 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 |
| + } |
| + if c.Holder != nil && c.Holder.Inc == r.Inc { |
| + return false |
| + } |
| + if c.Op.Kind == "creating" && c.Op.NewInc == r.Inc { |
| + return false |
| + } |
| + if !on("orphan-no-deadline") { |
| + for _, x := range c.Cancelled { |
| + if x.Inc == r.Inc && w.now <= x.Until { |
| + return true |
| + } |
| + } |
| + return false |
| + } |
| + return true |
| +} |
| + |
| // ---------- the operator (calm phase only) ---------- |
| func (w *world) operator() { |
diff --git a/internal/sim/hostlife/expected-outcomes.txt b/internal/sim/hostlife/expected-outcomes.txt| index 0b01f17df..cfed5cf08 100644 |
| --- a/internal/sim/hostlife/expected-outcomes.txt |
| +++ b/internal/sim/hostlife/expected-outcomes.txt |
| @@ -15,6 +15,5 @@ start-check-claim-gen missed one of three admission fences; caught with exec-adm |
| start-check missed caught with exec-admission and hold-op-open |
| strict-spawn missed caught with evidence-whole-tree |
| touched-incomplete missed caught with legacy-discovery |
| -location-per-incarnation missed unexercised: guards completions later than the model's delete-to-recreate window |
| -door-by-version missed unexercised: subsumed by C3a, and not caught with it dropped either |
| -door-reread missed unexercised: subsumed by C3a, and not caught with it dropped either |
| +door-reread missed subsumed by C3a: caught with location-per-incarnation |
| +door-by-version missed subsumed by C3a: caught with door-reread and location-per-incarnation |
diff --git a/internal/sim/hostlife/moves_test.go b/internal/sim/hostlife/moves_test.go| index 48e305ea5..c127debfa 100644 |
| --- a/internal/sim/hostlife/moves_test.go |
| +++ b/internal/sim/hostlife/moves_test.go |
| @@ -462,6 +462,7 @@ type stalledSign struct { |
| until int |
| checked bool // passed its SafeUntil check and signed, not yet sent |
| checkedAt int |
| + retry bool // a retry of a send that failed transiently |
| } |
| // runStalled lets paused goroutines resume: deferred registry writes and |
| @@ -483,10 +484,18 @@ func (w *world) runStalled() { |
| // timestamp is the check's, and S3 refuses it once older than |
| // the signature-age limit (model 18); signed at send time, it |
| // is accepted however late |
| - if on("sign-at-check") && w.now > s.checkedAt+sigAge { |
| + resigned := s.retry && !on("sdk-no-resign") // the SDK's retry refreshed the signature |
| + if on("sign-at-check") && !resigned && w.now > s.checkedAt+sigAge { |
| w.stats["stale signature refused"]++ |
| continue |
| } |
| + if !s.retry && w.rng.Intn(3) == 0 { |
| + // a transient error: the SDK retries the same request later, |
| + // after a pause a frozen box can stretch (CC19) |
| + s.retry, s.signAt = true, w.now+1+w.pauseLen() |
| + keep = append(keep, s) |
| + continue |
| + } |
| w.issue(b.ID, s.req) |
| continue |
| } |
| @@ -1189,57 +1198,82 @@ func sameStep(a, b *claim) bool { |
| x.Opened == y.Opened && len(a.Obl) == len(b.Obl) && (a.Holder == nil) == (b.Holder == nil) |
| } |
| -// sweep is the straggler sweep (moves rev 6 §6.4, CC15): a request accepted |
| -// before S3's signature limit can complete after it (claim C3a), so a |
| -// retirement's horizon listing can miss it. While the host is at rest (the |
| -// claim free, or serving with no operation and no obligation), each region's |
| -// box lists the host namespace in its own bucket and parks, as a retirement |
| -// event of its own, everything outside the live set: the claim's location |
| -// and current generation in the executor's region, and the parkers' locks. |
| -// It re-reads the claim on every visit and abandons the event the moment |
| -// the host is no longer at rest; every delete names a snapshot version, so |
| -// nothing written later is touched. |
| +// sweep is claim rev 5's at-rest sweep (§6.2a, CC15): for a host with no |
| +// operation running, each region's box lists the locations of the host's |
| +// retired incarnations and every generation within holder.location other |
| +// than holder.generation, and parks whatever it finds as a further |
| +// retirement event, under a park-sweep obligation it owns. The claim's |
| +// wording leaves out `moves/<host>/`; `sweep-staging` (CC20) adds it. |
| func (w *world) sweep(b *box, c *claim) { |
| - if !on("straggler-sweep") { |
| - return |
| - } |
| - rest := c == nil || c.Holder == nil && c.Op.Kind == "" && len(c.Obl) == 0 || |
| - c.Holder != nil && c.Op.Kind == "serving" && len(c.Obl) == 0 |
| - if !rest { |
| - b.sweepID = "" |
| + if !on("straggler-sweep") || c == nil || !(c.Op.Kind == "" || c.Op.Kind == "serving") { |
| return |
| } |
| - live := map[string]bool{} |
| - if c != nil && c.Holder != nil && c.Op.Exec == b.ID { |
| - loc, gen := c.Holder.Location, c.Holder.Gen |
| - live[dataKey(loc, gen, "base")], live[dataKey(loc, gen, "ltx")], live[genMarkerKey(loc)] = true, true, true |
| + for _, o := range c.Obl { |
| + if o.Kind == "park-sweep" && o.Region == b.Region { |
| + return // its own sweep is still running |
| + } |
| } |
| - keep := func(k string) bool { return live[k] } |
| bk := w.buckets[b.Region] |
| - any := false |
| + var prefixes []string |
| for _, p := range []string{"instances/" + host + "/", "moves/" + host + "/"} { |
| for _, k := range bk.keys(p) { |
| - if !strings.HasSuffix(k, "lock.json") && !live[k] && hasNonMarker(bk.objs[k]) { |
| - any = true |
| + if hasNonMarker(bk.objs[k]) && w.sweepable(c, b.Region, k) { |
| + prefixes = append(prefixes, p) |
| + break |
| } |
| } |
| } |
| - if !any && b.sweepID == "" { |
| + if len(prefixes) == 0 { |
| return |
| } |
| - if b.sweepID == "" { |
| - b.sweepID = w.newID("sw") |
| + w.cas(c, func(n *claim) bool { |
| + if !(n.Op.Kind == "" || n.Op.Kind == "serving") { |
| + return false |
| + } |
| + for _, p := range prefixes { |
| + n.Obl = append(n.Obl, obligation{ID: w.newID("ob"), Op: "sweep", Kind: "park-sweep", Region: b.Region, Box: -1, Prefix: p, Ret: "sweep"}) |
| + } |
| + return true |
| + }) |
| +} |
| + |
| +// sweepable: is k, in region r, one of the things the at-rest sweep parks? |
| +func (w *world) sweepable(c *claim, r int, k string) bool { |
| + if strings.HasSuffix(k, "lock.json") { |
| + return false |
| + } |
| + if strings.HasPrefix(k, "moves/") { |
| + return on("sweep-staging") // CC20 |
| } |
| - dest := fmt.Sprintf("parked/sweep/%s/%s/", host, b.sweepID) |
| - done := true |
| - for _, p := range []string{"instances/" + host + "/", "moves/" + host + "/"} { |
| - if !w.parkStep(b, p, dest+strings.TrimSuffix(strings.TrimPrefix(p, ""), "/")+"/", 0, keep) { |
| - done = false |
| + 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) |
| + } |
| + return isDataKey(k) |
| } |
| - if done { |
| - w.logf("box %d swept stragglers (%s)", b.ID, b.sweepID) |
| - w.stats["swept"]++ |
| - b.sweepID = "" |
| + for _, inc := range c.Retired { |
| + if strings.HasPrefix(k, locationFor(inc, false)) { |
| + return true |
| + } |
| } |
| + // a retired legacy incarnation's location is the bare namespace |
| + return w.legacyRetired(c) |
| +} |
| + |
| +// legacyRetired: the host once held a legacy incarnation, now retired, so |
| +// the bare namespace outside holder.location is a retired location. |
| +func (w *world) legacyRetired(c *claim) bool { |
| + for _, inc := range c.Retired { |
| + if w.legacyIncs[inc] { |
| + return true |
| + } |
| + } |
| + return false |
| } |
diff --git a/internal/sim/hostlife/protocol_test.go b/internal/sim/hostlife/protocol_test.go| index 620a24b5c..3ce546929 100644 |
| --- a/internal/sim/hostlife/protocol_test.go |
| +++ b/internal/sim/hostlife/protocol_test.go |
| @@ -583,7 +583,12 @@ func (w *world) doObligation(b *box, c *claim, o obligation) { |
| quiet = b.evidAt[o.ID] + horizonH |
| } |
| } |
| - if !w.parkStep(b, o.Prefix, o.Dest(), quiet, nil) { |
| + var keep func(string) bool |
| + if o.Kind == "park-sweep" { |
| + keep = func(k string) bool { return !w.sweepable(w.claim, b.Region, k) } |
| + quiet = 0 |
| + } |
| + if !w.parkStep(b, o.Prefix, o.Dest(), quiet, keep) { |
| return |
| } |
| } |
| @@ -610,6 +615,9 @@ func (w *world) doObligation(b *box, c *claim, o obligation) { |
| } |
| func (o obligation) Dest() string { |
| + if o.Kind == "park-sweep" { |
| + return fmt.Sprintf("parked/sweep/%s/%s/", host, o.ID) |
| + } |
| if o.Kind == "park-replica" { |
| return fmt.Sprintf("parked/%s/%s/%s/", o.Ret, host, o.ID) |
| } |
diff --git a/internal/sim/hostlife/rules_test.go b/internal/sim/hostlife/rules_test.go| index 07baf07d6..2cd9dbd42 100644 |
| --- a/internal/sim/hostlife/rules_test.go |
| +++ b/internal/sim/hostlife/rules_test.go |
| @@ -29,6 +29,7 @@ var allRules = []string{ |
| "revalidate-before-effect", // C3: a worker re-reads under its lease before acting |
| "sign-before-safeuntil", // C3/§3.1: a paused round signs only before its lease's SafeUntil |
| "sign-at-check", // model 18: signed at the check, so S3's age limit bounds any later pause |
| + "sdk-no-resign", // claim rev 5 C3 (CC19): the SDK\'s retry resends the original signature |
| "location-per-incarnation", // claim rev 4 C3a (J2-R2-1): no location shared between incarnations |
| "fresh-admission", // C4: admission reads the claim fresh |
| "exec-admission", // C4/K1: op.exec names this box (and the role column, which is op.exec here) |
| @@ -47,6 +48,7 @@ var allRules = []string{ |
| "purge-journal", // this model's finding: the reservation is the purge's journal |
| "admission-registration", // claim rev 4 §5.1 step 0, §5.3 step 1b (J2-R2-2) |
| "registration-recovery", // CC16: a registration is a lease, so a dead create cannot block purge |
| + "registration-check", // CC21: a create checks its registration immediately before its claim CAS |
| "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` |
| "door-by-version", // §6.5/J-N10 |
| @@ -62,7 +64,8 @@ var allRules = []string{ |
| "stale-hold-release", // this model's finding: release a hold whose op ended |
| "restore-by-generation", // C3a + moves rev 6 §5.1: restore replays the claim's generation only |
| "quiet-before-ack", // this model's finding (late writes after a park) |
| - "straggler-sweep", // CC15 + moves rev 6 §6.4: stragglers past H are parked at rest |
| + "straggler-sweep", // claim rev 5 §6.2a (CC15): the at-rest sweep |
| + "sweep-staging", // CC20: the sweep also covers moves/<host>/ |
| // 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 0d46d5ef3..2df214dd8 100644 |
| --- a/internal/sim/hostlife/sim_test.go |
| +++ b/internal/sim/hostlife/sim_test.go |
| @@ -17,12 +17,12 @@ const ( |
| func newWorld(seed int64, verbose bool) *world { |
| w := &world{seed: seed, rng: rand.New(rand.NewSource(seed)), verbose: verbose, |
| stores: map[string]bool{app0: true, app1: true}, cfgVer: map[string]int{app0: 1, app1: 1}, purgeRes: map[string]bool{}, purgeStep: map[string]int{}, |
| - control: newBucket(), delivered: map[int]bool{}, durable: map[string]map[int]bool{}, writeInc: map[int]int{}, genParent: map[string]string{}, execLease: map[int]execLease{}, fail: map[string]bool{}, stats: map[string]int{}} |
| + control: newBucket(), delivered: map[int]bool{}, durable: map[string]map[int]bool{}, writeInc: map[int]int{}, legacyIncs: map[int]bool{}, genParent: map[string]string{}, execLease: map[int]execLease{}, fail: map[string]bool{}, stats: map[string]int{}} |
| for r := 0; r < nRegions; r++ { |
| w.buckets[r] = newBucket() |
| } |
| w.admit = map[string]*admission{app0: {Reg: map[string]regEntry{}}, app1: {Reg: map[string]regEntry{}}} |
| - for _, f := range []string{"partition", "freeze", "pause", "destroy", "disk"} { |
| + for _, f := range []string{"partition", "freeze", "pause", "destroy", "disk", "recreate"} { |
| w.fail[f] = w.rng.Intn(2) == 0 |
| } |
| for r := 0; r < nRegions; r++ { |
| @@ -54,6 +54,7 @@ func (w *world) legacyStart() { |
| w.nextInc++ |
| inc := w.nextInc |
| w.rec = &record{Inc: inc, App: app0, Region: r} |
| + w.legacyIncs[inc] = true |
| key := 7 |
| var writes []int |
| for i := 0; i < 3; i++ { |
diff --git a/internal/sim/hostlife/world_test.go b/internal/sim/hostlife/world_test.go| index 082999935..ff8db6b52 100644 |
| --- a/internal/sim/hostlife/world_test.go |
| +++ b/internal/sim/hostlife/world_test.go |
| @@ -1,7 +1,7 @@ |
| // Package hostlife is a deterministic, randomized model of the host |
| // lifecycle claim (docs/superpowers/specs/2026-10-02-host-lifecycle-claim-design.md, |
| -// rev 4, a3c86fa5) and Phase 1 of move-any-app |
| -// (docs/superpowers/specs/2026-10-02-move-any-app-design.md, rev 6). |
| +// rev 5, 4a458a9c) and Phase 1 of move-any-app |
| +// (docs/superpowers/specs/2026-10-02-move-any-app-design.md, rev 7). |
| // |
| // Since joint round 2 the model encodes what the specs say and nothing |
| // stronger: restore reads the holder's location and the generation the |
| @@ -296,7 +296,6 @@ type box struct { |
| stopped map[string]bool |
| mem map[string]bool |
| evidAt map[string]int |
| - sweepID string |
| pendingTimers []int |
| } |
| @@ -319,7 +318,6 @@ func (b *box) forget() { |
| b.snap, b.stopped, b.stale = nil, nil, nil |
| b.mem = map[string]bool{} |
| b.evidAt = map[string]int{} |
| - b.sweepID = "" |
| b.pendingTimers = nil |
| } |
| @@ -495,37 +493,39 @@ type world struct { |
| ver int |
| verbose bool |
| - claim *claim // nil = absent |
| - rec *record |
| - stores map[string]bool |
| - cfgVer map[string]int // each app's current config bundle version |
| - purgeRes map[string]bool |
| - purgeStep map[string]int // the reservation's durable phase (purge journal) |
| - admit map[string]*admission |
| - h2 liteHost |
| - recPend *pendingRec // a record PUT whose response was lost |
| - floor bool |
| - buckets [nRegions]*bucket |
| - control *bucket |
| - boxes []*box |
| - pending []*request |
| - acks []ack |
| - writeInc map[int]int // which incarnation acknowledged each write |
| - durable map[string]map[int]bool // per generation prefix: writes a completed replica object holds |
| - genParent map[string]string // generation prefix -> the one it superseded |
| - nextW int |
| - nextInc int |
| - serial int |
| - nextID int |
| - delivered map[int]bool |
| - doorReads []*doorPlan |
| - execLease map[int]execLease |
| - staging [nRegions]stagingLease |
| - console []*consolePlan |
| - fail map[string]bool // which faults this seed exercises |
| - stats map[string]int |
| - stalled []*stalledSign |
| - ccache *claim // the console's short-lived claim cache |
| + claim *claim // nil = absent |
| + rec *record |
| + stores map[string]bool |
| + cfgVer map[string]int // each app's current config bundle version |
| + purgeRes map[string]bool |
| + purgeStep map[string]int // the reservation's durable phase (purge journal) |
| + admit map[string]*admission |
| + h2 liteHost |
| + recPend *pendingRec // a record PUT whose response was lost |
| + lastRegion int // where the host served when it was last deleted |
| + legacyIncs map[int]bool // incarnations that were adopted legacy hosts |
| + floor bool |
| + buckets [nRegions]*bucket |
| + control *bucket |
| + boxes []*box |
| + pending []*request |
| + acks []ack |
| + writeInc map[int]int // which incarnation acknowledged each write |
| + durable map[string]map[int]bool // per generation prefix: writes a completed replica object holds |
| + genParent map[string]string // generation prefix -> the one it superseded |
| + nextW int |
| + nextInc int |
| + serial int |
| + nextID int |
| + delivered map[int]bool |
| + doorReads []*doorPlan |
| + execLease map[int]execLease |
| + staging [nRegions]stagingLease |
| + console []*consolePlan |
| + fail map[string]bool // which faults this seed exercises |
| + stats map[string]int |
| + stalled []*stalledSign |
| + ccache *claim // the console's short-lived claim cache |
| violations []string |
| opsDone int |
| @@ -680,6 +680,11 @@ func (w *world) issue(actorBox int, r *request) int { |
| // bounds acceptance, not completion (claim C3a, J2-R2-1) |
| r.doneAt = w.now + horizonH + 1 + w.rng.Intn(10*horizonH) |
| r.beyond = true |
| + if w.fail["recreate"] && w.rng.Intn(2) == 0 { |
| + // the biased schedule: no bound at all, so it can outlive a |
| + // delete and a recreate; it lands at its worst moment |
| + r.doneAt = w.now + 40*horizonH |
| + } |
| } |
| } |
| r.by = fmt.Sprintf("box:%d", actorBox) |
| @@ -757,10 +762,30 @@ func (w *world) newGen(loc, old, gen string) { |
| } |
| } |
| +// worstMoment: the biased schedule completes a pending write of an earlier |
| +// incarnation's replica data the moment another incarnation holds the host |
| +// with an executor in that region, inside its own window or past H, which |
| +// is the interleaving C3a exists for (a recreate while the previous |
| +// incarnation's requests are still in flight). |
| +func (w *world) worstMoment(r *request) bool { |
| + if !w.fail["recreate"] || r.kind != rPut || r.b == nil || r.b.Inc == 0 || !isDataKey(r.key) { |
| + return false |
| + } |
| + c := w.claim |
| + if c == nil || c.Holder == nil || c.Holder.Inc == r.b.Inc { |
| + return false |
| + } |
| + if c.Op.Kind == "creating" && c.Op.NewRegion == r.region { |
| + return w.rng.Intn(2) == 0 |
| + } |
| + e := w.execBox(c) |
| + return e != nil && e.Region == r.region && w.rng.Intn(2) == 0 |
| +} |
| + |
| func (w *world) completeDue(force bool) { |
| var keep []*request |
| for _, r := range w.pending { |
| - if force || r.doneAt <= w.now { |
| + if force || r.doneAt <= w.now || w.worstMoment(r) { |
| w.complete(r) |
| if r.beyond { |
| w.stats["completed beyond H"]++ |