| index 4627712c5..66f63b268 100644 |
| --- a/internal/sim/hostlife/regionha_test.go |
| +++ b/internal/sim/hostlife/regionha_test.go |
| @@ -987,11 +987,432 @@ func (w *world) scopedCleanup(b *box, c *claim) { |
| } |
| } |
| |
| -// 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. |
| +// ---------- termination, enrollment and the fence (region HA §5.9; H1, H10, H11, H16, H17, H19) ---------- |
| + |
| +// terminate is the cloud terminating a box (H1): nothing on it runs |
| +// again, it never returns (a stopped box may; heal skips a terminated |
| +// one), and the requests it issued still complete at their own time, |
| +// which is the late-PUT-after-termination case. The two-box step draws |
| +// it; it never leaves the world without an enrolled live box, since H17's |
| +// cross-region confirmer must exist for a replacement to enroll. |
| +func (w *world) terminate(b *box) { |
| + if b.Destroyed { |
| + return |
| + } |
| + enrolled := 0 |
| + for _, x := range w.liveBoxes() { |
| + if x.Enrolled && x != b { |
| + enrolled++ |
| + } |
| + } |
| + if enrolled == 0 { |
| + return |
| + } |
| + b.Destroyed, b.Terminated, b.TerminatedAt = true, true, w.now |
| + b.Procs, b.plans = nil, nil |
| + w.stats["terminated"]++ |
| + w.logf("box %d terminated by the cloud (region %d)", b.ID, b.Region) |
| +} |
| + |
| +// launchReplacements: the group keeps the region at its minimum (H5): a |
| +// replacement launches replaceDelay steps after the termination that left |
| +// the region short, unenrolled (H16), with its volume flag drawn (two-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 { |
| + continue |
| + } |
| + last := 0 |
| + for _, b := range w.boxes { |
| + if b.Region == r && b.Terminated && b.TerminatedAt > last { |
| + last = b.TerminatedAt |
| + } |
| + } |
| + if last == 0 || w.now < last+replaceDelay { |
| + continue |
| + } |
| + w.nextID++ |
| + nb := &box{ID: 100 + w.nextID, Region: r, HasKey: true, EnrollAt: w.now, DeleteOnTermination: w.rng.Intn(8) != 0} |
| + nb.forget() |
| + w.boxes = append(w.boxes, nb) |
| + w.stats["replacements launched"]++ |
| + w.logf("box %d launched in region %d, unenrolled", nb.ID, r) |
| + } |
| +} |
| + |
| +// enrollStep is automatic enrollment (H16, L19): a launched box's boxid |
| +// evidence verifies and an enrolled box confirms its group membership |
| +// enrollDelay steps after launch. Any enrolled box of any region may |
| +// confirm (H17: the first box of an emptied region is confirmed from |
| +// another region); with none, nothing enrolls. |
| +func (w *world) enrollStep() { |
| + confirmer := false |
| + for _, b := range w.liveBoxes() { |
| + if b.Enrolled { |
| + confirmer = true |
| + } |
| + } |
| + if !confirmer { |
| + return |
| + } |
| + for _, b := range w.liveBoxes() { |
| + if !b.Enrolled && w.now >= b.EnrollAt+enrollDelay { |
| + b.Enrolled = true |
| + w.stats["boxes enrolled automatically"]++ |
| + w.logf("box %d enrolled (region %d)", b.ID, b.Region) |
| + } |
| + } |
| +} |
| + |
| +// twoBoxStep is the two-box shape's extra step (ruling 1): replacements |
| +// launch and enroll; during the chaos a box is terminated now and then, |
| +// and a drain is asked for now and then. |
| func (w *world) twoBoxStep() { |
| + w.launchReplacements() |
| + w.enrollStep() |
| + if !w.calm && w.fail["terminate"] && w.rng.Intn(200) == 0 { |
| + bs := w.liveBoxes() |
| + if b := bs[w.rng.Intn(len(bs))]; w.regionHAOwnsLoss(b) { |
| + w.terminate(b) |
| + } |
| + } |
| if !w.calm && w.rng.Intn(60) == 0 { |
| w.userRelocate() |
| } |
| } |
| + |
| +// regionHAOwnsLoss: the loss of b is region HA's to recover (model ruling |
| +// 15): the claim holds the host and names b, if at all, only as a serving |
| +// executor, a relocation's participant or a chore's owner; a box holding |
| +// a legacy host's state before its adoption is never terminated. A participant of a move, |
| +// a landing, a rollback, a revert, a push, a create or a delete is |
| +// recovered from a lost box by moves' and the claim's declare-lost paths |
| +// (L14), which the model walks for a destroyed box that is stopped and |
| +// may return; the sweep never terminates one. |
| +func (w *world) regionHAOwnsLoss(b *box) bool { |
| + c := w.claim |
| + if c == nil || c.Holder == nil { |
| + return b.Row == nil && b.DB == nil && b.Files == nil // a legacy host not yet adopted is not region HA's |
| + } |
| + switch c.Op.Kind { |
| + case "serving", "relocating": |
| + return true |
| + } |
| + return !(c.Op.Exec == b.ID || contains(c.Op.Parts, b.ID) || c.Op.Src == b.ID || c.Op.Tgt == b.ID || c.Op.NewBox == b.ID) |
| +} |
| + |
| +// fenceStep is the regional worker's termination fence (§5.9; claim L2 |
| +// to L5; Worker.Step's "evidence first"): for a terminated, enrolled box |
| +// of its own region that the claim still names, it writes the fence in |
| +// one CAS (fence). A stopped box is never fenced (rule |
| +// fence-terminated-only: "stopped and stopping do not count, because a |
| +// stopped box can start again with its disk"); the mutation fences any |
| +// destroyed box. An unenrolled box has no roster entry to bind the fence |
| +// to (HA7) and is never fenced. The source's fence is consumed before the |
| +// target's, as Worker.Step orders them. |
| +func (w *world) fenceStep(b *box, c *claim) bool { |
| + if c == nil || !b.Enrolled || contains(c.Lost, b.ID) { |
| + return false |
| + } |
| + var cands []*box |
| + for _, x := range w.boxes { |
| + if x.Region != b.Region || x == b || !x.Destroyed || !x.Enrolled || contains(c.Lost, x.ID) { |
| + continue |
| + } |
| + if !x.Terminated && on("fence-terminated-only") { |
| + continue |
| + } |
| + if !w.claimNames(c, x) { |
| + continue |
| + } |
| + if c.Op.Kind == "relocating" && x.ID == c.Op.Src { |
| + cands = append([]*box{x}, cands...) |
| + } else { |
| + cands = append(cands, x) |
| + } |
| + } |
| + if len(cands) == 0 { |
| + return false |
| + } |
| + before := w.claim.Ver |
| + w.fence(b, c, cands[0]) |
| + return w.claim.Ver != before |
| +} |
| + |
| +// claimNames: the claim gives x a role, so a fence changes it. |
| +func (w *world) claimNames(c *claim, x *box) bool { |
| + if c.Op.Exec == x.ID || contains(c.Op.Parts, x.ID) || c.Op.Kind == "creating" && c.Op.NewBox == x.ID || c.Op.Kind == "moving" && c.Op.Src == x.ID { |
| + return true |
| + } |
| + if c.Op.Kind == "relocating" && (c.Op.Src == x.ID || c.Op.Tgt == x.ID) { |
| + return true |
| + } |
| + for _, o := range c.Obl { |
| + if o.Owner == boxOwner(x.ID) { |
| + return true |
| + } |
| + } |
| + return w.owesLocal(c, x) |
| +} |
| + |
| +// boxOwner is an obligation's owner box:<b> (claim §2): the legacy form a |
| +// regional chore may carry; "" is region:<r>, any eligible worker of the |
| +// region (P6-D5). |
| +func boxOwner(id int) string { return fmt.Sprintf("box:%d", id) } |
| + |
| +// fence is the fence CAS for x, observed terminated by worker b. Moves' |
| +// cases keep their owners: a pre-flip move's source converts (moves |
| +// §7.10, the existing CAS); a move's target before the flip, a landing's |
| +// or a rollback's target are moves' declare-lost path, which this model |
| +// gives the operator (L14); a create's box is cancelled by the recovery |
| +// pass (Task 1). Everything else is one CAS here: the box goes on lost |
| +// with the fence reference and observed_at, its chores are discharged if |
| +// its volume evidence qualifies, its regional work passes to its region, |
| +// and the operation's rule applies (StartRelocation's failover, |
| +// FenceSource, ReplaceTarget, FenceExhaustedTarget). A target with no |
| +// spare to name is fenced on a later pass (Worker.next: "no eligible box |
| +// yet"). |
| +func (w *world) fence(b *box, c *claim, x *box) { |
| + op := c.Op |
| + switch { |
| + case op.Kind == "moving" && op.Src == x.ID: |
| + if on("fence-converts-moving") && !op.Committed && !(w.rec != nil && w.rec.MoveID == op.ID && w.rec.MoveState == "landing") { |
| + w.convertToRelocating(c, x) |
| + } |
| + return |
| + case op.Kind == "moving" && op.Tgt == x.ID, (op.Kind == "landing" || op.Kind == "restoring") && op.Tgt == x.ID, op.Kind == "creating": |
| + return |
| + case op.Kind == "relocating" && op.Stuck != "": |
| + return // Worker.Step consumes no fence of a stuck operation: the operator's resolve does |
| + } |
| + id := op.ID |
| + if w.cas(c, func(n *claim) bool { |
| + if !sameOp(n.Op.ID, id) || n.Op.Kind != op.Kind || contains(n.Lost, x.ID) { |
| + return false |
| + } |
| + switch { |
| + case n.Holder != nil && n.Op.Kind == "serving" && n.Op.Exec == x.ID: |
| + w.startFailover(n, x) |
| + case n.Op.Kind == "relocating" && n.Op.Stuck != "": |
| + return false |
| + case n.Op.Kind == "relocating" && n.Op.Src == x.ID: |
| + w.fenceSource(n, x) |
| + case n.Op.Kind == "relocating" && n.Op.Tgt == x.ID: |
| + if !w.replaceTarget(n, x) { |
| + return false // no spare yet |
| + } |
| + } |
| + w.fenceBox(n, x) |
| + return true |
| + }) { |
| + w.stats["fences written"]++ |
| + w.logf("box %d fenced box %d (terminated at %d) under %s/%s", b.ID, x.ID, x.TerminatedAt, w.claim.Op.Kind, w.claim.Op.ID) |
| + w.declareTimers(x, w.claim.Holder) |
| + } |
| +} |
| + |
| +// fenceBox is plan 1b-next's fenceBox: lost with the fence reference |
| +// (FenceBox, FenceAt); the box's regional work (a park-generation or |
| +// park-replica owned by box:<x>) passed to region:<r> keeping its |
| +// identity (rule fence-reassigns-regional, 1b-next rev 6 finding 2, as |
| +// DeclareLost does for a declared loss); and the box's park-local chores |
| +// discharged only when its volume evidence qualifies (L3, H19: every |
| +// attached volume DeleteOnTermination while it ran); otherwise they stay |
| +// open for the operator path, and nothing about recovery waits on them. |
| +// The mutation of fence-discharge-qualified discharges regardless (INV-26 |
| +// is the oracle); the mutation of fence-reassigns-regional leaves the |
| +// regional work with the dead box, where nothing runs it. |
| +func (w *world) fenceBox(n *claim, x *box) { |
| + n.Lost = addUniq(n.Lost, x.ID) |
| + n.Op.FenceBox, n.Op.FenceAt = x.ID, w.now |
| + var parts []int |
| + for _, p := range n.Op.Parts { |
| + if p != x.ID { |
| + parts = append(parts, p) |
| + } |
| + } |
| + n.Op.Parts = parts |
| + if on("fence-reassigns-regional") { |
| + for i := range n.Obl { |
| + if o := &n.Obl[i]; o.Kind != "park-local" && o.Owner == boxOwner(x.ID) { |
| + o.Owner = "" // region:<r>, the chore's id, operation, retirement and scope kept |
| + w.stats["fence: regional work passed to the region"]++ |
| + } |
| + } |
| + } |
| + qualified := x.DeleteOnTermination |
| + if !on("fence-discharge-qualified") { |
| + qualified = true |
| + } |
| + if !qualified { |
| + w.stats["fence: park-local chores left open (volume evidence)"]++ |
| + return |
| + } |
| + var keep []obligation |
| + for _, o := range n.Obl { |
| + if o.Kind == "park-local" && o.Box == x.ID { |
| + if !x.DeleteOnTermination { |
| + w.violate("INV-26: box %d's park-local chore %s discharged without qualifying volume evidence (§5.9, H19)", x.ID, o.ID) |
| + } |
| + w.stats["fence: park-local chores discharged"]++ |
| + continue |
| + } |
| + keep = append(keep, o) |
| + } |
| + n.Obl = keep |
| + n.Op.Discharged = addUniq(n.Op.Discharged, x.ID) |
| +} |
| + |
| +// declareTimers: the timers acknowledged on a fenced box and not yet |
| +// delivered are declared lost with it and alerted (moves §7.10: no return |
| +// lane carries them; §5.9: the loss record's timer knowledge is partial). |
| +// Task 4 narrows it to the timers its last published manifest does not |
| +// carry. The mutation of fence-declares-timers drops them silently. |
| +func (w *world) declareTimers(x *box, h *holder) { |
| + if h == nil || !on("fence-declares-timers") { |
| + return |
| + } |
| + n := 0 |
| + for i := range w.acks { |
| + a := &w.acks[i] |
| + if a.Box == x.ID && a.Inc == h.Inc && a.Kind == "timer" && !a.Exempt && !w.delivered[a.W] && !w.timerCarried(x, h, a.W) { |
| + a.Exempt = true |
| + n++ |
| + } |
| + } |
| + if n > 0 { |
| + w.stats["timers declared lost"] += n |
| + w.alert("box %d fenced: %d acknowledged timers registered on it are lost with it", x.ID, n) |
| + } |
| +} |
| + |
| +// timerCarried is Task 4's: a landed manifest carries the timer. Before |
| +// the files publisher nothing does. |
| +func (w *world) timerCarried(x *box, h *holder, id int) bool { return false } |
| + |
| +// deadBoxFiles is what a fenced box's files directory contributes to the |
| +// recovery: until Task 4's files publisher, its local directory stands in |
| +// for what it published (L17), as convertToRelocating's does. |
| +func (w *world) deadBoxFiles(x *box) *filesDir { |
| + return x.Files.clone() |
| +} |
| + |
| +// startFailover is the fence's start of a relocation for a serving |
| +// executor (§5.8 reason failover, StartRelocation with a fence; spec 3's |
| +// placer supplies the decision): op.exec none, the stamp kept, at pinning |
| +// with the target named there (ruling 4); the pin waits out |
| +// failoverPinDelay from the fence; deadBoxFiles is the files publisher's |
| +// stand-in until Task 4. |
| +func (w *world) startFailover(n *claim, x *box) { |
| + n.Op = opState{Kind: "relocating", ID: w.newID("rl"), Phase: "pinning", Exec: -1, Src: x.ID, Tgt: -1, SrcRegion: x.Region, |
| + RelocReason: "failover", ReqAt: w.now, App: n.Holder.App, SrcGen: n.Holder.Gen, SrcStamp: n.Holder.Stamp, StopFiles: w.deadBoxFiles(x)} |
| + w.stats["relocation started: failover"]++ |
| +} |
| + |
| +// fenceSource is §5.8's source loss (B1-6, FenceSource): a drain whose |
| +// source is terminated before its release is journaled becomes a |
| +// failover in the same CAS, op.exec none, the stamp kept, the source off |
| +// the barrier, its files directory the publisher's stand-in; after its |
| +// release only its liveness changes. (1b-next keeps a source lost in |
| +// starting at starting until the remaining participant acknowledges, |
| +// then PinFailover; the model goes to pinning at once, where the pin |
| +// waits out the delay and installing waits for the barrier.) The |
| +// mutation of reloc-source-loss takes a source lost in releasing as |
| +// released at what the remote holds, so its unuploaded writes go |
| +// undeclared. |
| +func (w *world) fenceSource(n *claim, x *box) { |
| + switch { |
| + case n.Op.Phase == "starting", n.Op.Phase == "releasing" && n.Op.Release == nil: |
| + if !on("reloc-source-loss") && n.Op.Phase == "releasing" { |
| + h := n.Holder |
| + n.Op.Release = &releaseEntry{Box: x.ID, Session: h.Session, Gen: h.Gen, FinalTX: w.remoteMax(w.buckets[x.Region], dataKey(h.Location, h.Gen, "")), Flushed: true, Files: w.deadBoxFiles(x), Timers: append([]int(nil), x.Timers...), At: w.now} |
| + n.Op.Exec, n.Op.Phase = -1, "pinning" |
| + return |
| + } |
| + n.Op.RelocReason, n.Op.Exec, n.Op.Phase = "failover", -1, "pinning" |
| + n.Op.Release, n.Op.StopFiles = nil, w.deadBoxFiles(x) |
| + w.stats["relocation: source lost before its release, converted to failover"]++ |
| + default: |
| + w.stats["relocation: source lost after its release"]++ |
| + } |
| +} |
| + |
| +// replaceTarget is §5.8's replacement table (ReplaceTarget) for a target |
| +// terminated by its fence, within the fence's CAS: |
| +// |
| +// starting, releasing, pinning -> the same phase, to' named |
| +// installing -> installing: to' is op.exec, a new stamp, a fresh P' |
| +// installed, or probing before P -> installed: to' is op.exec, a new stamp, the same P, no receipt |
| +// after P's first admission, or -> pinning: a nested failover from holder.generation as observed |
| +// probe-failed |
| +// |
| +// Exhaustion is checked first (Worker.replace, 1b-next R1-16): with the |
| +// replacements used the fence goes to fenceExhaustedTarget and no spare |
| +// is looked for. With no eligible spare it reports false and the fence |
| +// waits for a later pass (Worker.next). The mutation of |
| +// reloc-replacement-table resumes every late loss at installed with the |
| +// same P. |
| +func (w *world) replaceTarget(n *claim, x *box) bool { |
| + phase := n.Op.Phase |
| + if on("reloc-replacement-cap") && n.Op.Replacements >= maxReplacements { |
| + w.fenceExhaustedTarget(n, x) |
| + return true |
| + } |
| + next := w.chooseBoxExcept(n.Op.SrcRegion, n.Holder.App, relocExcept(n.Op, x.ID)...) |
| + if next == nil { |
| + w.stats["relocation: target lost, no spare yet"]++ |
| + return false |
| + } |
| + if !w.nameReplacement(n, next.ID, phase) { |
| + return n.Op.Stuck != "" |
| + } |
| + w.stats["relocation: target replaced at "+phase]++ |
| + late := preparedOpened(n) || phase == "probe-failed" || phase == "probed" || phase == "opened" |
| + switch { |
| + case phase == "starting" || phase == "releasing" || phase == "pinning": |
| + case phase == "installing": |
| + n.Op.BaseKey, n.Op.BaseVer, n.Op.BaseTX = "", 0, 0 |
| + w.handExec(n, next.ID, "installing", w.newID("P")) |
| + case !late || !on("reloc-replacement-table"): |
| + w.handExec(n, next.ID, "installed", n.Op.Prepared) // P was never opened: to' makes its own local install and opens it |
| + default: |
| + n.Op.Exec, n.Op.Phase = -1, "pinning" |
| + n.Op.Pin, n.Op.Prepared, n.Op.Receipt, n.Op.Release = nil, "", nil, nil |
| + n.Op.BaseKey, n.Op.BaseVer, n.Op.BaseTX = "", 0, 0 |
| + n.Op.ProbeTries, n.Op.Attempts = 0, 0 |
| + w.stats["nested failover after P was admitted"]++ |
| + } |
| + return true |
| +} |
| + |
| +// fenceExhaustedTarget is FenceExhaustedTarget (1b-next ruling 23 as rev |
| +// 9 amended it; rule reloc-exhausted-fence): a target terminated after |
| +// the operation used its replacements is fenced (the caller's fenceBox) |
| +// and the operation is stuck, with no third target chosen. While another |
| +// box is op.exec (the live source in starting or releasing) only stuck is |
| +// new: the target's fence is no evidence against the source, whose |
| +// execution identity, phase and release stay, so its own stop evidence |
| +// still decides. Otherwise (op.exec the dead target, or none) the dead |
| +// installation's authority is revoked: op.exec none at pinning, its |
| +// receipt and release dropped, and P's pin and remote build kept when P |
| +// was never opened, dropped for a nested pinning when it was. The |
| +// mutation is rev 8's: always op.exec none at pinning, which revokes a |
| +// live source without its stop evidence. |
| +func (w *world) fenceExhaustedTarget(n *claim, x *box) { |
| + why := fmt.Sprintf("box %d terminated after %d target replacements", x.ID, maxReplacements) |
| + w.stats["relocation: exhausted target fenced"]++ |
| + if on("reloc-exhausted-fence") && n.Op.Exec >= 0 && n.Op.Exec != x.ID { |
| + n.Op.Stuck = why |
| + return |
| + } |
| + opened := preparedOpened(n) |
| + n.Op.Exec, n.Op.Phase = -1, "pinning" |
| + n.Op.Receipt, n.Op.Release = nil, nil |
| + n.Op.ProbeTries, n.Op.Attempts = 0, 0 |
| + if opened { |
| + n.Op.Pin, n.Op.Prepared = nil, "" |
| + n.Op.BaseKey, n.Op.BaseVer, n.Op.BaseTX = "", 0, 0 |
| + } |
| + n.Op.Stuck = why |
| +} |
amadan