amadan
settings-4: simulation covers the wake check and graceful-move request carry
The simulated wake refreshes its copy, calls release.DecideHeldWake and enforces it as the activator's wakeCheck does (refuse, run the target or a retained copy, or wait for root; with no decision for the settings, run the installed build state's build or wait for root's decision), then HeldExecStale and NextBuildState. It never runs the live link blindly. Graceful moves call release.CarryRequest; lost boxes carry nothing. Invariant 1's watermark counts failed completions a graceful move carried (ruling R-INV1-2). New invariant 7: a wake runs only what the rules allow, from the model's own records of root's last decision on each box. Copies go stale as production keeps them: failed refreshes keep the last state with ReadErr, and a returning box may keep its row. The consistency check that forbade stale known copies is gone.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
1 file changed,
+310
−55
internal/release/updatesim_test.go+310 −55
diff --git a/internal/release/updatesim_test.go b/internal/release/updatesim_test.go| index 6f2adb290..9006b425e 100644 |
| --- a/internal/release/updatesim_test.go |
| +++ b/internal/release/updatesim_test.go |
| @@ -19,11 +19,15 @@ import ( |
| // unpins and holds, root and agent passes decide and repoint, wakes run |
| // builds against the database, boxes are lost and the instance moves. |
| // |
| -// The decisions are production's: rootPass calls Target and NextConsumed, |
| -// wake calls NextBuildState (ruling R-MERGE). What surrounds them is not |
| -// pure (settingsTarget's file and registry reads, adoptHost's bake, evidence |
| -// and repoint, beforeExec's bucket write) and is mirrored here in the |
| -// smallest form that keeps its decisions. |
| +// The decisions are production's: rootPass calls Target and NextConsumed; |
| +// wake calls DecideHeldWake (the held wake check, ruling R-HELD-PURE) and |
| +// enforces it as the activator's wakeCheck does (refuse, run the target, or |
| +// wait for root), then HeldExecStale and NextBuildState (beforeExec, ruling |
| +// R-MERGE); a graceful move calls CarryRequest (ruling R-SPEC-43A-2). What |
| +// surrounds them is not pure (settingsTarget's file and registry reads, |
| +// adoptHost's bake, evidence and repoint, beforeExec's bucket write, the |
| +// wake's wait) and is mirrored here in the smallest form that keeps its |
| +// decisions. |
| // |
| // The invariants are checked against the model's own records, never against |
| // production helpers (a mutant of Watermark must not also move the oracle): |
| @@ -35,8 +39,11 @@ import ( |
| // completes it. The watermark is spec §4.3 rule 2's (ruling R-INV1): the |
| // highest completed id in the bucket's build state (the true object, |
| // whatever the box's copy says) or in the consumed file of the box doing |
| -// the pass. UPDATESIM_STRICT=1 reads every box's consumed file at once |
| -// instead; that is documentation of a known gap, not the gate (below). |
| +// the pass, and also every failed completion a box had recorded when the |
| +// instance left it by a graceful move (ruling R-INV1-2: the move carries |
| +// it; only a lost box's records are exempt). UPDATESIM_STRICT=1 reads |
| +// every box's consumed file at once instead; that is documentation of a |
| +// known gap, not the gate (below). |
| // 2. The build state names the build that last touched the database. |
| // 3. No install lacks evidence. At the decision: Target names pointer |
| // evidence only for the head, and asks for bake only on the head. At |
| @@ -66,15 +73,26 @@ import ( |
| // resolution once more; when the build state and the box's file both |
| // hold one, the build state's is (ruling R-RESOLUTION-STATE-WINS), and |
| // root's next pass with the state read rewrites the file to agree. |
| +// 7. A wake runs only what the rules allow (§4.3 rule 3, "The wake checks |
| +// too"; ruling R-HELD-PURE), from the model's own records: a pinned |
| +// instance runs its pin; one with a pending request resolved to T runs |
| +// T; a held one runs the bucket's last_executed. Held is manual, or a |
| +// major setting whose head, as of root's last decision on this box, has |
| +// no tag or another major, or a major setting root has not decided for |
| +// yet (a missing or stale decision never makes a wake unheld). |
| +// |
| +// Copies (the agent's registry copy root and the wake read) go stale the ways |
| +// production keeps them stale: a refresh that fails keeps the last known |
| +// state and records ReadErr; a box the instance returns to may still hold its |
| +// row from the earlier stay, copy and all, its refreshes failed while the |
| +// instance was away. Root reads such a copy as unread (BuildStateCopy.Read). |
| +// The wake refreshes first and is refused when that fails (Astra round 1 |
| +// finding 1). |
| // |
| // Strict mode (UPDATESIM_STRICT=1) checks invariants 1 and 6 across every |
| // box's consumed file, not only the one the instance is on. It is not the |
| -// gate (ruling R-INV1), and production fails it by design of rule 2: root |
| -// records a resolution, or a failed completion, in its own consumed file |
| -// only, and the build state carries it only from the next pre-exec write. |
| -// An instance that moves before that write leaves the record behind, and |
| -// the destination resolves or installs the request again (spec §4.2 "Lost |
| -// requests" reasoning: T never ran). It stays here to replay that gap. |
| +// gate (ruling R-INV1): a LOST box's records are the spec's lost request |
| +// (§4.2), and strict mode counts them. |
| // |
| // Seeds: UPDATESIM_SEEDS (default 200), spread over UPDATESIM_PAR goroutines |
| // (default 1); each seed has its own rand source and world. UPDATESIM_SEED=n |
| @@ -151,17 +169,20 @@ func TestUpdateRequestLifecycleSimulation(t *testing.T) { |
| // testUpdateSimSeed531Unpinned replays the shape seed 531 found, through |
| // the model's own actions (so every invariant is checked at every step) and |
| -// so through the production Target, NextConsumed and NextBuildState. Box 0 |
| -// resolves R1 to b2 and the instance moves before any wake; box 1 resolves |
| -// R1 again, to b3, under a pin set after the request, and its wake (running |
| -// the pin) carries {R1, b3} into the build state; the instance returns to |
| -// box 0, whose file still says {R1, b2}, and the pin is cleared. Rule 2 must |
| -// then install the build state's b3 (R-RESOLUTION-STATE-WINS), and the wake |
| -// that runs it must complete R1. The random schedule reaches the |
| -// disagreement only under a pin, and rarely clears it in time, so this |
| -// guards resolvedFor's order by itself. |
| +// so through the production Target, NextConsumed, DecideHeldWake, |
| +// CarryRequest and NextBuildState. Box 0 resolves R1 to b2 in a root pass |
| +// that was already running when the cut began, so its write lands after the |
| +// cut carried box 0's record (the in-flight window; the random schedule does |
| +// not model it, as root skips a route once the cut has marked it moving): |
| +// the resolution stays in box 0's file only. Box 1 resolves R1 again, to b3, |
| +// under a pin set after the request, and its wake (running the pin) carries |
| +// {R1, b3} into the build state; the instance returns to box 0, whose file |
| +// still says {R1, b2}, and the pin is cleared. Rule 2 must then install the |
| +// build state's b3 (R-RESOLUTION-STATE-WINS), and the wake that runs it must |
| +// complete R1. This guards resolvedFor's order by itself. |
| func testUpdateSimSeed531Unpinned(t *testing.T) { |
| w := newUpdateSimWorld(0, false) |
| + w.scripted = true |
| for i := range w.boxes { |
| w.boxes[i] = newSimBox(fmt.Sprintf("box%d", i)) |
| } |
| @@ -181,9 +202,10 @@ func testUpdateSimSeed531Unpinned(t *testing.T) { |
| w.settings = UpdateSettings{Updates: UpdatesManual, InstallRequest: 1} |
| steps := []func() string{ |
| - func() string { return w.rootPass(w.boxes[0], true) }, |
| func() string { w.settings.Pin = "b1"; return "pin b1 (after the request)" }, |
| - func() string { return w.moveTo(1, true) }, |
| + func() string { |
| + return w.moveToRacing(1, true, func() string { return w.rootPass(w.boxes[0], true) }) |
| + }, |
| func() string { w.head = "b3"; w.boxes[1].eligible["b3"] = true; return "promote b3, baked on box1" }, |
| func() string { return w.rootPass(w.boxes[1], true) }, |
| func() string { return w.wake(w.boxes[1]) }, |
| @@ -226,6 +248,7 @@ var updateSimInvariants = map[int]string{ |
| 4: "failure records outrank", |
| 5: "unresolved requests block nothing", |
| 6: "a request resolves at its first eligible pass, pin or not", |
| + 7: "a wake runs only what the rules allow", |
| } |
| func updateSimEnv(t *testing.T, name string, def int) int { |
| @@ -252,6 +275,12 @@ type simBox struct { |
| staged map[string]bool |
| eligible map[string]bool |
| copy BuildStateCopy |
| + // The model's own record of root's last decision on this box (for |
| + // invariant 7, never Consumed.Settings): the settings column it decided |
| + // for and the head it saw. decided is false until root's first pass. |
| + decided bool |
| + decidedSettings string |
| + decidedHead string |
| } |
| // simWorld is the instance and everything around it. state is the bucket |
| @@ -274,6 +303,13 @@ type simWorld struct { |
| firstEligible map[uint64]string |
| completedByRun map[uint64]bool |
| + // carried is the highest failed completion any box had recorded when |
| + // the instance left it by a graceful move (ruling R-INV1-2): invariant |
| + // 1's watermark includes it. Only a lost box's records are exempt. |
| + carried uint64 |
| + // scripted turns off the random faults (a failed refresh, a wait root |
| + // does not answer), for the scripted shapes. |
| + scripted bool |
| trace []string |
| viols []updateSimViolation |
| @@ -312,6 +348,15 @@ type updateSimStats struct { |
| pickedUp int // a move or return made another record of R the one in force |
| leftBehind int // a resolution or rule 2 pick strict mode would refuse |
| moves, returns int |
| + carriedRequests int // graceful moves whose cut carried a request record |
| + carriedFailed int // ... a failed completion among them |
| + unreadRefusals int // wakes refused: their refresh failed |
| + askRoot int // wakes with no decision from root for the settings |
| + askRootRuns int // ... that ran the installed build at once |
| + rootWaits int // wakes that asked root and waited |
| + heldRuns int // wakes that ran a held target |
| + retainedRuns int // ... from a retained copy |
| + keptCopies int // returns onto a kept, possibly stale, copy |
| } |
| func (s *updateSimStats) add(o updateSimStats) { |
| @@ -329,16 +374,29 @@ func (s *updateSimStats) add(o updateSimStats) { |
| s.leftBehind += o.leftBehind |
| s.moves += o.moves |
| s.returns += o.returns |
| + s.carriedRequests += o.carriedRequests |
| + s.carriedFailed += o.carriedFailed |
| + s.unreadRefusals += o.unreadRefusals |
| + s.askRoot += o.askRoot |
| + s.askRootRuns += o.askRootRuns |
| + s.rootWaits += o.rootWaits |
| + s.heldRuns += o.heldRuns |
| + s.retainedRuns += o.retainedRuns |
| + s.keptCopies += o.keptCopies |
| } |
| func (s updateSimStats) String() string { |
| return fmt.Sprintf("resolutions %d (failed head %d, under a pin %d), run completions %d, failed completions %d, "+ |
| "held+baking passes %d (recoveries onto last_executed %d), unread state with the request completed %d, "+ |
| "unread state on a returning box %d, lost resolutions %d, records picked up by a move %d, "+ |
| - "left-behind records acted past %d, moves %d (returns %d)", |
| + "left-behind records acted past %d, moves %d (returns %d, onto a kept copy %d), "+ |
| + "cuts that carried a request record %d (a failed completion %d), wakes refused unread %d, "+ |
| + "wakes with no decision for the settings %d (ran the installed build %d), wakes that waited on root %d, "+ |
| + "held runs %d (from a retained copy %d)", |
| s.resolutions, s.failedHeadResolutions, s.pinnedEligible, s.runCompletions, s.failedCompletions, |
| s.heldBakingPasses, s.heldRecoveries, s.unknownWithCompleted, s.unknownReturning, s.lostResolutions, |
| - s.pickedUp, s.leftBehind, s.moves, s.returns) |
| + s.pickedUp, s.leftBehind, s.moves, s.returns, s.keptCopies, s.carriedRequests, s.carriedFailed, |
| + s.unreadRefusals, s.askRoot, s.askRootRuns, s.rootWaits, s.heldRuns, s.retainedRuns) |
| } |
| func newUpdateSimWorld(seed int64, strict bool) *simWorld { |
| @@ -491,16 +549,33 @@ func (w *simWorld) expireBake() string { |
| } |
| // refresh is the agent reading the bucket object into its registry copy. |
| +// One that fails keeps the last known copy and records ReadErr, as |
| +// buildStates.refresh does. |
| func (w *simWorld) refresh() string { |
| b := w.cur() |
| + if w.refreshCopy(b) { |
| + return "refresh " + b.name |
| + } |
| + return "refresh " + b.name + " FAILED (copy kept, read error)" |
| +} |
| + |
| +// refreshCopy is buildStates.refresh on b: true when the read succeeded. |
| +func (w *simWorld) refreshCopy(b *simBox) bool { |
| + if !w.scripted && w.rng.Intn(100) < 15 { |
| + b.copy.ReadErr = "s3: timeout" |
| + return false |
| + } |
| b.copy = BuildStateCopy{Known: true, Replica: w.replica, State: cloneSimState(w.state)} |
| - return "refresh " + b.name |
| + return true |
| } |
| -// move hands the instance to another box with its replica and build state. |
| -// The destination's registry row is new (copy unread) or carries the |
| -// source's column (registry coldhandover copies build_state). A box the |
| -// instance returns to still has its old consumed file and live link. |
| +// move hands the instance to another box with its replica and build state: |
| +// a graceful move (a legacy cut, a Phase 1 cut, a rollback's return). The |
| +// destination's registry row is new (copy unread) or carries the source's |
| +// column (registry coldhandover copies build_state); a box the instance |
| +// returns to may still hold its row from the earlier stay, old copy and all |
| +// (a rolled-back move's source keeps its row). It still has its old consumed |
| +// file and live link either way. |
| func (w *simWorld) move() string { |
| j := w.rng.Intn(len(w.boxes) - 1) |
| if j >= w.at { |
| @@ -512,21 +587,61 @@ func (w *simWorld) move() string { |
| // moveTo moves the instance to box j; carried is whether the destination's |
| // registry row carries the source's build-state copy. |
| func (w *simWorld) moveTo(j int, carried bool) string { |
| + return w.moveToRacing(j, carried, nil) |
| +} |
| + |
| +// moveToRacing is moveTo with race, when set, run on the source after the |
| +// cut's carry and before the hand-over (a root pass already in flight when |
| +// the cut began). Before the hand-over the cut carries the source's request |
| +// record into the build state under the lease (release.CarryRequest; ruling |
| +// R-SPEC-43A-2), and the source's registry copy follows the write, as |
| +// buildStates.write sets it. |
| +func (w *simWorld) moveToRacing(j int, carried bool, race func() string) string { |
| src := w.cur() |
| dst := w.boxes[j] |
| - if carried { |
| + note := "" |
| + next := CarryRequest(cloneSimState(w.state), cloneSimConsumed(src.consumed)) |
| + if !SameRequestState(w.state, &next) { |
| + next.Schema, next.Host = 1, updateSimHost |
| + w.state = &next |
| + src.copy = BuildStateCopy{Known: true, Replica: w.replica, State: cloneSimState(&next)} |
| + w.stats.carriedRequests++ |
| + note = " carried " + simRes(next.Resolved) + fmt.Sprintf(" done %d%s", next.Completed, simFailedMark(next.CompletedFailed)) |
| + } |
| + if c := src.consumed; c != nil && c.CompletedFailed && c.Completed > w.carried { |
| + w.carried = c.Completed |
| + w.stats.carriedFailed++ |
| + } |
| + if race != nil { |
| + note += " | racing " + race() |
| + } |
| + kept := false |
| + switch { |
| + case carried: |
| dst.copy = cloneSimCopy(src.copy) |
| - } else { |
| + case dst.copy.Known && !w.scripted && w.rng.Intn(100) < 50: |
| + kept = true // its row from the earlier stay |
| + w.stats.keptCopies++ |
| + default: |
| dst.copy = BuildStateCopy{} |
| } |
| - src.copy = BuildStateCopy{} |
| + if w.scripted || w.rng.Intn(100) < 60 { |
| + src.copy = BuildStateCopy{} // the route retires here |
| + } else if src.copy.Known { |
| + // The source keeps its row for a return. Its refreshes while the |
| + // instance is away read a location that is not this box's (another |
| + // bucket: refused) and fail, so the copy keeps its last state with a |
| + // read error; a refresh that succeeds would leave it fresh, which no |
| + // rule can mistake. |
| + src.copy.ReadErr = "s3: the instance is on another box" |
| + } |
| w.at = j |
| w.stats.moves++ |
| if dst.consumed != nil || dst.live != "" { |
| w.stats.returns++ |
| } |
| w.syncResolutions() |
| - return fmt.Sprintf("move %s->%s copy-carried=%v", src.name, dst.name, carried) |
| + return fmt.Sprintf("move %s->%s copy-carried=%v kept=%v%s", src.name, dst.name, carried, kept, note) |
| } |
| // loseBox replaces a box with an empty one: its consumed file, live link, |
| @@ -680,6 +795,9 @@ func (w *simWorld) wm(b *simBox) uint64 { |
| if b.consumed != nil && b.consumed.Completed > m { |
| m = b.consumed.Completed |
| } |
| + if w.carried > m { |
| + m = w.carried |
| + } |
| return m |
| } |
| @@ -743,7 +861,7 @@ func (w *simWorld) rootPass(b *simBox, resolve bool) string { |
| dec = TargetDecision{Version: head, Reason: ReasonAdopt, Evidence: EvidencePointer, Bake: true, Detail: head} |
| } else { |
| in = TargetInput{ |
| - Route: registry.Route{Host: updateSimHost, Kind: "instance"}, |
| + Route: registry.Route{Host: updateSimHost, Kind: "instance", UpdateSettings: u.Column()}, |
| Pointer: &ChannelPointer{Channel: "production", Version: head}, |
| HeadTag: w.tags[head], |
| Settings: u, |
| @@ -767,9 +885,10 @@ func (w *simWorld) rootPass(b *simBox, resolve bool) string { |
| if resolve { |
| next := NextConsumed(in, dec) |
| b.consumed = &next |
| + b.decided, b.decidedSettings, b.decidedHead = true, u.Column(), head |
| // Invariant 6: with the build state read, root's file agrees with |
| // it on the pending request's T once the pass is written. |
| - if r := u.InstallRequest; in.Build.Known && r > w.wm(b) && w.state != nil && w.state.Resolved != nil && w.state.Resolved.ID == r && |
| + if r := u.InstallRequest; in.Build.Read() && r > w.wm(b) && w.state != nil && w.state.Resolved != nil && w.state.Resolved.ID == r && |
| next.Resolved != nil && next.Resolved.ID == r && next.Resolved.Target != w.state.Resolved.Target { |
| w.fail(6, "after root's pass R%d has two resolutions: the build state says %s, %s's consumed file %s", |
| r, w.state.Resolved.Target, b.name, next.Resolved.Target) |
| @@ -783,7 +902,7 @@ func (w *simWorld) rootPass(b *simBox, resolve bool) string { |
| // Invariant 5's scenario: a held instance, no pin, the build state read |
| // with a last_executed, an unresolved request whose head bakes here. |
| recovery := "" |
| - if viaTarget && held && u.Pin == "" && in.Build.Known && in.Build.State != nil && in.Build.State.LastExecuted != "" { |
| + if viaTarget && held && u.Pin == "" && in.Build.Read() && in.Build.State != nil && in.Build.State.LastExecuted != "" { |
| le := in.Build.State.LastExecuted |
| pending, t := boxView(in.Consumed, in.Build.State, u.InstallRequest) |
| if pending && t == "" && in.HeadHeld != "" && !u.InstallFastTrack && !b.failed[le] && (w.promoted[le] || b.staged[le]) { |
| @@ -877,7 +996,7 @@ func (w *simWorld) checkDecision(b *simBox, in TargetInput, dec TargetDecision, |
| r := u.InstallRequest |
| head := in.Pointer.Version |
| - if !in.Build.Known && r != 0 { |
| + if !in.Build.Read() && r != 0 { |
| if w.state != nil && w.state.Completed >= r { |
| w.stats.unknownWithCompleted++ |
| } |
| @@ -902,8 +1021,9 @@ func (w *simWorld) checkDecision(b *simBox, in TargetInput, dec TargetDecision, |
| w.fail(1, "%s resolved R%d again (to %s) after it completed (watermark %d)", b.name, dec.Resolve.ID, dec.Resolve.Target, wmBefore) |
| } |
| - // Invariant 6: the first eligible pass resolves, pin or not. |
| - if in.Build.Known && r != 0 { |
| + // Invariant 6: the first eligible pass resolves, pin or not (with the |
| + // build state read: never read, or a refresh that failed, is unread). |
| + if in.Build.Read() && r != 0 { |
| pending, t := boxView(in.Consumed, in.Build.State, r) |
| eligible := in.HeadHeld == "" || u.InstallFastTrack |
| if pending && t == "" && eligible && r > wmBefore { |
| @@ -939,15 +1059,101 @@ func (w *simWorld) checkDecision(b *simBox, in TargetInput, dec TargetDecision, |
| } |
| } |
| -// wake is the agent's pre-exec write (buildStates.beforeExec: read the |
| -// consumed file, merge with release.NextBuildState, write the object and the |
| -// registry copy), then the run. It runs the live link; with nothing |
| -// installed the wake waits on root. |
| +// wake is the agent's wake on box b, as production runs it with no planner |
| +// and an identity it can exec by path: |
| +// |
| +// - for a route whose settings could hold it, the copy is refreshed first |
| +// (buildStates.wakeTarget); a refresh that fails leaves ReadErr in it; |
| +// - the held wake check's decision is production's (DecideHeldWake, ruling |
| +// R-HELD-PURE), enforced as the activator's wakeCheck does: not held runs |
| +// the live link (today's wake); unread, unknown, or a target root reports |
| +// failed is refused; a held target runs when it is installed, or from |
| +// this box's retained copy; otherwise root is asked and the wake waits |
| +// for the install, and a changed answer ends the wait with nothing run. |
| +// With no decision from root for the current settings (AskRoot) the |
| +// build state's build runs only if it is installed; otherwise the wake |
| +// asks root for a pass and waits for its decision, then decides again. |
| +// The live link never runs blindly; |
| +// - a wait is root's pass, run inline (the stage relay), or, half the |
| +// time, no answer within the bound: the wake ends with nothing run; |
| +// - then beforeExec: HeldExecStale against the bucket object read under |
| +// the lease, and the merge, NextBuildState; then the run. |
| func (w *simWorld) wake(b *simBox) string { |
| - run := b.live |
| - if run == "" { |
| - return "wake@" + b.name + ": nothing installed" |
| + u := w.settings |
| + col := u.Column() |
| + desc := "wake@" + b.name |
| + if !u.Default() { |
| + if !w.refreshCopy(b) { |
| + desc += " (refresh failed)" |
| + } |
| + } |
| + decide := func() HeldWakeDecision { |
| + return DecideHeldWake(HeldWakeInput{Settings: col, Build: cloneSimCopy(b.copy), Consumed: cloneSimConsumed(b.consumed), Installed: b.live}) |
| + } |
| + waitRoot := func() bool { |
| + w.stats.rootWaits++ |
| + if !w.scripted && w.rng.Intn(100) < 50 { |
| + return false |
| + } |
| + desc += " [waits; " + w.rootPass(b, true) + "]" |
| + return true |
| + } |
| + d := decide() |
| + if d.Held && d.AskRoot && !d.Failed { |
| + w.stats.askRoot++ |
| + if d.Target != "" && b.live == d.Target { |
| + w.stats.askRootRuns++ |
| + } else { |
| + if !waitRoot() { |
| + return desc + ": no decision from root for its settings within the bound, nothing run" |
| + } |
| + if d = decide(); d.AskRoot && (d.Target == "" || b.live != d.Target) { |
| + return desc + ": root has not decided for its settings, nothing run" |
| + } |
| + } |
| } |
| + run, retained := "", false |
| + switch { |
| + case !d.Held: |
| + run = b.live // today's wake |
| + if run == "" { |
| + return desc + ": nothing installed" |
| + } |
| + case d.Unread: |
| + w.stats.unreadRefusals++ |
| + return desc + ": refused, its build state could not be read" |
| + case d.Unknown || d.Target == "": |
| + return desc + ": refused, build unknown" |
| + case d.Failed: |
| + return desc + ": refused, its target " + d.Target + " failed here" |
| + case b.live == d.Target: |
| + run = d.Target |
| + case !d.AskRoot && b.staged[d.Target]: |
| + run, retained = d.Target, true |
| + default: |
| + if !waitRoot() { |
| + return desc + ": waited for root to install " + d.Target + ", nothing run" |
| + } |
| + if b.live != d.Target { |
| + return desc + ": " + d.Target + " not installed when the wait ended, nothing run" |
| + } |
| + run = d.Target |
| + } |
| + if d.Held { |
| + w.stats.heldRuns++ |
| + if retained { |
| + w.stats.retainedRuns++ |
| + desc += " (retained copy)" |
| + } |
| + } |
| + // beforeExec: the held target revalidated against the object under the |
| + // lease, then the merge. A refused record runs nothing. |
| + fresh := DecideHeldWake(HeldWakeInput{Settings: col, Build: BuildStateCopy{Known: true, Replica: true, State: cloneSimState(w.state)}, |
| + Consumed: cloneSimConsumed(b.consumed), Installed: b.live}) |
| + if err := HeldExecStale(fresh, w.state, run); err != nil { |
| + return desc + ": record refused: " + err.Error() |
| + } |
| + w.checkWakeRun(b, run) |
| wmBefore := w.wm(b) |
| cur := cloneSimState(w.state) |
| next := NextBuildState(cur, cloneSimConsumed(b.consumed), run) |
| @@ -980,19 +1186,68 @@ func (w *simWorld) wake(b *simBox) string { |
| w.lastRan = run |
| w.replica = true |
| b.copy = BuildStateCopy{Known: true, Replica: true, State: cloneSimState(&next)} |
| - return fmt.Sprintf("wake@%s runs %s", b.name, run) |
| + return fmt.Sprintf("%s runs %s", desc, run) |
| } |
| -// check is the per-step state check (invariant 2, and the model's own |
| -// consistency); event checks run inside the actions. |
| +// checkWakeRun is invariant 7 on a wake about to run build run on box b, from |
| +// the model's own records (never Consumed.Settings or Reason). |
| +func (w *simWorld) checkWakeRun(b *simBox, run string) { |
| + u := w.settings |
| + if u.Default() { |
| + return |
| + } |
| + if u.Pin != "" { |
| + if run != u.Pin { |
| + w.fail(7, "pinned on %s, the wake on %s ran %s", u.Pin, b.name, run) |
| + } |
| + return |
| + } |
| + if r := u.InstallRequest; r != 0 && r > w.wm(b) { |
| + t := "" |
| + if w.state != nil && w.state.Resolved != nil && w.state.Resolved.ID == r { |
| + t = w.state.Resolved.Target |
| + } else if b.consumed != nil && b.consumed.Resolved != nil && b.consumed.Resolved.ID == r { |
| + t = b.consumed.Resolved.Target |
| + } |
| + if t != "" { |
| + if run != t { |
| + w.fail(7, "R%d pending with T %s, the wake on %s ran %s", r, t, b.name, run) |
| + } |
| + return |
| + } |
| + } |
| + held := u.Updates == UpdatesManual |
| + if !held && u.Major != nil { |
| + if !b.decided || b.decidedSettings != u.Column() { |
| + held = true // root has not decided for these settings: the wake holds |
| + } else { |
| + m := w.major[b.decidedHead] |
| + held = m == 0 || m != *u.Major |
| + } |
| + } |
| + if le := simLE(w.state); held && le != "" && run != le { |
| + w.fail(7, "held (updates %s, major %v; root decided for these settings: %v), the wake on %s ran %s, not last_executed %s", |
| + u.Updates, simMajor(u.Major), b.decided && b.decidedSettings == u.Column(), b.name, run, le) |
| + } |
| +} |
| + |
| +func simMajor(m *int) string { |
| + if m == nil { |
| + return "-" |
| + } |
| + return strconv.Itoa(*m) |
| +} |
| + |
| +// check is the per-step state check (invariant 2); event checks run inside |
| +// the actions. A known copy that differs from the bucket is not a model |
| +// error: production keeps one after a failed refresh, and on a box the |
| +// instance returns to, until the next refresh (Astra round 1's note on this |
| +// simulation). The wake refreshes before it decides and is refused when |
| +// that fails; root's passes read the copy as it is. |
| func (w *simWorld) check() { |
| if w.lastRan != "" && (w.state == nil || w.state.LastExecuted != w.lastRan) { |
| w.fail(2, "the database last ran %s; the build state says %q", w.lastRan, simLE(w.state)) |
| } |
| - b := w.cur() |
| - if c := b.copy; c.Known && !simStatesEqual(c.State, w.state) { |
| - w.fail(0, "%s's known copy %+v differs from the bucket %+v", b.name, c.State, w.state) |
| - } |
| } |
| func (w *simWorld) summary() string { |