amadan
settings-4 task 11: request lifecycle simulation; 3000 seeds clean, M1-M7 and M8' each caught
TestUpdateRequestLifecycleSimulation runs one instance across three boxes: heads move and bake, Update now, pins, manual and major holds, root and agent passes, wakes, moves (fresh or carried registry copy), lost boxes and failure records. It calls the production Target, NextConsumed and NextBuildState (R-MERGE). settingsTarget's plain/stop branches and adoptHost's bake/evidence/repoint are mirrored minimally. The oracle uses its own records, never production helpers. Invariant 1 uses spec rule 2's watermark (R-INV1). UPDATESIM_STRICT=1 is the brief's every-box reading, kept as documentation only. UPDATESIM_SEEDS (default 200), UPDATESIM_PAR (default 1), UPDATESIM_SEED replays. Sweep on 5b8abb22: UPDATESIM_SEEDS=3000 UPDATESIM_PAR=2 nice -n 19 go test -p 1: PASS, ok 0.279s. Mutants: each ran in a fresh mktemp copy of 5b8abb22 plus this file, at 200 seeds, and the copy was deleted after the run: - M1 Watermark ignores the build state: INVARIANT 1, 56/200 (seed 4: "box1 resolved R4 again (to b3) after it completed"). - M2 resolves while the head bakes: INVARIANT 5, 20/200 (seed 6: held, R3 unresolved behind baking b5, live b5 not last_executed b4); also 6. - M3 completion moved from the wake to install: INVARIANT 1, 60/200 (seed 1: "wake running b3 records R7 newly completed; already completed"). - M4 rule 1 drops failed(pin): INVARIANT 4, 73/200 (seed 3: "box2 repointed onto b5, which it holds as failed"). - M5 rule 3 returns the head when the build state is unread: INVARIANT 5, 47/200 (seed 2: held instance repointed onto b5, not last_executed b2). - M6 pin returned before the request bookkeeping: INVARIANT 6, 86/200 (seed 1: "R3 pending and b3 eligible ... pin b1: the pass resolved -"). - M7 request block outside the Known guard: INVARIANT 1, 10/200 (seed 87: "rule 2 selected R1 (b3), already completed"); also 5, 6. - M8' the new-request resolution branch outside the Known guard: INVARIANT 1, 10/200 (seed 87, same line); INVARIANT 6, 77/200 (seed 1: "box0 resolved R1 to b1; first eligible"). - M8 (the completed-then-failed marking outside the guard) is retired as a proven equivalent (R-M8). The proof is in task-11-report.md. - M0, task 11a reverted: survives 200 seeds; at 3000, INVARIANT 6, 6/3000 (seed 642: "after root's pass R1 has two resolutions: the build state says b5, box0's consumed file b4").
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
1 file changed,
+989
−0
internal/release/updatesim_test.go+989 −0
diff --git a/internal/release/updatesim_test.go b/internal/release/updatesim_test.go| new file mode 100644 |
| index 000000000..6a367d92c |
| --- /dev/null |
| +++ b/internal/release/updatesim_test.go |
| @@ -0,0 +1,989 @@ |
| +package release |
| + |
| +import ( |
| + "fmt" |
| + "math/rand" |
| + "os" |
| + "sort" |
| + "strconv" |
| + "strings" |
| + "sync" |
| + "testing" |
| + |
| + "github.com/carlosframework/platform/internal/registry" |
| +) |
| + |
| +// TestUpdateRequestLifecycleSimulation runs random schedules of one |
| +// instance's update life across three boxes (settings plan 4 Task 11): the |
| +// channel head moves and bakes, the member presses "Update now", pins, |
| +// 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 invariants are checked against the model's own records, never against |
| +// production helpers (a mutant of Watermark must not also move the oracle): |
| +// |
| +// 1. A completed request never runs again: once the watermark is >= R, no |
| +// box resolves R again, rule 2 never selects R again, and no wake |
| +// records R as newly completed. A wake that completes R does so because |
| +// R's T ran, and a wake that runs the build state's T for a pending R |
| +// 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). |
| +// 2. The build state names the build that last touched the database. |
| +// 3. No install lacks evidence: every repoint is the head, a build with a |
| +// promotion record, or the box's own staged copy. |
| +// 4. Failure records outrank: no repoint a Target decision makes lands on a |
| +// build the box holds as failed (the model never sets GoodVersion, so no |
| +// instance has served a failed build; default routes with no consumed |
| +// file keep today's adoption, which never read the book: R-T6-BOOK). |
| +// 5. Unresolved requests block nothing: a held instance with an unresolved |
| +// request whose head is baking recovers onto last_executed; and a held |
| +// instance (no pin) never repoints anywhere but last_executed, a T its |
| +// pending request was resolved to, or, never having run, the head. |
| +// 6. A request resolves at its first eligible pass, pin or not: the world |
| +// records firstEligible[R], the head at the first root pass where R is |
| +// pending, the build state is read (R-TARGET-UNKNOWN) and the head is |
| +// eligible on that box (or the request asked for fast track). That pass |
| +// must resolve R to it; every resolution of R a box records, and every |
| +// rule 2 install of R, names exactly that build. A resolution the |
| +// instance can no longer see was never run (a run completes R in the |
| +// build state), so it is spec §4.2's "Lost requests": firstEligible[R] |
| +// is cleared and the next eligible pass resolves R again. A record the |
| +// instance sees again (it returned to the box holding it) is R's |
| +// 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. |
| +// |
| +// 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. |
| +// |
| +// Seeds: UPDATESIM_SEEDS (default 200), spread over UPDATESIM_PAR goroutines |
| +// (default 1); each seed has its own rand source and world. UPDATESIM_SEED=n |
| +// replays seed n alone. A failure prints the seed, the step and the trace, |
| +// and a line "INVARIANT <n> ..." per invariant any seed violated. |
| +func TestUpdateRequestLifecycleSimulation(t *testing.T) { |
| + seeds := updateSimEnv(t, "UPDATESIM_SEEDS", 200) |
| + par := updateSimEnv(t, "UPDATESIM_PAR", 1) |
| + first := 0 |
| + if v := os.Getenv("UPDATESIM_SEED"); v != "" { |
| + n, err := strconv.Atoi(v) |
| + if err != nil { |
| + t.Fatal(err) |
| + } |
| + first, seeds = n, 1 |
| + } |
| + if par < 1 { |
| + par = 1 |
| + } |
| + strict := os.Getenv("UPDATESIM_STRICT") == "1" |
| + results := make([]updateSimResult, seeds) |
| + jobs := make(chan int) |
| + var wg sync.WaitGroup |
| + for i := 0; i < par; i++ { |
| + wg.Add(1) |
| + go func() { |
| + defer wg.Done() |
| + for i := range jobs { |
| + results[i] = runUpdateSim(int64(first+i), updateSimSteps, strict) |
| + } |
| + }() |
| + } |
| + for i := 0; i < seeds; i++ { |
| + jobs <- i |
| + } |
| + close(jobs) |
| + wg.Wait() |
| + |
| + var total updateSimStats |
| + byInv := map[int][]*updateSimFailure{} |
| + for i := range results { |
| + total.add(results[i].stats) |
| + if f := results[i].fail; f != nil { |
| + seen := map[int]bool{} |
| + for _, v := range f.viols { |
| + if !seen[v.inv] { |
| + seen[v.inv] = true |
| + byInv[v.inv] = append(byInv[v.inv], f) |
| + } |
| + } |
| + } |
| + } |
| + t.Logf("%d seeds x %d steps (par %d, strict %v): %s", seeds, updateSimSteps, par, strict, total) |
| + invs := make([]int, 0, len(byInv)) |
| + for inv := range byInv { |
| + invs = append(invs, inv) |
| + } |
| + sort.Ints(invs) |
| + for _, inv := range invs { |
| + fs := byInv[inv] |
| + f := fs[0] |
| + var msg string |
| + for _, v := range f.viols { |
| + if v.inv == inv { |
| + msg = v.msg |
| + break |
| + } |
| + } |
| + t.Errorf("INVARIANT %d (%s) violated in %d of %d seeds; first: seed %d step %d (%s): %s\ntrace (replay with UPDATESIM_SEED=%d):\n%s", |
| + inv, updateSimInvariants[inv], len(fs), seeds, f.seed, f.step, f.action, msg, f.seed, strings.Join(f.trace, "\n")) |
| + } |
| +} |
| + |
| +const ( |
| + updateSimHost = "blog.example.com" |
| + updateSimSteps = 80 |
| + updateSimBoxes = 3 |
| +) |
| + |
| +var updateSimInvariants = map[int]string{ |
| + 0: "model consistency", |
| + 1: "a completed request never runs again", |
| + 2: "the build state names the build that last touched the database", |
| + 3: "no install lacks evidence", |
| + 4: "failure records outrank", |
| + 5: "unresolved requests block nothing", |
| + 6: "a request resolves at its first eligible pass, pin or not", |
| +} |
| + |
| +func updateSimEnv(t *testing.T, name string, def int) int { |
| + v := os.Getenv(name) |
| + if v == "" { |
| + return def |
| + } |
| + n, err := strconv.Atoi(v) |
| + if err != nil || n < 0 { |
| + t.Fatalf("%s=%q: want a count", name, v) |
| + } |
| + return n |
| +} |
| + |
| +// simBox is one box's view of the instance: root's consumed file, the live |
| +// link, the failure book, the version store's staged copies, the bake clock |
| +// (versions whose window has run here) and the agent's registry copy of the |
| +// build state, which is what root reads. |
| +type simBox struct { |
| + name string |
| + consumed *Consumed |
| + live string |
| + failed map[string]bool |
| + staged map[string]bool |
| + eligible map[string]bool |
| + copy BuildStateCopy |
| +} |
| + |
| +// simWorld is the instance and everything around it. state is the bucket |
| +// object (nil until the first pre-exec write). replica is whether the |
| +// instance has a database (a legacy instance has one with no build state). |
| +type simWorld struct { |
| + boxes []*simBox |
| + at int |
| + state *BuildState |
| + replica bool |
| + settings UpdateSettings |
| + head string |
| + builds []string |
| + tags map[string]string |
| + major map[string]int // 0: the build has no semver tag |
| + promoted map[string]bool |
| + lastRan string |
| + rng *rand.Rand |
| + strict bool |
| + |
| + firstEligible map[uint64]string |
| + completedByRun map[uint64]bool |
| + |
| + trace []string |
| + viols []updateSimViolation |
| + stats updateSimStats |
| +} |
| + |
| +type updateSimViolation struct { |
| + inv int |
| + msg string |
| +} |
| + |
| +type updateSimFailure struct { |
| + seed int64 |
| + step int |
| + action string |
| + viols []updateSimViolation |
| + trace []string |
| +} |
| + |
| +type updateSimResult struct { |
| + fail *updateSimFailure |
| + stats updateSimStats |
| +} |
| + |
| +// updateSimStats counts the scenarios the invariants need, so a clean run |
| +// shows they were reached. |
| +type updateSimStats struct { |
| + resolutions, runCompletions, failedCompletions int |
| + failedHeadResolutions int // R-TARGET-FAILEDHEAD |
| + heldRecoveries int // invariant 5's scenario, repointing onto last_executed |
| + heldBakingPasses int // invariant 5's scenario, any |
| + unknownWithCompleted int // Known false, the current request already completed (R-TARGET-UNKNOWN) |
| + unknownReturning int // Known false on a box whose consumed file names the current request |
| + pinnedEligible int // invariant 6 under a pin |
| + lostResolutions int |
| + 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 |
| +} |
| + |
| +func (s *updateSimStats) add(o updateSimStats) { |
| + s.resolutions += o.resolutions |
| + s.runCompletions += o.runCompletions |
| + s.failedCompletions += o.failedCompletions |
| + s.failedHeadResolutions += o.failedHeadResolutions |
| + s.heldRecoveries += o.heldRecoveries |
| + s.heldBakingPasses += o.heldBakingPasses |
| + s.unknownWithCompleted += o.unknownWithCompleted |
| + s.unknownReturning += o.unknownReturning |
| + s.pinnedEligible += o.pinnedEligible |
| + s.lostResolutions += o.lostResolutions |
| + s.pickedUp += o.pickedUp |
| + s.leftBehind += o.leftBehind |
| + s.moves += o.moves |
| + s.returns += o.returns |
| +} |
| + |
| +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)", |
| + 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) |
| +} |
| + |
| +func newUpdateSimWorld(seed int64, strict bool) *simWorld { |
| + w := &simWorld{ |
| + rng: rand.New(rand.NewSource(seed)), |
| + strict: strict, |
| + settings: UpdateSettings{Updates: UpdatesAuto}, |
| + tags: map[string]string{}, |
| + major: map[string]int{}, |
| + promoted: map[string]bool{}, |
| + firstEligible: map[uint64]string{}, |
| + completedByRun: map[uint64]bool{}, |
| + } |
| + for i := 0; i < updateSimBoxes; i++ { |
| + w.boxes = append(w.boxes, newSimBox(fmt.Sprintf("box%d", i))) |
| + } |
| + w.head = "b1" |
| + w.builds = []string{"b1"} |
| + w.tags["b1"], w.major["b1"], w.promoted["b1"] = "1.1.0", 1, true |
| + w.boxes[0].eligible["b1"] = true |
| + if w.rng.Intn(100) < 30 { |
| + // An instance from before this feature: a database, a live link, no |
| + // build state. |
| + w.replica = true |
| + w.boxes[0].live = "b1" |
| + w.boxes[0].staged["b1"] = true |
| + } |
| + if w.rng.Intn(100) < 25 { |
| + w.settings.Updates = UpdatesManual |
| + } |
| + return w |
| +} |
| + |
| +func newSimBox(name string) *simBox { |
| + return &simBox{name: name, failed: map[string]bool{}, staged: map[string]bool{}, eligible: map[string]bool{}} |
| +} |
| + |
| +func runUpdateSim(seed int64, steps int, strict bool) updateSimResult { |
| + w := newUpdateSimWorld(seed, strict) |
| + for step := 1; step <= steps; step++ { |
| + w.viols = nil |
| + action := w.act() |
| + w.trace = append(w.trace, fmt.Sprintf("%3d %s %s", step, action, w.summary())) |
| + w.check() |
| + if len(w.viols) > 0 { |
| + return updateSimResult{stats: w.stats, fail: &updateSimFailure{seed: seed, step: step, action: action, viols: w.viols, trace: w.trace}} |
| + } |
| + } |
| + return updateSimResult{stats: w.stats} |
| +} |
| + |
| +func (w *simWorld) fail(inv int, format string, args ...any) { |
| + w.viols = append(w.viols, updateSimViolation{inv: inv, msg: fmt.Sprintf(format, args...)}) |
| +} |
| + |
| +func (w *simWorld) cur() *simBox { return w.boxes[w.at] } |
| + |
| +// act picks one action at random and applies it. |
| +func (w *simWorld) act() string { |
| + weights := []int{8, 7, 9, 22, 5, 9, 14, 4, 2, 5, 5, 5, 3} |
| + sum := 0 |
| + for _, x := range weights { |
| + sum += x |
| + } |
| + n := w.rng.Intn(sum) |
| + i := 0 |
| + for ; n >= weights[i]; i++ { |
| + n -= weights[i] |
| + } |
| + switch i { |
| + case 0: |
| + return w.updateNow() |
| + case 1: |
| + return w.promote() |
| + case 2: |
| + return w.expireBake() |
| + case 3: |
| + return w.rootPass(w.cur(), true) |
| + case 4: |
| + return w.rootPass(w.cur(), false) |
| + case 5: |
| + return w.refresh() |
| + case 6: |
| + return w.wake(w.cur()) |
| + case 7: |
| + return w.move() |
| + case 8: |
| + return w.loseBox() |
| + case 9: |
| + return w.markFailed() |
| + case 10: |
| + return w.toggleManual() |
| + case 11: |
| + return w.pin() |
| + default: |
| + return w.setMajor() |
| + } |
| +} |
| + |
| +// updateNow is the console's "Update now": a new request id. The console |
| +// refuses it on a pinned instance (console apiupdates.go); a pin set while a |
| +// request is pending is allowed, so the model sets pins either way. |
| +func (w *simWorld) updateNow() string { |
| + if w.settings.Pin != "" { |
| + return "update-now refused: pinned" |
| + } |
| + w.settings.InstallRequest++ |
| + w.settings.InstallFastTrack = w.rng.Intn(100) < 20 |
| + return fmt.Sprintf("update-now R%d fast=%v", w.settings.InstallRequest, w.settings.InstallFastTrack) |
| +} |
| + |
| +// promote moves the channel head: a new build (no box has baked it yet), or |
| +// a pull-back to an earlier one, which stays eligible wherever it baked. |
| +func (w *simWorld) promote() string { |
| + if len(w.builds) > 1 && w.rng.Intn(100) < 15 { |
| + var older []string |
| + for _, b := range w.builds { |
| + if b != w.head { |
| + older = append(older, b) |
| + } |
| + } |
| + w.head = older[w.rng.Intn(len(older))] |
| + return "promote pull-back " + w.head |
| + } |
| + n := len(w.builds) + 1 |
| + b := fmt.Sprintf("b%d", n) |
| + w.builds = append(w.builds, b) |
| + w.head = b |
| + w.promoted[b] = w.rng.Intn(100) < 85 |
| + switch r := w.rng.Intn(100); { |
| + case r < 10: |
| + w.major[b], w.tags[b] = 0, "" |
| + default: |
| + m := 1 |
| + if r >= 75 { |
| + m = 2 |
| + } |
| + w.major[b], w.tags[b] = m, fmt.Sprintf("%d.%d.0", m, n) |
| + } |
| + return fmt.Sprintf("promote %s record=%v tag=%q", b, w.promoted[b], w.tags[b]) |
| +} |
| + |
| +func (w *simWorld) expireBake() string { |
| + b := w.cur() |
| + if w.rng.Intn(100) >= 60 { |
| + b = w.boxes[w.rng.Intn(len(w.boxes))] |
| + } |
| + b.eligible[w.head] = true |
| + return fmt.Sprintf("bake-expired %s on %s", w.head, b.name) |
| +} |
| + |
| +// refresh is the agent reading the bucket object into its registry copy. |
| +func (w *simWorld) refresh() string { |
| + b := w.cur() |
| + b.copy = BuildStateCopy{Known: true, Replica: w.replica, State: cloneSimState(w.state)} |
| + return "refresh " + b.name |
| +} |
| + |
| +// 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. |
| +func (w *simWorld) move() string { |
| + src := w.cur() |
| + j := w.rng.Intn(len(w.boxes) - 1) |
| + if j >= w.at { |
| + j++ |
| + } |
| + dst := w.boxes[j] |
| + carried := w.rng.Intn(100) < 50 |
| + if carried { |
| + dst.copy = cloneSimCopy(src.copy) |
| + } else { |
| + dst.copy = BuildStateCopy{} |
| + } |
| + src.copy = BuildStateCopy{} |
| + 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) |
| +} |
| + |
| +// loseBox replaces a box with an empty one: its consumed file, live link, |
| +// version store, failure book and bake clock are gone. If the instance was |
| +// on it, its registry row is new too. |
| +func (w *simWorld) loseBox() string { |
| + k := w.rng.Intn(len(w.boxes)) |
| + name := w.boxes[k].name |
| + w.boxes[k] = newSimBox(name) |
| + w.syncResolutions() |
| + return "lose " + name |
| +} |
| + |
| +// syncResolutions runs after a move or a lost box, for every request with a |
| +// first eligible build. A resolution the instance can no longer see (no |
| +// record in the build state or, strict mode aside, its box's consumed file) |
| +// never ran, since a run completes the request in the build state: spec |
| +// §4.2 "Lost requests", so the next eligible pass resolves it again. A |
| +// record it can see is R's resolution from now on (the instance returned to |
| +// a box holding one); of two, the build state's (R-RESOLUTION-STATE-WINS). |
| +func (w *simWorld) syncResolutions() { |
| + b := w.cur() |
| + records := map[uint64]map[string]bool{} |
| + note := func(r *ResolvedRequest) { |
| + if r == nil { |
| + return |
| + } |
| + if records[r.ID] == nil { |
| + records[r.ID] = map[string]bool{} |
| + } |
| + records[r.ID][r.Target] = true |
| + } |
| + if w.state != nil { |
| + note(w.state.Resolved) |
| + } |
| + for _, x := range w.boxes { |
| + if (x == b || w.strict) && x.consumed != nil { |
| + note(x.consumed.Resolved) |
| + } |
| + } |
| + ids := map[uint64]bool{} |
| + for r := range w.firstEligible { |
| + ids[r] = true |
| + } |
| + for r := range records { |
| + ids[r] = true |
| + } |
| + for r := range ids { |
| + if r <= w.wm(b) { |
| + continue |
| + } |
| + seen := records[r] |
| + fe, had := w.firstEligible[r] |
| + switch { |
| + case len(seen) == 0: |
| + delete(w.firstEligible, r) |
| + w.stats.lostResolutions++ |
| + case !w.strict: |
| + // One record, or the build state's when both hold one |
| + // (R-RESOLUTION-STATE-WINS). |
| + t := "" |
| + for x := range seen { |
| + t = x |
| + } |
| + if w.state != nil && w.state.Resolved != nil && w.state.Resolved.ID == r { |
| + t = w.state.Resolved.Target |
| + } |
| + if !had || t != fe { |
| + w.firstEligible[r] = t |
| + w.stats.pickedUp++ |
| + } |
| + } |
| + } |
| +} |
| + |
| +func (w *simWorld) markFailed() string { |
| + b := w.cur() |
| + var cands []string |
| + add := func(v string) { |
| + if v != "" { |
| + cands = append(cands, v) |
| + } |
| + } |
| + add(b.live) |
| + add(w.head) |
| + add(w.settings.Pin) |
| + if w.state != nil { |
| + add(w.state.LastExecuted) |
| + if w.state.Resolved != nil { |
| + add(w.state.Resolved.Target) |
| + } |
| + } |
| + if b.consumed != nil && b.consumed.Resolved != nil { |
| + add(b.consumed.Resolved.Target) |
| + } |
| + v := cands[w.rng.Intn(len(cands))] |
| + b.failed[v] = true |
| + return fmt.Sprintf("mark-failed %s on %s", v, b.name) |
| +} |
| + |
| +func (w *simWorld) toggleManual() string { |
| + if w.settings.Updates == UpdatesManual { |
| + w.settings.Updates = UpdatesAuto |
| + } else { |
| + w.settings.Updates = UpdatesManual |
| + } |
| + return "updates=" + w.settings.Updates |
| +} |
| + |
| +func (w *simWorld) pin() string { |
| + if w.settings.Pin != "" && w.rng.Intn(100) < 50 { |
| + w.settings.Pin = "" |
| + return "unpin" |
| + } |
| + w.settings.Pin = w.builds[w.rng.Intn(len(w.builds))] |
| + return "pin " + w.settings.Pin |
| +} |
| + |
| +func (w *simWorld) setMajor() string { |
| + switch w.rng.Intn(3) { |
| + case 0: |
| + w.settings.Major = nil |
| + return "major=none" |
| + default: |
| + m := 1 + w.rng.Intn(2) |
| + w.settings.Major = &m |
| + return fmt.Sprintf("major=%d", m) |
| + } |
| +} |
| + |
| +// heldNow is rule 3's condition from the model's own records. |
| +func (w *simWorld) heldNow() bool { |
| + u := w.settings |
| + if u.Updates == UpdatesManual { |
| + return true |
| + } |
| + return u.Major != nil && (w.major[w.head] == 0 || w.major[w.head] != *u.Major) |
| +} |
| + |
| +// wm is invariant 1's watermark for a pass or wake on box b: the highest |
| +// completed id in the bucket's build state or b's consumed file (spec §4.3 |
| +// rule 2), or in every box's consumed file in strict mode. |
| +func (w *simWorld) wm(b *simBox) uint64 { |
| + if w.strict { |
| + return w.watermarkAnywhere() |
| + } |
| + var m uint64 |
| + if w.state != nil { |
| + m = w.state.Completed |
| + } |
| + if b.consumed != nil && b.consumed.Completed > m { |
| + m = b.consumed.Completed |
| + } |
| + return m |
| +} |
| + |
| +// watermarkAnywhere is the highest completed id any record holds: the |
| +// build state and every box's consumed file. |
| +func (w *simWorld) watermarkAnywhere() uint64 { |
| + var m uint64 |
| + if w.state != nil { |
| + m = w.state.Completed |
| + } |
| + for _, b := range w.boxes { |
| + if b.consumed != nil && b.consumed.Completed > m { |
| + m = b.consumed.Completed |
| + } |
| + } |
| + return m |
| +} |
| + |
| +// boxView is what a pass on b can see of request r: pending (above both |
| +// sources' completed ids) and the T either source resolved it to. |
| +func boxView(c *Consumed, st *BuildState, r uint64) (pending bool, t string) { |
| + var m uint64 |
| + if c != nil { |
| + m = c.Completed |
| + } |
| + if st != nil && st.Completed > m { |
| + m = st.Completed |
| + } |
| + if r == 0 || r <= m { |
| + return false, "" |
| + } |
| + if c != nil && c.Resolved != nil && c.Resolved.ID == r { |
| + return true, c.Resolved.Target |
| + } |
| + if st != nil && st.Resolved != nil && st.Resolved.ID == r { |
| + return true, st.Resolved.Target |
| + } |
| + return true, "" |
| +} |
| + |
| +// rootPass is settingsTarget then adoptHost for the instance on box b. |
| +// resolve is root's pass (it writes the consumed file); false is the agent's |
| +// pass, which stops when the decision needs root's resolution. |
| +func (w *simWorld) rootPass(b *simBox, resolve bool) string { |
| + who := "root" |
| + if !resolve { |
| + who = "agent" |
| + } |
| + u := w.settings |
| + head := w.head |
| + wmBefore := w.wm(b) |
| + held := w.heldNow() |
| + |
| + // settingsTarget: a route with default settings and no consumed file is |
| + // today's adoption (no Target, no book, no consumed write). |
| + viaTarget := !(u.Default() && b.consumed == nil) |
| + var dec TargetDecision |
| + var in TargetInput |
| + if !viaTarget { |
| + dec = TargetDecision{Version: head, Reason: ReasonAdopt, Evidence: EvidencePointer, Bake: true, Detail: head} |
| + } else { |
| + in = TargetInput{ |
| + Route: registry.Route{Host: updateSimHost, Kind: "instance"}, |
| + Pointer: &ChannelPointer{Channel: "production", Version: head}, |
| + HeadTag: w.tags[head], |
| + Settings: u, |
| + Build: cloneSimCopy(b.copy), |
| + Consumed: cloneSimConsumed(b.consumed), |
| + Installed: b.live, |
| + } |
| + if !b.eligible[head] { |
| + in.HeadHeld = "in its supply-chain bake window" |
| + } |
| + failed := b.failed |
| + in.Failed = func(v string) bool { return failed[v] } |
| + dec = Target(in) |
| + w.checkDecision(b, in, dec, resolve, wmBefore, held) |
| + if resolve { |
| + next := NextConsumed(in, dec) |
| + b.consumed = &next |
| + // 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 && |
| + 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) |
| + } |
| + } else if dec.Resolve != nil && dec.Reason == ReasonRequest { |
| + return fmt.Sprintf("%s@%s %s: stops, relays to root", who, b.name, simDec(dec)) |
| + } |
| + } |
| + desc := fmt.Sprintf("%s@%s %s", who, b.name, simDec(dec)) |
| + |
| + // 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 != "" { |
| + 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]) { |
| + recovery = le |
| + w.stats.heldBakingPasses++ |
| + } |
| + } |
| + defer func() { |
| + if recovery != "" && b.live != recovery { |
| + w.fail(5, "held, request R%d unresolved behind baking head %s, last_executed %s authorized: live is %q after the pass (%s)", |
| + u.InstallRequest, head, recovery, b.live, simDec(dec)) |
| + } |
| + }() |
| + |
| + // adoptHost. |
| + ver := dec.Version |
| + if ver == "" { |
| + return desc + ": nothing installed" |
| + } |
| + if b.live == ver { |
| + return desc + ": up to date" |
| + } |
| + if (!viaTarget || dec.Bake) && !b.eligible[ver] { |
| + return desc + ": " + ver + " baking" |
| + } |
| + stagedBefore := b.staged[ver] |
| + switch { |
| + case !viaTarget || dec.Evidence == EvidencePointer: |
| + if ver != head { |
| + return desc + ": not the signed head, not staged" |
| + } |
| + case dec.Evidence == EvidenceRecord: |
| + if !w.promoted[ver] && !stagedBefore { |
| + return desc + ": no promotion record, no staged copy: refused" |
| + } |
| + default: |
| + return desc + ": no evidence" |
| + } |
| + |
| + // The repoint. |
| + if !(ver == head || w.promoted[ver] || stagedBefore) { |
| + w.fail(3, "repointed onto %s: not the head %s, no promotion record, not staged on %s", ver, head, b.name) |
| + } |
| + if viaTarget && b.failed[ver] { |
| + w.fail(4, "%s repointed onto %s, which it holds as failed (%s)", b.name, ver, simDec(dec)) |
| + } |
| + if viaTarget && held && u.Pin == "" { |
| + ok := !w.replica && ver == head |
| + if w.state != nil && w.state.LastExecuted == ver { |
| + ok = true |
| + } |
| + if r := u.InstallRequest; r > w.wm(b) { |
| + if _, t := boxView(b.consumed, w.state, r); t == ver { |
| + ok = true |
| + } |
| + } |
| + if !ok { |
| + w.fail(5, "held instance repointed onto %s: not last_executed %q, not a T of pending R%d, not a new instance's head (%s)", |
| + ver, simLE(w.state), u.InstallRequest, simDec(dec)) |
| + } |
| + } |
| + if recovery != "" && ver == recovery { |
| + w.stats.heldRecoveries++ |
| + } |
| + prev := b.live |
| + b.staged[ver] = true |
| + b.live = ver |
| + return fmt.Sprintf("%s: repoint %q->%s", desc, prev, ver) |
| +} |
| + |
| +// checkDecision checks invariants 1 and 6 on one Target decision, before |
| +// root writes it. |
| +func (w *simWorld) checkDecision(b *simBox, in TargetInput, dec TargetDecision, resolve bool, wmBefore uint64, held bool) { |
| + u := in.Settings |
| + r := u.InstallRequest |
| + head := in.Pointer.Version |
| + |
| + if !in.Build.Known && r != 0 { |
| + if w.state != nil && w.state.Completed >= r { |
| + w.stats.unknownWithCompleted++ |
| + } |
| + if in.Consumed != nil && in.Consumed.Resolved != nil && in.Consumed.Resolved.ID == r { |
| + w.stats.unknownReturning++ |
| + } |
| + } |
| + |
| + if all := w.watermarkAnywhere(); (dec.Reason == ReasonRequest && r <= all && r > wmBefore) || |
| + (resolve && dec.Resolve != nil && dec.Resolve.ID <= all && dec.Resolve.ID > wmBefore) { |
| + w.stats.leftBehind++ |
| + } |
| + |
| + // Invariant 1: rule 2 never selects a completed request. |
| + if dec.Reason == ReasonRequest && r <= wmBefore { |
| + w.fail(1, "rule 2 selected R%d (%s), already completed (watermark %d)", r, dec.Version, wmBefore) |
| + } |
| + if !resolve { |
| + return |
| + } |
| + if dec.Resolve != nil && dec.Resolve.ID <= wmBefore { |
| + 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 { |
| + pending, t := boxView(in.Consumed, in.Build.State, r) |
| + eligible := in.HeadHeld == "" || u.InstallFastTrack |
| + if pending && t == "" && eligible && r > wmBefore { |
| + if _, ok := w.firstEligible[r]; !ok { |
| + w.firstEligible[r] = head |
| + } |
| + if u.Pin != "" { |
| + w.stats.pinnedEligible++ |
| + } |
| + want := w.firstEligible[r] |
| + if dec.Resolve == nil || dec.Resolve.ID != r || dec.Resolve.Target != want { |
| + w.fail(6, "R%d pending and %s eligible on %s (first eligible %s), pin %q: the pass resolved %s", r, head, b.name, want, u.Pin, simRes(dec.Resolve)) |
| + } |
| + } |
| + } |
| + if dec.Resolve != nil { |
| + want, ok := w.firstEligible[dec.Resolve.ID] |
| + if !ok || want != dec.Resolve.Target { |
| + w.fail(6, "%s resolved R%d to %s; first eligible %q", b.name, dec.Resolve.ID, dec.Resolve.Target, want) |
| + } |
| + w.stats.resolutions++ |
| + if b.failed[dec.Resolve.Target] { |
| + w.stats.failedHeadResolutions++ |
| + } |
| + } |
| + if dec.Reason == ReasonRequest { |
| + if want := w.firstEligible[r]; dec.Version != want { |
| + w.fail(6, "rule 2 installs %s for R%d; first eligible %q", dec.Version, r, want) |
| + } |
| + } |
| + if dec.Fail != 0 { |
| + w.stats.failedCompletions++ |
| + } |
| +} |
| + |
| +// 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. |
| +func (w *simWorld) wake(b *simBox) string { |
| + run := b.live |
| + if run == "" { |
| + return "wake@" + b.name + ": nothing installed" |
| + } |
| + wmBefore := w.wm(b) |
| + cur := cloneSimState(w.state) |
| + next := NextBuildState(cur, cloneSimConsumed(b.consumed), run) |
| + next.Schema, next.Host = 1, updateSimHost |
| + |
| + if next.LastExecuted != run { |
| + w.fail(2, "wake ran %s; the build state says last_executed %q", run, next.LastExecuted) |
| + } |
| + var prev uint64 |
| + if cur != nil { |
| + prev = cur.Completed |
| + } |
| + // Only the current request: a newer one supersedes an older resolution. |
| + if r := w.settings.InstallRequest; cur != nil && cur.Resolved != nil && cur.Resolved.ID == r && cur.Resolved.Target == run && r > w.wm(b) && next.Completed < r { |
| + w.fail(1, "wake ran %s, the build state's T for pending R%d, and R%d stays pending (completed %d)", |
| + run, cur.Resolved.ID, cur.Resolved.ID, next.Completed) |
| + } |
| + if next.Completed > prev && !next.CompletedFailed { |
| + r := next.Completed |
| + if r <= wmBefore || w.completedByRun[r] { |
| + w.fail(1, "wake running %s records R%d newly completed; already completed (watermark %d)", run, r, wmBefore) |
| + } |
| + if next.Resolved == nil || next.Resolved.ID != r || next.Resolved.Target != run { |
| + w.fail(1, "wake running %s records R%d completed, but R%d's T is %s", run, r, r, simRes(next.Resolved)) |
| + } |
| + w.completedByRun[r] = true |
| + w.stats.runCompletions++ |
| + } |
| + w.state = &next |
| + 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) |
| +} |
| + |
| +// check is the per-step state check (invariant 2, and the model's own |
| +// consistency); event checks run inside the actions. |
| +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 { |
| + b := w.cur() |
| + u := w.settings |
| + s := fmt.Sprintf("[at %s live %q head %s req %d pin %q upd %s", b.name, b.live, w.head, u.InstallRequest, u.Pin, u.Updates) |
| + if u.Major != nil { |
| + s += fmt.Sprintf(" major %d", *u.Major) |
| + } |
| + if w.state != nil { |
| + s += fmt.Sprintf(" | state le %s res %s done %d%s", w.state.LastExecuted, simRes(w.state.Resolved), w.state.Completed, simFailedMark(w.state.CompletedFailed)) |
| + } |
| + if b.consumed != nil { |
| + s += fmt.Sprintf(" | consumed res %s done %d%s", simRes(b.consumed.Resolved), b.consumed.Completed, simFailedMark(b.consumed.CompletedFailed)) |
| + } |
| + if !b.copy.Known { |
| + s += " | copy unread" |
| + } |
| + return s + "]" |
| +} |
| + |
| +func simFailedMark(f bool) string { |
| + if f { |
| + return " failed" |
| + } |
| + return "" |
| +} |
| + |
| +func simDec(d TargetDecision) string { |
| + s := fmt.Sprintf("{%s %q", d.Reason, d.Version) |
| + if d.Resolve != nil { |
| + s += " resolve " + simRes(d.Resolve) |
| + } |
| + if d.Fail != 0 { |
| + s += fmt.Sprintf(" fail R%d", d.Fail) |
| + } |
| + return s + "}" |
| +} |
| + |
| +func simRes(r *ResolvedRequest) string { |
| + if r == nil { |
| + return "-" |
| + } |
| + return fmt.Sprintf("R%d->%s", r.ID, r.Target) |
| +} |
| + |
| +func simLE(s *BuildState) string { |
| + if s == nil { |
| + return "" |
| + } |
| + return s.LastExecuted |
| +} |
| + |
| +func simStatesEqual(a, b *BuildState) bool { |
| + if a == nil || b == nil { |
| + return a == nil && b == nil |
| + } |
| + ra, rb := simRes(a.Resolved), simRes(b.Resolved) |
| + return a.LastExecuted == b.LastExecuted && ra == rb && a.Completed == b.Completed && a.CompletedFailed == b.CompletedFailed |
| +} |
| + |
| +func cloneSimState(s *BuildState) *BuildState { |
| + if s == nil { |
| + return nil |
| + } |
| + v := *s |
| + v.Resolved = cloneSimResolved(s.Resolved) |
| + return &v |
| +} |
| + |
| +func cloneSimConsumed(c *Consumed) *Consumed { |
| + if c == nil { |
| + return nil |
| + } |
| + v := *c |
| + v.Resolved = cloneSimResolved(c.Resolved) |
| + return &v |
| +} |
| + |
| +func cloneSimCopy(c BuildStateCopy) BuildStateCopy { |
| + c.State = cloneSimState(c.State) |
| + return c |
| +} |
| + |
| +func cloneSimResolved(r *ResolvedRequest) *ResolvedRequest { |
| + if r == nil { |
| + return nil |
| + } |
| + v := *r |
| + return &v |
| +} |