carlos / platform Public

sim: relocation by drain through region HA §5.8's phase table with plan 1b-next rev 16's guards: the release and its deadline, the barrier on every phase change, a pin bound to its claim version and to evidenced emptiness, EnsureLocal and VerifyReceipt around P's first admission, prepared_opened journaled, three probe attempts counted first, released coverage, the row cases and the replacement cap

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Paul Campbell pushed by claude agent, operated by paul@keymail.dev 9fe7634389373c6982e580253ba0c07661c043f2 parent beebe87
11 files changed, +1325 −96
  • internal/sim/hostlife/background_test.go +9 −1
  • internal/sim/hostlife/console_test.go +49 −0
  • internal/sim/hostlife/moves_test.go +29 −79
  • internal/sim/hostlife/protocol_test.go +32 −2
  • internal/sim/hostlife/regionha_test.go +997 −0
  • internal/sim/hostlife/regionha_witness_test.go +53 −0
  • internal/sim/hostlife/rules_test.go +23 −1
  • internal/sim/hostlife/sim_test.go +13 −2
  • internal/sim/hostlife/twobox_test.go +19 −10
  • internal/sim/hostlife/witness_test.go +1 −1
  • internal/sim/hostlife/world_test.go +100 −0
diff --git a/internal/sim/hostlife/background_test.go b/internal/sim/hostlife/background_test.go
index cf45639e0..19c587478 100644
--- a/internal/sim/hostlife/background_test.go
+++ b/internal/sim/hostlife/background_test.go
@@ -232,6 +232,14 @@ func (w *world) reconcileClaimed(b *box, c *claim) {
w.retireRow(b)
}
default:
+ if c.Op.Kind == "relocating" && b.ID == c.Op.Src && b.Row != nil && b.Row.Status == "ready" && c.Op.Release != nil {
+ // §5.3, L12 (rule reloc-row-cases): the former executor's row is
+ // held once its admission fence closed, never ready, until its
+ // park-local retires it. The mutation reopens it as a stale hold
+ if on("reloc-row-cases") {
+ b.Row.Status, b.Row.HoldOp = "relocating", c.Op.ID
+ }
+ }
if w.isParticipant(c, b) {
if !on("participant-rows") && w.rec.Region != b.Region && b.Row != nil {
w.retireRow(b) // region mismatch retires a participant's row
@@ -470,7 +478,7 @@ 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
w.nextID++
- nb := &box{ID: 100 + w.nextID, Region: r, HasKey: true}
+ nb := &box{ID: 100 + w.nextID, Region: r, HasKey: true, Enrolled: w.perRegion == 1, EnrollAt: w.now, DeleteOnTermination: true}
nb.forget()
w.boxes = append(w.boxes, nb)
w.logf("box %d replaces the destroyed box in region %d", nb.ID, r)
diff --git a/internal/sim/hostlife/console_test.go b/internal/sim/hostlife/console_test.go
index 10cad9a39..b08964bcb 100644
--- a/internal/sim/hostlife/console_test.go
+++ b/internal/sim/hostlife/console_test.go
@@ -1224,6 +1224,55 @@ func (w *world) operator() {
return
}
}
+ // a stuck relocation (§5.8): carlos ops host resolve (model ruling 13;
+ // the spec names the command and leaves its effect open). Nothing
+ // moves away from a live box without its stop evidence:
+ // - a live source still op.exec (starting, releasing, no release):
+ // the relocation is abandoned and the host serves on the source;
+ // - a live target op.exec without a release (its receipt lost after
+ // P opened, its release overdue): it is sent to probe-failed, where
+ // it runs its release sequence;
+ // - op.exec none, released, or lost: replayed from pinning with the
+ // replacement count reset, the exclusions cleared and the source
+ // eligible again (Resolved), an empty listing accepted
+ if c.Holder != nil && c.Op.Kind == "relocating" && c.Op.Stuck != "" {
+ op := c.Op
+ released := op.Release != nil && op.Release.Box == op.Exec
+ var what string
+ if w.cas(c, func(n *claim) bool {
+ if !sameOp(n.Op.ID, op.ID) || n.Op.Kind != "relocating" || n.Op.Stuck == "" {
+ return false
+ }
+ switch {
+ case op.Exec >= 0 && op.Exec == op.Src && !released && !contains(n.Lost, op.Exec) && (op.Phase == "starting" || op.Phase == "releasing"):
+ src := op.Src
+ n.Op = opState{Kind: "serving", Exec: src, Parts: []int{src}}
+ what = "abandoned; the host serves on its source"
+ case op.Exec >= 0 && !released && !contains(n.Lost, op.Exec):
+ n.Op.Stuck, n.Op.Phase, n.Op.FailedAt, n.Op.Release = "", "probe-failed", w.now, nil
+ what = "sent its live target to probe-failed"
+ default:
+ n.Op.Stuck, n.Op.Replacements, n.Op.Excluded, n.Op.Resolved = "", 0, nil, true
+ 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
+ n.Op.ProbeTries, n.Op.Attempts = 0, 0
+ var parts []int
+ for _, p := range n.Op.Parts {
+ if !contains(n.Lost, p) && p != op.Exec {
+ parts = append(parts, p)
+ }
+ }
+ n.Op.Parts = parts
+ what = "replayed from pinning"
+ }
+ return true
+ }) {
+ w.stats["operator resolved a stuck relocation"]++
+ w.logf("operator resolved stuck relocation %s: %s", op.ID, what)
+ }
+ return
+ }
// a host marked failed by the retry policy (rev 7.11 §7.14): the operator
// looks at it and clears the mark; the next attempt is a new session
for _, b := range w.liveBoxes() {
diff --git a/internal/sim/hostlife/moves_test.go b/internal/sim/hostlife/moves_test.go
index d547b8de9..078094e01 100644
--- a/internal/sim/hostlife/moves_test.go
+++ b/internal/sim/hostlife/moves_test.go
@@ -151,6 +151,9 @@ func (w *world) role(b *box, c *claim) {
w.initRecord(b, c)
// exec lease (claim §7.1)
if w.isParticipant(c, b) && !contains(c.Lost, b.ID) {
+ if b.ExecUntil > 0 && w.localNow(b) > b.ExecUntil {
+ w.scopedCleanup(b, c) // the relocation controller's lease was lost (1b-next rev 14 finding 1)
+ }
if b.ExecUntil == 0 || 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}
@@ -242,6 +245,8 @@ func (w *world) convertToRelocating(c *claim, src *box) {
return false
}
n.Op.Kind, n.Op.Phase, n.Op.Exec, n.Op.FenceBox = "relocating", "pinning", -1, src.ID
+ n.Op.RelocReason, n.Op.FenceAt, n.Op.Tgt, n.Op.Src = "failover", w.now, -1, src.ID
+ n.Op.Pin, n.Op.Prepared, n.Op.Receipt, n.Op.Release = nil, "", nil, nil
// the files the relocation installs: region HA §5.6's files
// publisher kept the source's files directory in S3 as it served
// (L17); this model has no publisher, so the fence takes the
@@ -267,92 +272,34 @@ func (w *world) convertToRelocating(c *claim, src *box) {
}
}
-// relocate is the relocation's worker on a box of the source's region
-// (claim rev 6.28 §4's table, collapsed as this model collapses an install:
-// pinning hands execution to the region's one eligible box with a new
-// installation stamp, the install and the probe are the cold admission's
-// restore of the pinned generation from this region's remote, and the
-// release preserves the outstanding lane park, which is disjoint from the
-// serving location).
+// relocate is the relocation's worker on a box of the operation's region
+// (region HA §5.8's phase table; claim rev 6.30 §4): every live, enrolled
+// box of the region that is not on lost may act, and each phase's CAS is
+// conditional on the operation, the phase and the ETag, so two workers
+// racing make the same CAS and one fails. The phases live in
+// regionha_test.go. A stuck operation waits for the operator.
func (w *world) relocate(b *box, c *claim) {
op := c.Op
- if b.Region != op.SrcRegion || b.Destroyed || contains(c.Lost, b.ID) {
+ if b.Region != op.SrcRegion || b.Destroyed || contains(c.Lost, b.ID) || !b.Enrolled || op.Stuck != "" {
return
}
switch op.Phase {
+ case "starting":
+ w.relocStarting(b, c)
+ case "releasing":
+ w.relocReleasing(b, c)
case "pinning":
- if op.Exec != -1 {
- return
- }
- if w.cas(c, func(n *claim) bool {
- if !sameOp(n.Op.ID, op.ID) || n.Op.Kind != "relocating" || n.Op.Phase != "pinning" || n.Op.Exec != -1 {
- return false
- }
- n.Op.Exec, n.Op.Tgt, n.Op.Phase = b.ID, b.ID, "probing"
- n.Op.Parts = []int{b.ID}
- n.Boxes = addUniq(n.Boxes, b.ID)
- n.Holder.Stamp = w.issueStamp(n, b.ID) // a new installation's stamp (claim rev 6.28 §4)
- return true
- }) {
- // the local install (collapsed): the published files directory
- // (L17) materialized under the new stamp, before the probe
- if op.StopFiles != nil && b.Files == nil {
- f := op.StopFiles.clone()
- f.Done = true
- b.Files = f
- }
- w.logf("relocation %s: box %d takes the host in region %d", op.ID, b.ID, b.Region)
- }
+ w.relocPinning(b, c)
+ case "installing":
+ w.relocInstalling(b, c)
+ case "installed":
+ w.relocInstalled(b, c)
case "probing":
- if op.Exec != b.ID {
- return
- }
- if b.Row == nil {
- w.holdRow(b, "landing", op.ID, c)
- return
- }
- if !w.admits(b, c, op.ID) {
- return
- }
- if b.HasKey { // RenderHeld + MaterializeHeld before every probe
- b.Config, b.CfgVer, b.Live, b.LiveInc = c.Holder.Inc, w.cfgVer[c.Holder.App], c.Holder.App, c.Holder.Inc
- }
- if hasMain(b) || w.spawn(b, c, c.Holder.Gen, true) {
- w.probeAccepted(b, c)
- w.cas(c, func(n *claim) bool { n.Op.Phase = "probed"; return sameOp(n.Op.ID, op.ID) })
- return
- }
- if b.hostFailed && !b.failCounted {
- b.failCounted = true
- } else if b.open != nil || b.hostFailed {
- return
- }
- w.cas(c, func(n *claim) bool {
- n.Op.ProbeTries++
- if n.Op.ProbeTries >= probeTries*3 {
- n.Op.Phase = "stuck"
- }
- return sameOp(n.Op.ID, op.ID)
- })
- case "probed":
- if op.Exec != b.ID {
- return
- }
- if b.open != nil {
- return
- }
- if !hasMain(b) {
- w.stats["probe restarted"]++
- w.cas(c, func(n *claim) bool { n.Op.Phase = "probing"; return sameOp(n.Op.ID, op.ID) })
- return
- }
- if w.openRow(b, op.ID) {
- w.cas(c, func(n *claim) bool { n.Op.Phase = "opened"; return sameOp(n.Op.ID, op.ID) })
- }
- case "opened":
- if op.Exec == b.ID {
- w.release(c, b.ID) // outstanding disjoint parks do not block serving (claim rev 6.28 §4)
- }
+ w.relocProbing(b, c)
+ case "probe-failed":
+ w.relocProbeFailed(b, c)
+ case "probed", "opened":
+ w.relocSettle(b, c)
}
}
@@ -1343,6 +1290,9 @@ func (w *world) release(c *claim, execBox int) {
// holder.admissions survives the release by living in the holder
// (claim rev 6.12): an admission whose start is unfinished at the
// release stays explained (seed 1052 / 30,000)
+ if op.Kind == "relocating" {
+ w.relocationLeftovers(n, op) // the abandoned installations' park-local chores (claim §4)
+ }
n.Op = opState{Kind: "serving", Exec: execBox, Parts: []int{execBox}}
return true
}) {
diff --git a/internal/sim/hostlife/protocol_test.go b/internal/sim/hostlife/protocol_test.go
index ec383bb1f..8ff23c13f 100644
--- a/internal/sim/hostlife/protocol_test.go
+++ b/internal/sim/hostlife/protocol_test.go
@@ -1435,6 +1435,9 @@ func (w *world) admits(b *box, c *claim, probe string) bool {
if probe != "" {
return probe == op.ID && role(op.Tgt) && op.Phase == "probing"
}
+ if role(op.Src) && (op.Phase == "starting" || op.Phase == "releasing" && op.Release == nil) {
+ return b.Row.Status == "ready" // the source serves until its admission fence closes (§5.3, §5.8)
+ }
return role(op.Tgt) && op.Phase == "opened" && b.Row.Status == "ready"
}
return false
@@ -1485,8 +1488,11 @@ func (w *world) certificate(b *box, c *claim) *version {
// holder.generation is the only authoritative generation, in every kind
// and phase).
func installGen(op *opState) string {
- if op.Kind == "restoring" {
+ switch op.Kind {
+ case "restoring":
return op.RollbackID
+ case "relocating":
+ return op.Prepared // P, fresh per installation (region HA §5.8)
}
return op.ID
}
@@ -1651,6 +1657,26 @@ func (w *world) admitWriter(b *box, c *claim, want string, probe bool) (admitInp
covers = c.Op.ReturnFromDB
}
a.Mode, a.NewGeneration = "cold", want
+ if c.Op.Kind == "relocating" {
+ // released (claim §6.4a item 2, L9): only on the admission that
+ // opens P, and only when the predecessor is exactly the box and
+ // session whose flushed release this operation journaled and whose
+ // final_txid the pin reached; a failover's first admission and every
+ // later attempt declare (coverage ""). The mutation of
+ // reloc-released-coverage grants it to every first opening of P
+ r := c.Op.Release
+ predBox, predSession, predGen := h.WriterBox, h.Session, h.Gen // the predecessor's identity as admitCommit journals it
+ if l := lastAdmission(h); l != nil {
+ predBox, predSession, predGen = l.Box, l.Session, l.Gen
+ }
+ switch {
+ case !on("reloc-released-coverage"):
+ a.Coverage = "released"
+ case r != nil && r.Flushed && c.Op.Pin != nil && c.Op.Pin.TX >= r.FinalTX && predBox == r.Box && predSession == r.Session && predGen == r.Gen:
+ a.Coverage = "released"
+ }
+ return a, true
+ }
if covers {
a.Coverage = "sealed"
}
@@ -1869,7 +1895,7 @@ func (w *world) admitCommit(b *box, c *claim, a admitInput) bool {
// unfinished admission until generation.json names the new
// generation; the chore is queued then (claim rev 6.10, R10-2).
// The mutation of baseline-live queues it now, as rev 7.10 did
- if !on("baseline-live") && a.Coverage != "sealed" {
+ if !on("baseline-live") && a.Coverage != "sealed" && a.Coverage != "released" {
ret := h.Gen
if ret == "" {
ret = "@root"
@@ -1877,6 +1903,9 @@ func (w *world) admitCommit(b *box, c *claim, a admitInput) bool {
n.Obl = append(n.Obl, w.scoped(obligation{ID: w.newID("ob"), Op: fmt.Sprintf("session:%d", n.Holder.Session), Kind: "park-generation", Region: b.Region, Box: -1, Prefix: n.Holder.Location, Ret: ret, Quiet: w.now + horizonH}, w.now, n.Holder.Inc))
}
}
+ if n.Op.Kind == "relocating" && n.Op.Prepared != "" && gen == n.Op.Prepared {
+ n.Op.PreparedOpened = gen // prepared_opened, journaled with the admission that opens P (1b-next rev 12 S1)
+ }
n.Holder.Admissions = append(n.Holder.Admissions, e)
entry = e
return true
@@ -2169,6 +2198,7 @@ func (w *world) localPark(b *box, inc int) bool {
case len(b.Timers) > 0 || len(b.History) > 0 || b.Attempt != 0:
b.Timers, b.History, b.Attempt = nil, nil, 0
default:
+ b.receipt = nil // a relocation's install journal goes with the installation
return true
}
b.Parked++
diff --git a/internal/sim/hostlife/regionha_test.go b/internal/sim/hostlife/regionha_test.go
new file mode 100644
index 000000000..4627712c5
--- /dev/null
+++ b/internal/sim/hostlife/regionha_test.go
@@ -0,0 +1,997 @@
+package hostlife
+
+import "fmt"
+
+// ---------- relocation (region HA spec 1 §5.8; claim rev 6.30 §4, L1; plan 1b-next rev 16) ----------
+//
+// A same-region executor change. The model's steps are abstract time:
+// probeStartWindow (30) is a probe attempt's readiness window, so the
+// probe deadline holds three attempts; sigAgeH (45) is the 15-minute
+// signature age, so the failover pin delay (30 s) is two steps. Each
+// guard names the plan 1b-next rev 16 function it mirrors.
+
+const (
+ failoverPinDelay = 2 // §5.8: pin no earlier than the fence's observed_at plus 30 s (hostclaim.FailoverPinDelay)
+ probeDeadline = 3*probeStartWindow + 10 // §5.8: at most three attempts within the probe deadline (hostrelocate.ProbeDeadline)
+ releaseDeadline = probeDeadline // 1b-next ruling 14: a release not journaled this long after releasing or probe-failed began is stuck (hostrelocate.ReleaseDeadline, 10 minutes like the probe deadline)
+ maxReplacements = 2 // §5.8: after two replacements of the target, stuck (hostclaim.MaxTargetReplacements)
+ enrollDelay = 20 // H16, H17: a launched box is confirmed and enrolled by a worker some time later
+ replaceDelay = 30 // H5: the group launches a replacement for a terminated box
+)
+
+// userRelocate is a scale-in drain (§5.8, reason drain; spec 4 owns the
+// decision): the serving host's executor is asked to give the host to
+// another eligible box of its region. The start CAS (StartRelocation)
+// records the intent, op.exec stays on the source, and both participants
+// acknowledge by writing execution leases (role()). The two-box step
+// draws it. A host that never admitted a writer is not drained (1b-next
+// ruling 11, Worker.Start; rule reloc-drain-needs-writer): its release has
+// no writer session to stop, so root refuses its stop evidence and the
+// drain could only wait for its release deadline; a failover relocates it.
+func (w *world) userRelocate() {
+ c := w.claim
+ if c == nil || c.Holder == nil || c.Op.Kind != "serving" {
+ return
+ }
+ from := w.execBox(c)
+ if from == nil || from.Destroyed || from.Old || !from.Enrolled {
+ return
+ }
+ if ad := w.admit[c.Holder.App]; ad != nil && ad.Closed {
+ return // a box-started relocation needs the app's admission registration (1b-next ruling 4): a purge closed it
+ }
+ if on("reloc-drain-needs-writer") && c.Holder.Session == 0 {
+ w.stats["drain refused: the host never had a writer"]++
+ return
+ }
+ to := w.chooseBoxExcept(from.Region, c.Holder.App, from.ID)
+ if to == nil || to.Old {
+ return
+ }
+ id := w.newID("rl")
+ if w.cas(c, func(n *claim) bool {
+ if n.Holder == nil || n.Op.Kind != "serving" || n.Op.Exec != from.ID || !w.relocationStartAllowed(n, from, to) {
+ return false
+ }
+ n.Op = opState{Kind: "relocating", ID: id, Phase: "starting", Exec: from.ID, Parts: []int{from.ID, to.ID},
+ Src: from.ID, Tgt: to.ID, SrcRegion: from.Region, RelocReason: "drain", ReqAt: w.now, App: n.Holder.App,
+ SrcGen: n.Holder.Gen, SrcStamp: n.Holder.Stamp}
+ return true
+ }) {
+ w.stats["relocation started: drain"]++
+ w.logf("relocation %s: drain of inc %d from box %d to box %d in region %d", id, c.Holder.Inc, from.ID, to.ID, from.Region)
+ }
+}
+
+// relocationStartAllowed is the claim's start guard as L11 amends it for
+// relocating (RelocationStartGuard): a park-replica or any other
+// whole-location chore in the region blocks (CC11), a park-local on the
+// target or on a live source blocks, and a park-generation in the region
+// does not: relocation writes only its own new prepared generation, never
+// one being retired. The mutation of reloc-start-guard starts over
+// anything.
+func (w *world) relocationStartAllowed(c *claim, from, to *box) bool {
+ if !on("reloc-start-guard") {
+ return true
+ }
+ for _, o := range c.Obl {
+ switch {
+ case o.Kind == "park-generation":
+ continue // L11
+ case o.Kind == "park-local":
+ if o.Box == to.ID || o.Box == from.ID && !contains(c.Lost, from.ID) {
+ return false
+ }
+ case o.Region == from.Region:
+ return false
+ }
+ }
+ return true
+}
+
+// relocExcept is every box the operation may not name as its target
+// (replaceTargetSlot, Worker.next): the source, unless an operator's
+// resolve made it eligible again (model ruling 13), every replaced target,
+// and the extra boxes given.
+func relocExcept(op opState, extra ...int) []int {
+ var out []int
+ if !op.Resolved {
+ out = append(out, op.Src)
+ }
+ out = append(out, op.Excluded...)
+ return append(out, extra...)
+}
+
+// relocRelease is the release sequence (§5.8, A3-2; 1b-next Task 7's
+// Release) a live box runs to give the host up: the source in releasing,
+// a failed target in probe-failed. One step per call; it returns the
+// journal entry once every step is done, nil while one is owed.
+//
+// 1. stop every writer: admission closed (the row held), the process
+// tree stopped and empty; an escaped descendant fails the step (L10);
+// 2. flush: the final checkpoint and SyncAndWait, passing only once the
+// listing shows the stopped database's position N (moves §5.1 step
+// 1). When the session's replicator died with its agent (claim rev
+// 6.10) nothing can flush: the entry names what the remote holds,
+// Flushed false, and the next admission declares the rest;
+// 3. publish every pending file and wake-state mutation: the entry
+// carries them until Task 4's manifest.
+func (w *world) relocRelease(b *box, c *claim) *releaseEntry {
+ h := c.Holder
+ if b.Row != nil && b.Row.Status == "ready" {
+ w.holdRow(b, "relocating", c.Op.ID, c)
+ }
+ if !w.evidence(b, c.Op.ID) {
+ w.stats["release: a process survives the stop"]++
+ return nil
+ }
+ prefix := dataKey(h.Location, h.Gen, "")
+ remote := w.remoteMax(w.buckets[b.Region], prefix)
+ n, flushed := remote, false
+ if db := b.DB; db != nil && db.Inc == h.Inc && db.Gen == h.Gen {
+ if db.Epoch == b.Epoch && db.Session == h.Session {
+ if len(db.Pending) > 0 {
+ bl := w.deltaOf(db, db.Inc)
+ db.FirstFull = false
+ db.Queue = append(db.Queue, bl)
+ db.Pos, db.Pending = bl.Max, nil
+ }
+ w.ship(b)
+ if len(db.Queue) > 0 || db.InFlight != nil || remote < db.Pos {
+ w.stats["release: waits for the flush"]++
+ return nil
+ }
+ n, flushed = db.Pos, true
+ } else {
+ w.stats["release: the session's replicator is gone, unflushed"]++
+ }
+ }
+ // the files the box holds, or, when it holds none of this incarnation's
+ // (a failed target whose unopened install a scoped cleanup retired),
+ // the set its own installation applied: a release never invents a
+ // files identity
+ files := b.Files.clone()
+ if files == nil || files.Inc != h.Inc {
+ files = w.relocFiles(c).clone()
+ }
+ return &releaseEntry{Box: b.ID, Session: h.Session, Gen: h.Gen, FinalTX: n, Flushed: flushed,
+ Files: files, Timers: append([]int(nil), b.Timers...), At: w.now}
+}
+
+// pinSource is the generation the pin reads (StorePinner's genselect.Select
+// over the admitted chain): holder.generation when it holds an object or
+// the marker names it; else the baseline the recovery walk selects for an
+// unfinished run of cold admissions (claim rev 6.22 §6.2a), as a cold
+// admission would restore it. An unexplained empty generation refuses:
+// absence is never evidence (§5.9).
+func (w *world) pinSource(b *box, c *claim) (string, bool) {
+ h := c.Holder
+ loc := h.Location
+ if w.hasFiles(b, loc, h.Gen) {
+ return h.Gen, true
+ }
+ bg, _ := w.bucketGen(b, loc)
+ if bg == h.Gen {
+ return h.Gen, true
+ }
+ run, ok := w.unfinishedRun(c, bg)
+ if !ok {
+ return "", false
+ }
+ return w.runBaseline(b, c, run, bg)
+}
+
+// selectPin is StorePinner.Pin against the observation c: the source
+// generation and its listing's newest position N, after a release only
+// once N reaches the release's final_txid (rule reloc-pin-reaches-release),
+// and an empty listing only with evidence (ruling 15, rule
+// reloc-pin-evidenced-empty): a journaled release that flushed at 0, or a
+// holder that never admitted a writer; any other empty listing marks the
+// operation stuck for an operator. The pin carries the claim version it
+// was selected against (ruling 16, RecoveryPinKey). Task 4 adds the files
+// pin. It returns nil while the pin must wait.
+func (w *world) selectPin(b *box, c *claim) *pinEntry {
+ op, h := c.Op, c.Holder
+ src, ok := w.pinSource(b, c)
+ if !ok {
+ w.stats["pin: the source generation cannot be selected yet"]++
+ return nil
+ }
+ n := w.remoteMax(w.buckets[b.Region], dataKey(h.Location, src, ""))
+ r := op.Release
+ if r != nil && on("reloc-pin-reaches-release") && n < r.FinalTX {
+ w.stats["pin: waits for the release's final txid"]++
+ return nil
+ }
+ if n == 0 && on("reloc-pin-evidenced-empty") && !op.Resolved && h.Session != 0 && !(r != nil && r.Flushed && r.FinalTX == 0) {
+ w.markStuck(c, fmt.Sprintf("an empty listing of %q is no evidence of an empty database (session %d)", src, h.Session))
+ return nil
+ }
+ return &pinEntry{Gen: src, TX: n, ClaimVer: c.Ver, At: w.now, Files: w.relocFiles(c).clone(), Timers: append([]int(nil), w.relocTimers(c)...)}
+}
+
+// restoreUpTo restores generation gen of region r from its current
+// listing, capped at TXID upto: the newest current snapshot at or below
+// upto as the root, then the planner's rule (ltx.IsContiguous, highest
+// max, lowest min, higher level) over the current level-0 and level-1
+// files whose range ends at or below upto. It is §5.8's build from the
+// pinned recovery set: nothing past the pin is restored, and a listing
+// that does not reach upto refuses (nil), as a pin short of its release
+// would. It reads the bucket and writes nothing.
+func (w *world) restoreUpTo(r, inc int, loc, gen string, upto int) *localDB {
+ bk := w.buckets[r]
+ prefix := dataKey(loc, gen, "")
+ db := &localDB{Inc: inc, Loc: loc, Gen: gen, State: map[string]int{}}
+ var root *blob
+ for _, s := range w.currentLTX(bk, prefix, 9) {
+ if s.B.Max <= upto && (root == nil || s.B.Max > root.Max) {
+ root = s.B
+ }
+ }
+ cur := 0
+ var applied []*blob
+ if root != nil {
+ apply(db.State, root)
+ cur = root.Max
+ applied = append(applied, root)
+ db.Key = root.SealKey
+ if root.Inc != 0 {
+ db.Inc = root.Inc
+ }
+ }
+ var cands []*blob
+ for _, level := range []int{0, 1} {
+ for _, f := range w.currentLTX(bk, prefix, level) {
+ if f.B.Max <= upto {
+ cands = append(cands, f.B)
+ }
+ }
+ }
+ for cur < upto {
+ var best *blob
+ for _, f := range cands {
+ if f.Min <= cur+1 && f.Max > cur && (best == nil || f.Max > best.Max || f.Max == best.Max && (f.Min < best.Min || f.Min == best.Min && f.Level > best.Level)) {
+ best = f
+ }
+ }
+ if best == nil {
+ return nil // the listing does not reach upto: a gap, or objects still landing
+ }
+ apply(db.State, best)
+ cur = best.Max
+ applied = append(applied, best)
+ if db.Key == 0 {
+ db.Key = best.SealKey
+ }
+ if best.Inc != 0 {
+ db.Inc = best.Inc
+ }
+ }
+ db.Log = txsOf(applied...)
+ db.TX = w.lineageTX(applied...)
+ db.Pos = cur
+ return db
+}
+
+// relocFiles is the files directory the local install applies: the
+// pinned set's (the pin carries the files and wake state it was taken
+// with), else the release's (a drain, a nested relocation), else the
+// converted move's or the failover's stand-in for the files publisher
+// (moves §14.2.6). Task 4 puts the pinned manifest first.
+func (w *world) relocFiles(c *claim) *filesDir {
+ if p := c.Op.Pin; p != nil && p.Files != nil {
+ return p.Files
+ }
+ if r := c.Op.Release; r != nil && r.Files != nil {
+ return r.Files
+ }
+ return c.Op.StopFiles
+}
+
+// relocTimers is the wake state the local install replaces timers with.
+func (w *world) relocTimers(c *claim) []int {
+ if p := c.Op.Pin; p != nil && p.Files != nil {
+ return p.Timers
+ }
+ if r := c.Op.Release; r != nil {
+ return r.Timers
+ }
+ return nil
+}
+
+// nameReplacement names next as the operation's target in n, counting a
+// replacement when it replaces another box (replaceTargetSlot): the
+// replaced box is excluded for this host, and past maxReplacements the
+// operation is marked stuck at the current phase instead (rule
+// reloc-replacement-cap). Inside the CAS it refuses a box that owes a
+// park-local for the host (rule reloc-replace-not-owing, Task 3). It
+// reports whether next was named.
+func (w *world) nameReplacement(n *claim, next int, phase string) bool {
+ if on("reloc-replace-not-owing") {
+ if b := w.boxByID(next); b != nil && w.owesLocal(n, b) {
+ w.stats["replacement refused: the box owes a park-local"]++
+ return false
+ }
+ }
+ old := n.Op.Tgt
+ if old >= 0 && old != next {
+ if on("reloc-replacement-cap") && n.Op.Replacements >= maxReplacements {
+ n.Op.Stuck = fmt.Sprintf("two replacements of the target used; a third was needed at %s", n.Op.Phase)
+ w.stats["relocation stuck: replacement cap"]++
+ return false
+ }
+ n.Op.Replacements++
+ n.Op.Excluded = addUniq(n.Op.Excluded, old)
+ var parts []int
+ for _, p := range n.Op.Parts {
+ if p != old {
+ parts = append(parts, p)
+ }
+ }
+ n.Op.Parts = parts
+ }
+ n.Op.Tgt = next
+ n.Op.Parts = addUniq(n.Op.Parts, next)
+ n.Op.Phase = phase
+ return true
+}
+
+// markStuck is MarkStuck: a journal entry, never a phase; every relocation
+// step refuses afterwards until the operator resolves it. It never stops
+// an operation between installed and a probe while P is unopened: that
+// live target's safe point is its probe.
+func (w *world) markStuck(c *claim, why string) {
+ id := c.Op.ID
+ if w.cas(c, func(n *claim) bool {
+ if !sameOp(n.Op.ID, id) || n.Op.Kind != "relocating" || n.Op.Stuck != "" {
+ return false
+ }
+ if n.Op.Phase == "installed" && n.Op.Receipt != nil && !preparedOpened(n) {
+ return false
+ }
+ n.Op.Stuck = why
+ return true
+ }) {
+ w.alerts++
+ w.stats["relocation stuck"]++
+ w.logf("relocation %s stuck: %s", id, why)
+ }
+}
+
+// relocationLeftovers queues, inside the serving CAS (CompleteRelocation),
+// the park-local chore every abandoned installation owes (claim §4: "every
+// abandoned local installation receives an exact park-local"): the
+// source, when it is alive and its fence did not discharge it, and every
+// other box this operation handed op.exec to.
+func (w *world) relocationLeftovers(n *claim, op opState) {
+ owed := append([]int{op.Src}, op.InstalledOn...)
+ for _, id := range owed {
+ if id < 0 || id == op.Exec || contains(op.Discharged, id) {
+ continue
+ }
+ if b := w.boxByID(id); b == nil || w.owesLocal(n, b) {
+ continue
+ }
+ n.Obl = append(n.Obl, obligation{ID: w.newID("ob"), Op: op.ID, Kind: "park-local", Box: id, Region: -1, Ret: op.ID})
+ }
+}
+
+// relocStarting: the barrier (claim D6, requireAcks in ToReleasing). A
+// drain leaves starting for releasing once both participants' execution
+// leases are current (role() writes them on every read of the claim), and
+// the CAS records releasing_since for the release deadline; a failover
+// never enters starting in this model (it starts at pinning, Task 3). The
+// 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) {
+ return
+ }
+ w.cas(c, func(n *claim) bool {
+ if !sameOp(n.Op.ID, op.ID) || n.Op.Kind != "relocating" || n.Op.Phase != "starting" {
+ return false
+ }
+ n.Op.Phase, n.Op.ReleasingSince = "releasing", w.now
+ return true
+ })
+}
+
+// relocReleasing: the source runs the release sequence and journals it
+// (JournalRelease); then a worker's CAS (PinAfterRelease) cites the entry
+// and leaves for pinning with op.exec none and the stamp kept (claim
+// R6-4), once every participant has acknowledged (rule
+// reloc-ack-before-pinning: a target replaced in releasing acknowledges
+// before the operation leaves the phase; 1b-next rev 4 N6). A source that
+// has not journaled its release releaseDeadline after releasing began is
+// stuck (rule reloc-release-deadline, Worker.releaseOverdue): nothing
+// moves away from a live box without its stop evidence. The mutation of
+// reloc-release-first pins without the entry: the source is never
+// stopped.
+func (w *world) relocReleasing(b *box, c *claim) {
+ op := c.Op
+ if op.Release == nil {
+ if on("reloc-release-deadline") && w.now > op.ReleasingSince+releaseDeadline {
+ w.markStuck(c, fmt.Sprintf("box %d has not released the host %d steps after releasing", op.Exec, releaseDeadline))
+ return
+ }
+ if b.ID != op.Exec {
+ if !on("reloc-release-first") {
+ w.cas(c, func(n *claim) bool {
+ ok := sameOp(n.Op.ID, op.ID) && n.Op.Kind == "relocating" && n.Op.Phase == "releasing"
+ if ok {
+ n.Op.Phase, n.Op.Exec = "pinning", -1
+ }
+ return ok
+ })
+ }
+ return
+ }
+ r := w.relocRelease(b, c)
+ if r == nil {
+ return
+ }
+ if w.cas(c, func(n *claim) bool {
+ ok := sameOp(n.Op.ID, op.ID) && n.Op.Kind == "relocating" && n.Op.Phase == "releasing" && n.Op.Exec == b.ID && n.Op.Release == nil
+ if ok {
+ n.Op.Release = r
+ }
+ return ok
+ }) {
+ w.stats["release journaled: source"]++
+ w.logf("relocation %s: box %d released the host at TXID %d (flushed=%v)", op.ID, b.ID, r.FinalTX, r.Flushed)
+ }
+ return
+ }
+ if on("reloc-ack-before-pinning") && !w.leasesSeen(c) {
+ w.stats["pin after release: waits for the acknowledgements"]++
+ return
+ }
+ w.cas(c, func(n *claim) bool {
+ ok := sameOp(n.Op.ID, op.ID) && n.Op.Kind == "relocating" && n.Op.Phase == "releasing" && n.Op.Release != nil && n.Op.Release.Box == n.Op.Exec
+ if ok {
+ n.Op.Phase, n.Op.Exec = "pinning", -1
+ }
+ return ok
+ })
+}
+
+// relocPinning: a worker selects the pin against its observation and
+// journals it (JournalPin) in a CAS bound to that observation's claim
+// version (rule reloc-pin-claim-gen, ruling 16: a pin selected against an
+// older claim is abandoned, and the next pass selects afresh); a failover
+// pins no earlier than the fence's observed_at plus failoverPinDelay (rule
+// reloc-failover-pin-delay, a loss bound). Then it names a target when the
+// operation has none (NameTarget: a converted move, a resolved stuck
+// operation, a target lost with no spare); then, with every participant's
+// lease current (rule reloc-exec-ack-barrier), hands op.exec to the
+// target for a new installation (ToInstalling): a new stamp, journaled as
+// install_stamp, and a fresh prepared generation id (claim R6-4). The
+// target must owe no park-local for the host.
+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 {
+ return
+ }
+ pin := w.selectPin(b, c)
+ if pin == nil {
+ return
+ }
+ if w.cas(c, func(n *claim) bool {
+ ok := sameOp(n.Op.ID, op.ID) && n.Op.Kind == "relocating" && n.Op.Phase == "pinning" && n.Op.Pin == nil && n.Op.Stuck == ""
+ if ok && on("reloc-pin-claim-gen") && n.Ver != pin.ClaimVer {
+ w.stats["pin: selected against an older claim, abandoned"]++
+ ok = false
+ }
+ if ok {
+ n.Op.Pin = pin
+ }
+ return ok
+ }) {
+ w.logf("relocation %s: pinned %q at TXID %d (selected against claim version %d)", op.ID, pin.Gen, pin.TX, pin.ClaimVer)
+ }
+ return
+ }
+ if op.Tgt < 0 {
+ to := w.chooseBoxExcept(op.SrcRegion, h.App, relocExcept(op)...)
+ if to == nil {
+ return // no eligible box: the recovery pass alerts once (moves §7.10)
+ }
+ w.cas(c, func(n *claim) bool {
+ ok := sameOp(n.Op.ID, op.ID) && n.Op.Kind == "relocating" && n.Op.Phase == "pinning" && n.Op.Tgt < 0
+ if ok {
+ ok = w.nameReplacement(n, to.ID, "pinning")
+ }
+ return ok
+ })
+ return
+ }
+ if on("reloc-exec-ack-barrier") && !w.leasesSeen(c) {
+ return
+ }
+ to := op.Tgt
+ if w.cas(c, func(n *claim) bool {
+ if !sameOp(n.Op.ID, op.ID) || n.Op.Kind != "relocating" || n.Op.Phase != "pinning" || n.Op.Tgt != to || n.Op.Pin == nil || n.Op.Stuck != "" || contains(n.Lost, to) {
+ return false
+ }
+ if t := w.boxByID(to); t == nil || w.owesLocal(n, t) {
+ return false
+ }
+ w.handExec(n, to, "installing", w.newID("P"))
+ n.Op.BaseKey, n.Op.BaseVer, n.Op.BaseTX = "", 0, 0
+ return true
+ }) {
+ w.logf("relocation %s: box %d installs with stamp %d", op.ID, to, w.claim.Holder.Stamp)
+ }
+}
+
+// handExec is install() in hostclaim: op.exec to box at phase with
+// prepared generation P, a new stamp (this CAS's), journaled as
+// install_stamp, no receipt, the probe attempts reset for the new
+// executor (BeginProbeAttempt counts per box), and the box noted as owing
+// a park-local should it be abandoned.
+func (w *world) handExec(n *claim, box int, phase, prepared string) {
+ n.Op.Exec, n.Op.Phase, n.Op.Prepared = box, phase, prepared
+ n.Holder.Stamp = w.issueStamp(n, box)
+ n.Op.InstallStamp = n.Holder.Stamp
+ if on("reloc-install-receipt") {
+ n.Op.Receipt = nil
+ }
+ n.Op.Attempts = 0
+ n.Op.InstalledOn = addUniq(n.Op.InstalledOn, box)
+ n.Boxes = addUniq(n.Boxes, box)
+}
+
+// relocInstalling: the target builds P, the remote prepared generation,
+// exactly as a landing builds its generation (moves §7.6, L16): the
+// snapshot [1, N] of the pinned generation, create-only and acknowledged,
+// then the level-0 anchor [N, N], acknowledged, then the installed CAS
+// (ToInstalled, R7-4). A pin at N = 0 builds nothing: the probe is an
+// empty bootstrap (claim P6-D3). Only op.exec installs (rule
+// reloc-exec-only-installs, HA2: being in the region is never enough).
+func (w *world) relocInstalling(b *box, c *claim) {
+ op, h := c.Op, c.Holder
+ if on("reloc-exec-only-installs") && op.Exec != b.ID {
+ return
+ }
+ loc, g := h.Location, op.Prepared
+ 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 {
+ n.Op.Phase = "installed"
+ }
+ return ok
+ }
+ if !w.buildPreparedFiles(b, c) {
+ return // Task 4: P's prepared files manifest first
+ }
+ if op.Pin.TX == 0 {
+ w.cas(c, installed)
+ return
+ }
+ if op.BaseKey == "" {
+ db := w.restoreUpTo(b.Region, h.Inc, loc, op.Pin.Gen, op.Pin.TX)
+ if db == nil || db.Pos != op.Pin.TX {
+ w.stats["build: the pinned set cannot be restored yet"]++
+ return
+ }
+ key := snapKey(loc, g, op.Pin.TX)
+ if !w.ackedPut(b, key, snapshotOf(db, h.Inc), true) {
+ return
+ }
+ v := bk.current(key)
+ if v == nil {
+ return
+ }
+ w.cas(c, 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 && n.Op.BaseKey == ""
+ if ok {
+ n.Op.BaseKey, n.Op.BaseVer, n.Op.BaseTX = key, v.ID, op.Pin.TX
+ }
+ return ok
+ })
+ return
+ }
+ if !w.anchorAcked(b, loc, g, op.BaseKey, op.BaseVer, op.BaseTX) {
+ return
+ }
+ if w.cas(c, installed) {
+ w.logf("relocation %s: P %q built on box %d at TXID %d", op.ID, g, b.ID, op.BaseTX)
+ }
+}
+
+// buildPreparedFiles is Task 4's prepared files manifest; before it, the
+// build has nothing to write for files.
+func (w *world) buildPreparedFiles(b *box, c *claim) bool { return true }
+
+// localInstall advances the executor's local install by one step (§5.8,
+// B1-2; 1b-next Task 8c's Install) and reports whether it is whole: park
+// what an earlier stay left as retire-artifacts of its stamp (claim §6.4),
+// extract the files, replace the timers with the pinned wake state (the
+// files Done marker last), render and materialize with current inputs,
+// and write the box's install journal (its receipt) under install_stamp.
+// EnsureLocal reuses it to restore a retired install under the same
+// stamp.
+func (w *world) localInstall(b *box, c *claim) bool {
+ op, h := c.Op, c.Holder
+ g := op.Prepared
+ if b.Files == nil || b.Files.Gen != g {
+ for _, st := range []int{dbStamp(b.DB), filesStamp(b.Files)} {
+ if st != 0 && st != b.stampOf(h.Inc) {
+ w.retireArtifacts(b, h.Inc, st)
+ }
+ }
+ if b.DB != nil {
+ b.DB = nil // never reused (claim R6); the probe's admission restores
+ b.Parked++
+ }
+ src := w.relocFiles(c)
+ if src == nil {
+ w.nextID++
+ src = &filesDir{Inc: h.Inc, Key: w.nextID, Env: w.nextID}
+ }
+ f := src.clone()
+ f.Inc, f.Gen, f.Done, f.Stamp = h.Inc, g, false, b.stampOf(h.Inc)
+ if !on("markers-last") {
+ f.Done = true
+ }
+ b.Files = f
+ b.pendingTimers = append([]int(nil), w.relocTimers(c)...)
+ return false
+ }
+ if !b.Files.Done {
+ b.Timers = append([]int(nil), b.pendingTimers...) // ReplaceTimers: the pinned wake state
+ b.Attempt, b.History = 0, nil
+ b.Files.Done = true
+ b.installEpoch = b.Epoch
+ return false
+ }
+ if b.HasKey {
+ b.Config, b.CfgVer = h.Inc, w.cfgVer[h.App]
+ }
+ b.Live, b.LiveInc = h.App, h.Inc
+ b.receipt = &receiptEntry{Op: op.ID, Box: b.ID, Stamp: op.InstallStamp}
+ return true
+}
+
+// relocInstalled: the executor's local install, then its receipt by CAS
+// (RecordLocalInstall), bound to this box and install_stamp; probing
+// needs that exact receipt (ToProbing; rule reloc-install-receipt), and
+// the install is verified, and restored if a lost lease's scoped cleanup
+// retired it, before the probing CAS (EnsureLocal; rule
+// reloc-ensure-local). The mutation of reloc-install-receipt lets a
+// replacement inherit its predecessor's receipt and skip its install.
+func (w *world) relocInstalled(b *box, c *claim) {
+ op := c.Op
+ if on("reloc-exec-only-installs") && op.Exec != b.ID {
+ return
+ }
+ 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 {
+ n.Op.Phase, n.Op.ProbingSince = "probing", w.now
+ }
+ return ok
+ }
+ if r := op.Receipt; r != nil {
+ mine := r.Box == b.ID && r.Stamp == op.InstallStamp
+ if !mine && !on("reloc-install-receipt") {
+ w.cas(c, probing) // the mutation: any receipt will do, the install is skipped
+ return
+ }
+ if mine {
+ if w.ensureLocal(b, c) {
+ w.cas(c, probing)
+ }
+ return
+ }
+ }
+ if op.Exec != b.ID || !w.localInstall(b, c) {
+ return
+ }
+ w.cas(c, func(n *claim) bool {
+ ok := sameOp(n.Op.ID, op.ID) && n.Op.Kind == "relocating" && n.Op.Phase == "installed" && n.Op.Exec == b.ID && n.Op.InstallStamp == op.InstallStamp && !preparedOpened(n)
+ if ok {
+ n.Op.Receipt = &receiptEntry{Op: op.ID, Box: b.ID, Stamp: op.InstallStamp}
+ }
+ return ok
+ })
+}
+
+// ensureLocal is EnsureLocal (1b-next rev 15 finding 2): before P's first
+// admission the executor's local install must be whole, so it is
+// verified before the probing CAS and before every attempt, and a
+// retired one (the scoped cleanup of a lost controller lease retires an
+// unopened P's local install, role()) is restored under the same
+// install_stamp. It never touches an opened P. It reports whether the
+// install is whole now. The mutation goes on without verifying, so P's
+// first admission can meet a missing install.
+func (w *world) ensureLocal(b *box, c *claim) bool {
+ op := c.Op
+ if preparedOpened(c) || !on("reloc-ensure-local") {
+ return true
+ }
+ if b.Files != nil && b.Files.Gen == op.Prepared && b.Files.Done && b.receipt != nil && b.receipt.Op == op.ID && b.receipt.Stamp == op.InstallStamp {
+ return true
+ }
+ if w.localInstall(b, c) {
+ w.stats["local install restored before the first admission"]++
+ w.logf("relocation %s: box %d restored its retired local install under stamp %d", op.ID, b.ID, op.InstallStamp)
+ return true
+ }
+ return false
+}
+
+// verifyReceipt is VerifyReceipt (1b-next rev 16 finding 1): once P is
+// opened the local install is never remade, and before every attempt the
+// box's durable receipt (its install journal) must still be the one the
+// claim journaled; a missing or different one marks the operation stuck
+// and nothing is admitted. Files, env and timers the admitted writers
+// changed are never compared. The mutation goes on to the next attempt.
+func (w *world) verifyReceipt(b *box, c *claim) bool {
+ op := c.Op
+ if r := b.receipt; r != nil && r.Op == op.ID && r.Box == b.ID && r.Stamp == op.InstallStamp {
+ return true
+ }
+ if !on("reloc-verify-receipt") {
+ w.stats["receipt missing after P opened, attempt made anyway (mutation)"]++
+ return true
+ }
+ w.markStuck(c, fmt.Sprintf("box %d's local install receipt is missing after P was admitted", b.ID))
+ return false
+}
+
+// preparedOpened is PreparedOpened: an admission has named P (B2-5). The
+// admission that opens P journals prepared_opened in the same CAS
+// (admitCommit), so the fact outlives holder.admissions' trim to eight
+// (1b-next rev 12 S1; rule reloc-prepared-opened-journal); the mutation
+// reads the retained admissions alone, as rev 11 did.
+func preparedOpened(c *claim) bool {
+ if c.Op.Prepared == "" || c.Holder == nil {
+ return false
+ }
+ if on("reloc-prepared-opened-journal") && c.Op.PreparedOpened == c.Op.Prepared {
+ return true
+ }
+ for _, e := range c.Holder.Admissions {
+ if e.Gen == c.Op.Prepared {
+ return true
+ }
+ }
+ return false
+}
+
+// relocProbing: each attempt is counted in the claim before it is made
+// (BeginProbeAttempt, ruling 19; rule reloc-probe-attempts: a crash, a
+// lost response or a restart never buys a fourth), then one cold
+// AdmitWriter by op.exec into P (the first) or a fresh generation
+// restored from the previous attempt's (claim §6.4a; spawn and admitWriter
+// do both), then the probe. The fourth is refused and the target enters
+// probe-failed, as it does past the probe deadline. Before P's first
+// admission the local install is verified and restored (ensureLocal);
+// after it, the receipt alone is verified (verifyReceipt) and the install
+// is never remade (rule reloc-no-reinstall; its mutation reapplies the
+// pinned wake state on every agent restart, as rev 4.2's install marker
+// did, over the timers the admitted session registered).
+func (w *world) relocProbing(b *box, c *claim) {
+ op, h := c.Op, c.Holder
+ failed := func(n *claim) bool {
+ ok := sameOp(n.Op.ID, op.ID) && n.Op.Kind == "relocating" && n.Op.Phase == "probing" && n.Op.Exec == op.Exec
+ if ok {
+ n.Op.Phase, n.Op.FailedAt, n.Op.Release = "probe-failed", w.now, nil
+ }
+ return ok
+ }
+ if op.Exec != b.ID {
+ if w.now > op.ProbingSince+probeDeadline && op.Exec >= 0 {
+ w.stats["probe-failed: deadline"]++
+ w.cas(c, failed) // the worker's: ToProbeFailed past the probe deadline
+ }
+ return
+ }
+ if b.Row == nil || b.Row.Status == "ready" {
+ w.holdRow(b, "relocating", op.ID, c)
+ }
+ opened := preparedOpened(c)
+ if !opened {
+ if !w.ensureLocal(b, c) {
+ return
+ }
+ } else if !w.verifyReceipt(b, c) {
+ return
+ }
+ if !on("reloc-no-reinstall") && opened && b.installEpoch != b.Epoch {
+ b.Timers = append([]int(nil), w.relocTimers(c)...) // the mutation: the install marker re-applied after a restart
+ b.installEpoch = b.Epoch
+ w.stats["local install remade after admission (mutation)"]++
+ }
+ if !w.admits(b, c, op.ID) {
+ return
+ }
+ if b.HasKey {
+ b.Config, b.CfgVer, b.Live, b.LiveInc = h.Inc, w.cfgVer[h.App], h.App, h.Inc
+ }
+ probed := func(n *claim) bool {
+ ok := sameOp(n.Op.ID, op.ID) && n.Op.Phase == "probing" && n.Op.Exec == b.ID
+ if ok {
+ n.Op.Phase = "probed"
+ }
+ return ok
+ }
+ if hasMain(b) {
+ w.probeAccepted(b, c)
+ w.cas(c, probed)
+ return
+ }
+ if w.now > op.ProbingSince+probeDeadline {
+ w.stats["probe-failed: deadline"]++
+ w.cas(c, failed)
+ return
+ }
+ tag := fmt.Sprintf("%s/%d", op.ID, op.Attempts)
+ if b.open == nil {
+ // a new attempt: counted before it is made. attemptTag is the
+ // attempt this agent counted (tag) or made (tag+"+"); one made and
+ // ended, or none counted, is counted now
+ if on("reloc-probe-attempts") && b.attemptTag != tag {
+ if op.Attempts >= probeTries {
+ w.stats["probe-failed: attempts"]++
+ w.cas(c, failed)
+ return
+ }
+ if w.cas(c, func(n *claim) bool {
+ ok := sameOp(n.Op.ID, op.ID) && n.Op.Phase == "probing" && n.Op.Exec == b.ID && n.Op.Attempts == op.Attempts
+ if ok {
+ n.Op.Attempts++
+ }
+ return ok
+ }) {
+ b.attemptTag = fmt.Sprintf("%s/%d", op.ID, op.Attempts+1)
+ }
+ return
+ }
+ if !on("reloc-probe-attempts") && op.ProbeTries >= probeTries {
+ w.stats["probe-failed: attempts"]++
+ w.cas(c, failed) // the mutation: failures counted after the fact, as rev 1 did
+ return
+ }
+ }
+ if b.open == nil {
+ b.attemptTag = tag + "+" // made now
+ }
+ if w.spawn(b, c, op.Prepared, true) {
+ w.probeAccepted(b, c)
+ w.cas(c, probed)
+ }
+}
+
+// relocProbeFailed: the live target runs its own release sequence (§5.8
+// probe-failed; JournalRelease), then a worker starts the nested
+// relocation from pinning (PinAfterRelease with a next target), pinned to
+// at least the target's final TXID (the release entry, which
+// relocPinning reads), the failed target excluded and counted as a
+// replacement. Exhaustion is checked before a replacement is looked for
+// (1b-next R1-16): with the replacements used the operation is stuck. A
+// target that cannot finish its release within releaseDeadline goes to
+// stuck (ruling 14): nothing moves away from a live box without its stop
+// evidence. With no eligible box for releaseDeadline the operation is
+// stuck too (model ruling 14: 1b-next waits for a spare with no bound,
+// and in a two-box region the source is never a spare).
+func (w *world) relocProbeFailed(b *box, c *claim) {
+ op, h := c.Op, c.Holder
+ if op.Release == nil || op.Release.Box != op.Exec {
+ if on("reloc-release-deadline") && w.now > op.FailedAt+releaseDeadline {
+ w.markStuck(c, fmt.Sprintf("box %d cannot finish its release sequence", op.Exec))
+ return
+ }
+ if b.ID != op.Exec {
+ return
+ }
+ r := w.relocRelease(b, c)
+ if r == nil {
+ return
+ }
+ if w.cas(c, func(n *claim) bool {
+ ok := sameOp(n.Op.ID, op.ID) && n.Op.Kind == "relocating" && n.Op.Phase == "probe-failed" && n.Op.Exec == b.ID && (n.Op.Release == nil || n.Op.Release.Box != b.ID)
+ if ok {
+ n.Op.Release = r
+ }
+ return ok
+ }) {
+ w.stats["release journaled: failed target"]++
+ }
+ return
+ }
+ if on("reloc-replacement-cap") && op.Replacements >= maxReplacements {
+ w.markStuck(c, fmt.Sprintf("two replacements of the target used; a third was needed at %s", op.Phase))
+ return
+ }
+ next := w.chooseBoxExcept(op.SrcRegion, h.App, relocExcept(op, op.Exec)...)
+ if next == nil {
+ if w.now > op.FailedAt+releaseDeadline {
+ w.markStuck(c, "no eligible box for the nested relocation")
+ }
+ return
+ }
+ w.cas(c, func(n *claim) bool {
+ if !sameOp(n.Op.ID, op.ID) || n.Op.Kind != "relocating" || n.Op.Phase != "probe-failed" || n.Op.Release == nil || n.Op.Release.Box != n.Op.Exec {
+ return false
+ }
+ if !w.nameReplacement(n, next.ID, "pinning") {
+ return n.Op.Stuck != "" // stuck: the CAS records it
+ }
+ n.Op.Exec = -1
+ n.Op.Pin, n.Op.Prepared, n.Op.Receipt = nil, "", nil
+ n.Op.BaseKey, n.Op.BaseVer, n.Op.BaseTX = "", 0, 0
+ n.Op.ProbeTries, n.Op.Attempts = 0, 0
+ w.stats["nested relocation after probe-failed"]++
+ return true
+ })
+}
+
+// relocSettle is the settle window and the open (rev 7.20's steps, kept):
+// a probe that died in its window is restarted, cold, from its own
+// generation; then the row opens and the operation is released to
+// serving (CompleteRelocation), where the leftovers' park-local chores
+// are queued (release()).
+func (w *world) relocSettle(b *box, c *claim) {
+ op := c.Op
+ if op.Exec != b.ID {
+ return
+ }
+ switch op.Phase {
+ case "probed":
+ if b.open != nil {
+ return
+ }
+ if !hasMain(b) {
+ w.stats["probe restarted"]++
+ w.cas(c, func(n *claim) bool {
+ ok := sameOp(n.Op.ID, op.ID) && n.Op.Phase == "probed"
+ if ok {
+ n.Op.Phase = "probing"
+ }
+ return ok
+ })
+ return
+ }
+ if w.openRow(b, op.ID) {
+ w.cas(c, func(n *claim) bool {
+ ok := sameOp(n.Op.ID, op.ID) && n.Op.Phase == "probed"
+ if ok {
+ n.Op.Phase = "opened"
+ }
+ return ok
+ })
+ }
+ case "opened":
+ w.release(c, b.ID) // outstanding disjoint parks do not block serving (claim rev 6.28 §4)
+ }
+}
+
+// scopedCleanup is the relocation controller's scoped cleanup when its
+// lease was lost (1b-next rev 14 finding 1, Task 7's live): an unopened
+// P's local install is retired and its receipt (the install journal)
+// kept, so EnsureLocal restores it before the first admission. role()
+// calls it when the executor's execution lease expired before it renewed
+// it (a freeze, a pause, a partition longer than the TTL).
+func (w *world) scopedCleanup(b *box, c *claim) {
+ if c == nil || c.Holder == nil || c.Op.Kind != "relocating" || c.Op.Exec != b.ID || preparedOpened(c) {
+ return
+ }
+ if f := b.Files; f != nil && f.Gen == c.Op.Prepared && f.Gen != "" {
+ w.retireArtifacts(b, c.Holder.Inc, f.Stamp)
+ w.stats["relocation controller lost: unopened local install retired"]++
+ w.logf("box %d: relocation %s's controller lease was lost; the scoped cleanup retired its unopened local install", b.ID, c.Op.ID)
+ }
+}
+
+// twoBoxStep is the two-box shape's extra step: a drain now and then
+// during the chaos (Task 3 adds termination, enrollment and replacement
+// launches). It draws only in the two-box shape.
+func (w *world) twoBoxStep() {
+ if !w.calm && w.rng.Intn(60) == 0 {
+ w.userRelocate()
+ }
+}
diff --git a/internal/sim/hostlife/regionha_witness_test.go b/internal/sim/hostlife/regionha_witness_test.go
new file mode 100644
index 000000000..82ffbceb9
--- /dev/null
+++ b/internal/sim/hostlife/regionha_witness_test.go
@@ -0,0 +1,53 @@
+package hostlife
+
+import "testing"
+
+// twoBoxWitness is newWitness with a second enrolled box in every region.
+func twoBoxWitness() *world {
+ w := newWitness()
+ w.perRegion = 2
+ for r := 0; r < nRegions; r++ {
+ w.addBox(r)
+ }
+ return w
+}
+
+// TestDrainEndToEnd: a serving host is drained from box 0 to box 3 in
+// region 0 through every phase of §5.8's table; the host serves on box 3
+// with every acknowledged write and timer, box 0's installation is
+// retired by its park-local, and the first probe admission's coverage is
+// released (no writes_lost declared, L9).
+func TestDrainEndToEnd(t *testing.T) {
+ w := twoBoxWitness()
+ from, to := w.boxes[0], w.boxes[3]
+ w.serve(from, 1, app0)
+ w.reach(t, 50, "the host runs on box 0", func() bool { return hasMain(from) }, w.actAll(), func() { w.wake(from) })
+ w.appWrite(from)
+ w.nextW++
+ from.Timers = append(from.Timers, w.nextW)
+ w.acks = append(w.acks, ack{W: w.nextW, Inc: 1, Box: from.ID, Session: w.claim.Holder.Session, At: w.now, Kind: "timer"})
+ w.userRelocate()
+ if c := w.claim; c.Op.Kind != "relocating" || c.Op.Src != from.ID || c.Op.Tgt != to.ID || c.Op.Phase != "starting" {
+ t.Fatalf("the drain did not start: %s", w.state())
+ }
+ seen := map[string]bool{}
+ w.reach(t, 1500, "serving on box 3", func() bool {
+ seen[w.claim.Op.Phase] = true
+ return w.claim.Op.Kind == "serving" && w.claim.Op.Exec == to.ID
+ }, w.actAll(), w.recoveryPass, func() { w.wake(to) })
+ for _, p := range []string{"starting", "releasing", "pinning", "installing", "installed", "probing", "probed", "opened"} {
+ if !seen[p] {
+ t.Errorf("phase %s never observed", p)
+ }
+ }
+ 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 len(w.violations) > 0 {
+ t.Fatalf("%s", w.violations[0])
+ }
+ if from.DB != nil || from.Files != nil || from.Row != nil {
+ t.Errorf("box 0 still holds local state after its park-local: db=%v files=%v row=%v", from.DB != nil, from.Files != nil, from.Row)
+ }
+}
diff --git a/internal/sim/hostlife/rules_test.go b/internal/sim/hostlife/rules_test.go
index a4f337d18..545acade9 100644
--- a/internal/sim/hostlife/rules_test.go
+++ b/internal/sim/hostlife/rules_test.go
@@ -145,5 +145,27 @@ var allRules = []string{
"config-before-probe", // L3 (the kpmg outage)
"recovery-current-inputs", // rev 6 §7.7 (J2-R2-5): a recovery probe is not bound to the move's pinned inputs
// region HA (two boxes per region, L18)
- "create-choice-once", // region HA §5.2, claim P5-D2/P5-D6: the create's executor is chosen once and recorded in the intent; recovery never substitutes, it cancels a create whose box is gone
+ "create-choice-once", // region HA §5.2, claim P5-D2/P5-D6: the create's executor is chosen once and recorded in the intent; recovery never substitutes, it cancels a create whose box is gone
+ "reloc-start-guard", // region HA §5.8, claim §4 CC11 as L11 amends it (plan 1b-next RelocationStartGuard): a park-generation in the region never blocks a relocation start; a park-replica in the region and a park-local on the target or a live source do
+ "reloc-exec-ack-barrier", // claim D6, region HA §5.8 (requireAcks): every participant's execution lease is current before the operation leaves starting or hands op.exec to the target
+ "reloc-release-first", // region HA §5.8 releasing, A3-2 (PinAfterRelease): pinning cites the source's journaled release; the mutation pins while the source still runs
+ "reloc-pin-reaches-release", // region HA §5.8 (JournalPin): a pin after a release reaches its final_txid; the mutation pins the listing as it stands
+ "reloc-failover-pin-delay", // region HA §5.8 (JournalPin, FailoverPinDelay): a failover pins no earlier than the fence's observed_at plus 30 s; a loss bound, not a safety bound (expected miss)
+ "reloc-exec-only-installs", // region HA §5.8 Exclusion, HA2: only op.exec builds P and makes the local install; the mutation lets every box of the region materialize
+ "reloc-install-receipt", // region HA §5.8 B1-2 (RecordLocalInstall, ToProbing): probing needs a receipt for exactly op.exec and install_stamp; the mutation lets a replacement inherit its predecessor's and skip its install
+ "reloc-no-reinstall", // region HA §5.8 B2-5 (RecordLocalInstall after preparedOpened): after P's first admission the local install is never remade; the mutation reapplies the pinned wake state on every agent restart
+ "reloc-released-coverage", // claim §6.4a item 2, L9 (AdmitWriter): released only on the admission opening P whose predecessor is exactly the flushed release's box and session and whose pin reached final_txid; the mutation grants it to every first opening of P, a failover's included
+ "reloc-row-cases", // region HA §5.3, L12 (hostbox.RelocationRow): the former executor's row is held once its admission fence closed; the mutation reopens it as a stale hold (an admission fence: caught with exec-admission and its partners)
+ "reloc-replacement-cap", // region HA §5.8 (replaceTargetSlot, MaxTargetReplacements): a third replacement of the target marks the operation stuck; an operator bound (expected miss)
+ "reloc-enrolled-only", // region HA §2, HA7 (eligibleBoxes): an unenrolled reference is never chosen as a target; Task 3 gives it its witness
+ // plan 1b-next rev 16's additions to the phase table (rev 2 of this plan)
+ "reloc-drain-needs-writer", // 1b-next ruling 11 (Worker.Start): a host that never admitted a writer is never drained, only failed over; liveness (expected miss)
+ "reloc-ack-before-pinning", // 1b-next rev 4 N6 (PinAfterRelease requires requireAcks from releasing): a target replaced in releasing acknowledges before the operation leaves the phase; defence in depth (expected miss)
+ "reloc-pin-claim-gen", // 1b-next ruling 16 (JournalPin, RecoveryPinKey pin-<gen>.json): a pin is journaled only against the claim version it was selected against; the mutation journals a pin selected before a nested reset
+ "reloc-pin-evidenced-empty", // 1b-next ruling 15 (JournalPin, StorePinner's Empty evidence): an empty pin needs a release flushed at 0 or a holder that never had a writer; otherwise stuck for an operator (expected miss: the model's listings are exact and the probe declares)
+ "reloc-release-deadline", // 1b-next ruling 14 (Worker.releaseOverdue, ReleaseDeadline): a release not journaled 10 minutes after releasing or probe-failed began marks the operation stuck; the mutation waits forever (INV-3)
+ "reloc-probe-attempts", // 1b-next ruling 19 (BeginProbeAttempt, MaxProbeAttempts): each probe attempt is counted in the claim before it is made, the fourth is probe-failed; liveness (expected miss)
+ "reloc-ensure-local", // 1b-next rev 15 finding 2 (Effects.EnsureLocal): before P's first admission the local install is verified, and restored under the same install_stamp if a lost lease's scoped cleanup retired it; the mutation admits over a missing install
+ "reloc-verify-receipt", // 1b-next rev 16 finding 1 (Effects.VerifyReceipt, MarkStuck in probing): after P opens, a missing or different receipt marks the operation stuck before any further admission; the mutation makes the attempt anyway
+ "reloc-prepared-opened-journal", // 1b-next rev 12 S1 (prepared_opened, PreparedOpened): P's opening is journaled with its admission and outlives holder.admissions' trim; the mutation reads the trimmed list and remakes the install after P opened
}
diff --git a/internal/sim/hostlife/sim_test.go b/internal/sim/hostlife/sim_test.go
index fbe5f8e62..92813d585 100644
--- a/internal/sim/hostlife/sim_test.go
+++ b/internal/sim/hostlife/sim_test.go
@@ -27,7 +27,7 @@ func newWorld(seed int64, verbose bool) *world {
w.fail[f] = w.rng.Intn(2) == 0
}
for r := 0; r < nRegions; r++ {
- b := &box{ID: r, Region: r, HasKey: r == 0 || w.rng.Intn(4) != 0, Skew: w.rng.Intn(3) - 1, Nested: w.rng.Intn(2) == 0}
+ b := &box{ID: r, Region: r, HasKey: r == 0 || w.rng.Intn(4) != 0, Skew: w.rng.Intn(3) - 1, Nested: w.rng.Intn(2) == 0, Enrolled: true}
if r != 0 && w.rng.Intn(4) == 0 {
b.FailApp = true
}
@@ -49,7 +49,7 @@ func newWorld(seed int64, verbose bool) *world {
// region, drawn after every one-box draw of this world, so the one-box
// stream is untouched; id nRegions+r, as addBox gives a witness
for r := 0; r < nRegions && w.perRegion > 1; r++ {
- b := &box{ID: nRegions + r, Region: r, HasKey: w.rng.Intn(4) != 0, Skew: w.rng.Intn(3) - 1, Nested: w.rng.Intn(2) == 0}
+ b := &box{ID: nRegions + r, Region: r, HasKey: w.rng.Intn(4) != 0, Skew: w.rng.Intn(3) - 1, Nested: w.rng.Intn(2) == 0, Enrolled: true}
if w.rng.Intn(4) == 0 {
b.FailApp = true
}
@@ -149,6 +149,9 @@ func (w *world) step() {
}
}
w.runStalled()
+ if w.perRegion > 1 {
+ w.twoBoxStep() // the two-box shape's own draws, after the one-box ones (ruling 1)
+ }
bs := w.liveBoxes()
b := bs[w.rng.Intn(len(bs))]
n := w.rng.Intn(100)
@@ -388,6 +391,14 @@ func (w *world) checkStep() {
if c := w.claim; c != nil && c.Op.Kind == "reverting" && c.Op.RevPhase == "stuck" {
w.violate("stuck: source could not revert %s", c.Op.ID)
}
+ // INV-27 (region HA HA1, HA7): while relocating, op.exec is none or an
+ // 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) {
+ w.violate("INV-27: relocation %s names box %d as op.exec, which is unenrolled or lost", c.Op.ID, c.Op.Exec)
+ }
+ }
}
func (w *world) boxesState() string {
diff --git a/internal/sim/hostlife/twobox_test.go b/internal/sim/hostlife/twobox_test.go
index 5b6de6032..e54a6cf30 100644
--- a/internal/sim/hostlife/twobox_test.go
+++ b/internal/sim/hostlife/twobox_test.go
@@ -40,7 +40,7 @@ func (w *world) regionBoxes(r int) []*box {
// key held, no faults, id nRegions+r (the sweep's second boxes carry the
// same ids; replacements are 100 and up).
func (w *world) addBox(r int) *box {
- b := &box{ID: nRegions + r, Region: r, HasKey: true}
+ b := &box{ID: nRegions + r, Region: r, HasKey: true, Enrolled: true, DeleteOnTermination: true}
b.forget()
w.boxes = append(w.boxes, b)
w.logf("witness: box %d enrolled in region %d", b.ID, r)
@@ -87,17 +87,23 @@ func (w *world) owesLocal(c *claim, b *box) bool {
}
// chooseBox is region HA §5.2's choose() (H12, L8; a move's target under
-// L15): among the eligible boxes of region r (§2: live, running the
-// claim's executable, holding the secrets key, not on lost, not owing a
-// park-local for the host), prefer one running no instance of app, then
-// the fewest hosts, then the greatest tieHash. With one box in the region
-// it is that box, as today (spec §4). It is a pure function of the world;
-// the caller records the choice in the claim's intent and never
+// L15) with nothing excluded.
+func (w *world) chooseBox(r int, app string) *box { return w.chooseBoxExcept(r, app) }
+
+// chooseBoxExcept is choose() over the region's eligible boxes minus
+// except (a relocation's source, its replaced targets): among the
+// eligible boxes of region r (§2: live, running the claim's executable,
+// holding the secrets key, not on lost, not owing a park-local for the
+// host, enrolled: an unenrolled reference is never eligible, HA7; rule
+// reloc-enrolled-only, Task 3), prefer one running no instance of app,
+// then the fewest hosts, then the greatest tieHash. With one box in the
+// region it is that box, as today (spec §4). It is a pure function of the
+// world; the caller records the choice in the claim's intent and never
// substitutes (rule create-choice-once).
-func (w *world) chooseBox(r int, app string) *box {
+func (w *world) chooseBoxExcept(r int, app string, except ...int) *box {
bs := w.regionBoxes(r)
if len(bs) <= 1 {
- if len(bs) == 0 {
+ if len(bs) == 0 || contains(except, bs[0].ID) {
return nil
}
return bs[0]
@@ -106,7 +112,10 @@ func (w *world) chooseBox(r int, app string) *box {
var best *box
var bestKey [3]int
for _, b := range bs {
- if b.Old || !b.HasKey || (c != nil && contains(c.Lost, b.ID)) || w.owesLocal(c, b) {
+ if contains(except, b.ID) || b.Old || !b.HasKey || (c != nil && contains(c.Lost, b.ID)) || w.owesLocal(c, b) {
+ continue
+ }
+ if on("reloc-enrolled-only") && !b.Enrolled {
continue
}
key := [3]int{w.hostsOn(b, app), w.hostsOn(b, ""), -int(tieHash(b.ID))}
diff --git a/internal/sim/hostlife/witness_test.go b/internal/sim/hostlife/witness_test.go
index 94a4f5c7c..88394c375 100644
--- a/internal/sim/hostlife/witness_test.go
+++ b/internal/sim/hostlife/witness_test.go
@@ -350,7 +350,7 @@ func newWitness() *world {
control: newBucket(), delivered: map[int]bool{}, durable: map[string]map[int]bool{}, writeInc: map[int]int{}, txs: map[int]tx{}, legacyIncs: map[int]bool{}, purgeOp: map[string]string{}, genParent: map[string]string{}, markerAlerted: map[string]bool{}, execLease: map[int]execLease{}, fail: map[string]bool{}, stats: map[string]int{}}
for r := 0; r < nRegions; r++ {
w.buckets[r] = newBucket()
- b := &box{ID: r, Region: r, HasKey: true}
+ b := &box{ID: r, Region: r, HasKey: true, Enrolled: true, DeleteOnTermination: true}
b.forget()
w.boxes = append(w.boxes, b)
}
diff --git a/internal/sim/hostlife/world_test.go b/internal/sim/hostlife/world_test.go
index ef69ba791..f945e1f42 100644
--- a/internal/sim/hostlife/world_test.go
+++ b/internal/sim/hostlife/world_test.go
@@ -359,6 +359,21 @@ type box struct {
FailArchive bool // the final archive fails (too large) on this box
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
+ 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
+ installEpoch int // the agent process that made this box's local install for a relocation (B2-5): a later process never remakes it once an admission named P
+ // receipt is the box's install journal for a relocation (1b-next Task 8c,
+ // VerifyReceipt): durable, it survives an agent restart; a park of the
+ // installation removes it, and so does a lost volume (a witness)
+ receipt *receiptEntry
+ // attemptTag is the probe attempt this agent process has counted and
+ // not yet ended (memory: a restart forgets it, and the next attempt is
+ // counted again, ruling 19)
+ attemptTag string
Row *row
DB *localDB
@@ -558,6 +573,7 @@ func (b *box) forget() {
b.mem = map[string]bool{}
b.evidAt = map[string]int{}
b.pendingTimers = nil
+ b.attemptTag = ""
if b.DB != nil {
b.DB.InFlight = nil // the upload's client is gone; the restarted replica uploads the same file again
// a writer that was draining before its clean close is gone with
@@ -781,6 +797,27 @@ type opState struct {
NewRegion int
NewSerial int
NewBox int // the executor a create named once (region HA §5.2, H12): never substituted
+ // region HA relocation (spec 1 §5.8; claim rev 6.30 §4 L1). The
+ // journal entries below are what the claim's op.journal carries
+ RelocReason string // drain or failover
+ FenceAt int // fence.<box>.observed_at of the latest fence the operation cites; 0 none
+ FailedAt int // when the target entered probe-failed
+ Release *releaseEntry // the release sequence's journal entry (§5.8): the source's in releasing, a failed target's in probe-failed
+ Pin *pinEntry // the pinned recovery set
+ Prepared string // P, the prepared generation this installation builds; "" before installing
+ InstallStamp int // the stamp of the CAS that handed op.exec to the current target (op.journal.install_stamp)
+ Receipt *receiptEntry // the executor's local install receipt (local_install)
+ ProbingSince int
+ Replacements int // targets replaced in this operation; two, then stuck
+ Excluded []int // replaced targets, never named again for this host
+ InstalledOn []int // every box this operation handed op.exec for an installation: each owes a park-local at serving unless discharged
+ Discharged []int // fenced boxes whose park-local chores the fence CAS discharged (L3, H19)
+ Stuck string
+ // 1b-next rev 16's journal additions
+ ReleasingSince int // releasing_since: the release deadline's start (ruling 14)
+ 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
// journal
ReportAt int
@@ -859,6 +896,50 @@ type opState struct {
BaseVer int
}
+// releaseEntry is §5.8's release journal entry: the box, generation and
+// session that gave the host up, its stopped database's final TXID (the
+// listing shows it before pinning may cite it), and, until Task 4's files
+// manifest, the files directory and wake state the box published. Flushed
+// is false when the session's replicator was gone (an agent restart) and
+// the entry names what the remote held: released coverage never applies
+// to it, and the next admission declares the rest.
+type releaseEntry struct {
+ Box, Session int
+ Gen string
+ FinalTX int
+ ManifestSeq int
+ Flushed bool
+ Files *filesDir
+ Timers []int
+ At int
+}
+
+// pinEntry is §5.8's pinned recovery set: the database position N the
+// build restores to (exact versions in the real pin; the model's build
+// never restores past N), the files manifest version (Task 4), and when
+// the pin was taken (after a release's final_txid is visible, or after a
+// fence's observed_at plus failoverPinDelay).
+type pinEntry struct {
+ Gen string // the generation the pin reads (genselect over the admitted chain)
+ TX int
+ ManKey string
+ ManVer, ManSeq int
+ At int
+ ClaimVer int // the claim version it was selected against (1b-next ruling 16: pin-<gen>.json)
+ // Files and Timers are the files set the pin was taken with, until
+ // Task 4's manifest: the release's, or a failover's stand-in
+ Files *filesDir
+ Timers []int
+}
+
+// receiptEntry is the local install receipt (§5.8 local_install): the
+// box and the install_stamp of the CAS that handed it op.exec. A
+// replacement executor never inherits its predecessor's.
+type receiptEntry struct {
+ Op string
+ Box, Stamp int
+}
+
type digest struct {
Writes string
Files string
@@ -1122,6 +1203,25 @@ func (c *claim) clone() *claim {
}
n.Op.Parts = append([]int(nil), c.Op.Parts...)
n.Op.StopFiles = c.Op.StopFiles.clone()
+ n.Op.Excluded = append([]int(nil), c.Op.Excluded...)
+ n.Op.InstalledOn = append([]int(nil), c.Op.InstalledOn...)
+ n.Op.Discharged = append([]int(nil), c.Op.Discharged...)
+ if r := c.Op.Release; r != nil {
+ cp := *r
+ cp.Files = r.Files.clone()
+ cp.Timers = append([]int(nil), r.Timers...)
+ n.Op.Release = &cp
+ }
+ if p := c.Op.Pin; p != nil {
+ cp := *p
+ cp.Files = p.Files.clone()
+ cp.Timers = append([]int(nil), p.Timers...)
+ n.Op.Pin = &cp
+ }
+ if r := c.Op.Receipt; r != nil {
+ cp := *r
+ n.Op.Receipt = &cp
+ }
if c.Holder != nil {
n.Holder.Admissions = append([]admissionRecord(nil), c.Holder.Admissions...)
for i := range n.Holder.Admissions {