amadan
sim: Astra's round 1 on the two-box model: stuck refuses admission, region HA checks a sole box, durable acknowledgements gate every transition, deadlines from the fence record, the exact phase matrix, a discriminating test per guard, files objects with origins and region binding, moves' parks keep the files live set, committed-landing and record-race fences, the controller record that blocks updates, the forced open boundaries, and the tie-break over the real host
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
12 files changed,
+1175
−67
internal/sim/hostlife/console_test.go+13 −1internal/sim/hostlife/moves_test.go+20 −5internal/sim/hostlife/protocol_test.go+10 −3internal/sim/hostlife/regionha_cases_test.go+0 −40internal/sim/hostlife/regionha_round1_test.go+572 −0internal/sim/hostlife/regionha_test.go+347 −9internal/sim/hostlife/regionha_witness_test.go+145 −0internal/sim/hostlife/rules_test.go+11 −0internal/sim/hostlife/sim_test.go+2 −1internal/sim/hostlife/twobox_test.go+26 −6internal/sim/hostlife/witness_test.go+11 −0internal/sim/hostlife/world_test.go+18 −2
diff --git a/internal/sim/hostlife/console_test.go b/internal/sim/hostlife/console_test.go| index 88980b190..1e7f99d23 100644 |
| --- a/internal/sim/hostlife/console_test.go |
| +++ b/internal/sim/hostlife/console_test.go |
| @@ -387,7 +387,7 @@ func (w *world) userMove() { |
| // choose() in region 0, where the model keeps the control-plane-only |
| // host. With one box per region it is box 0, as the model always implied. |
| func (w *world) h2Box(app string) int { |
| - if b := w.chooseBox(0, app); b != nil { |
| + if b := w.chooseBoxFor("h2", 0, app); b != nil { |
| return b.ID |
| } |
| return 0 |
| @@ -1274,6 +1274,9 @@ func (w *world) operator() { |
| default: |
| w.abandonPrepared(n) |
| n.Op.Stuck, n.Op.Replacements, n.Op.Excluded, n.Op.Resolved = "", 0, nil, true |
| + if released && op.Exec >= 0 { |
| + n.Op.Excluded = []int{op.Exec} // the target that just failed its probe is not the operator's fresh choice (rev 4) |
| + } |
| n.Op.Phase, n.Op.Exec, n.Op.Tgt = "pinning", -1, -1 |
| n.Op.Pin, n.Op.Prepared, n.Op.Receipt = nil, "", nil |
| n.Op.BaseKey, n.Op.BaseVer, n.Op.BaseTX = "", 0, 0 |
| @@ -1326,6 +1329,15 @@ func (w *world) operator() { |
| return |
| } |
| } |
| + w.declareTargetLost(c) |
| +} |
| + |
| +// declareTargetLost is the declared loss of a landing's or a rollback's |
| +// target that is gone (claim D2, moves §7.10): the operator's path, and, |
| +// for a terminated target, the regional worker's automatic fence (claim |
| +// D2 "Automatic termination", rev 4). It proceeds record first, so a loss |
| +// racing the record's commit CAS follows whichever the record holds. |
| +func (w *world) declareTargetLost(c *claim) { |
| if c.Holder == nil { |
| return |
| } |
diff --git a/internal/sim/hostlife/moves_test.go b/internal/sim/hostlife/moves_test.go| index a12678ab1..6150cf544 100644 |
| --- a/internal/sim/hostlife/moves_test.go |
| +++ b/internal/sim/hostlife/moves_test.go |
| @@ -152,6 +152,7 @@ func (w *world) resumeStale(b *box, old *claim) { |
| // acting on the claim c it read. |
| func (w *world) role(b *box, c *claim) { |
| w.initRecord(b, c) |
| + w.finishParticipation(b, c) // a relocation controller whose participation ended (rev 4) |
| // exec lease (claim §7.1) |
| if w.isParticipant(c, b) && !contains(c.Lost, b.ID) { |
| if b.ExecUntil > 0 && w.localNow(b) > b.ExecUntil { |
| @@ -161,6 +162,14 @@ func (w *world) role(b *box, c *claim) { |
| b.ExecUntil = w.localNow(b) + execTTL |
| w.execLease[b.ID] = execLease{Op: c.Op.ID, Expires: w.now + execTTL} |
| } |
| + if c.Op.Kind == "relocating" { |
| + w.recordAck(b, c) // exec_ack.<box>, durable (rev 4) |
| + if cur := w.claim; cur != nil && cur.Ver != c.Ver { |
| + nc := cur.clone() |
| + nc.readStamp = c.readStamp |
| + c = nc |
| + } |
| + } |
| } else if c == nil || !w.isParticipant(c, b) { |
| b.ExecUntil = 0 |
| } |
| @@ -1022,7 +1031,7 @@ func (w *world) landTarget(b *box, c *claim) { |
| w.violate("INV-9: the cut of %s waits on quiet_after[%d] until %d", op.ID, b.Region, c.Quiet[b.Region]) |
| } |
| // an earlier stay of this incarnation, in its location here |
| - if w.parkStep(b, loc, fmt.Sprintf("superseded/%s/%s/install/", op.ID, host), c.Quiet[b.Region], w.opScope(c, loc), confine(loc)) { |
| + if w.parkStep(b, loc, fmt.Sprintf("superseded/%s/%s/install/", op.ID, host), c.Quiet[b.Region], w.opScope(c, loc), w.keepFilesLive(confine(loc))) { |
| w.cas(c, func(n *claim) bool { n.Op.LandPhase = "install-copy"; return sameOp(n.Op.ID, op.ID) }) |
| } |
| case "install-copy": |
| @@ -1217,6 +1226,9 @@ func (w *world) landTarget(b *box, c *claim) { |
| // written last (R2-6). seal names the files archive version. |
| func (w *world) installLocal(b *box, c *claim, gen string, seal ref, _ string, next func(n *claim)) { |
| if b.Files != nil && b.Files.Gen == gen && b.Files.Done && b.Files.Inc == c.Holder.Inc { |
| + if w.perRegion > 1 && !w.preparedManifestHere(b, c, gen) { |
| + return // moves §7.6 (L17, R18-1) in the two-box shape: the generation's prepared manifest first |
| + } |
| // the marker vouches for everything before it |
| w.cas(c, func(n *claim) bool { next(n); return true }) |
| return |
| @@ -1281,6 +1293,9 @@ func (w *world) installLocal(b *box, c *claim, gen string, seal ref, _ string, n |
| b.Row.Repl, b.Row.Next = c.Op.Repl, c.Op.Next |
| } |
| b.Files.Done = true |
| + if w.perRegion > 1 && !w.preparedManifestHere(b, c, gen) { |
| + return // the first branch finishes once the prepared manifest is acknowledged |
| + } |
| w.cas(c, func(n *claim) bool { next(n); return true }) |
| } |
| @@ -1503,7 +1518,7 @@ func (w *world) recoverSource(b *box, c *claim) { |
| if !w.evidence(b, op.RollbackID) { |
| return |
| } |
| - if w.parkStep(b, c.Holder.Location, fmt.Sprintf("superseded/%s/%s/return/", op.ID, host), op.StopAt+horizonH, w.opScope(c, c.Holder.Location), confine(c.Holder.Location)) { |
| + if w.parkStep(b, c.Holder.Location, fmt.Sprintf("superseded/%s/%s/return/", op.ID, host), op.StopAt+horizonH, w.opScope(c, c.Holder.Location), w.keepFilesLive(confine(c.Holder.Location))) { |
| w.cas(c, func(n *claim) bool { n.Op.SrcPhase = "install-copy"; return sameOp(n.Op.ID, op.ID) }) |
| } |
| case "install-copy": |
| @@ -1635,7 +1650,7 @@ func (w *world) pushStep(b *box, c *claim) { |
| return true |
| }) |
| case "park": |
| - if w.parkStep(b, loc, fmt.Sprintf("superseded/%s/%s/push/", op.ID, host), op.StopAt+horizonH, w.opScope(c, loc), confine(loc)) { |
| + if w.parkStep(b, loc, fmt.Sprintf("superseded/%s/%s/push/", op.ID, host), op.StopAt+horizonH, w.opScope(c, loc), w.keepFilesLive(confine(loc))) { |
| w.cas(c, func(n *claim) bool { n.Op.Phase = "install"; return sameOp(n.Op.ID, op.ID) }) |
| } |
| case "install": |
| @@ -1947,8 +1962,8 @@ func (w *world) deadGeneration(c *claim, r int, k string) bool { |
| } |
| return true // a dead generation's certificates |
| } |
| - if isManifestKey(k) { |
| - // a files manifest outside the files live set (region HA §5.6, L13): |
| + if isFilesKey(k) { |
| + // a files manifest or object outside the files live set (region HA §5.6, L13): |
| // its generation's, as the data keys are |
| if genOf(h.Location, k) == h.Gen { |
| return !authoritative |
diff --git a/internal/sim/hostlife/protocol_test.go b/internal/sim/hostlife/protocol_test.go| index 3ad1cc317..219c9e2c5 100644 |
| --- a/internal/sim/hostlife/protocol_test.go |
| +++ b/internal/sim/hostlife/protocol_test.go |
| @@ -592,7 +592,7 @@ func (w *world) appStart(b *box, c *claim, want string, probe bool, mode string) |
| return false // not an app failure: the agent waits for its config pass |
| } |
| // FailApp is the injected "the target cannot run it" fault: landing probes only |
| - healthy := !(probe && b.FailApp && (c.Op.Kind == "landing" || c.Op.Kind == "relocating")) // and relocation probes (region HA, Task 5) |
| + healthy := !(probe && b.FailApp && (c.Op.Kind == "landing" || c.Op.Kind == "relocating" && b.ID != c.Op.Src)) // and relocation probes (region HA, Task 5) |
| // §7.7: the probe checks the launch environment at spawn. The forward |
| // path requires the inputs pinned at admission. A recovery probe (the |
| // source's revert or rollback) runs on the inputs it rendered now and |
| @@ -1146,7 +1146,7 @@ func (w *world) coverParkedPredecessors(n *claim, region int, gens []string) { |
| // that never had anything (INV-17). |
| func (w *world) hadFilesIn(r int, loc, gen string) bool { |
| for _, k := range w.buckets[r].keys(dataKey(loc, gen, "")) { |
| - if genOf(loc, k) == gen && !isManifestKey(k) { // a files manifest is no database object (region HA §5.6) |
| + if genOf(loc, k) == gen && !isFilesKey(k) { // a files manifest is no database object (region HA §5.6) |
| return true |
| } |
| } |
| @@ -1158,7 +1158,7 @@ func (w *world) hadFilesIn(r int, loc, gen string) bool { |
| func (w *world) hasFilesIn(r int, loc, gen string) bool { |
| bk := w.buckets[r] |
| for _, k := range bk.keys(dataKey(loc, gen, "")) { |
| - if genOf(loc, k) == gen && bk.current(k) != nil && !isManifestKey(k) { // a files manifest is no database object (region HA §5.6) |
| + if genOf(loc, k) == gen && bk.current(k) != nil && !isFilesKey(k) { // a files manifest is no database object (region HA §5.6) |
| return true |
| } |
| } |
| @@ -1432,6 +1432,9 @@ func (w *world) admits(b *box, c *claim, probe string) bool { |
| case "pushing": |
| return probe == op.ID && op.Phase == "probing" |
| case "relocating": |
| + if op.Stuck != "" && on("reloc-stuck-refuses-admission") { |
| + return false // relocationAdmission: a stuck operation admits nobody, the source's wake included (ruling 9, R1-16; rev 4, Astra R1-2) |
| + } |
| if probe != "" { |
| return probe == op.ID && role(op.Tgt) && op.Phase == "probing" |
| } |
| @@ -1607,6 +1610,10 @@ func (w *world) admitWriter(b *box, c *claim, want string, probe bool) (admitInp |
| w.stats["admission refused: op kind"]++ |
| return a, false |
| } |
| + if c.Op.Kind == "relocating" && c.Op.Stuck != "" && on("reloc-stuck-refuses-admission") { |
| + w.stats["admission refused: relocation stuck"]++ |
| + return a, false |
| + } |
| a.KeepStamp = h.Stamp > h.Session |
| if !on("admit-everywhere") && c.Op.Kind != "serving" { |
| a.Mode, a.NewGeneration = "unguarded", want // the mutation: writer sessions for ordinary wakes only (rev 7.8) |
diff --git a/internal/sim/hostlife/regionha_cases_test.go b/internal/sim/hostlife/regionha_cases_test.go| index 6086dcba6..36efb1e61 100644 |
| --- a/internal/sim/hostlife/regionha_cases_test.go |
| +++ b/internal/sim/hostlife/regionha_cases_test.go |
| @@ -128,46 +128,6 @@ func TestL18TerminationDuringServing(t *testing.T) { |
| }) |
| } |
| -func TestL18TerminationInEveryRelocationPhase(t *testing.T) { |
| - phases := []string{"starting", "releasing", "pinning", "installing", "installed", "probing", "probed", "opened"} |
| - for _, boxes := range []int{1, 2} { |
| - for _, who := range []string{"source", "target"} { |
| - for _, phase := range phases { |
| - if boxes == 1 && (who == "source" || phase == "starting" || phase == "releasing") { |
| - continue // a one-box region relocates only by failover, which starts at pinning with the source fenced |
| - } |
| - name := map[int]string{1: "one-box region", 2: "two-box region"}[boxes] + "/" + who + "@" + phase |
| - t.Run(name, func(t *testing.T) { |
| - w := regionWorld(boxes) |
| - from := w.serveAndPublish(t) |
| - w.appWrite(from) |
| - w.timerOn(from) |
| - w.extraBox(0, spareID()) // a spare for the replacement table |
| - if boxes == 2 { |
| - w.drainTo(t, nil) |
| - } else { |
| - w.terminate(from) |
| - if w.relocTarget(t) == nil { |
| - t.Fatalf("%s", w.violations[0]) |
| - } |
| - } |
| - if !w.relocPhase(t, phase, w.actAll(), w.recoveryPass) { |
| - t.Fatalf("%s", w.violations[0]) |
| - } |
| - if who == "source" { |
| - w.terminate(from) |
| - } else if x := w.boxByID(w.claim.Op.Tgt); x != nil && w.claim.Op.Kind == "relocating" { |
| - w.terminate(x) |
| - } |
| - w.servingOn(t, nil) |
| - w.finish(t) |
| - w.mustHold(t) |
| - }) |
| - } |
| - } |
| - } |
| -} |
| - |
| func TestL18NestedFailover(t *testing.T) { |
| bothShapes(t, func(t *testing.T, w *world, boxes int) { |
| from := w.serveAndPublish(t) |
diff --git a/internal/sim/hostlife/regionha_round1_test.go b/internal/sim/hostlife/regionha_round1_test.go| new file mode 100644 |
| index 000000000..ad0f45d10 |
| --- /dev/null |
| +++ b/internal/sim/hostlife/regionha_round1_test.go |
| @@ -0,0 +1,572 @@ |
| +package hostlife |
| + |
| +import ( |
| + "crypto/sha256" |
| + "fmt" |
| + "testing" |
| +) |
| + |
| +// Astra's round 1 on the two-box plan (rev 4): a direct test for every |
| +// guard the round found unproven, the phase matrix stopped between single |
| +// actor transitions, and claim §11's additional witnesses that rev 3 left |
| +// outside the model. Each test names the rule whose mutation makes it |
| +// fail. |
| + |
| +// stepUntil advances the world one actor at a time and stops the moment |
| +// done holds: the tick's own work (completions, stalls, the two-box |
| +// step), then each live box's worker, obligation runner, reconcile and |
| +// passes, the executor's wake, then the recovery pass, with done checked |
| +// after every single one. A fault injected after it returns lands |
| +// exactly between two transitions. |
| +func (w *world) stepUntil(t *testing.T, max int, what string, done func() bool) bool { |
| + t.Helper() |
| + if done() { |
| + return true |
| + } |
| + for i := 0; i < max; i++ { |
| + w.now++ |
| + w.completeDue(false) |
| + if p := w.recPend; p != nil && p.at <= w.now { |
| + w.recPend = nil |
| + if w.rec == nil { |
| + w.rec = p.rec |
| + } |
| + } |
| + w.runStalled() |
| + if w.perRegion > 1 { |
| + w.twoBoxStep() |
| + } |
| + if done() { |
| + return true |
| + } |
| + for _, b := range w.liveBoxes() { |
| + for _, act := range []func(){ |
| + func() { w.worker(b) }, func() { w.obligationRunner(b) }, func() { w.reconcile(b) }, |
| + func() { |
| + if len(b.plans) == 0 { |
| + w.passPlan(b, "config") |
| + w.passPlan(b, "adopt") |
| + } |
| + w.passExec(b) |
| + }, |
| + w.wakeExec, |
| + } { |
| + act() |
| + if len(w.violations) > 0 { |
| + return false |
| + } |
| + if done() { |
| + return true |
| + } |
| + } |
| + } |
| + w.recoveryPass() |
| + w.checkStep() |
| + if len(w.violations) > 0 { |
| + return false |
| + } |
| + if done() { |
| + return true |
| + } |
| + } |
| + w.violate("INV-3 (witness): %s not reached within %d steps: %s", what, max, w.state()) |
| + return false |
| +} |
| + |
| +// atPhase: the relocation is exactly in phase p (not beyond it). |
| +func (w *world) atPhase(p string) func() bool { |
| + return func() bool { c := w.claim; return c.Op.Kind == "relocating" && c.Op.Phase == p && c.Op.Stuck == "" } |
| +} |
| + |
| +// liveIn counts region r's live boxes. |
| +func (w *world) liveIn(r int) int { return len(w.regionBoxes(r)) } |
| + |
| +// ---------- finding 6: the termination matrix, exact ---------- |
| + |
| +// TestL18TerminationAtEveryExactPhase (L18 "termination during every |
| +// relocation phase", rev 4): the relocation is stopped exactly in each |
| +// phase of §5.8's table, probe-failed included, between two single |
| +// actor transitions; the phase and the region's live topology are |
| +// asserted immediately before the participant is terminated; no spare |
| +// exists beforehand, and replacements come only from the modelled group |
| +// after the loss. One-box region: the failover's target (the box the |
| +// group launched) is terminated. Two-box region: the drain's source or |
| +// target is. |
| +func TestL18TerminationAtEveryExactPhase(t *testing.T) { |
| + phases := []string{"starting", "releasing", "pinning", "installing", "installed", "probing", "probe-failed", "probed", "opened"} |
| + for _, boxes := range []int{1, 2} { |
| + for _, who := range []string{"source", "target"} { |
| + for _, phase := range phases { |
| + if boxes == 1 && (who == "source" || phase == "starting" || phase == "releasing") { |
| + continue // a one-box region relocates only by failover, which starts at pinning with the source fenced |
| + } |
| + if phase == "probe-failed" && who == "source" { |
| + continue // the source has released before any probe; its loss is the pinning case |
| + } |
| + name := fmt.Sprintf("%s/%s@%s", map[int]string{1: "one-box region", 2: "two-box region"}[boxes], who, phase) |
| + t.Run(name, func(t *testing.T) { |
| + w := regionWorld(boxes) |
| + from := w.serveAndPublish(t) |
| + w.appWrite(from) |
| + w.timerOn(from) |
| + var target func() *box |
| + if boxes == 2 { |
| + w.drainTo(t, nil) |
| + tgt := w.boxByID(w.claim.Op.Tgt) |
| + tgt.FailApp = phase == "probe-failed" |
| + target = func() *box { return w.boxByID(w.claim.Op.Tgt) } |
| + } else { |
| + w.terminate(from) |
| + if !w.stepUntil(t, 400, "a target named", func() bool { c := w.claim; return c.Op.Kind == "relocating" && c.Op.Tgt >= 0 }) { |
| + w.mustHold(t) |
| + } |
| + w.boxByID(w.claim.Op.Tgt).FailApp = phase == "probe-failed" |
| + target = func() *box { return w.boxByID(w.claim.Op.Tgt) } |
| + } |
| + if !w.stepUntil(t, 2000, "relocation exactly at "+phase, w.atPhase(phase)) { |
| + w.mustHold(t) |
| + } |
| + // immediately before the injection: the exact phase, and the |
| + // region's live topology (no spare) |
| + if c := w.claim; c.Op.Phase != phase { |
| + t.Fatalf("not at %s: %s", phase, w.state()) |
| + } |
| + if n := w.liveIn(0); n != boxes { |
| + t.Fatalf("region 0 has %d live boxes before the injection, want %d", n, boxes) |
| + } |
| + victim := from |
| + if who == "target" { |
| + victim = target() |
| + } |
| + if victim == nil || victim.Destroyed { |
| + t.Fatalf("no live %s at %s: %s", who, phase, w.state()) |
| + } |
| + w.terminate(victim) |
| + w.servingOn(t, nil) |
| + w.finish(t) |
| + w.mustHold(t) |
| + if c := w.claim; c.Op.Exec == victim.ID { |
| + t.Fatalf("serving on the terminated %s", who) |
| + } |
| + }) |
| + } |
| + } |
| + } |
| +} |
| + |
| +// ---------- finding 2: stuck refuses admission ---------- |
| + |
| +// TestStuckSourceRefusesAdmission (reloc-stuck-refuses-admission): three |
| +// targets die in starting, so the exhausted fence leaves the live source |
| +// op.exec with its ready row and the operation stuck. A request then |
| +// reaches the source, whose app has stopped: no writer is admitted. |
| +func TestStuckSourceRefusesAdmission(t *testing.T) { |
| + w := twoBoxWitness() |
| + from := w.boxes[0] |
| + w.serve(from, 1, app0) |
| + w.running(t, from) |
| + b30, b31 := w.extraBox(0, 30), w.extraBox(0, 31) |
| + w.userRelocate() |
| + for _, x := range []*box{w.boxByID(w.claim.Op.Tgt), b30, b31, w.boxes[3]} { |
| + if x == nil || x.Destroyed || x.ID != w.claim.Op.Tgt { |
| + continue |
| + } |
| + w.terminate(x) |
| + w.reach(t, 60, "the dead target fenced", func() bool { return contains(w.claim.Lost, x.ID) }, w.act(from)) |
| + } |
| + if c := w.claim; c.Op.Stuck == "" || c.Op.Exec != from.ID || c.Op.Phase != "starting" || from.Row == nil || from.Row.Status != "ready" { |
| + t.Fatalf("not stuck in starting with the live source op.exec and its row ready: %s", w.state()) |
| + } |
| + from.Procs = nil // the app stopped; the next request wakes it |
| + before := w.stats["admissions: cold"] + w.stats["admissions: warm"] |
| + w.drive(30, never, func() { w.wake(from) }) |
| + w.mustHold(t) |
| + if n := w.stats["admissions: cold"] + w.stats["admissions: warm"] - before; n != 0 || hasMain(from) { |
| + t.Fatalf("a stuck operation admitted %d writers on its source (running %v)", n, hasMain(from)) |
| + } |
| +} |
| + |
| +// ---------- finding 3: the sole box is checked in an HA region ---------- |
| + |
| +// TestHASoleBoxIsCheckedLikeAnyOther (ha-sole-box-eligibility): in a |
| +// one-box region with region HA on, the only box is refused when it is |
| +// unenrolled, lacks the secrets key, runs an old executable, is on lost or |
| +// owes a park-local for the host; in the one-box shape (region HA off) |
| +// the region's box is chosen as today. |
| +func TestHASoleBoxIsCheckedLikeAnyOther(t *testing.T) { |
| + for _, why := range []string{"unenrolled", "no key", "old executable", "lost", "owes a park-local"} { |
| + t.Run(why, func(t *testing.T) { |
| + w := regionWorld(1) |
| + b := w.boxes[0] |
| + w.serve(w.boxes[1], 1, app0) // the claim lives in region 1; region 0 is the create's |
| + switch why { |
| + case "unenrolled": |
| + b.Enrolled = false |
| + case "no key": |
| + b.HasKey = false |
| + case "old executable": |
| + b.Old = true |
| + case "lost": |
| + w.claim.Lost = addUniq(w.claim.Lost, b.ID) |
| + case "owes a park-local": |
| + w.claim.Obl = append(w.claim.Obl, obligation{ID: "pl", Op: "old", Kind: "park-local", Box: b.ID, Region: -1, Ret: "old"}) |
| + } |
| + if got := w.chooseBox(0, app0); got != nil { |
| + t.Fatalf("region HA chose its sole box %d although it is %s", got.ID, why) |
| + } |
| + }) |
| + } |
| + t.Run("one-box shape keeps today's pick", func(t *testing.T) { |
| + w := newWitness() |
| + w.boxes[0].Enrolled = false |
| + if got := w.chooseBox(0, app0); got != w.boxes[0] { |
| + t.Fatalf("the one-box shape did not pick the region's box: %v", got) |
| + } |
| + }) |
| +} |
| + |
| +// ---------- finding 4: the acknowledgement barrier at every transition ---------- |
| + |
| +// TestReplacementWithoutAcknowledgementHoldsEachTransition |
| +// (reloc-exec-ack-barrier): the target dies at installing and the spare |
| +// that replaces it has not acknowledged. Driving the installation's steps |
| +// without the spare's acknowledgement, the operation stays at installing |
| +// (ToInstalled's requireAcks); once the spare acknowledges, it proceeds. |
| +func TestReplacementWithoutAcknowledgementHoldsEachTransition(t *testing.T) { |
| + w := twoBoxWitness() |
| + from, to := w.boxes[0], w.boxes[3] |
| + w.serve(from, 1, app0) |
| + w.running(t, from) |
| + w.published(t, from) |
| + w.drainTo(t, to) |
| + spare := w.extraBox(0, 30) |
| + if !w.reach(t, 1500, "installing", w.atPhase("installing"), w.act(from, to), w.recoveryPass) { |
| + w.mustHold(t) |
| + } |
| + w.terminate(to) |
| + w.reach(t, 60, "replaced at installing", func() bool { return w.claim.Op.Exec == spare.ID }, w.act(from)) |
| + if contains(w.claim.Op.Acks, spare.ID) { |
| + t.Fatalf("the spare acknowledged before it ran") |
| + } |
| + // the spare's installation steps, without its acknowledgement |
| + spare.ExecUntil = w.localNow(spare) + execTTL |
| + for i := 0; i < 40; i++ { |
| + w.tick() |
| + w.relocInstalling(spare, w.claim.clone()) |
| + } |
| + w.mustHold(t) |
| + if c := w.claim; c.Op.Phase != "installing" { |
| + t.Fatalf("left installing without the spare's acknowledgement: %s", w.state()) |
| + } |
| + w.servingOn(t, spare) |
| + w.finish(t) |
| + w.mustHold(t) |
| +} |
| + |
| +// ---------- finding 5: deadlines and delays from the fence record ---------- |
| + |
| +// TestPinWaitsForEveryFenceObservation (reloc-pin-delay-every-fence): the |
| +// source's release is journaled, then the target is terminated and |
| +// replaced by a spare before any pin. The pin waits out the target's |
| +// fence observation plus the delay, a release notwithstanding. |
| +func TestPinWaitsForEveryFenceObservation(t *testing.T) { |
| + w := twoBoxWitness() |
| + from, to := w.boxes[0], w.boxes[3] |
| + w.serve(from, 1, app0) |
| + w.running(t, from) |
| + w.published(t, from) |
| + w.drainTo(t, to) |
| + spare := w.extraBox(0, 30) |
| + if !w.stepUntil(t, 1500, "the source's release journaled", func() bool { c := w.claim; return c.Op.Release != nil && c.Op.Pin == nil }) { |
| + w.mustHold(t) |
| + } |
| + w.terminate(to) |
| + ok := w.stepUntil(t, 400, "the pin", func() bool { |
| + c := w.claim |
| + if c.Op.Pin != nil && len(c.Op.Observed) > 0 && w.now < latestObservation(c.Op)+failoverPinDelay { |
| + t.Fatalf("pinned at %d, before the target's observation %d plus %d", w.now, latestObservation(c.Op), failoverPinDelay) |
| + } |
| + return c.Op.Pin != nil |
| + }) |
| + if !ok { |
| + w.mustHold(t) |
| + } |
| + if !contains(w.claim.Lost, to.ID) || w.claim.Op.Tgt != spare.ID { |
| + t.Fatalf("the target was not replaced before the pin: %s", w.state()) |
| + } |
| + w.servingOn(t, spare) |
| + w.finish(t) |
| + w.mustHold(t) |
| +} |
| + |
| +// TestDeadTargetDeadlineFromObservation (reloc-deadline-from-observed-at): |
| +// the drain's target dies at installing while no worker of the region can |
| +// observe it (the source is frozen) for longer than the deadline, and the |
| +// group launches no spare. The first observation writes the fence record; |
| +// the operation waits a whole deadline from it before it is stuck. |
| +func TestDeadTargetDeadlineFromObservation(t *testing.T) { |
| + w := twoBoxWitness() |
| + from, to := w.boxes[0], w.boxes[3] |
| + w.serve(from, 1, app0) |
| + w.running(t, from) |
| + w.published(t, from) |
| + w.drainTo(t, to) |
| + w.oneBoxRegion[0] = true // no replacement launches: no spare |
| + if !w.reach(t, 1500, "installing", w.atPhase("installing"), w.act(from, to), w.recoveryPass) { |
| + w.mustHold(t) |
| + } |
| + w.terminate(to) |
| + from.Frozen = true |
| + w.drive(releaseDeadline+20, never, w.act(w.boxes[1], w.boxes[2])) |
| + from.Frozen = false |
| + w.stepUntil(t, 40, "the fence record", func() bool { return to.FenceObservedAt > 0 }) |
| + seen := w.now |
| + w.drive(releaseDeadline-5, never, w.act(from), w.recoveryPass) |
| + if w.claim.Op.Stuck != "" { |
| + t.Fatalf("stuck %d steps after the observation at %d, before its deadline (terminated at %d)", w.now-seen, seen, to.TerminatedAt) |
| + } |
| + w.reach(t, 60, "stuck after the deadline", func() bool { return w.claim.Op.Stuck != "" }, w.act(from), w.recoveryPass) |
| + w.mustHold(t) |
| +} |
| + |
| +// ---------- finding 7: the five guards, each discriminated ---------- |
| + |
| +// TestOnlyTheExecutorWritesP (reloc-exec-only-installs): at installing, |
| +// only the source (not op.exec) runs: nothing is written under P and no |
| +// local install is made on it. |
| +func TestOnlyTheExecutorWritesP(t *testing.T) { |
| + w := twoBoxWitness() |
| + from, to := w.boxes[0], w.boxes[3] |
| + w.serve(from, 1, app0) |
| + w.running(t, from) |
| + w.published(t, from) |
| + w.drainTo(t, to) |
| + if !w.stepUntil(t, 1500, "installing", w.atPhase("installing")) { |
| + w.mustHold(t) |
| + } |
| + p := w.claim.Op.Prepared |
| + for _, k := range w.buckets[0].keys(dataKey(w.claim.Holder.Location, p, "")) { |
| + w.buckets[0].objs[k] = nil // whatever the target began is set aside: only the source acts now |
| + delete(w.buckets[0].objs, k) |
| + } |
| + w.drive(40, never, w.act(from)) |
| + if ks := w.buckets[0].keys(dataKey(w.claim.Holder.Location, p, "")); len(ks) > 0 || from.receipt != nil || from.Files != nil && from.Files.Gen == p { |
| + t.Fatalf("the source, not op.exec, wrote P or installed it: %v", ks) |
| + } |
| +} |
| + |
| +// TestInstallAppliesThePinnedManifest (files-pin-exact): a newer manifest |
| +// of the dead executor lands between the pin and the install; the install |
| +// applies the pinned version, never the newest. |
| +func TestInstallAppliesThePinnedManifest(t *testing.T) { |
| + w := twoBoxWitness() |
| + from, to := w.boxes[0], w.boxes[3] |
| + w.serve(from, 1, app0) |
| + w.running(t, from) |
| + w.published(t, from) |
| + loc := w.claim.Holder.Location |
| + late := w.timerOn(from) |
| + w.holdKey(loc + "files/") |
| + w.publishFiles(from) // the newer manifest, carrying the timer, held |
| + w.hold = nil |
| + w.terminate(from) |
| + if !w.stepUntil(t, 400, "the pin journaled", func() bool { c := w.claim; return c.Op.Pin != nil }) { |
| + w.mustHold(t) |
| + } |
| + if n := w.completeHeld(loc + "files/"); n == 0 { |
| + t.Fatalf("no held manifest to land") |
| + } |
| + if !w.servingOn(t, to) { |
| + w.mustHold(t) |
| + } |
| + if contains(to.Timers, late) { |
| + t.Fatalf("the install applied the manifest that landed after the pin") |
| + } |
| +} |
| + |
| +// TestFailoverPinWaitsOutTheDelay (reloc-failover-pin-delay): no pin |
| +// before the fence's observed_at plus the delay. |
| +func TestFailoverPinWaitsOutTheDelay(t *testing.T) { |
| + w := twoBoxWitness() |
| + from, to := w.boxes[0], w.boxes[3] |
| + w.serve(from, 1, app0) |
| + w.running(t, from) |
| + w.published(t, from) |
| + w.terminate(from) |
| + ok := w.stepUntil(t, 400, "the pin", func() bool { |
| + c := w.claim |
| + if c.Op.Pin != nil && w.now < c.Op.FenceAt+failoverPinDelay { |
| + t.Fatalf("pinned at %d, before the fence's observation %d plus %d", w.now, c.Op.FenceAt, failoverPinDelay) |
| + } |
| + return c.Op.Kind == "relocating" && c.Op.Pin != nil |
| + }) |
| + if !ok { |
| + w.mustHold(t) |
| + } |
| + w.servingOn(t, to) |
| + w.finish(t) |
| + w.mustHold(t) |
| +} |
| + |
| +// TestPinNeverShortOfTheRelease (reloc-pin-reaches-release): the listing |
| +// lags behind the journaled release (its newest file is not yet visible); |
| +// no pin is journaled short of the release's final_txid. |
| +func TestPinNeverShortOfTheRelease(t *testing.T) { |
| + w := twoBoxWitness() |
| + from, to := w.boxes[0], w.boxes[3] |
| + w.serve(from, 1, app0) |
| + w.running(t, from) |
| + w.published(t, from) |
| + w.appWrite(from) |
| + w.drainTo(t, to) |
| + if !w.stepUntil(t, 1500, "the release journaled", func() bool { c := w.claim; return c.Op.Release != nil && c.Op.Pin == nil }) { |
| + w.mustHold(t) |
| + } |
| + c := w.claim |
| + bk := w.buckets[0] |
| + var hidden string |
| + var vs []*version |
| + for _, k := range bk.keys(dataKey(c.Holder.Location, c.Op.Release.Gen, "")) { |
| + if l, _, max, ok := ltxLevel(k); ok && l == 0 && max == c.Op.Release.FinalTX { |
| + hidden, vs = k, bk.objs[k] |
| + delete(bk.objs, k) |
| + } |
| + } |
| + if hidden == "" { |
| + t.Fatalf("no level-0 file at the release's final_txid %d", c.Op.Release.FinalTX) |
| + } |
| + w.drive(20, never, w.act(from, to)) |
| + if p := w.claim.Op.Pin; p != nil && p.TX < c.Op.Release.FinalTX { |
| + t.Fatalf("pinned at TXID %d, short of the release's %d", p.TX, c.Op.Release.FinalTX) |
| + } |
| + bk.objs[hidden] = vs |
| + w.servingOn(t, to) |
| + w.finish(t) |
| + w.mustHold(t) |
| +} |
| + |
| +// ---------- finding 8: claim §11's additional witnesses ---------- |
| + |
| +// TestCrashAtEachOpenBoundary (claim §11 "Crash between prepared |
| +// admission, marker publication and replication opening"): the target's |
| +// agent crashes exactly at each boundary of P's first admitted session: |
| +// admitted with the app starting (its launch environment held unready), |
| +// admitted with generation.json's PUT in flight (held), and replication |
| +// open; in a one-box and a two-box region. |
| +func TestCrashAtEachOpenBoundary(t *testing.T) { |
| + for _, stage := range []string{"app", "marker", "open"} { |
| + t.Run(stage, func(t *testing.T) { |
| + bothShapes(t, func(t *testing.T, w *world, boxes int) { |
| + from := w.serveAndPublish(t) |
| + w.timerOn(from) |
| + loc := w.claim.Holder.Location |
| + if boxes == 2 { |
| + w.drainTo(t, nil) |
| + } else { |
| + w.terminate(from) |
| + } |
| + if stage == "marker" { |
| + w.holdKey(genMarkerKey(loc)) |
| + } |
| + var to *box |
| + hit := w.stepUntil(t, 2000, "P's open at "+stage, func() bool { |
| + c := w.claim |
| + if c.Op.Kind != "relocating" || c.Op.Tgt < 0 { |
| + return false |
| + } |
| + to = w.boxByID(c.Op.Tgt) |
| + if stage == "app" && c.Op.Phase == "probing" && to.envUnreadyFor == 0 { |
| + to.envUnreadyFor = 20 // the launch environment is not ready yet |
| + } |
| + if stage == "open" { |
| + return preparedOpened(c) && to.open == nil && hasMain(to) |
| + } |
| + return to.open != nil && to.open.Prepared && to.open.stage == stage |
| + }) |
| + if !hit { |
| + return |
| + } |
| + w.crash(to) |
| + to.envUnreadyFor = 0 |
| + w.hold = nil |
| + w.servingOn(t, nil) |
| + w.finish(t) |
| + }) |
| + }) |
| + } |
| +} |
| + |
| +// TestAutomaticTargetLossRacesRecordCommit (claim §11 "Automatic target |
| +// loss racing the record commit CAS"): a move's target is terminated |
| +// just before, and just after, its record commit CAS; the regional |
| +// worker's automatic fence takes the operator's record-first path, so the |
| +// claim follows whichever the record holds: a rollback to the source |
| +// before the commit, a committed landing (then a failover in the target's |
| +// region) after it. |
| +func TestAutomaticTargetLossRacesRecordCommit(t *testing.T) { |
| + for _, when := range []string{"before the commit", "after the commit"} { |
| + t.Run(when, func(t *testing.T) { |
| + w := twoBoxWitness() |
| + src := w.boxes[0] |
| + w.serve(src, 1, app0) |
| + w.running(t, src) |
| + w.published(t, src) |
| + w.moveTo(1) |
| + if w.claim.Op.Kind != "moving" { |
| + t.Fatalf("no move: %s", w.state()) |
| + } |
| + tgt := w.boxByID(w.claim.Op.Tgt) |
| + ok := w.stepUntil(t, 1500, "the commit boundary", func() bool { |
| + c := w.claim |
| + if when == "before the commit" { |
| + return c.Op.Kind == "landing" && c.Op.LandPhase == "probed" && w.rec != nil && w.rec.MoveState == "landing" && w.now >= c.Op.ProbedAt+15 |
| + } |
| + return w.rec != nil && w.rec.MoveState == "committed" && c.Op.Kind == "landing" && !c.Op.Committed |
| + }) |
| + if !ok { |
| + w.mustHold(t) |
| + } |
| + w.terminate(tgt) |
| + w.servingOn(t, nil) |
| + w.finish(t) |
| + w.mustHold(t) |
| + c := w.claim |
| + if when == "before the commit" && (w.rec.Region != src.Region || w.execBox(c).Region != src.Region) { |
| + t.Fatalf("a loss before the commit did not return the host to the source's region: %s", w.state()) |
| + } |
| + if when == "after the commit" && (w.rec.Region != 1 || w.execBox(c).Region != 1) { |
| + t.Fatalf("a loss after the commit did not keep the host in the target's region: %s", w.state()) |
| + } |
| + }) |
| + } |
| +} |
| + |
| +// ---------- R18-2: the tie-break follows the host ---------- |
| + |
| +// TestTieHashFollowsTheHost (tie-hash-host; 1b-next R18-2): on equal |
| +// loads two hostnames may choose different boxes; the model's tie-break |
| +// hashes each host's own name. |
| +func TestTieHashFollowsTheHost(t *testing.T) { |
| + w := regionWorld(2) |
| + a, b := w.boxes[0], w.peer() |
| + sum := func(host string, id int) uint32 { // claim P5-D2, computed here independently of the model |
| + s := sha256.Sum256([]byte(fmt.Sprintf("%s\x00%d", host, id))) |
| + return uint32(s[0])<<24 | uint32(s[1])<<16 | uint32(s[2])<<8 | uint32(s[3]) |
| + } |
| + wantH, wantH2 := a, a |
| + if sum("h", b.ID) > sum("h", a.ID) { |
| + wantH = b |
| + } |
| + if sum("h2", b.ID) > sum("h2", a.ID) { |
| + wantH2 = b |
| + } |
| + if wantH == wantH2 { |
| + t.Skip("hosts h and h2 choose the same box among boxes 0 and 3") |
| + } |
| + if got := w.chooseBoxFor("h", 0, app0); got != wantH { |
| + t.Fatalf("host h chose %v, want %d", got, wantH.ID) |
| + } |
| + if got := w.chooseBoxFor("h2", 0, app0); got != wantH2 { |
| + t.Fatalf("host h2 chose %v, want %d", got, wantH2.ID) |
| + } |
| +} |
diff --git a/internal/sim/hostlife/regionha_test.go b/internal/sim/hostlife/regionha_test.go| index 9d8e987af..11c1ee7af 100644 |
| --- a/internal/sim/hostlife/regionha_test.go |
| +++ b/internal/sim/hostlife/regionha_test.go |
| @@ -166,6 +166,10 @@ func (w *world) relocRelease(b *box, c *claim) *releaseEntry { |
| if b.pubGen != h.Gen { |
| b.pubGen, b.pubSeq, b.releaseSeq = h.Gen, 0, 0 |
| } |
| + if !w.ensureObject(b, h, files) { |
| + w.stats["release: waits for its files object"]++ |
| + return nil |
| + } |
| if b.releaseSeq == 0 { |
| b.pubSeq++ |
| b.releaseSeq = b.pubSeq |
| @@ -257,9 +261,86 @@ func (w *world) selectPin(b *box, c *claim) *pinEntry { |
| w.markStuck(c, fmt.Sprintf("the pinned files carry no instance.key for a nonempty database (TXID %d)", n)) |
| return nil |
| } |
| + if m := w.pinnedManifestOf(b.Region, pin); m != nil && m.Files != nil && m.Files.Obj != "" && !w.originAuthorized(b.Region, c, m.Files.Obj) { |
| + // filesPin's referencedOrigins (1b-next rev 12 finding 1, R11-1): |
| + // the object the pinned manifest names must be current in this |
| + // region's bucket, under this holder's location, at an origin the |
| + // pin may cite; otherwise the pin refuses (ErrOrigin) and the |
| + // worker retries on a later pass |
| + w.stats["pin: files object refused"]++ |
| + w.logf("DEBUG pin refused obj %s cur=%v", m.Files.Obj, w.buckets[b.Region].current(m.Files.Obj) != nil) |
| + return nil |
| + } |
| return pin |
| } |
| +// ---------- files objects (rev 4, Astra R1-8; spec §5.6 "Objects are immutable") ---------- |
| + |
| +// objectKey is a files object: <holder.location>/files/<generation>/objects/<content>, |
| +// written create-only by the generation that first held the content. |
| +func objectKey(loc, gen string, f *filesDir) string { |
| + return dataKey(loc, gen, fmt.Sprintf("files/objects/%d-%d", f.Key, f.Env)) |
| +} |
| + |
| +// isFilesKey: a manifest or an object of the files tree. |
| +func isFilesKey(k string) bool { |
| + return strings.Contains(k, "files/m-") || strings.Contains(k, "files/objects/") |
| +} |
| + |
| +// objectCurrent: f names an object holding its content, in b's region |
| +// (the region binding; the mutation of files-objects-region-bound accepts |
| +// another region's object, as a moved host's carried reference). |
| +func (w *world) objectCurrent(b *box, f *filesDir) bool { |
| + if f == nil || f.Obj == "" || !strings.HasSuffix(f.Obj, fmt.Sprintf("/%d-%d", f.Key, f.Env)) { |
| + return false |
| + } |
| + return f.ObjRegion == b.Region || !on("files-objects-region-bound") |
| +} |
| + |
| +// ensureObject uploads f's content as an object of the current |
| +// generation when f names none for it in this region (a changed file, or |
| +// a host that came from another region), and reports once one is |
| +// acknowledged; an unchanged file keeps naming the object an older |
| +// generation wrote, which is what keeps that generation's objects live. |
| +func (w *world) ensureObject(b *box, h *holder, f *filesDir) bool { |
| + if f == nil || w.objectCurrent(b, f) { |
| + return true |
| + } |
| + k := objectKey(h.Location, h.Gen, f) |
| + if !w.ackedPut(b, k, &blob{Kind: "files-object", Inc: h.Inc, Gen: h.Gen, Files: f.clone()}, true) { |
| + return false |
| + } |
| + f.Obj, f.ObjRegion = k, b.Region |
| + w.stats["files objects written"]++ |
| + return true |
| +} |
| + |
| +// originAuthorized is the pin's check of one referenced object: current |
| +// in region r's bucket under the holder's location, and at an authorized |
| +// origin. With the rule (files-origins-referenced) the origins are the |
| +// generations the pinned manifest references, so any such object is |
| +// authorized; the mutation derives them from holder.generation and the |
| +// retained admissions, as rev 11 did, which the trim to eight shortens. |
| +func (w *world) originAuthorized(r int, c *claim, obj string) bool { |
| + h := c.Holder |
| + if !strings.HasPrefix(obj, h.Location) || w.buckets[r].current(obj) == nil { |
| + return false |
| + } |
| + if on("files-origins-referenced") { |
| + return true |
| + } |
| + g := genOf(h.Location, obj) |
| + if g == h.Gen || c.Op.Prepared != "" && g == c.Op.Prepared { |
| + return true |
| + } |
| + for _, e := range h.Admissions { |
| + if e.Gen == g || e.Predecessor.Gen == g { |
| + return true |
| + } |
| + } |
| + return false |
| +} |
| + |
| // pinnedManifestOf is the manifest pin names, read by version. |
| func (w *world) pinnedManifestOf(r int, pin *pinEntry) *blob { |
| if pin.ManKey == "" { |
| @@ -469,7 +550,7 @@ func (w *world) relocationLeftovers(n *claim, op opState) { |
| // mutation of reloc-exec-ack-barrier moves on with no acknowledgement. |
| func (w *world) relocStarting(b *box, c *claim) { |
| op := c.Op |
| - if on("reloc-exec-ack-barrier") && !w.leasesSeen(c) { |
| + if on("reloc-exec-ack-barrier") && !acked(c) { |
| return |
| } |
| w.cas(c, func(n *claim) bool { |
| @@ -527,7 +608,7 @@ func (w *world) relocReleasing(b *box, c *claim) { |
| } |
| return |
| } |
| - if on("reloc-ack-before-pinning") && !w.leasesSeen(c) { |
| + if on("reloc-ack-before-pinning") && !acked(c) { |
| w.stats["pin after release: waits for the acknowledgements"]++ |
| return |
| } |
| @@ -555,7 +636,7 @@ func (w *world) relocReleasing(b *box, c *claim) { |
| func (w *world) relocPinning(b *box, c *claim) { |
| op, h := c.Op, c.Holder |
| if op.Pin == nil { |
| - if op.Release == nil && on("reloc-failover-pin-delay") && w.now < op.FenceAt+failoverPinDelay { |
| + if on("reloc-failover-pin-delay") && (op.Release == nil || on("reloc-pin-delay-every-fence")) && w.now < latestObservation(op)+failoverPinDelay { |
| return |
| } |
| pin := w.selectPin(b, c) |
| @@ -591,7 +672,7 @@ func (w *world) relocPinning(b *box, c *claim) { |
| }) |
| return |
| } |
| - if on("reloc-exec-ack-barrier") && !w.leasesSeen(c) { |
| + if on("reloc-exec-ack-barrier") && !acked(c) { |
| return |
| } |
| to := op.Tgt |
| @@ -661,6 +742,9 @@ func (w *world) relocInstalling(b *box, c *claim) { |
| bk := w.buckets[b.Region] |
| installed := func(n *claim) bool { |
| ok := sameOp(n.Op.ID, op.ID) && n.Op.Kind == "relocating" && n.Op.Phase == "installing" && n.Op.Exec == op.Exec && n.Op.Prepared == g |
| + if ok && on("reloc-exec-ack-barrier") && !acked(n) { |
| + ok = false // ToInstalled's requireAcks (rev 4, Astra R1-4) |
| + } |
| if ok { |
| n.Op.Phase = "installed" |
| } |
| @@ -793,6 +877,9 @@ func (w *world) relocInstalled(b *box, c *claim) { |
| } |
| probing := func(n *claim) bool { |
| ok := sameOp(n.Op.ID, op.ID) && n.Op.Kind == "relocating" && n.Op.Phase == "installed" && n.Op.Exec == op.Exec && n.Op.Receipt != nil |
| + if ok && on("reloc-exec-ack-barrier") && !acked(n) { |
| + ok = false // ToProbing's requireAcks (rev 4, Astra R1-4) |
| + } |
| if ok { |
| n.Op.Phase, n.Op.ProbingSince = "probing", w.now |
| } |
| @@ -1201,6 +1288,7 @@ func (w *world) twoBoxStep() { |
| w.launchReplacements() |
| w.enrollStep() |
| for _, b := range w.liveBoxes() { |
| + w.renewController(b) |
| w.publishFiles(b) |
| } |
| if !w.calm && w.fail["terminate"] && w.rng.Intn(200) == 0 { |
| @@ -1212,6 +1300,10 @@ func (w *world) twoBoxStep() { |
| if !w.calm && w.rng.Intn(60) == 0 { |
| w.userRelocate() |
| } |
| + if !w.calm && w.rng.Intn(400) == 0 { |
| + bs := w.liveBoxes() |
| + w.updateExecutable(bs[w.rng.Intn(len(bs))]) // claim §5.10: refused while a controller record exists (rev 4) |
| + } |
| } |
| // regionHAOwnsLoss: the loss of b is region HA's to recover (model ruling |
| @@ -1278,6 +1370,14 @@ func (w *world) fenceStep(b *box, c *claim) bool { |
| if len(cands) == 0 { |
| return false |
| } |
| + if x := cands[0]; x.FenceObservedAt == 0 { |
| + // hostfence.TerminationWorker: the first worker to observe the |
| + // terminated state writes the box-fences record with that |
| + // observed_at; every deadline and delay runs from it, never from |
| + // the termination itself, which no worker saw (rev 4, Astra R1-5) |
| + x.FenceObservedAt = w.now |
| + w.logf("box %d observed box %d terminated: fence record, observed_at %d", b.ID, x.ID, w.now) |
| + } |
| before := w.claim.Ver |
| w.fence(b, c, cands[0]) |
| return w.claim.Ver != before |
| @@ -1324,7 +1424,34 @@ func (w *world) fence(b *box, c *claim, x *box) { |
| w.convertToRelocating(c, x) |
| } |
| return |
| - case op.Kind == "moving" && op.Tgt == x.ID, (op.Kind == "landing" || op.Kind == "restoring") && op.Tgt == x.ID, op.Kind == "creating": |
| + case op.Kind == "landing" && op.Committed && op.Tgt == x.ID && on("fence-converts-committed-landing"): |
| + // finding F5 (rev 4): the record committed the landing, so no |
| + // rollback is possible, and its dead target can never finish it. |
| + // The fence makes it a failover in the target's region, as a |
| + // serving executor's fence does (plan ruling 20); the mutation |
| + // leaves it to the operator's path, which has nothing to do |
| + id := op.ID |
| + if w.cas(c, func(n *claim) bool { |
| + if !sameOp(n.Op.ID, id) || n.Op.Kind != "landing" || !n.Op.Committed || contains(n.Lost, x.ID) { |
| + return false |
| + } |
| + w.startFailover(n, x) |
| + w.fenceBox(n, x) |
| + return true |
| + }) { |
| + w.stats["fences written"]++ |
| + w.stats["relocation started: failover of a committed landing"]++ |
| + w.logf("box %d fenced box %d, the committed landing %s's dead target: failover in region %d", b.ID, x.ID, id, x.Region) |
| + w.declareTimers(x, w.claim.Holder) |
| + } |
| + return |
| + case (op.Kind == "landing" || op.Kind == "restoring") && op.Tgt == x.ID: |
| + // claim D2's automatic termination for a move's target (rev 4, |
| + // claim §11 "automatic target loss racing the record commit CAS"): |
| + // the same record-first declared loss the operator makes |
| + w.declareTargetLost(c) |
| + return |
| + case op.Kind == "moving" && op.Tgt == x.ID, op.Kind == "creating": |
| return |
| case op.Kind == "relocating" && op.Stuck != "": |
| return // Worker.Step consumes no fence of a stuck operation: the operator's resolve does |
| @@ -1368,7 +1495,12 @@ func (w *world) fence(b *box, c *claim, x *box) { |
| // regional work with the dead box, where nothing runs it. |
| func (w *world) fenceBox(n *claim, x *box) { |
| n.Lost = addUniq(n.Lost, x.ID) |
| - n.Op.FenceBox, n.Op.FenceAt = x.ID, w.now |
| + at := x.FenceObservedAt |
| + if at == 0 { |
| + at = w.now |
| + } |
| + n.Op.FenceBox, n.Op.FenceAt = x.ID, at |
| + n.Op.Observed = append(n.Op.Observed, at) // fence.<box>.observed_at, retained for every later pin (JournalPin) |
| var parts []int |
| for _, p := range n.Op.Parts { |
| if p != x.ID { |
| @@ -1521,7 +1653,7 @@ func (w *world) replaceTarget(n *claim, x *box) bool { |
| } |
| next := w.chooseBoxExcept(n.Op.SrcRegion, n.Holder.App, relocExcept(n.Op, x.ID)...) |
| if next == nil { |
| - if on("reloc-dead-target-bound") && w.now > x.TerminatedAt+releaseDeadline { |
| + if on("reloc-dead-target-bound") && x.FenceObservedAt > 0 && w.now > observedAt(x)+releaseDeadline { |
| // FenceTargetWithoutSpare (1b-next rev 18 finding 2): the fence |
| // is consumed ReleaseDeadline after its observed_at and the |
| // operation is stuck; the mutation waits for a spare for ever |
| @@ -1633,9 +1765,12 @@ func (w *world) publishFiles(b *box) { |
| b.pubGen, b.pubSeq, b.releaseSeq = h.Gen, 0, 0 |
| } |
| state := filesState(b.Timers, b.Files) |
| - if state == b.published { |
| + if state == b.published && w.objectCurrent(b, b.Files) { |
| return |
| } |
| + if !w.ensureObject(b, h, b.Files) { |
| + return // the object first: a manifest names only durable objects (§5.6) |
| + } |
| b.pubSeq++ |
| w.issued++ |
| bl := &blob{Kind: "files", Inc: h.Inc, Gen: h.Gen, Seq: b.pubSeq, Files: b.Files.clone(), Timers: append([]int(nil), b.Timers...), Base: w.issued} |
| @@ -1710,9 +1845,12 @@ func (w *world) filesLive(c *claim, k string) bool { |
| // filesLiveSet is the files live set itself, which the residue oracle |
| // reads whatever is mutated. |
| func (w *world) filesLiveSet(c *claim, k string) bool { |
| - if c == nil || c.Holder == nil || !isManifestKey(k) { |
| + if c == nil || c.Holder == nil || !isFilesKey(k) { |
| return false |
| } |
| + if !isManifestKey(k) { |
| + return w.objectReferenced(c, k) |
| + } |
| loc := c.Holder.Location |
| if !strings.HasPrefix(k, loc) { |
| return false |
| @@ -1766,3 +1904,203 @@ func (w *world) regionMin(r int) int { |
| } |
| return w.perRegion |
| } |
| + |
| +// ---------- acknowledgements (rev 4, Astra R1-4) ---------- |
| + |
| +// acked is requireAcks: every current participant has a durable |
| +// exec_ack.<box> entry in the journal. It reads only the claim; whether a |
| +// participant's controller is ready now is the participant's own check |
| +// before its effects (recordAck, and role()'s lease), never the barrier. |
| +func acked(c *claim) bool { |
| + for _, p := range c.Op.Parts { |
| + if !contains(c.Op.Acks, p) { |
| + return false |
| + } |
| + } |
| + return true |
| +} |
| + |
| +// recordAck is AcknowledgeExecution: a participant whose controller is |
| +// ready (its execution lease current, role() renews it first) journals |
| +// exec_ack.<box> once; the entry outlives a lost lease or an agent |
| +// restart (1b-next rev 2 finding 10: the claim keeps the first |
| +// acknowledgement). A box replaced out of the participants keeps its |
| +// entry, which the barrier no longer reads. |
| +func (w *world) recordAck(b *box, c *claim) { |
| + if c == nil || c.Op.Kind != "relocating" || !contains(c.Op.Parts, b.ID) || contains(c.Op.Acks, b.ID) || contains(c.Lost, b.ID) { |
| + return |
| + } |
| + if b.ExecUntil == 0 || w.localNow(b) > b.ExecUntil { |
| + return // no ready controller: nothing to acknowledge with |
| + } |
| + id := c.Op.ID |
| + // the controller's durable record exists before the acknowledgement |
| + // (1b-next Task 7: journaled before the open), and stays until a |
| + // successful scoped cleanup clears it (finishParticipation) |
| + b.execRecord, b.cleanupPending = id, true |
| + if w.cas(c, func(n *claim) bool { |
| + ok := sameOp(n.Op.ID, id) && n.Op.Kind == "relocating" && contains(n.Op.Parts, b.ID) && !contains(n.Op.Acks, b.ID) |
| + if ok { |
| + n.Op.Acks = append(n.Op.Acks, b.ID) |
| + } |
| + return ok |
| + }) { |
| + w.logf("relocation %s: box %d acknowledged execution", id, b.ID) |
| + } |
| +} |
| + |
| +// finishParticipation is the participant's Sweep and Finish (1b-next |
| +// Task 6 and 7, rulings 20): once the claim no longer runs the operation |
| +// with this box as a live participant, the scoped cleanup runs (it |
| +// retires an unopened P's local install of that operation, and is a |
| +// no-op on a box that admitted a writer or serves the host); only when it |
| +// succeeds is the durable record cleared (rule reloc-clear-after-cleanup; |
| +// the mutation clears it after a failed cleanup, as rev 4 of 1b-next |
| +// did). A box whose cleanup fails keeps the record, and root refuses an |
| +// executable update while it exists (claim §5.10). |
| +func (w *world) finishParticipation(b *box, c *claim) { |
| + if b.execRecord == "" || c == nil { |
| + return |
| + } |
| + if c.Op.Kind == "relocating" && c.Op.ID == b.execRecord && contains(c.Op.Parts, b.ID) && !contains(c.Lost, b.ID) { |
| + return // still a participant |
| + } |
| + if b.cleanupFails { |
| + w.stats["relocation controller: scoped cleanup failed"]++ |
| + if on("reloc-clear-after-cleanup") { |
| + return // the record stays, and so does the refusal of updates |
| + } |
| + b.execRecord = "" // the mutation: cleared anyway |
| + return |
| + } |
| + if f := b.Files; f != nil && f.Gen != "" && c.Holder != nil && f.Inc == c.Holder.Inc && strings.HasPrefix(f.Gen, "P") && !(c.Op.Kind == "serving" && c.Op.Exec == b.ID) && f.Gen != c.Holder.Gen && !w.ancestorGen(c.Holder.Location, c.Holder.Gen, f.Gen) { |
| + w.retireArtifacts(b, f.Inc, f.Stamp) // an unopened P's local install of the finished operation |
| + } |
| + b.execRecord, b.cleanupPending = "", false |
| + w.stats["relocation controller: record cleared"]++ |
| +} |
| + |
| +// updateExecutable is an executable update on b (claim §5.10, region HA |
| +// §5.10): root refuses it while a relocation controller's record exists. |
| +// INV-29 is the oracle: an update never runs on a box whose relocation |
| +// participation's scoped cleanup has not succeeded. |
| +func (w *world) updateExecutable(b *box) bool { |
| + if b.Destroyed { |
| + return false |
| + } |
| + if b.execRecord != "" { |
| + w.stats["executable update refused: controller record"]++ |
| + return false |
| + } |
| + if b.cleanupPending { |
| + w.violate("INV-29: box %d updated its executable while a relocation's scoped cleanup had not succeeded (claim §5.10)", b.ID) |
| + } |
| + w.stats["executable updated"]++ |
| + return true |
| +} |
| + |
| +// latestObservation is the newest observed_at the operation's journal |
| +// retains (JournalPin checks every fence.<box>.observed_at, a release or |
| +// not: rev 4, Astra R1-5); FenceAt covers a converted move's fence. |
| +func latestObservation(op opState) int { |
| + at := op.FenceAt |
| + for _, o := range op.Observed { |
| + if o > at { |
| + at = o |
| + } |
| + } |
| + return at |
| +} |
| + |
| +// observedAt is when the fence record says the box was observed |
| +// terminated (FenceTargetWithoutSpare's deadline basis); the mutation of |
| +// reloc-deadline-from-observed-at uses the termination itself, which no |
| +// worker may have seen yet. |
| +func observedAt(x *box) int { |
| + if !on("reloc-deadline-from-observed-at") { |
| + return x.TerminatedAt |
| + } |
| + return x.FenceObservedAt |
| +} |
| + |
| +// objectReferenced: a live manifest (the chain's newest in any region, |
| +// the pinned one, holder.generation's or P's) names the object, or a |
| +// live box's files directory does (its next manifest will): the files |
| +// live set is every object the live manifests reference (claim §6.2a). |
| +func (w *world) objectReferenced(c *claim, k string) bool { |
| + loc := c.Holder.Location |
| + names := func(m *blob) bool { return m != nil && m.Files != nil && m.Files.Obj == k } |
| + for r := 0; r < nRegions; r++ { |
| + if _, _, _, _, m := w.newestManifest(r, loc, c.Holder.Gen); names(m) { |
| + return true |
| + } |
| + bk := w.buckets[r] |
| + for _, g := range []string{c.Holder.Gen, c.Op.Prepared} { |
| + if g == "" && g != c.Holder.Gen { |
| + continue |
| + } |
| + for _, mk := range bk.keys(dataKey(loc, g, "files/m-")) { |
| + if v := bk.current(mk); v != nil && names(v.B) { |
| + return true |
| + } |
| + } |
| + } |
| + } |
| + if c.Op.Kind == "relocating" && c.Op.Pin != nil && c.Op.Pin.ManKey != "" { |
| + if names(w.pinnedManifestOf(c.Op.SrcRegion, c.Op.Pin)) { |
| + return true |
| + } |
| + } |
| + for _, b := range w.liveBoxes() { |
| + if b.Files != nil && b.Files.Obj == k { |
| + return true |
| + } |
| + } |
| + return false |
| +} |
| + |
| +// keepFilesLive wraps a moves park's keep (a push's whole-location park, |
| +// a landing's install park, a rollback's return park) so it never |
| +// archives the files live set (finding F4, rev 4: claim §6.2a's live set |
| +// binds every park; moves' parks predate region HA's files tree). Only |
| +// the two-box shape has files keys, so the one-box shape is unchanged. |
| +// The mutation of files-live-set-moves-parks archives them with the rest. |
| +func (w *world) keepFilesLive(keep func(string) bool) func(string) bool { |
| + return func(k string) bool { |
| + return keep(k) || on("files-live-set-moves-parks") && w.filesLive(w.claim, k) |
| + } |
| +} |
| + |
| +// renewController is a relocation controller's own renewal loop (hostexec |
| +// renews its lease on its own clock, not when the regional worker happens |
| +// to run; rev 4): an agent that is up and holds a current lease for a |
| +// relocation it participates in keeps it current. A lease is still lost |
| +// when the agent is down, paused, frozen or partitioned past the TTL, |
| +// which is the scoped cleanup's case. Two-box shape only. |
| +func (w *world) renewController(b *box) { |
| + c := w.claim |
| + if c == nil || c.Op.Kind != "relocating" || !contains(c.Op.Parts, b.ID) || !w.agentUp(b) || b.Partitioned { |
| + return |
| + } |
| + if b.ExecUntil > 0 && w.localNow(b) <= b.ExecUntil && b.ExecUntil-w.localNow(b) < execRenew { |
| + b.ExecUntil = w.localNow(b) + execTTL |
| + w.execLease[b.ID] = execLease{Op: c.Op.ID, Expires: w.now + execTTL} |
| + } |
| +} |
| + |
| +// preparedManifestHere is moves rev 7.22 §7.6's one install routine (L16, |
| +// L17; claim R18-1) for a landing or a return in the two-box shape (rev |
| +// 4, claim §11 "move landing, source cleanup, then target failure with an |
| +// unchanged file"): the generation's prepared files manifest, create-only |
| +// at sequence 0 in this region, naming objects in this region's bucket |
| +// (an unchanged file the host carried from another region is uploaded |
| +// here first), acknowledged before the install's CAS. Without it a |
| +// target lost right after its commit would leave no files in its region. |
| +func (w *world) preparedManifestHere(b *box, c *claim, gen string) bool { |
| + h := c.Holder |
| + if !w.ensureObject(b, h, b.Files) { |
| + return false |
| + } |
| + bl := &blob{Kind: "files", Inc: h.Inc, Gen: gen, Seq: 0, Files: b.Files.clone(), Timers: append([]int(nil), b.Timers...), Text: c.Op.ID, Base: w.issued} |
| + return w.ackedPut(b, manifestKey(h.Location, gen, 0), bl, true) |
| +} |
diff --git a/internal/sim/hostlife/regionha_witness_test.go b/internal/sim/hostlife/regionha_witness_test.go| index 2523a7f01..575717734 100644 |
| --- a/internal/sim/hostlife/regionha_witness_test.go |
| +++ b/internal/sim/hostlife/regionha_witness_test.go |
| @@ -822,3 +822,148 @@ func wDeadTargetBound(t *testing.T, w *world) { |
| w.servingOn(t, from) |
| w.finish(t) |
| } |
| + |
| +// rev 4: Astra's round 1, claim §11's witnesses |
| + |
| +// wMoveUnchangedFile (files-objects-region-bound; claim §11 "move |
| +// landing, source cleanup, then target failure with an unchanged file"): |
| +// the host moves to region 1 carrying a file unchanged since region 0 |
| +// published it; the landing's prepared manifest and the target's |
| +// publications name an object in region 1's bucket; the source region is |
| +// cleaned up; the target is terminated and the failover in region 1 pins |
| +// that object. Without the region binding the manifests keep naming |
| +// region 0's object, which no failover in region 1 can pin (INV-3). |
| +func wMoveUnchangedFile(t *testing.T, w *world) { |
| + w.twoBox() |
| + src := w.boxes[0] |
| + w.serve(src, 1, app0) |
| + w.running(t, src) |
| + w.published(t, src) |
| + w.moveTo(1) |
| + if !w.servingOn(t, nil) { |
| + return |
| + } |
| + e := w.execBox(w.claim) |
| + if e.Region != 1 { |
| + w.violate("witness: the move did not land in region 1: %s", w.state()) |
| + return |
| + } |
| + w.reach(t, 1200, "the source region cleaned up", func() bool { return len(w.claim.Obl) == 0 }, w.actAll(), w.recoveryPass) |
| + w.published(t, e) |
| + w.terminate(e) |
| + w.reach(t, 3000, "serving again after the target's failover", func() bool { |
| + c := w.claim |
| + return c.Op.Kind == "serving" && c.Op.Exec >= 0 && c.Op.Exec != e.ID |
| + }, w.actAll(), w.recoveryPass, w.operator, w.wakeExec) |
| + w.finish(t) |
| +} |
| + |
| +// wOriginsAfterTrim (files-origins-referenced; 1b-next rev 12 finding 1, |
| +// R11-1): a file published in the origin generation never changes while |
| +// ten cold admissions follow, so holder.admissions is trimmed past it |
| +// while the live manifest still names the origin's object. The failover |
| +// pins that object; authorized from the trimmed admissions alone, the pin |
| +// is refused for ever (INV-3). |
| +func wOriginsAfterTrim(t *testing.T, w *world) { |
| + w.twoBox() |
| + from := w.boxes[0] |
| + w.serve(from, 1, app0) |
| + w.running(t, from) |
| + w.published(t, from) |
| + for i := 0; i < 10; i++ { |
| + w.crash(from) |
| + if !w.reach(t, 400, "a fresh cold admission serving", func() bool { |
| + return hasMain(from) && from.open == nil && len(w.claim.Obl) == 0 |
| + }, w.actAll(), w.recoveryPass, func() { w.wake(from) }) { |
| + return |
| + } |
| + } |
| + for _, e := range w.claim.Holder.Admissions { |
| + if e.Gen == "" || e.Predecessor.Gen == "" { |
| + w.violate("witness: the origin generation is still in holder.admissions: %s", w.state()) |
| + return |
| + } |
| + } |
| + w.terminate(from) |
| + w.servingOn(t, w.boxes[3]) |
| + w.finish(t) |
| +} |
| + |
| +// wClearAfterCleanup (reloc-clear-after-cleanup; claim §11 "a failed |
| +// cleanup leaving a controller record that blocks executable updates"): |
| +// the drain completes; the former source's participation is over, but its |
| +// scoped cleanup fails, so its controller record stays and root refuses |
| +// an executable update; once the cleanup succeeds the record is cleared |
| +// and the update runs. Without the rule the record is cleared after the |
| +// failed cleanup and the update runs over it (INV-29). |
| +func wClearAfterCleanup(t *testing.T, w *world) { |
| + w.twoBox() |
| + from, to := w.boxes[0], w.boxes[3] |
| + w.serve(from, 1, app0) |
| + w.running(t, from) |
| + w.published(t, from) |
| + w.drainTo(t, to) |
| + from.cleanupFails = true |
| + if !w.servingOn(t, to) { |
| + return |
| + } |
| + w.drive(20, never, w.act(from)) |
| + if w.updateExecutable(from) { |
| + if on("reloc-clear-after-cleanup") { |
| + w.violate("witness: an update ran while the controller record existed") |
| + } |
| + return |
| + } |
| + from.cleanupFails = false |
| + w.reach(t, 100, "the record cleared", func() bool { return from.execRecord == "" }, w.act(from)) |
| + if !w.updateExecutable(from) { |
| + w.violate("INV-3 (witness): the update stayed refused after a successful cleanup") |
| + } |
| + w.finish(t) |
| +} |
| + |
| +// wCommittedLandingTargetLost (fence-converts-committed-landing; claim |
| +// §11 "automatic target loss racing the record commit CAS", finding F5): |
| +// the record commits the landing, and the target is terminated before |
| +// the claim follows; the fence makes the committed landing a failover in |
| +// region 1, which serves; without it nothing ever finishes it (INV-3). |
| +func wCommittedLandingTargetLost(t *testing.T, w *world) { |
| + w.twoBox() |
| + src := w.boxes[0] |
| + w.serve(src, 1, app0) |
| + w.running(t, src) |
| + w.published(t, src) |
| + w.moveTo(1) |
| + tgt := w.boxByID(w.claim.Op.Tgt) |
| + if !w.stepUntil(t, 1500, "the record committed, the claim not yet", func() bool { |
| + c := w.claim |
| + return w.rec != nil && w.rec.MoveState == "committed" && c.Op.Kind == "landing" && !c.Op.Committed |
| + }) { |
| + return |
| + } |
| + w.terminate(tgt) |
| + w.servingOn(t, nil) |
| + w.finish(t) |
| +} |
| + |
| +// wPushKeepsLiveFiles (files-live-set-moves-parks; finding F4): a push |
| +// parks the whole location before installing its generation; the files |
| +// live set survives it, so a later failover pins the live manifest's |
| +// object. Without the rule the push archives them, and the failover can |
| +// never pin the host's files (INV-3). |
| +func wPushKeepsLiveFiles(t *testing.T, w *world) { |
| + w.twoBox() |
| + from := w.boxes[0] |
| + w.serve(from, 1, app0) |
| + w.running(t, from) |
| + w.published(t, from) |
| + w.userPush() |
| + if !w.reach(t, 800, "the push served", func() bool { c := w.claim; return c.Op.Kind == "serving" && c.Holder.Gen != "" && len(c.Obl) == 0 }, w.actAll(), w.recoveryPass, func() { w.wake(from) }) { |
| + return |
| + } |
| + w.drive(10, never, w.act(from)) |
| + w.completeDue(true) |
| + w.terminate(from) |
| + w.servingOn(t, w.boxes[3]) |
| + w.finish(t) |
| +} |
diff --git a/internal/sim/hostlife/rules_test.go b/internal/sim/hostlife/rules_test.go| index 7af7a8064..598d7ba0a 100644 |
| --- a/internal/sim/hostlife/rules_test.go |
| +++ b/internal/sim/hostlife/rules_test.go |
| @@ -186,4 +186,15 @@ var allRules = []string{ |
| "reloc-dead-target-bound", // 1b-next rev 18 finding 2 (FenceTargetWithoutSpare): a dead target with no spare is fenced into stuck ReleaseDeadline after its observed_at; the mutation waits for ever (INV-3) |
| "reloc-abandoned-prepared", // 1b-next ruling 27, rev 18 finding 3 (abandonPrepared, abandoned_prepared): every unopened P that is replaced or dropped, on every path, is parked at completion; the mutation records none (INV-10) |
| "files-pin-needs-key", // 1b-next ruling 25 as rev 18 amended it (F2, L21): a nonempty database with an admitted writer pins only a manifest carrying instance.key, else stuck; the mutation pins it keyless and the install mints a fresh key (INV-4) |
| + // Astra's round 1 on this plan (rev 4) |
| + "reloc-stuck-refuses-admission", // 1b-next relocationAdmission's stuck check (ruling 9, R1-16): a stuck operation admits no writer, the live source's ordinary wake included; the mutation admits it |
| + "ha-sole-box-eligibility", // region HA §2 with region HA on: the last remaining box of a region is checked for enrollment, key, executable, lost and park-local like any other; the mutation keeps the one-box shortcut |
| + "reloc-pin-delay-every-fence", // JournalPin checks every retained fence observation, after a release too (a target replaced after the source's release); the mutation skips the delay once a release exists |
| + "reloc-deadline-from-observed-at", // FenceTargetWithoutSpare's deadline runs from the fence record's observed_at; the mutation runs it from the termination, which no worker saw |
| + "tie-hash-host", // claim P5-D2, 1b-next R18-2 (ExecutorChooser hashes the record's host): the tie-break is SHA-256(host + "\x00" + box); the mutation hashes a constant name |
| + "files-origins-referenced", // 1b-next rev 12 finding 1 (filesPin's referencedOrigins, R11-1): the pin authorizes the generations the pinned manifest's objects lie in, never only those the trimmed admission list names; the mutation refuses an unchanged file's old origin and the failover waits for ever (INV-3) |
| + "files-objects-region-bound", // §5.6 region binding (filesPin: the object in this region's data bucket): a host that came from another region uploads its unchanged files again before naming them; the mutation keeps naming the source region's objects and the failover can never pin (INV-3) |
| + "files-live-set-moves-parks", // finding F4 (rev 4), claim §6.2a: moves' parks (a push's whole-location park, a landing's install park, a rollback's return park) keep the files live set; the mutation archives it with the rest and the next failover can never pin the live files (INV-3) |
| + "reloc-clear-after-cleanup", // 1b-next ruling 20 and rev 6 R4-5 (Finish clears the record only after a successful scoped cleanup): a failed cleanup keeps the controller record, which blocks executable updates (claim §11's witness); the mutation clears it and an update runs over the unfinished cleanup (INV-29) |
| + "fence-converts-committed-landing", // finding F5 (rev 4; claim §11 "automatic target loss racing the record commit CAS"): a landing whose record committed and whose target is then terminated becomes a failover in the target's region; the mutation leaves it to the operator, and it never completes (INV-3) |
| } |
diff --git a/internal/sim/hostlife/sim_test.go b/internal/sim/hostlife/sim_test.go| index da4a709fb..acce63db3 100644 |
| --- a/internal/sim/hostlife/sim_test.go |
| +++ b/internal/sim/hostlife/sim_test.go |
| @@ -401,7 +401,8 @@ func (w *world) checkStep() { |
| // enrolled box that is not on lost; execution authority never names a |
| // fenced or unenrolled reference |
| if c := w.claim; c != nil && c.Op.Kind == "relocating" && c.Op.Exec >= 0 { |
| - if e := w.boxByID(c.Op.Exec); e == nil || !e.Enrolled || contains(c.Lost, e.ID) { |
| + released := c.Op.Release != nil && c.Op.Release.Box == c.Op.Exec // a released executor fenced before PinAfterRelease (FenceSource after the release, rev 4) |
| + if e := w.boxByID(c.Op.Exec); e == nil || !e.Enrolled || contains(c.Lost, e.ID) && !released { |
| w.violate("INV-27: relocation %s names box %d as op.exec, which is unenrolled or lost", c.Op.ID, c.Op.Exec) |
| } |
| } |
diff --git a/internal/sim/hostlife/twobox_test.go b/internal/sim/hostlife/twobox_test.go| index 0d6c828e6..34a2f02dd 100644 |
| --- a/internal/sim/hostlife/twobox_test.go |
| +++ b/internal/sim/hostlife/twobox_test.go |
| @@ -1,11 +1,14 @@ |
| package hostlife |
| import ( |
| + "crypto/sha256" |
| "fmt" |
| "hash/fnv" |
| "os" |
| ) |
| +var _ = fnv.New32a // rev 1's stand-in hash, kept importable |
| + |
| // Two boxes per region (region HA spec 1 §9 L18; claim rev 6.30 §11). |
| // |
| // boxesPerRegion is the world's shape: one box per region, today's model, |
| @@ -50,10 +53,19 @@ func (w *world) addBox(r int) *box { |
| // tieHash is the model's stand-in for claim P5-D2's SHA-256 of |
| // host + "\x00" + box reference: a fixed function of the reference, never |
| // a draw, so the choice is the same on every replay. |
| -func tieHash(id int) uint32 { |
| - h := fnv.New32a() |
| - h.Write([]byte(fmt.Sprintf("%s\x00%d", host, id))) |
| - return h.Sum32() |
| +func tieHash(id int) uint32 { return tieHashFor(host, id) } |
| + |
| +// tieHashFor is claim P5-D2's tie-break for the named host (rev 4, Astra |
| +// R1-8 and 1b-next R18-2): the first four bytes of SHA-256(host + "\x00" + |
| +// box reference), so two hostnames on equal loads may choose different |
| +// boxes. The mutation of tie-hash-host hashes a constant name, as the |
| +// round-18 chooser bug did. |
| +func tieHashFor(hostName string, id int) uint32 { |
| + if !on("tie-hash-host") { |
| + hostName = host |
| + } |
| + sum := sha256.Sum256([]byte(fmt.Sprintf("%s\x00%d", hostName, id))) |
| + return uint32(sum[0])<<24 | uint32(sum[1])<<16 | uint32(sum[2])<<8 | uint32(sum[3]) |
| } |
| // hostsOn counts the instances of app placed on b (app "" counts every |
| @@ -105,8 +117,16 @@ func (w *world) chooseBox(r int, app string) *box { return w.chooseBoxExcept(r, |
| // world; the caller records the choice in the claim's intent and never |
| // substitutes (rule create-choice-once). |
| func (w *world) chooseBoxExcept(r int, app string, except ...int) *box { |
| + return w.chooseBoxFor(host, r, app, except...) |
| +} |
| + |
| +// chooseBoxFor is choose() for the named host (its tie-break hashes that |
| +// name). The sole-box shortcut, today's behaviour, is the one-box shape's |
| +// alone: with region HA on, one remaining candidate is checked like any |
| +// other (rev 4, Astra R1-3; rule ha-sole-box-eligibility). |
| +func (w *world) chooseBoxFor(hostName string, r int, app string, except ...int) *box { |
| bs := w.regionBoxes(r) |
| - if len(bs) <= 1 { |
| + if len(bs) <= 1 && (w.perRegion <= 1 || !on("ha-sole-box-eligibility")) { |
| if len(bs) == 0 || contains(except, bs[0].ID) { |
| return nil |
| } |
| @@ -125,7 +145,7 @@ func (w *world) chooseBoxExcept(r int, app string, except ...int) *box { |
| if on("reloc-enrolled-only") && !b.Enrolled { |
| continue |
| } |
| - key := [3]int{w.hostsOn(b, app), w.hostsOn(b, ""), -int(tieHash(b.ID))} |
| + key := [3]int{w.hostsOn(b, app), w.hostsOn(b, ""), -int(tieHashFor(hostName, b.ID))} |
| if best == nil || key[0] < bestKey[0] || key[0] == bestKey[0] && (key[1] < bestKey[1] || key[1] == bestKey[1] && key[2] < bestKey[2]) { |
| best, bestKey = b, key |
| } |
diff --git a/internal/sim/hostlife/witness_test.go b/internal/sim/hostlife/witness_test.go| index 5b7fa7720..a93c223cf 100644 |
| --- a/internal/sim/hostlife/witness_test.go |
| +++ b/internal/sim/hostlife/witness_test.go |
| @@ -241,6 +241,17 @@ var witnesses = []witness{ |
| {"files-prepared-seq-zero", "files-prepared-seq-zero", "INV-28", |
| "the source's manifests reach sequence 3; P's prepared manifest keeps 3, the probe session publishes its timer at 1, and the nested failover pins and declares from the stale prepared manifest", wFilesPreparedSeqZero}, |
| // rev 3: 1b-next rev 17 to 19's fixes for the model's findings, and the L21 window |
| + // rev 4: Astra's round 1 and claim §11's additional witnesses |
| + {"files-objects-region-bound", "files-objects-region-bound", "INV-3", |
| + "claim §11: the host moves to region 1 with a file unchanged since region 0 published it, the source region is cleaned up, then the target dies; the failover pins an object in region 1's bucket, or, without the region binding, can never pin region 0's", wMoveUnchangedFile}, |
| + {"files-origins-referenced", "files-origins-referenced", "INV-3", |
| + "R11-1: a file unchanged through ten cold admissions, holder.admissions trimmed past its origin; the failover pins the origin's object, or, authorized from the trimmed list, is refused for ever", wOriginsAfterTrim}, |
| + {"reloc-clear-after-cleanup", "reloc-clear-after-cleanup", "INV-29", |
| + "claim §11: the former source's scoped cleanup fails after the drain; its controller record stays and root refuses an executable update until the cleanup succeeds; without the rule the update runs over the unfinished cleanup", wClearAfterCleanup}, |
| + {"fence-converts-committed-landing", "fence-converts-committed-landing", "INV-3", |
| + "claim §11, F5: the record commits a landing and its target dies before the claim follows; the fence makes it a failover in the target's region, or nothing ever finishes it", wCommittedLandingTargetLost}, |
| + {"files-live-set-moves-parks", "files-live-set-moves-parks", "INV-3", |
| + "F4: a push parks the whole location; the files live set survives, so the later failover pins the live object, or can never pin the host's files", wPushKeepsLiveFiles}, |
| {"files-pin-needs-key", "files-pin-needs-key", "INV-4", |
| "L21, explicit: the pre-start manifest copy landed without instance.key, the app minted the key after starting and replicated rows sealed with it, and the box died before the keyed manifest landed; with the rule recovery is stuck and installs nothing, without it the keyless pin installs a fresh key over the sealed rows", wL21Window}, |
| {"reloc-no-spare-bound", "reloc-no-spare-bound", "INV-3", |
diff --git a/internal/sim/hostlife/world_test.go b/internal/sim/hostlife/world_test.go| index cfb51f788..a1b97b293 100644 |
| --- a/internal/sim/hostlife/world_test.go |
| +++ b/internal/sim/hostlife/world_test.go |
| @@ -259,6 +259,11 @@ type filesDir struct { |
| Env int // admin token identity in <host>.env |
| Done bool // markers written last |
| Stamp int // the installation stamp that produced it (claim rev 6.5 §6.3) |
| + // Obj is the files object that holds this content (region HA §5.6, |
| + // rev 4): written by the generation that first held it, in ObjRegion's |
| + // bucket; an unchanged file keeps naming it generations later |
| + Obj string |
| + ObjRegion int |
| } |
| func (f *filesDir) clone() *filesDir { |
| @@ -360,8 +365,15 @@ type box struct { |
| FailSettle bool // the app passes one readiness check, works, then fails |
| Nested bool // nested layout: children survive an agent crash |
| // region HA (two boxes per region, L18) |
| - Terminated bool // the cloud terminated the instance (H1): it never runs again and never returns; a Destroyed box that is not Terminated is stopped and may start again with its disk |
| - TerminatedAt int |
| + Terminated bool // the cloud terminated the instance (H1): it never runs again and never returns; a Destroyed box that is not Terminated is stopped and may start again with its disk |
| + TerminatedAt int |
| + // a relocation controller's durable record (hostexec, 1b-next Task 7): |
| + // the operation it belongs to, whether its scoped cleanup is still owed |
| + // (ground truth for INV-29), and the fault that makes the cleanup fail |
| + execRecord string |
| + cleanupPending bool |
| + cleanupFails bool |
| + FenceObservedAt int // the box-fences record's observed_at: when a worker first saw it terminated; 0 no record (rev 4) |
| Enrolled bool // the roster holds an active entry with its proven cloud identity (H11); a replacement box is enrolled automatically enrollDelay steps after it launches (H16, H17) |
| EnrollAt int |
| DeleteOnTermination bool // every volume the box had attached carried the flag while it ran (§5.9): decides only the automatic discharge of its park-local chores (H19), never a fence |
| @@ -826,6 +838,8 @@ type opState struct { |
| Attempts int // probe_attempts.<op.exec>: counted before each attempt, at most probeTries (ruling 19) |
| PreparedOpened string // prepared_opened: journaled by the admission that opened P (rev 12 S1) |
| Resolved bool // an operator's resolve (model ruling 13): the source is eligible as a target again, and an empty listing is accepted |
| + Observed []int // every fence.<box>.observed_at the operation consumed, kept through replacements (rev 4) |
| + Acks []int // exec_ack.<box>: the participants that acknowledged, durable (rev 4) |
| Abandoned []string // abandoned_prepared: every unopened P the operation replaced or dropped, parked at serving (1b-next ruling 27) |
| // journal |
| @@ -1222,6 +1236,8 @@ func (c *claim) clone() *claim { |
| n.Op.InstalledOn = append([]int(nil), c.Op.InstalledOn...) |
| n.Op.Discharged = append([]int(nil), c.Op.Discharged...) |
| n.Op.Abandoned = append([]string(nil), c.Op.Abandoned...) |
| + n.Op.Acks = append([]int(nil), c.Op.Acks...) |
| + n.Op.Observed = append([]int(nil), c.Op.Observed...) |
| if r := c.Op.Release; r != nil { |
| cp := *r |
| cp.Files = r.Files.clone() |