amadan
sim: region HA scenarios: every L18 case in a one-box and a two-box region, claim §11's extras, twenty witnesses for the relocation, fence and files guards, direct evidence for every bound, and reproductions of findings F1 to F3
Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
9 files changed,
+1389
−16
internal/sim/hostlife/background_test.go+1 −1internal/sim/hostlife/console_test.go+11 −1internal/sim/hostlife/protocol_test.go+1 −1internal/sim/hostlife/regionha_cases_test.go+717 −0internal/sim/hostlife/regionha_test.go+10 −1internal/sim/hostlife/regionha_witness_test.go+590 −5internal/sim/hostlife/twobox_test.go+8 −4internal/sim/hostlife/witness_test.go+44 −0internal/sim/hostlife/world_test.go+7 −3
diff --git a/internal/sim/hostlife/background_test.go b/internal/sim/hostlife/background_test.go| index 19c587478..91b0da4ae 100644 |
| --- a/internal/sim/hostlife/background_test.go |
| +++ b/internal/sim/hostlife/background_test.go |
| @@ -476,7 +476,7 @@ func (w *world) fault() { |
| func (w *world) replaceDestroyed() { |
| for r := 0; r < nRegions; r++ { |
| - for len(w.regionBoxes(r)) < w.perRegion { // the region's minimum (H5): the group launches replacements |
| + for len(w.regionBoxes(r)) < w.regionMin(r) { // the region's minimum (H5): the group launches replacements |
| w.nextID++ |
| nb := &box{ID: 100 + w.nextID, Region: r, HasKey: true, Enrolled: w.perRegion == 1, EnrollAt: w.now, DeleteOnTermination: true} |
| nb.forget() |
diff --git a/internal/sim/hostlife/console_test.go b/internal/sim/hostlife/console_test.go| index 57c09ad44..cf98bfc3a 100644 |
| --- a/internal/sim/hostlife/console_test.go |
| +++ b/internal/sim/hostlife/console_test.go |
| @@ -201,7 +201,7 @@ func (w *world) createSteps(p *consolePlan) bool { |
| if on("fence-etag") && w.h2Epoch != p.SeenVer { |
| return restart() // If-Match the epoch read at registration (If-None-Match: * when it was 0) |
| } |
| - w.h2 = liteHost{Inc: p.Inc, App: p.App, Kind: "creating", OpID: p.OpID, At: w.now} |
| + w.h2 = liteHost{Inc: p.Inc, App: p.App, Kind: "creating", OpID: p.OpID, At: w.now, Box: w.h2Box(p.App)} |
| w.h2Epoch++ // every write changes the claim's ETag |
| w.logf("create %s: second host claimed for app %s", p.OpID, p.App) |
| p.Step = 2 |
| @@ -383,6 +383,16 @@ func (w *world) userMove() { |
| w.moveTo(w.rng.Intn(nRegions)) // drawn only when a move is possible, as before rev 7.3 |
| } |
| +// h2Box is the executor the second host's create names (region HA §5.2): |
| +// 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 { |
| + return b.ID |
| + } |
| + return 0 |
| +} |
| + |
| // createExecutor is the box a create's step 4 hands op.exec to: the one |
| // its intent named, never another (region HA §5.2, claim P5-D2: recovery |
| // never substitutes a newly available box); nil while that box is gone. |
diff --git a/internal/sim/hostlife/protocol_test.go b/internal/sim/hostlife/protocol_test.go| index a0d45bd97..3ad1cc317 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") |
| + healthy := !(probe && b.FailApp && (c.Op.Kind == "landing" || c.Op.Kind == "relocating")) // 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 |
diff --git a/internal/sim/hostlife/regionha_cases_test.go b/internal/sim/hostlife/regionha_cases_test.go| new file mode 100644 |
| index 000000000..9a52eea4b |
| --- /dev/null |
| +++ b/internal/sim/hostlife/regionha_cases_test.go |
| @@ -0,0 +1,717 @@ |
| +package hostlife |
| + |
| +import "testing" |
| + |
| +// The cases region HA spec 1 §9 L18 and claim rev 6.30 §11 require of the |
| +// joint model, each in a one-box and in a two-box region (bothShapes): |
| +// region 0 holds box 0 alone, kept at one box by its group, or boxes 0 |
| +// and 3. Each is a direct test: it drives the case through the model's |
| +// own actors and asserts the outcome the spec names; the final oracle |
| +// (finish) checks every invariant. The witnesses (regionha_witness_test.go) |
| +// are the mutation evidence; these are the coverage. |
| + |
| +// serveAndPublish serves inc 1 of app A on box 0, runs it, and lets its |
| +// first files manifest land, so a later failover has the host's files |
| +// in S3 (finding F2 is the case where none landed). |
| +func (w *world) serveAndPublish(t *testing.T) *box { |
| + from := w.boxes[0] |
| + w.serve(from, 1, app0) |
| + w.running(t, from) |
| + w.published(t, from) |
| + return from |
| +} |
| + |
| +// failedOver drives the failover of the terminated executor dead until |
| +// the host serves again elsewhere, and returns the box it serves on: the |
| +// peer in a two-box region, the box the group launched in a one-box |
| +// region. |
| +func (w *world) failedOver(t *testing.T, dead *box) *box { |
| + if !w.reach(t, 3000, "serving after the failover", func() bool { |
| + c := w.claim |
| + return c.Op.Kind == "serving" && c.Op.Exec >= 0 && c.Op.Exec != dead.ID |
| + }, w.actAll(), w.recoveryPass, w.operator, w.wakeExec) { |
| + return nil |
| + } |
| + return w.execBox(w.claim) |
| +} |
| + |
| +// relocTarget drives until the relocation names a target with its pin, |
| +// and returns it (a one-box region's failover names the replacement the |
| +// group launched once it enrolls). |
| +func (w *world) relocTarget(t *testing.T) *box { |
| + if !w.reach(t, 400, "a target named and pinned", func() bool { |
| + c := w.claim |
| + return c.Op.Kind == "relocating" && c.Op.Tgt >= 0 && c.Op.Pin != nil |
| + }, w.actAll(), w.recoveryPass) { |
| + return nil |
| + } |
| + return w.boxByID(w.claim.Op.Tgt) |
| +} |
| + |
| +func TestL18CreateSpread(t *testing.T) { |
| + bothShapes(t, func(t *testing.T, w *world, boxes int) { |
| + w.serve(w.boxes[0], 1, app0) |
| + w.h2 = liteHost{} |
| + w.console = append(w.console, &consolePlan{Kind: "create", Host: "h2", App: app0, OpID: w.newID("cr"), Inc: 9}) |
| + w.reach(t, 50, "the second host of app A placed", func() bool { return w.h2.Kind == "serving" }, w.runConsole) |
| + want := 0 |
| + if boxes == 2 { |
| + want = 3 // the box running no instance of A (H12) |
| + } |
| + if w.h2.Box != want { |
| + t.Fatalf("the second instance of app A landed on box %d, want %d", w.h2.Box, want) |
| + } |
| + if boxes == 1 { |
| + return |
| + } |
| + w.h2 = liteHost{} |
| + w.console = append(w.console, &consolePlan{Kind: "create", Host: "h2", App: app1, OpID: w.newID("cr"), Inc: 10}) |
| + w.reach(t, 50, "the second host of app B placed", func() bool { return w.h2.Kind == "serving" }, w.runConsole) |
| + tie := 0 |
| + if tieHash(3) > tieHash(0) { |
| + tie = 3 |
| + } |
| + if w.h2.Box != tie { |
| + t.Fatalf("tie-break: app B landed on box %d, want the greater tieHash (%d)", w.h2.Box, tie) |
| + } |
| + }) |
| +} |
| + |
| +func TestL18RelocationByDrain(t *testing.T) { |
| + bothShapes(t, func(t *testing.T, w *world, boxes int) { |
| + from := w.serveAndPublish(t) |
| + wr := w.appWrite(from) |
| + id := w.timerOn(from) |
| + w.userRelocate() |
| + if boxes == 1 { |
| + // no eligible target: the drain never starts and the host keeps |
| + // serving where it is (spec §4) |
| + if c := w.claim; c.Op.Kind != "serving" || c.Op.Exec != from.ID { |
| + t.Fatalf("a drain started in a one-box region: %s", w.state()) |
| + } |
| + w.finish(t) |
| + return |
| + } |
| + to := w.peer() |
| + if c := w.claim; c.Op.Kind != "relocating" || c.Op.Tgt != to.ID { |
| + t.Fatalf("the drain did not start: %s", w.state()) |
| + } |
| + w.servingOn(t, to) |
| + if w.stats["admissions covered: released"] != 1 || w.stats["writes_lost declared"] != 0 { |
| + t.Errorf("released coverage: %d released, %d writes_lost (want 1 and 0)", w.stats["admissions covered: released"], w.stats["writes_lost declared"]) |
| + } |
| + w.finish(t) |
| + if !contains(to.DB.Log, wr) || !contains(to.Timers, id) && !w.delivered[id] { |
| + t.Errorf("the drain lost write %d or timer %d", wr, id) |
| + } |
| + }) |
| +} |
| + |
| +func TestL18TerminationDuringServing(t *testing.T) { |
| + bothShapes(t, func(t *testing.T, w *world, boxes int) { |
| + from := w.serveAndPublish(t) |
| + wr := w.appWrite(from) |
| + w.replicate(from) |
| + w.completeDue(true) |
| + w.terminate(from) |
| + to := w.failedOver(t, from) |
| + if to == nil { |
| + return |
| + } |
| + if boxes == 2 && to != w.peer() || boxes == 1 && to.ID < 100 { |
| + t.Errorf("served on box %d after the failover (one-box regions wait for the group's replacement)", to.ID) |
| + } |
| + w.finish(t) |
| + if to.DB == nil || !contains(to.DB.Log, wr) { |
| + t.Errorf("the failover lost the replicated write %d", wr) |
| + } |
| + }) |
| +} |
| + |
| +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) |
| + w.extraBox(0, spareID()) |
| + var to *box |
| + if boxes == 2 { |
| + w.drainTo(t, nil) |
| + to = w.boxByID(w.claim.Op.Tgt) |
| + } else { |
| + w.terminate(from) |
| + to = w.relocTarget(t) |
| + } |
| + if to == nil || !w.reach(t, 1500, "the probe runs on the target", func() bool { return preparedOpened(w.claim) && hasMain(to) }, w.actAll(), w.recoveryPass, func() { w.wake(to) }) { |
| + return |
| + } |
| + wr := w.appWrite(to) |
| + w.replicate(to) |
| + w.completeDue(true) // the target's write is in P's remote before it dies |
| + w.terminate(to) |
| + next := w.failedOver(t, to) |
| + w.finish(t) |
| + if next == nil || next.DB == nil || !contains(next.DB.Log, wr) { |
| + t.Fatalf("the nested failover lost the target's replicated write %d", wr) |
| + } |
| + if w.stats["nested failover after P was admitted"] != 1 { |
| + t.Fatalf("no nested failover: %v", w.stats) |
| + } |
| + }) |
| +} |
| + |
| +func TestL18StaleEdgesFile(t *testing.T) { |
| + bothShapes(t, func(t *testing.T, w *world, boxes int) { |
| + from := w.serveAndPublish(t) |
| + if boxes == 1 { |
| + // a one-box region's former executor is gone: a request through |
| + // its stale edges file reaches nothing |
| + w.terminate(from) |
| + w.failedOver(t, from) |
| + w.drive(30, never, func() { w.reconcile(from); w.wake(from) }) |
| + if hasMain(from) { |
| + t.Fatalf("the terminated box ran the host") |
| + } |
| + w.finish(t) |
| + return |
| + } |
| + to := w.peer() |
| + w.drainTo(t, to) |
| + w.servingOn(t, to) |
| + if from.Row == nil || from.Row.Status == "ready" { |
| + t.Fatalf("the former executor's row is not held: %+v", from.Row) |
| + } |
| + w.drive(30, never, func() { w.reconcile(from); w.wake(from) }) |
| + if hasMain(from) { |
| + t.Fatalf("a request through the stale edges file started the host on the former executor") |
| + } |
| + w.finish(t) |
| + }) |
| +} |
| + |
| +func TestL18UnenrolledReference(t *testing.T) { |
| + bothShapes(t, func(t *testing.T, w *world, boxes int) { |
| + from := w.serveAndPublish(t) |
| + if p := w.peer(); p != nil { |
| + p.HasKey = false // the region's other box may work, never take the host (R9) |
| + } |
| + w.terminate(from) |
| + w.now += replaceDelay |
| + w.launchReplacements() |
| + nb := w.boxes[len(w.boxes)-1] |
| + if nb.Region != 0 || nb.Enrolled { |
| + t.Fatalf("no unenrolled replacement in region 0: %+v", nb) |
| + } |
| + nb.EnrollAt = w.now + 10*enrollDelay // its confirmation is slow |
| + w.drive(3*enrollDelay, never, w.actAll(), w.recoveryPass) |
| + c := w.claim |
| + if c.Op.Exec == nb.ID || c.Op.Tgt == nb.ID { |
| + t.Fatalf("an unenrolled box was named: %s", w.state()) |
| + } |
| + if boxes == 2 && (c.Op.Kind != "relocating" || c.Op.Tgt != -1 || c.Op.Exec != -1) { |
| + // the peer fenced the executor; the failover waits at pinning |
| + t.Fatalf("the relocation did not wait at pinning with no target: %s", w.state()) |
| + } |
| + if boxes == 1 && c.Op.Kind != "serving" { |
| + // no enrolled worker of the region exists to write the fence: the |
| + // claim still names the dead box until the replacement enrolls |
| + t.Fatalf("a one-box region was fenced with no enrolled worker in it: %s", w.state()) |
| + } |
| + nb.EnrollAt = w.now - enrollDelay |
| + if to := w.failedOver(t, from); to != nb { |
| + t.Fatalf("served on %v, want the replacement %d once enrolled", to, nb.ID) |
| + } |
| + w.finish(t) |
| + }) |
| +} |
| + |
| +func TestL18AdverseVolume(t *testing.T) { |
| + bothShapes(t, func(t *testing.T, w *world, boxes int) { |
| + from := w.serveAndPublish(t) |
| + from.DeleteOnTermination = false |
| + if boxes == 2 { |
| + // a former executor that still owes its park-local |
| + w.drainTo(t, w.peer()) |
| + w.servingOn(t, w.peer()) |
| + if !w.owesLocal(w.claim, from) { |
| + t.Fatalf("the former executor owes no park-local: %s", w.state()) |
| + } |
| + } |
| + w.terminate(from) |
| + if boxes == 2 { |
| + w.reach(t, 60, "the former executor fenced", func() bool { return contains(w.claim.Lost, from.ID) }, w.act(w.peer())) |
| + if !w.owesLocal(w.claim, from) { |
| + t.Fatalf("the fence discharged the park-local without qualifying evidence: %s", w.state()) |
| + } |
| + } else { |
| + w.failedOver(t, from) // execution recovery proceeds (H19) |
| + } |
| + if w.stats["fence: park-local chores left open (volume evidence)"] == 0 || w.stats["fence: park-local chores discharged"] != 0 { |
| + t.Fatalf("the fence's discharge ignored the volume evidence: %v", w.stats) |
| + } |
| + w.finish(t) // the operator's destroyed-local declaration clears it |
| + }) |
| +} |
| + |
| +func TestL18CrashDuringInstallation(t *testing.T) { |
| + for _, boxes := range []int{1, 2} { |
| + for _, at := range []string{"installing", "installed", "probing"} { |
| + t.Run(map[int]string{1: "one-box region", 2: "two-box region"}[boxes]+"/"+at, func(t *testing.T) { |
| + w := regionWorld(boxes) |
| + from := w.serveAndPublish(t) |
| + w.timerOn(from) |
| + if boxes == 2 { |
| + w.drainTo(t, nil) |
| + } else { |
| + w.terminate(from) |
| + } |
| + w.relocPhase(t, at, w.actAll(), w.recoveryPass) |
| + to := w.boxByID(w.claim.Op.Tgt) |
| + w.drive(2, never, w.act(to)) // a step into the phase: a PUT issued, a files directory extracted |
| + w.crash(to) |
| + w.servingOn(t, to) |
| + w.finish(t) |
| + w.mustHold(t) |
| + }) |
| + } |
| + } |
| +} |
| + |
| +func TestL18LateFileUploads(t *testing.T) { |
| + bothShapes(t, func(t *testing.T, w *world, boxes int) { |
| + from := w.serveAndPublish(t) |
| + late := w.timerOn(from) |
| + loc := w.claim.Holder.Location |
| + w.holdKey(loc + "files/") |
| + w.publishFiles(from) // the manifest carrying the timer, held |
| + w.hold = nil |
| + w.terminate(from) |
| + to := w.failedOver(t, from) |
| + if to == nil { |
| + return |
| + } |
| + if contains(to.Timers, late) { |
| + t.Fatalf("the install applied a manifest that had not landed at the pin") |
| + } |
| + declared := false |
| + for _, a := range w.acks { |
| + if a.W == late && a.Exempt { |
| + declared = true |
| + } |
| + } |
| + if !declared { |
| + t.Fatalf("the timer the late manifest carried was not declared with the fence") |
| + } |
| + if n := w.completeHeld(loc + "files/"); n != 1 { |
| + t.Fatalf("held manifest PUTs completed: %d, want 1", n) |
| + } |
| + w.finish(t) |
| + }) |
| +} |
| + |
| +func TestL18LatePutAfterTermination(t *testing.T) { |
| + bothShapes(t, func(t *testing.T, w *world, boxes int) { |
| + from := w.serveAndPublish(t) |
| + late := w.appWrite(from) |
| + loc := w.claim.Holder.Location |
| + w.holdKey(loc) |
| + w.replicate(from) // the upload of the late write is held |
| + w.hold = nil |
| + w.terminate(from) |
| + to := w.failedOver(t, from) |
| + if to == nil { |
| + return |
| + } |
| + if contains(to.DB.Log, late) { |
| + t.Fatalf("the install restored a write whose upload had not landed at the pin") |
| + } |
| + if n := w.completeHeld(loc); n == 0 { |
| + t.Fatalf("no held upload to complete") |
| + } |
| + w.finish(t) // the late object lands in generation_from, read by nothing, parked |
| + }) |
| +} |
| + |
| +// ---------- claim §11's region HA witnesses beyond L18 (two-box) ---------- |
| + |
| +// TestRelocationStartRacesPurge: a worker read the serving claim, then |
| +// paused; a purge started meanwhile. A fresh start reads the purging |
| +// claim and refuses; no relocation runs over a purging host. |
| +func TestRelocationStartRacesPurge(t *testing.T) { |
| + w := twoBoxWitness() |
| + w.serve(w.boxes[0], 1, app0) |
| + w.userPurge() |
| + w.reach(t, 100, "the purge started", func() bool { return w.claim.Op.Kind == "purging" || w.admit[app0].Closed }, w.runConsole) |
| + w.userRelocate() |
| + if w.claim.Op.Kind == "relocating" { |
| + t.Fatalf("a relocation started over a purging host: %s", w.state()) |
| + } |
| + w.finish(t) |
| + w.mustHold(t) |
| +} |
| + |
| +// TestEmptyDatabaseDrain: a created host whose database never committed |
| +// (nothing replicated) but has files and a timer is drained: the release |
| +// flushes at 0, the pin is an evidenced empty one, and the files and the |
| +// timer arrive through the manifests. |
| +func TestEmptyDatabaseDrain(t *testing.T) { |
| + w := twoBoxWitness() |
| + w.console = append(w.console, &consolePlan{Kind: "create", Host: "h", App: app0, OpID: w.newID("cr"), Inc: 1, Region: 0}) |
| + w.reach(t, 100, "created", func() bool { c := w.claim; return c != nil && c.Holder != nil && c.Op.Kind == "serving" }, w.runConsole, w.recoveryPass) |
| + from := w.execBox(w.claim) |
| + w.reach(t, 100, "the host runs", func() bool { return hasMain(from) }, w.actAll(), func() { w.wake(from) }) |
| + id := w.timerOn(from) |
| + key := from.Files.Key |
| + w.published(t, from) |
| + w.drainTo(t, nil) |
| + to := w.boxByID(w.claim.Op.Tgt) |
| + w.servingOn(t, to) |
| + w.finish(t) |
| + w.mustHold(t) |
| + if !contains(to.Timers, id) && !w.delivered[id] { |
| + t.Fatalf("the timer did not survive the empty-database drain") |
| + } |
| + if to.Files == nil || to.Files.Key != key { |
| + t.Fatalf("the files did not survive the empty-database drain: %+v", to.Files) |
| + } |
| +} |
| + |
| +// TestReleasedThenFailedProbe: the drain's first probe admission is |
| +// covered released; the target cannot run the app, fails its probe, |
| +// releases, and the nested relocation's admission is covered by the |
| +// failed target's own release: nothing is declared. |
| +func TestReleasedThenFailedProbe(t *testing.T) { |
| + w := twoBoxWitness() |
| + from, to := w.boxes[0], w.boxes[3] |
| + to.FailApp = true |
| + w.serve(from, 1, app0) |
| + w.running(t, from) |
| + w.drainTo(t, to) |
| + third := w.extraBox(0, 30) |
| + w.servingOn(t, third) |
| + w.finish(t) |
| + w.mustHold(t) // nothing acknowledged is lost: each later attempt declares its predecessor's session, which acknowledged nothing |
| + if w.stats["admissions covered: released"] < 1 { |
| + t.Fatalf("the drain's first probe admission was not covered released: %v", w.stats) |
| + } |
| +} |
| + |
| +// TestStuckAfterTwoReplacements (reloc-replacement-cap, an operator |
| +// bound): three targets die at installing; the third death is the |
| +// exhausted fence, the operation is stuck, and the operator's resolve |
| +// replays it onto a spare. |
| +func TestStuckAfterTwoReplacements(t *testing.T) { |
| + w := twoBoxWitness() |
| + from := w.boxes[0] |
| + w.serve(from, 1, app0) |
| + w.running(t, from) |
| + w.extraBox(0, 30) |
| + w.extraBox(0, 31) |
| + w.drainTo(t, nil) |
| + for i := 0; i < 3; i++ { |
| + if !w.reach(t, 1500, "a target installing", func() bool { |
| + c := w.claim |
| + return c.Op.Kind == "relocating" && c.Op.Phase == "installing" && c.Op.Stuck == "" |
| + }, w.act(w.liveBoxes()...), w.recoveryPass) { |
| + t.Fatalf("target %d never installed: %s", i, w.state()) |
| + } |
| + x := w.boxByID(w.claim.Op.Exec) |
| + w.terminate(x) |
| + w.reach(t, 100, "fenced", func() bool { return contains(w.claim.Lost, x.ID) }, w.act(w.liveBoxes()...)) |
| + } |
| + if w.claim.Op.Stuck == "" { |
| + t.Fatalf("a third loss did not make the operation stuck: %s", w.state()) |
| + } |
| + w.extraBox(0, spareID()) |
| + w.servingOn(t, nil) // the operator resolves it |
| + w.finish(t) |
| + w.mustHold(t) |
| + if w.stats["operator resolved a stuck relocation"] != 1 { |
| + t.Fatalf("the operator did not resolve it: %v", w.stats) |
| + } |
| +} |
| + |
| +// TestReleaseStopsAnEscapedDescendant (L10): a process that escaped the |
| +// cgroup is stopped with the whole tree before release step 1 passes |
| +// (the model's evidence-whole-tree: the cleanup-only reopen kills the |
| +// cgroup and every identified stray); the source's release is journaled |
| +// only once nothing of the host runs on it. |
| +func TestReleaseStopsAnEscapedDescendant(t *testing.T) { |
| + w := twoBoxWitness() |
| + from, to := w.boxes[0], w.boxes[3] |
| + w.serve(from, 1, app0) |
| + w.running(t, from) |
| + from.Procs = append(from.Procs, &proc{Main: false, Strict: false, Inc: 1, Box: from.ID, Session: w.claim.Holder.Session}) |
| + w.drainTo(t, to) |
| + if !w.reach(t, 300, "the source's release journaled", func() bool { return w.claim.Op.Release != nil }, w.act(from, to), w.recoveryPass) { |
| + w.mustHold(t) |
| + } |
| + if len(from.Procs) != 0 { |
| + t.Fatalf("the release was journaled with %d processes of the host alive on the source", len(from.Procs)) |
| + } |
| + w.servingOn(t, to) |
| + w.finish(t) |
| + w.mustHold(t) |
| +} |
| + |
| +// ---------- the bounds: direct evidence for the rules no invariant catches alone ---------- |
| + |
| +// TestDrainRefusedForANeverWokenHost (reloc-drain-needs-writer, ruling |
| +// 11): a host with no writer session is never drained; its failover |
| +// relocates it. |
| +func TestDrainRefusedForANeverWokenHost(t *testing.T) { |
| + w := twoBoxWitness() |
| + w.serve(w.boxes[0], 1, app0) |
| + w.cas(w.claim, func(n *claim) bool { n.Holder.Session = 0; return true }) |
| + w.userRelocate() |
| + if w.claim.Op.Kind != "serving" || w.stats["drain refused: the host never had a writer"] != 1 { |
| + t.Fatalf("a never-woken host was drained: %s", w.state()) |
| + } |
| +} |
| + |
| +// TestReplacedTargetAcknowledgesBeforePinning (reloc-ack-before-pinning): |
| +// the target is replaced in releasing; the operation leaves releasing |
| +// only once the replacement's execution lease is current. |
| +func TestReplacedTargetAcknowledgesBeforePinning(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) |
| + w.relocPhase(t, "releasing", w.act(from, to), w.recoveryPass) |
| + w.terminate(to) |
| + w.reach(t, 100, "the target replaced in releasing", func() bool { return w.claim.Op.Tgt == spare.ID }, w.act(from)) |
| + // the spare never acts: no lease, so the operation must stay in releasing |
| + w.drive(40, never, w.act(from)) |
| + if c := w.claim; c.Op.Phase != "releasing" || w.stats["pin after release: waits for the acknowledgements"] == 0 { |
| + t.Fatalf("left releasing without the replacement's acknowledgement: %s", w.state()) |
| + } |
| + w.servingOn(t, spare) |
| + w.finish(t) |
| + w.mustHold(t) |
| +} |
| + |
| +// TestProbeAttemptsCountedBeforeTheyAreMade (reloc-probe-attempts, |
| +// ruling 19): an agent that crashes in every attempt never buys a |
| +// fourth; the target goes to probe-failed after three. |
| +func TestProbeAttemptsCountedBeforeTheyAreMade(t *testing.T) { |
| + w := twoBoxWitness() |
| + from, to := w.boxes[0], w.boxes[3] |
| + w.serve(from, 1, app0) |
| + w.running(t, from) |
| + w.drainTo(t, to) |
| + w.relocPhase(t, "probing", w.act(from, to), w.recoveryPass) |
| + to.envUnreadyFor = 1000 // the launch environment never gets ready: each attempt is still starting when the agent dies |
| + before := w.stats["admissions: cold"] |
| + for i := 0; i < 8 && w.claim.Op.Phase == "probing"; i++ { |
| + w.drive(3, func() bool { return to.open != nil }, w.act(to)) |
| + w.crash(to) // each attempt dies before its probe |
| + } |
| + if n := w.stats["admissions: cold"] - before; n > probeTries || w.claim.Op.Phase == "probing" { |
| + t.Fatalf("%d attempts admitted, phase %s; want at most %d, then probe-failed", n, w.claim.Op.Phase, probeTries) |
| + } |
| +} |
| + |
| +// TestCreateNamesItsExecutorOnce (create-choice-once, claim P5-D2, |
| +// P5-D6): a create names its executor in the intent; when that box is |
| +// gone before the create completes, recovery cancels the create and |
| +// never substitutes the region's other box. |
| +func TestCreateNamesItsExecutorOnce(t *testing.T) { |
| + w := twoBoxWitness() |
| + p := &consolePlan{Kind: "create", Host: "h", App: app0, OpID: w.newID("cr"), Inc: 1, Region: 0} |
| + w.admit[app0].Reg[p.OpID] = regEntry{Until: w.now + 1000} |
| + w.console = append(w.console, p) |
| + w.reach(t, 50, "the create claimed the host", func() bool { c := w.claim; return c != nil && c.Op.Kind == "creating" }, w.runConsole) |
| + chosen := w.boxByID(w.claim.Op.NewBox) |
| + w.terminate(chosen) |
| + w.drive(200, func() bool { c := w.claim; return c == nil || c.Holder == nil || c.Op.Kind == "serving" }, w.runConsole, w.recoveryPass) |
| + if c := w.claim; c != nil && c.Holder != nil && c.Op.Kind == "serving" { |
| + t.Fatalf("the create substituted box %d for its chosen box %d", c.Op.Exec, chosen.ID) |
| + } |
| + if w.stats["create cancelled: its box is gone"] != 1 { |
| + t.Fatalf("the create was not cancelled: %v", w.stats) |
| + } |
| +} |
| + |
| +// TestStoppedBoxNeverFenced (fence-terminated-only): a stopped executor |
| +// is never fenced; when it starts again with its disk, it serves. |
| +func TestStoppedBoxNeverFenced(t *testing.T) { |
| + w := twoBoxWitness() |
| + from, to := w.boxes[0], w.boxes[3] |
| + w.serve(from, 1, app0) |
| + w.running(t, from) |
| + from.Destroyed, from.Procs = true, nil // stopped, not terminated |
| + w.drive(100, never, w.act(to), w.recoveryPass) |
| + if contains(w.claim.Lost, from.ID) || w.claim.Op.Kind != "serving" { |
| + t.Fatalf("a stopped box was fenced: %s", w.state()) |
| + } |
| + from.Destroyed = false |
| + w.running(t, from) |
| + w.finish(t) |
| + w.mustHold(t) |
| +} |
| + |
| +// TestRelocationStartGuardRefuses (reloc-start-guard): a whole-location |
| +// chore in the region refuses the start; a park-generation does not. |
| +func TestRelocationStartGuardRefuses(t *testing.T) { |
| + w := twoBoxWitness() |
| + w.serve(w.boxes[0], 1, app0) |
| + w.claim.Obl = append(w.claim.Obl, obligation{ID: "pg", Op: "old", Kind: "park-generation", Region: 0, Box: -1, Prefix: w.claim.Holder.Location, Ret: "old"}) |
| + if !w.relocationStartAllowed(w.claim, w.boxes[0], w.boxes[3]) { |
| + t.Fatalf("a park-generation refused the start (L11)") |
| + } |
| + w.claim.Obl = append(w.claim.Obl, obligation{ID: "pr", Op: "old", Kind: "park-replica", Region: 0, Box: -1, Prefix: w.claim.Holder.Location}) |
| + if w.relocationStartAllowed(w.claim, w.boxes[0], w.boxes[3]) { |
| + t.Fatalf("a park-replica in the region did not refuse the start (CC11)") |
| + } |
| +} |
| + |
| +// TestOnlyTheExecutorInstalls (reloc-exec-only-installs, HA2): through a |
| +// drain, no box but op.exec writes P or makes a local install. |
| +func TestOnlyTheExecutorInstalls(t *testing.T) { |
| + w := twoBoxWitness() |
| + from, to := w.boxes[0], w.boxes[3] |
| + w.serve(from, 1, app0) |
| + w.running(t, from) |
| + w.drainTo(t, to) |
| + w.servingOn(t, to) |
| + if from.receipt != nil || from.Files != nil && from.Files.Gen != "" && from.Files.Gen == w.claim.Holder.Gen { |
| + t.Fatalf("the source made a local install of P") |
| + } |
| +} |
| + |
| +// ---------- findings: hazards the model shows in 1b-next rev 16 ---------- |
| + |
| +// TestFailoverBeforeTheFirstManifest (finding F2): a host none of whose |
| +// files manifests has landed is terminated; 1b-next pins its files as |
| +// empty (StorePinner: "Empty for a host that never published files"), so |
| +// the install mints a fresh instance.key over data sealed with the old |
| +// one. The model reproduces it (INV-4); the sweep never terminates such |
| +// an executor (model ruling 17). |
| +func TestFailoverBeforeTheFirstManifest(t *testing.T) { |
| + w := twoBoxWitness() |
| + from := w.boxes[0] |
| + w.serve(from, 1, app0) |
| + loc := w.claim.Holder.Location |
| + w.holdKey(loc + "files/") // the first manifest's PUT has not landed |
| + w.running(t, from) |
| + w.hold = nil |
| + w.terminate(from) |
| + w.drive(400, func() bool { |
| + return len(w.violations) > 0 || w.claim.Op.Kind == "serving" && w.claim.Op.Exec != from.ID |
| + }, w.actAll(), w.recoveryPass, w.operator, w.wakeExec) |
| + if len(w.violations) == 0 || !contains([]int{4}, invNumber(w.violations[0])) { |
| + t.Fatalf("finding F2 no longer reproduces (want INV-4): %v", w.violations) |
| + } |
| +} |
| + |
| +// TestProbeFailedInATwoBoxRegion (finding F1): a drain's target cannot |
| +// run the app; its probe fails and it releases. 1b-next's worker looks |
| +// for a spare with no bound (Worker.Step: "no eligible box yet: a later |
| +// pass may find one"), and replaceTargetSlot refuses the source, so in a |
| +// two-box region the host serves nowhere until an operator acts. The |
| +// model marks it stuck after the release deadline (model ruling 14) and |
| +// the operator's resolve returns it to the source (model ruling 13). |
| +func TestProbeFailedInATwoBoxRegion(t *testing.T) { |
| + w := twoBoxWitness() |
| + from, to := w.boxes[0], w.boxes[3] |
| + to.FailApp = true |
| + w.serve(from, 1, app0) |
| + w.running(t, from) |
| + w.drainTo(t, to) |
| + w.reach(t, 1500, "stuck with no spare", func() bool { return w.claim.Op.Stuck == "no eligible box for the nested relocation" }, w.actAll(), w.recoveryPass) |
| + w.servingOn(t, from) |
| + w.finish(t) |
| + w.mustHold(t) |
| +} |
| + |
| +// TestAbandonedPreparedGenerationParked (finding F3): a target replaced |
| +// at installing leaves its partial build of P behind (the replacement |
| +// builds a fresh P'); 1b-next's CompleteRelocation queues park-local |
| +// chores only. The model parks every unopened P in the serving CAS |
| +// (model ruling 16); without it INV-10 finds P's objects at the release. |
| +func TestAbandonedPreparedGenerationParked(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) |
| + third := w.extraBox(0, 30) |
| + w.reach(t, 1500, "P's snapshot written", func() bool { c := w.claim; return c.Op.Phase == "installing" && c.Op.BaseKey != "" }, w.act(from, to), w.recoveryPass) |
| + p := w.claim.Op.Prepared |
| + w.terminate(to) |
| + w.reach(t, 100, "replaced", func() bool { return w.claim.Op.Exec == third.ID }, w.act(third)) |
| + if w.claim.Op.Prepared == p { |
| + t.Fatalf("the replacement at installing kept P") |
| + } |
| + w.servingOn(t, third) |
| + if w.stats["relocation: abandoned prepared generation parked"] == 0 { |
| + t.Fatalf("the abandoned P %q was not parked at serving", p) |
| + } |
| + w.finish(t) |
| + w.mustHold(t) |
| +} |
| + |
| +// invNumber is the n of the first "INV-n" in a violation, 0 if none. |
| +func invNumber(v string) int { |
| + for i := 0; i+4 < len(v); i++ { |
| + if v[i:i+4] == "INV-" { |
| + n := 0 |
| + for j := i + 4; j < len(v) && v[j] >= '0' && v[j] <= '9'; j++ { |
| + n = n*10 + int(v[j]-'0') |
| + } |
| + return n |
| + } |
| + } |
| + return 0 |
| +} |
| + |
| +// mustHold fails the test, with the trace, if any invariant was violated. |
| +func (w *world) mustHold(t *testing.T) { |
| + t.Helper() |
| + if len(w.violations) > 0 { |
| + dump(t, w) |
| + t.Fatalf("%s", w.violations[0]) |
| + } |
| +} |
diff --git a/internal/sim/hostlife/regionha_test.go b/internal/sim/hostlife/regionha_test.go| index 2884f0524..47effbedf 100644 |
| --- a/internal/sim/hostlife/regionha_test.go |
| +++ b/internal/sim/hostlife/regionha_test.go |
| @@ -1100,7 +1100,7 @@ func (w *world) terminate(b *box) { |
| // sweeps only: a witness world's quiet source draws nothing). |
| func (w *world) launchReplacements() { |
| for r := 0; r < nRegions; r++ { |
| - if len(w.regionBoxes(r)) >= w.perRegion { |
| + if len(w.regionBoxes(r)) >= w.regionMin(r) { |
| continue |
| } |
| last := 0 |
| @@ -1691,3 +1691,12 @@ func (w *world) pinnedManifest(c *claim) *blob { |
| } |
| return nil |
| } |
| + |
| +// regionMin is the region's minimum box count (H5): the shape's, or one |
| +// for a witness's one-box region. |
| +func (w *world) regionMin(r int) int { |
| + if w.oneBoxRegion[r] { |
| + return 1 |
| + } |
| + return w.perRegion |
| +} |
diff --git a/internal/sim/hostlife/regionha_witness_test.go b/internal/sim/hostlife/regionha_witness_test.go| index 790220b5d..2b9079246 100644 |
| --- a/internal/sim/hostlife/regionha_witness_test.go |
| +++ b/internal/sim/hostlife/regionha_witness_test.go |
| @@ -62,8 +62,8 @@ func TestUnenrolledReferenceNeverChosen(t *testing.T) { |
| w := twoBoxWitness() |
| from, peer := w.boxes[0], w.boxes[3] |
| w.serve(from, 1, app0) |
| - w.publishFiles(from) // its files are in S3 before it dies (Task 4: a dead box's disk is never read) |
| - w.completeDue(true) |
| + w.reach(t, 50, "the host runs on box 0", func() bool { return hasMain(from) }, w.actAll(), func() { w.wake(from) }) |
| + w.published(t, from) |
| peer.HasKey = false |
| w.terminate(from) |
| w.now += replaceDelay |
| @@ -72,16 +72,17 @@ func TestUnenrolledReferenceNeverChosen(t *testing.T) { |
| if nb.Region != 0 || nb.Enrolled { |
| t.Fatalf("no unenrolled replacement in region 0: %+v", nb) |
| } |
| + nb.EnrollAt = w.now + 10*enrollDelay // its confirmation is slow |
| w.reach(t, 100, "the executor fenced by the peer", func() bool { |
| return contains(w.claim.Lost, from.ID) && w.claim.Op.Kind == "relocating" |
| }, w.act(peer), w.recoveryPass) |
| - // the witness schedule never runs enrollStep: nb stays unenrolled, and |
| - // the relocation must wait at pinning with no target |
| + // nb stays unenrolled, and the relocation must wait at pinning with no |
| + // target |
| w.drive(enrollDelay, func() bool { return false }, w.actAll(), w.recoveryPass) |
| if c := w.claim; c.Op.Kind != "relocating" || c.Op.Tgt != -1 || c.Op.Exec != -1 { |
| t.Fatalf("an unenrolled box was named, or the relocation moved on: %s", w.state()) |
| } |
| - w.now += enrollDelay |
| + nb.EnrollAt = w.now - enrollDelay |
| w.enrollStep() |
| if !nb.Enrolled { |
| t.Fatalf("the replacement did not enroll") |
| @@ -166,3 +167,587 @@ func TestLateFileUploads(t *testing.T) { |
| t.Fatalf("the late manifest was never parked: %v", r) |
| } |
| } |
| + |
| +// ---------- Task 5: the scenarios ---------- |
| + |
| +// twoBox turns a witness world into the two-box shape. |
| +func (w *world) twoBox() { |
| + w.perRegion = 2 |
| + for r := 0; r < nRegions; r++ { |
| + w.addBox(r) |
| + } |
| +} |
| + |
| +// regionWorld is a witness world with region HA on (the two-box shape's |
| +// rules, its publisher and its group) whose region 0 holds boxes boxes: |
| +// 2 is a two-box region (boxes 0 and 3); 1 is a one-box region (box 0 |
| +// alone, kept at one box by its group, H5's minimum being per region). |
| +// Regions 1 and 2 have two boxes either way. |
| +func regionWorld(boxes int) *world { |
| + w := newWitness() |
| + w.perRegion = 2 |
| + for r := 0; r < nRegions; r++ { |
| + if r == 0 && boxes == 1 { |
| + w.oneBoxRegion[0] = true |
| + continue |
| + } |
| + w.addBox(r) |
| + } |
| + return w |
| +} |
| + |
| +// bothShapes runs an L18 case in a one-box and in a two-box region. |
| +func bothShapes(t *testing.T, f func(t *testing.T, w *world, boxes int)) { |
| + for _, n := range []int{1, 2} { |
| + n := n |
| + t.Run(map[int]string{1: "one-box region", 2: "two-box region"}[n], func(t *testing.T) { |
| + w := regionWorld(n) |
| + f(t, w, n) |
| + if len(w.violations) > 0 { |
| + dump(t, w) |
| + t.Fatalf("%s", w.violations[0]) |
| + } |
| + }) |
| + } |
| +} |
| + |
| +// peer is region 0's second box, nil in a one-box region. |
| +func (w *world) peer() *box { |
| + for _, b := range w.boxes { |
| + if b.ID == nRegions && !b.Destroyed { |
| + return b |
| + } |
| + } |
| + return nil |
| +} |
| + |
| +// extraBox enrolls another box in region r with the given id (a spare |
| +// for the nested scenarios). |
| +func (w *world) extraBox(r, id int) *box { |
| + b := &box{ID: id, Region: r, HasKey: true, Enrolled: true, DeleteOnTermination: true} |
| + b.forget() |
| + w.boxes = append(w.boxes, b) |
| + return b |
| +} |
| + |
| +// running drives the serving host until it runs on b. |
| +func (w *world) running(t *testing.T, b *box) { |
| + w.reach(t, 60, "the host runs", func() bool { return hasMain(b) }, w.actAll(), func() { w.wake(b) }) |
| +} |
| + |
| +// drainTo starts a drain of the serving host and fails the test unless |
| +// it named to (any target when to is nil). |
| +func (w *world) drainTo(t *testing.T, to *box) { |
| + w.userRelocate() |
| + if c := w.claim; c.Op.Kind != "relocating" || to != nil && c.Op.Tgt != to.ID { |
| + t.Fatalf("witness: the drain did not start (to %v): %s", to, w.state()) |
| + } |
| +} |
| + |
| +// relocPhase drives until the relocation is in phase p (or beyond it, by |
| +// the table's order), with the actors given. |
| +func (w *world) relocPhase(t *testing.T, p string, actors ...func()) bool { |
| + order := []string{"starting", "releasing", "pinning", "installing", "installed", "probing", "probed", "opened"} |
| + at := func(x string) int { |
| + for i, o := range order { |
| + if o == x { |
| + return i |
| + } |
| + } |
| + return -1 |
| + } |
| + return w.reach(t, 1500, "relocation at "+p, func() bool { |
| + c := w.claim |
| + return c.Op.Kind == "relocating" && at(c.Op.Phase) >= at(p) || c.Op.Kind == "serving" && p == "serving" |
| + }, actors...) |
| +} |
| + |
| +// servingOn drives until the host serves on b (on any box, when b is |
| +// nil), with every actor the at-rest model has. |
| +func (w *world) servingOn(t *testing.T, b *box) bool { |
| + return w.reach(t, 3000, "serving on the new executor", func() bool { |
| + c := w.claim |
| + return c.Op.Kind == "serving" && (b == nil && c.Op.Exec >= 0 || b != nil && c.Op.Exec == b.ID) |
| + }, w.actAll(), w.recoveryPass, w.operator, w.wakeExec) |
| +} |
| + |
| +// wakeExec wakes the executor, whichever box it is. |
| +func (w *world) wakeExec() { |
| + if e := w.execBox(w.claim); e != nil { |
| + w.wake(e) |
| + } |
| +} |
| + |
| +// timerOn registers an acknowledged timer on b's running host. |
| +func (w *world) timerOn(b *box) int { |
| + w.nextW++ |
| + b.Timers = append(b.Timers, w.nextW) |
| + sess, gen := w.sessionOf(b) |
| + w.acks = append(w.acks, ack{W: w.nextW, Inc: w.claim.Holder.Inc, Box: b.ID, Session: sess, Gen: gen, At: w.now, Kind: "timer"}) |
| + return w.nextW |
| +} |
| + |
| +// spareID is an id for an extra box of region 0 whose tieHash beats box |
| +// 0's, so choose() prefers it to the source. |
| +func spareID() int { |
| + for id := 40; ; id++ { |
| + if tieHash(id) > tieHash(0) { |
| + return id |
| + } |
| + } |
| +} |
| + |
| +func never() bool { return false } |
| + |
| +// published drives until a manifest of b's host has landed (the files |
| +// publisher runs in every two-box tick): a failover of a host none of |
| +// whose manifests landed is finding F2's, not the scenario's. |
| +func (w *world) published(t *testing.T, b *box) bool { |
| + return w.reach(t, 60, "the host's first manifest landed", func() bool { |
| + _, _, _, _, m := w.newestManifest(b.Region, w.claim.Holder.Location, w.claim.Holder.Gen) |
| + return m != nil |
| + }, w.act(b), func() { w.completeDue(true) }) |
| +} |
| + |
| +// ---------- the witnesses (one per safety guard) ---------- |
| + |
| +func wRelocReleaseFirst(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.drainTo(t, to) |
| + // only the target's worker runs while the source should be releasing: |
| + // with the rule it waits for the release; without it, it pins and |
| + // installs while the source still runs the host |
| + w.drive(12, never, w.act(to)) |
| + w.servingOn(t, to) |
| + w.finish(t) |
| +} |
| + |
| +func wRelocInstallReceipt(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.drainTo(t, to) |
| + third := w.extraBox(0, 30) |
| + if !w.reach(t, 1500, "the target's receipt", func() bool { |
| + c := w.claim |
| + return c.Op.Kind == "relocating" && c.Op.Phase == "installed" && c.Op.Receipt != nil && c.Op.Receipt.Box == to.ID |
| + }, w.act(from, to), w.recoveryPass) { |
| + return |
| + } |
| + w.terminate(to) |
| + w.servingOn(t, third) |
| + w.finish(t) |
| +} |
| + |
| +func wRelocNoReinstall(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.drainTo(t, to) |
| + if !w.reach(t, 1500, "the probe runs on the target", func() bool { |
| + return preparedOpened(w.claim) && hasMain(to) |
| + }, w.act(from, to), w.recoveryPass) { |
| + return |
| + } |
| + w.timerOn(to) |
| + w.crash(to) |
| + w.servingOn(t, to) |
| + w.finish(t) |
| +} |
| + |
| +func wRelocReleasedCoverage(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.appWrite(from) |
| + loc := w.claim.Holder.Location |
| + w.holdKey(loc) // every upload of the executor is held |
| + w.replicate(from) |
| + w.hold = nil |
| + w.terminate(from) |
| + w.servingOn(t, to) |
| + w.completeHeld(loc) // the dead box's upload lands late, after the pin |
| + w.finish(t) |
| +} |
| + |
| +func wRelocSourceLoss(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.appWrite(from) |
| + loc := w.claim.Holder.Location |
| + w.holdKey(loc) // the flush and the final manifest are held: no release |
| + w.drainTo(t, to) |
| + w.relocPhase(t, "releasing", w.act(from, to), w.recoveryPass) |
| + w.drive(20, never, w.act(from, to)) |
| + if w.claim.Op.Release != nil { |
| + t.Fatalf("witness: the release was journaled while its uploads were held") |
| + } |
| + w.hold = nil |
| + w.terminate(from) |
| + w.servingOn(t, to) |
| + w.completeHeld(loc) |
| + w.finish(t) |
| +} |
| + |
| +func wRelocRowCases(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.drainTo(t, to) |
| + if !w.reach(t, 1500, "the source released", func() bool { |
| + c := w.claim |
| + return c.Op.Kind == "relocating" && c.Op.Release != nil && c.Op.Release.Box == from.ID && !hasMain(from) |
| + }, w.act(from, to), w.recoveryPass) { |
| + return |
| + } |
| + // a paused duplicate of the source's earlier open lands now: its row |
| + // is ready again while its admission fence is closed. Reconcile |
| + // decides the row; a request reaches the box through its stale edges |
| + // file |
| + from.Row.Status, from.Row.HoldOp = "ready", "" |
| + w.drive(40, never, func() { |
| + w.reconcile(from) |
| + w.wake(from) |
| + }, w.act(to), w.recoveryPass, func() { w.wake(to) }) |
| + w.servingOn(t, to) |
| + w.finish(t) |
| +} |
| + |
| +func wFenceDischargeQualified(t *testing.T, w *world) { |
| + w.twoBox() |
| + from, to := w.boxes[0], w.boxes[3] |
| + from.DeleteOnTermination = false |
| + w.serve(from, 1, app0) |
| + w.running(t, from) |
| + w.drainTo(t, to) |
| + w.servingOn(t, to) |
| + if !w.owesLocal(w.claim, from) { |
| + t.Fatalf("witness: the former executor owes no park-local: %s", w.state()) |
| + } |
| + w.terminate(from) |
| + w.reach(t, 60, "the former executor fenced", func() bool { return contains(w.claim.Lost, from.ID) }, w.act(to)) |
| + w.finish(t) |
| +} |
| + |
| +func wFenceDeclaresTimers(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.publishFiles(from) |
| + w.completeDue(true) |
| + w.holdKey(w.claim.Holder.Location + "files/") // the manifest that would carry the timer never lands |
| + w.timerOn(from) |
| + w.publishFiles(from) |
| + w.hold = nil |
| + w.terminate(from) |
| + w.servingOn(t, to) |
| + w.completeHeld(w.claim.Holder.Location + "files/") // it lands after the pin: a version nothing reads |
| + w.finish(t) |
| +} |
| + |
| +func wRelocEnrolledOnly(t *testing.T, w *world) { |
| + w.twoBox() |
| + from, peer := w.boxes[0], w.boxes[3] |
| + w.serve(from, 1, app0) |
| + w.published(t, from) |
| + peer.HasKey = false |
| + w.terminate(from) |
| + w.reach(t, 100, "the executor fenced", func() bool { return contains(w.claim.Lost, from.ID) }, w.act(peer), w.recoveryPass) |
| + // the replacement launches unenrolled; under the mutation it is named |
| + // before it enrolls (INV-27) |
| + w.servingOn(t, nil) |
| + w.finish(t) |
| +} |
| + |
| +func wFilesLiveSet(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.timerOn(from) |
| + if !w.reach(t, 30, "the origin's manifest landed", func() bool { |
| + _, _, _, _, m := w.newestManifest(0, w.claim.Holder.Location, w.claim.Holder.Gen) |
| + return m != nil |
| + }, w.actAll(), func() { w.completeDue(true) }) { |
| + return |
| + } |
| + // the agent restarts: the next wake is a cold admission into a fresh |
| + // generation, which publishes nothing (nothing changed), and the |
| + // origin's park-generation runs once the new marker lands |
| + w.crash(from) |
| + if !w.reach(t, 600, "a fresh generation serving and the origin parked", func() bool { |
| + c := w.claim |
| + if c.Holder.Gen == "" || !hasMain(from) || from.open != nil { |
| + return false |
| + } |
| + for _, o := range c.Obl { |
| + if o.Kind == "park-generation" { |
| + return false |
| + } |
| + } |
| + return true |
| + }, w.actAll(), w.recoveryPass, func() { w.wake(from) }) { |
| + return |
| + } |
| + w.terminate(from) |
| + w.servingOn(t, to) |
| + w.finish(t) |
| +} |
| + |
| +// rev 2: 1b-next rev 16's guards |
| + |
| +func wRelocPinClaimGen(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.drainTo(t, to) |
| + third := w.extraBox(0, 30) |
| + // the first round, observed by a pinner after the source's release and |
| + // before any pin; it stalls before its journal CAS |
| + if !w.reach(t, 1500, "the source's release journaled", func() bool { |
| + c := w.claim |
| + return c.Op.Kind == "relocating" && c.Op.Release != nil && c.Op.Pin == nil |
| + }, w.act(from, to)) { |
| + return |
| + } |
| + stale := w.claim.clone() |
| + if !w.reach(t, 1500, "the target's probe writes into P", func() bool { return preparedOpened(w.claim) && hasMain(to) }, w.act(from, to), w.recoveryPass, func() { w.wake(to) }) { |
| + return |
| + } |
| + w.appWrite(to) |
| + w.replicate(to) |
| + w.completeDue(true) // the target's write is in P's remote before it dies |
| + w.terminate(to) |
| + if !w.reach(t, 100, "the nested pinning", func() bool { |
| + c := w.claim |
| + return c.Op.Kind == "relocating" && c.Op.Phase == "pinning" && c.Op.Pin == nil && contains(c.Lost, to.ID) |
| + }, w.act(third)) { |
| + return |
| + } |
| + w.now += failoverPinDelay |
| + w.relocPinning(third, stale) // the stalled pinner resumes with the first round's selection |
| + w.servingOn(t, third) |
| + w.finish(t) |
| +} |
| + |
| +func wRelocReleaseDeadline(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.appWrite(from) |
| + loc := w.claim.Holder.Location |
| + w.holdKey(loc) // the source's flush never completes |
| + w.drainTo(t, to) |
| + w.reach(t, 3*releaseDeadline+200, "the host serving again", func() bool { |
| + c := w.claim |
| + return c.Op.Kind == "serving" |
| + }, w.actAll(), w.recoveryPass, w.operator) |
| + w.hold = nil |
| + w.completeHeld(loc) |
| + w.finish(t) |
| +} |
| + |
| +func wRelocEnsureLocal(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.drainTo(t, to) |
| + if !w.reach(t, 1500, "the target's receipt journaled", func() bool { |
| + c := w.claim |
| + return c.Op.Kind == "relocating" && c.Op.Receipt != nil && c.Op.Receipt.Box == to.ID |
| + }, w.act(from, to), w.recoveryPass) { |
| + return |
| + } |
| + // the target freezes past its execution lease: its relocation |
| + // controller is lost, and the scoped cleanup retires the unopened |
| + // local install when it runs again |
| + to.Frozen = true |
| + w.drive(execTTL+2, never, w.act(from)) |
| + to.Frozen = false |
| + w.servingOn(t, to) |
| + w.finish(t) |
| +} |
| + |
| +func wRelocVerifyReceipt(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.drainTo(t, to) |
| + third := w.extraBox(0, 30) |
| + if !w.reach(t, 1500, "the probe runs on the target", func() bool { return preparedOpened(w.claim) && hasMain(to) }, w.act(from, to), w.recoveryPass, func() { w.wake(to) }) { |
| + return |
| + } |
| + // the volume holding the host's directory is replaced and the agent |
| + // restarts: the files, the database and the install journal are gone |
| + w.crash(to) |
| + to.Files, to.DB, to.receipt = nil, nil, nil |
| + w.servingOn(t, nil) |
| + _ = third |
| + w.finish(t) |
| +} |
| + |
| +func wRelocPreparedOpenedJournal(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.drainTo(t, to) |
| + if !w.reach(t, 1500, "the probe runs on the target", func() bool { return preparedOpened(w.claim) && hasMain(to) }, w.act(from, to), w.recoveryPass, func() { w.wake(to) }) { |
| + return |
| + } |
| + w.timerOn(to) |
| + w.crash(to) // the next attempt admits a fresh generation from P's |
| + if !w.reach(t, 400, "the second attempt runs", func() bool { return hasMain(to) && w.claim.Holder.Gen != w.claim.Op.Prepared }, w.act(from, to), w.recoveryPass) { |
| + return |
| + } |
| + // holder.admissions is trimmed as AdmitWriter trims it past eight: |
| + // P's admission is no longer listed |
| + w.cas(w.claim, func(n *claim) bool { |
| + var keep []admissionRecord |
| + for _, e := range n.Holder.Admissions { |
| + if e.Gen != n.Op.Prepared { |
| + keep = append(keep, e) |
| + } |
| + } |
| + n.Holder.Admissions = keep |
| + return true |
| + }) |
| + w.crash(to) |
| + w.servingOn(t, to) |
| + w.finish(t) |
| +} |
| + |
| +func wFenceReassignsRegional(t *testing.T, w *world) { |
| + w.twoBox() |
| + from, to := w.boxes[0], w.boxes[3] |
| + w.serve(from, 1, app0) |
| + w.running(t, from) |
| + // a dead generation of the location, with an object in region 0, whose |
| + // park-generation chore carries the legacy owner form box:0 |
| + loc := w.claim.Holder.Location |
| + k := ltxKey(loc, "old", 0, 1, 1) |
| + w.buckets[0].objs[k] = []*version{{ID: w.newVer(), B: &blob{Kind: "ltx", Level: 0, Min: 1, Max: 1, Inc: 1}}} |
| + id := w.newID("ob") |
| + w.cas(w.claim, func(n *claim) bool { |
| + n.Obl = append(n.Obl, w.scoped(obligation{ID: id, Op: "old-op", Kind: "park-generation", Region: 0, Box: -1, Prefix: loc, Ret: "old", Quiet: w.now, Owner: boxOwner(from.ID)}, w.now, 1)) |
| + return true |
| + }) |
| + w.terminate(from) |
| + w.servingOn(t, to) |
| + w.reach(t, 600, "the dead box's regional chore done", func() bool { return !hasObl(w.claim.Obl, id) }, w.actAll(), w.recoveryPass) |
| + w.finish(t) |
| +} |
| + |
| +func wRelocReplaceNotOwing(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.drainTo(t, to) |
| + // box 30 owes a park-local for the host: stale artifacts of an earlier |
| + // stay under stamp 7 |
| + spare := w.extraBox(0, 30) |
| + spare.DB = &localDB{Inc: 1, Loc: w.claim.Holder.Location, State: map[string]int{}, Stamp: 7, Epoch: spare.Epoch} |
| + spare.install(1, 7) |
| + w.cas(w.claim, func(n *claim) bool { |
| + n.Obl = append(n.Obl, obligation{ID: w.newID("ob"), Op: "stay", Kind: "park-local", Box: spare.ID, Region: -1, Ret: "stay"}) |
| + return true |
| + }) |
| + if !w.relocPhase(t, "installing", w.act(from, to), w.recoveryPass) { |
| + return |
| + } |
| + w.terminate(to) |
| + w.servingOn(t, nil) |
| + w.finish(t) |
| +} |
| + |
| +func wRelocExhaustedFence(t *testing.T, w *world) { |
| + w.twoBox() |
| + from, to := w.boxes[0], w.boxes[3] |
| + w.serve(from, 1, app0) |
| + w.running(t, from) |
| + b30, b31 := w.extraBox(0, 30), w.extraBox(0, 31) |
| + w.userRelocate() |
| + if w.claim.Op.Kind != "relocating" { |
| + t.Fatalf("witness: no drain") |
| + } |
| + // three targets die in starting, the live source op.exec throughout |
| + for _, x := range []*box{w.boxByID(w.claim.Op.Tgt), b30, b31, to} { |
| + 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 w.claim.Op.Stuck == "" { |
| + t.Fatalf("witness: the exhausted target did not make the operation stuck: %s", w.state()) |
| + } |
| + w.extraBox(0, spareID()) // a spare the operator's replay may choose |
| + w.servingOn(t, nil) |
| + w.finish(t) |
| +} |
| + |
| +func wFilesPreparedSeqZero(t *testing.T, w *world) { |
| + w.twoBox() |
| + from, to := w.boxes[0], w.boxes[3] |
| + w.serve(from, 1, app0) |
| + w.running(t, from) |
| + for i := 0; i < 3; i++ { // the source publishes three manifests: its sequence reaches 3 |
| + w.timerOn(from) |
| + w.publishFiles(from) |
| + w.completeDue(true) |
| + } |
| + w.drainTo(t, to) |
| + third := w.extraBox(0, 30) |
| + if !w.reach(t, 1500, "the probe runs on the target", func() bool { return preparedOpened(w.claim) && hasMain(to) }, w.act(from, to), w.recoveryPass, func() { w.wake(to) }) { |
| + return |
| + } |
| + w.timerOn(to) // the probe session's timer, published at P's next sequence |
| + w.publishFiles(to) |
| + w.completeDue(true) |
| + w.terminate(to) |
| + w.servingOn(t, third) |
| + w.finish(t) |
| +} |
| + |
| +func wRelocPinEvidencedEmpty(t *testing.T, w *world) { |
| + w.twoBox() |
| + from, to := w.boxes[0], w.boxes[3] |
| + _ = to |
| + w.serve(from, 1, app0) |
| + w.running(t, from) |
| + w.published(t, from) |
| + // the listing finds nothing although the writes are durable (ruling |
| + // 15: a listing that finds nothing is no evidence); the model hides |
| + // the objects for a while, then the listing shows them again |
| + bk := w.buckets[0] |
| + hidden := map[string][]*version{} |
| + for _, k := range bk.keys(w.claim.Holder.Location) { |
| + if isDataKey(k) { |
| + hidden[k] = bk.objs[k] |
| + delete(bk.objs, k) |
| + } |
| + } |
| + w.terminate(from) |
| + w.drive(60, never, w.act(to), w.recoveryPass) |
| + for k, vs := range hidden { |
| + bk.objs[k] = vs |
| + } |
| + w.servingOn(t, nil) |
| + w.finish(t) |
| +} |
diff --git a/internal/sim/hostlife/twobox_test.go b/internal/sim/hostlife/twobox_test.go| index d837ae00f..0d6c828e6 100644 |
| --- a/internal/sim/hostlife/twobox_test.go |
| +++ b/internal/sim/hostlife/twobox_test.go |
| @@ -60,17 +60,21 @@ func tieHash(id int) uint32 { |
| // app): the claimed host on its executor, or on the box its create or |
| // move named. |
| func (w *world) hostsOn(b *box, app string) int { |
| + n := 0 |
| + if w.h2.Kind != "" && w.h2.Box == b.ID && (app == "" || w.h2.App == app) { |
| + n = 1 // the second host, placed by its create (Task 5) |
| + } |
| c := w.claim |
| if c == nil || c.Holder == nil || (app != "" && c.Holder.App != app) { |
| - return 0 |
| + return n |
| } |
| switch { |
| case c.Op.Kind == "creating" && c.Op.NewBox == b.ID: |
| - return 1 |
| + return n + 1 |
| case c.Op.Exec == b.ID: |
| - return 1 |
| + return n + 1 |
| } |
| - return 0 |
| + return n |
| } |
| // owesLocal: an open park-local chore names b. |
diff --git a/internal/sim/hostlife/witness_test.go b/internal/sim/hostlife/witness_test.go| index 88394c375..34544e7ba 100644 |
| --- a/internal/sim/hostlife/witness_test.go |
| +++ b/internal/sim/hostlife/witness_test.go |
| @@ -199,6 +199,47 @@ var witnesses = []witness{ |
| "an upload times out and its retry succeeds while the original stays unresolved; the writer's clean close must write no certificate, because a request of its lifetime is unaccounted for; looking at the level-0 queue alone it certifies (claim rev 6.8 §6.4a, R8-5)", wRetryUnresolved}, |
| {"build-completion", "build-completion", "INV-2", |
| "a push's build with its snapshot, then its anchor, held, the agent crashing in between each; since rev 7.11 the marker is the admission's, so a build completed from its intent gives the probe nothing to restore from its pinned snapshot, and the next session restores an empty generation (INV-2); rev 7.10 caught it at the marker (INV-11)", wBuildCrashes}, |
| + // region HA, two boxes per region (L18; plan 2026-10-07-region-ha-hostlife-two-box rev 2) |
| + {"reloc-release-first", "reloc-release-first", "INV-1", |
| + "a drain: the target's worker pins while the source still runs the host, and the target's probe starts beside it", wRelocReleaseFirst}, |
| + {"reloc-install-receipt", "reloc-install-receipt,reloc-ensure-local", "INV-4", |
| + "the target is terminated at installed, after its receipt; its replacement inherits the receipt and skips its local install, and with EnsureLocal gone too (it restores the install otherwise: 1b-next rev 14's 'each covers the other') it starts over data sealed with the old key", wRelocInstallReceipt}, |
| + {"reloc-no-reinstall", "reloc-no-reinstall", "acknowledged timer", |
| + "the first probe admitted P and registered a timer; the agent restarts and re-applies the pinned wake state over it", wRelocNoReinstall}, |
| + {"reloc-released-coverage", "reloc-released-coverage", "INV-2", |
| + "a failover: the executor is terminated with an acknowledged write whose upload is still in flight; the first admission of P takes released coverage and the write is neither restored nor declared", wRelocReleasedCoverage}, |
| + {"reloc-source-loss", "reloc-source-loss", "INV-2", |
| + "a drain whose source is terminated in releasing before its release is journaled, with an unuploaded write; taken as released at what the remote holds, the write goes undeclared", wRelocSourceLoss}, |
| + {"reloc-row-cases", "reloc-row-cases,exec-admission,exec-writer", "INV-6", |
| + "a stale edges file: after the source's release a paused duplicate open makes its row ready again; reconcile holds it, and with the row case, the exec check and AdmitWriter's op.exec check gone a request admits the released source as a writer, and the stamp its admission issued is activated under the target (INV-6)", wRelocRowCases}, |
| + {"fence-discharge-qualified", "fence-discharge-qualified", "INV-26", |
| + "a terminated box with a volume that was not DeleteOnTermination has its park-local chores discharged automatically", wFenceDischargeQualified}, |
| + {"fence-declares-timers", "fence-declares-timers", "acknowledged timer", |
| + "the executor registers a timer whose manifest never lands and is terminated; the fence drops the timer silently", wFenceDeclaresTimers}, |
| + {"reloc-enrolled-only", "reloc-enrolled-only", "INV-27", |
| + "the only other box of the region holds no key and a replacement has launched unenrolled; the failover names the unenrolled reference", wRelocEnrolledOnly}, |
| + {"files-live-set", "files-live-set", "INV-4", |
| + "the chain's live manifest is the origin generation's, which a cold admission superseded without publishing (nothing changed: 1b-next rev 12's unchanged file); the origin's park-generation archives it, and the failover's install starts over data sealed with a key no manifest carries", wFilesLiveSet}, |
| + {"reloc-pin-claim-gen", "reloc-pin-claim-gen", "INV-3", |
| + "a pinner observed the first round after the source's release and stalled; after the target wrote into P and died, its stale selection of generation_from is journaled for the nested pinning, and the build waits forever for objects generation_from's own park retired", wRelocPinClaimGen}, |
| + {"reloc-release-deadline", "reloc-release-deadline", "INV-3", |
| + "a drain whose source can never flush: with the deadline the operation is stuck and the operator's resolve returns the host to the source; without it the drain waits forever", wRelocReleaseDeadline}, |
| + {"reloc-ensure-local", "reloc-ensure-local", "INV-4", |
| + "the target freezes past its lease after its receipt; the scoped cleanup retires the unopened local install, and without EnsureLocal P's first admission starts over data sealed with a key no files directory carries", wRelocEnsureLocal}, |
| + {"reloc-verify-receipt", "reloc-verify-receipt", "INV-4", |
| + "after P opened the target's volume is replaced and its agent restarts; without VerifyReceipt the next attempt is admitted with no install and starts over data sealed with the old key", wRelocVerifyReceipt}, |
| + {"reloc-prepared-opened-journal", "reloc-prepared-opened-journal", "acknowledged timer", |
| + "P opened, a timer registered, a second attempt admitted, and P's admission trimmed from holder.admissions; read from the list alone, P looks unopened after the next restart and the local install is remade over the timer", wRelocPreparedOpenedJournal}, |
| + {"fence-reassigns-regional", "fence-reassigns-regional", "INV-3", |
| + "the terminated executor owns a park-generation chore in the legacy box:<b> form; without the reassignment nothing ever runs it", wFenceReassignsRegional}, |
| + {"reloc-replace-not-owing", "reloc-replace-not-owing", "INV-3", |
| + "the only spare owes a park-local for the host when the target dies at installing; named anyway, its pending retirement retires the new installation's stamp under it, and the operation never converges", wRelocReplaceNotOwing}, |
| + {"reloc-exhausted-fence", "reloc-exhausted-fence", "INV-1", |
| + "three targets die while the live source is still op.exec in starting; with rev 8's exhausted fence op.exec goes to none, the operator's replay installs a spare, and it runs beside the source", wRelocExhaustedFence}, |
| + {"reloc-pin-evidenced-empty", "reloc-pin-evidenced-empty", "INV-2", |
| + "a failover whose listing finds nothing although the writes are durable: with the rule the operation is stuck until an operator resolves it on a listing that shows them; without it the pin is empty and the install loses the durable writes", wRelocPinEvidencedEmpty}, |
| + {"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}, |
| } |
| // TestWitnesses is the deterministic half of the mutation evidence. |
| @@ -457,6 +498,9 @@ func (w *world) tick(actors ...func()) { |
| } |
| } |
| w.runStalled() |
| + if w.perRegion > 1 { |
| + w.twoBoxStep() // replacements launch and enroll, the publisher runs; the quiet source terminates and drains nothing |
| + } |
| for _, a := range actors { |
| a() |
| } |
diff --git a/internal/sim/hostlife/world_test.go b/internal/sim/hostlife/world_test.go| index 7426cd5fc..19ce89d71 100644 |
| --- a/internal/sim/hostlife/world_test.go |
| +++ b/internal/sim/hostlife/world_test.go |
| @@ -991,6 +991,7 @@ type cancelledCreate struct { |
| type liteHost struct { |
| Inc int |
| App string |
| + Box int // the box its create named (region HA §5.2); control-plane only |
| Kind string // "", "creating", "serving", "purging", "fenced" |
| OpID string |
| Rec bool // its record is published |
| @@ -1052,9 +1053,12 @@ type intner interface{ Intn(n int) int } |
| type world struct { |
| perRegion int // boxes per region at the start (region HA L18): 1, today's model, or 2 |
| issued int // files manifests issued, in order: INV-28's ground truth (blob.Base) |
| - t testingT |
| - seed int64 |
| - rng intner |
| + // oneBoxRegion: a witness's region kept at one box by its group in the |
| + // two-box shape (H5's minimum is per region) |
| + oneBoxRegion [nRegions]bool |
| + t testingT |
| + seed int64 |
| + rng intner |
| // hold, when set, is a witness's hand on S3: a request it answers true |
| // for is accepted and completes only when the witness says so |
| // (witness_test.go). The random sweep never sets it. |