carlos / platform Public

Clone
git clone https://amadan.net/carlos/platform

Plain git — no account needed to clone.

Download

Download this file

1package release
2
3import (
4 "fmt"
5 "math/rand"
6 "os"
7 "sort"
8 "strconv"
9 "strings"
10 "sync"
11 "testing"
12
13 "github.com/carlosframework/platform/internal/registry"
14)
15
16// TestUpdateRequestLifecycleSimulation runs random schedules of one
17// instance's update life across three boxes (settings plan 4 Task 11): the
18// channel head moves and bakes, the member presses "Update now", pins,
19// unpins and holds, root and agent passes decide and repoint, wakes run
20// builds against the database, boxes are lost and the instance moves.
21//
22// The decisions are production's: rootPass calls Target and NextConsumed;
23// wake calls DecideHeldWake (the held wake check, ruling R-HELD-PURE) and
24// enforces it as the activator's wakeCheck does (refuse, run the target, or
25// wait for root), then HeldExecStale and NextBuildState (beforeExec, ruling
26// R-MERGE); a graceful move calls CarryRequest (ruling R-SPEC-43A-2), and
27// root's write of its record passes publishGate, the re-check root makes
28// under the carry fence (ruling R-CARRY-FENCE). What
29// surrounds them is not pure (settingsTarget's file and registry reads,
30// adoptHost's bake, evidence and repoint, beforeExec's bucket write, the
31// wake's wait) and is mirrored here in the smallest form that keeps its
32// decisions.
33//
34// The invariants are checked against the model's own records, never against
35// production helpers (a mutant of Watermark must not also move the oracle):
36//
37// 1. A completed request never runs again: once the watermark is >= R, no
38// box resolves R again, rule 2 never selects R again, and no wake
39// records R as newly completed. A wake that completes R does so because
40// R's T ran, and a wake that runs the build state's T for a pending R
41// completes it. The watermark is spec §4.3 rule 2's (ruling R-INV1): the
42// highest completed id in the bucket's build state (the true object,
43// whatever the box's copy says) or in the consumed file of the box doing
44// the pass, and also every failed completion a box had recorded when the
45// instance left it by a graceful move (ruling R-INV1-2: the move carries
46// it; only a lost box's records are exempt). UPDATESIM_STRICT=1 reads
47// every box's consumed file at once instead; that is documentation of a
48// known gap, not the gate (below).
49// 2. The build state names the build that last touched the database.
50// 3. No install lacks evidence. At the decision: Target names pointer
51// evidence only for the head, and asks for bake only on the head. At
52// the repoint: the build is the head, has a promotion record, or is the
53// box's own staged copy; that half holds by construction of the
54// adoptHost mirror (its evidence switch), and is kept as a tripwire.
55// 4. Failure records outrank: no repoint a Target decision makes for a
56// route with settings lands on a build the box holds as failed (the
57// model never sets GoodVersion, so no instance has served a failed
58// build). A route with default settings keeps today's adoption, which
59// never reads the book, consumed file or not (rulings R-T6-BOOK,
60// R-T6-BOOK-2; adopt.go settingsTarget's !plain), so it is out of scope.
61// 5. Unresolved requests block nothing: a held instance with an unresolved
62// request whose head is baking recovers onto last_executed; and a held
63// instance (no pin) never repoints anywhere but last_executed, a T its
64// pending request was resolved to, or, never having run, the head.
65// 6. A request resolves at its first eligible pass, pin or not: the world
66// records firstEligible[R], the head at the first root pass where R is
67// pending, the build state is read (R-TARGET-UNKNOWN) and the head is
68// eligible on that box (or the request asked for fast track). That pass
69// must resolve R to it; every resolution of R a box records, and every
70// rule 2 install of R, names exactly that build. A resolution the
71// instance can no longer see was never run (a run completes R in the
72// build state), so it is spec §4.2's "Lost requests": firstEligible[R]
73// is cleared and the next eligible pass resolves R again. A record the
74// instance sees again (it returned to the box holding it) is R's
75// resolution once more; when the build state and the box's file both
76// hold one, the build state's is (ruling R-RESOLUTION-STATE-WINS), and
77// root's next pass with the state read rewrites the file to agree.
78// 7. A wake runs only what the rules allow (§4.3 rule 3, "The wake checks
79// too"; ruling R-HELD-PURE), from the model's own records: a pinned
80// instance runs its pin; one with a pending request resolved to T runs
81// T; a held one runs the bucket's last_executed. Held is manual, or a
82// major setting whose head, as of root's last decision on this box, has
83// no tag or another major, or a major setting root has not decided for
84// yet (a missing or stale decision never makes a wake unheld).
85//
86// Copies (the agent's registry copy root and the wake read) go stale the ways
87// production keeps them stale: a refresh that fails keeps the last known
88// state and records ReadErr; a box the instance returns to may still hold its
89// row from the earlier stay, copy and all, its refreshes failed while the
90// instance was away. Root reads such a copy as unread (BuildStateCopy.Read).
91// The wake refreshes first and is refused when that fails (Astra round 1
92// finding 1).
93//
94// Strict mode (UPDATESIM_STRICT=1) checks invariants 1 and 6 across every
95// box's consumed file, not only the one the instance is on. It is not the
96// gate (ruling R-INV1): a LOST box's records are the spec's lost request
97// (§4.2), and strict mode counts them.
98//
99// Seeds: UPDATESIM_SEEDS (default 200), spread over UPDATESIM_PAR goroutines
100// (default 1); each seed has its own rand source and world. UPDATESIM_SEED=n
101// replays seed n alone. A failure prints the seed, the step and the trace,
102// and a line "INVARIANT <n> ..." per invariant any seed violated.
103func TestUpdateRequestLifecycleSimulation(t *testing.T) {
104 t.Run("seed 531 shape, unpinned", testUpdateSimSeed531Unpinned)
105 t.Run("carry fence, a failed completion racing a cut", testUpdateSimCarryFence)
106 t.Run("a file and the build state disagree on R1", testUpdateSimDisagreement)
107 seeds := updateSimEnv(t, "UPDATESIM_SEEDS", 200)
108 par := updateSimEnv(t, "UPDATESIM_PAR", 1)
109 first := 0
110 if v := os.Getenv("UPDATESIM_SEED"); v != "" {
111 n, err := strconv.Atoi(v)
112 if err != nil {
113 t.Fatal(err)
114 }
115 first, seeds = n, 1
116 }
117 if par < 1 {
118 par = 1
119 }
120 strict := os.Getenv("UPDATESIM_STRICT") == "1"
121 results := make([]updateSimResult, seeds)
122 jobs := make(chan int)
123 var wg sync.WaitGroup
124 for i := 0; i < par; i++ {
125 wg.Add(1)
126 go func() {
127 defer wg.Done()
128 for i := range jobs {
129 results[i] = runUpdateSim(int64(first+i), updateSimSteps, strict)
130 }
131 }()
132 }
133 for i := 0; i < seeds; i++ {
134 jobs <- i
135 }
136 close(jobs)
137 wg.Wait()
138
139 var total updateSimStats
140 byInv := map[int][]*updateSimFailure{}
141 for i := range results {
142 total.add(results[i].stats)
143 if f := results[i].fail; f != nil {
144 seen := map[int]bool{}
145 for _, v := range f.viols {
146 if !seen[v.inv] {
147 seen[v.inv] = true
148 byInv[v.inv] = append(byInv[v.inv], f)
149 }
150 }
151 }
152 }
153 t.Logf("%d seeds x %d steps (par %d, strict %v): %s", seeds, updateSimSteps, par, strict, total)
154 invs := make([]int, 0, len(byInv))
155 for inv := range byInv {
156 invs = append(invs, inv)
157 }
158 sort.Ints(invs)
159 for _, inv := range invs {
160 fs := byInv[inv]
161 f := fs[0]
162 var msg string
163 for _, v := range f.viols {
164 if v.inv == inv {
165 msg = v.msg
166 break
167 }
168 }
169 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",
170 inv, updateSimInvariants[inv], len(fs), seeds, f.seed, f.step, f.action, msg, f.seed, strings.Join(f.trace, "\n"))
171 }
172}
173
174// testUpdateSimSeed531Unpinned replays the shape seed 531 found, through
175// the model's own actions (so every invariant is checked at every step) and
176// so through the production Target, NextConsumed, DecideHeldWake,
177// CarryRequest, publishGate and NextBuildState. Box 0 runs a root pass that
178// was already running when the cut began; before the carry fence its write
179// landed after the cut carried box 0's record and stayed in box 0's file
180// only. Under the fence (ruling R-CARRY-FENCE) it comes after the carry, so
181// it meets the cut's hold and writes nothing. Box 1 resolves R1, to b3,
182// under a pin set after the request, and its wake (running the pin) carries
183// {R1, b3} into the build state; the instance returns to box 0, which holds
184// no record of R1, and the pin is cleared. Rule 2 must then install the
185// build state's b3, and the wake that runs it must complete R1.
186func testUpdateSimSeed531Unpinned(t *testing.T) {
187 w := newUpdateSimWorld(0, false)
188 w.scripted = true
189 for i := range w.boxes {
190 w.boxes[i] = newSimBox(fmt.Sprintf("box%d", i))
191 }
192 w.builds = []string{"b1", "b2", "b3"}
193 for i, b := range w.builds {
194 w.tags[b], w.major[b], w.promoted[b] = fmt.Sprintf("1.%d.0", i+1), 1, true
195 }
196 w.head = "b2"
197 for _, b := range w.boxes[:2] {
198 b.eligible["b1"], b.eligible["b2"] = true, true
199 }
200 w.state = &BuildState{Schema: 1, Host: updateSimHost, LastExecuted: "b1"}
201 w.lastRan, w.replica = "b1", true
202 w.at = 0
203 w.boxes[0].live, w.boxes[0].staged["b1"] = "b1", true
204 w.boxes[0].copy = BuildStateCopy{Known: true, Replica: true, State: cloneSimState(w.state)}
205 w.settings = UpdateSettings{Updates: UpdatesManual, InstallRequest: 1}
206
207 steps := []func() string{
208 func() string { w.settings.Pin = "b1"; return "pin b1 (after the request)" },
209 func() string {
210 return w.moveToRacing(1, true, func() string { return w.rootPass(w.boxes[0], true) }, true)
211 },
212 func() string { w.head = "b3"; w.boxes[1].eligible["b3"] = true; return "promote b3, baked on box1" },
213 func() string { return w.rootPass(w.boxes[1], true) },
214 func() string { return w.wake(w.boxes[1]) },
215 func() string { return w.moveTo(0, true) },
216 func() string { w.settings.Pin = ""; return "unpin" },
217 func() string { return w.rootPass(w.boxes[0], true) },
218 func() string { return w.wake(w.boxes[0]) },
219 }
220 if !runScriptedSim(t, "the scripted seed-531 shape", w, steps) {
221 return
222 }
223 if c := w.boxes[0].consumed; c != nil && c.Resolved != nil && c.Resolved.Target == "b2" {
224 t.Errorf("scripted seed-531 shape: box0's racing pass published {R1, b2} under the cut's hold\ntrace:\n%s", strings.Join(w.trace, "\n"))
225 }
226 if st := w.state; st == nil || st.Completed != 1 || st.CompletedFailed || w.boxes[0].live != "b3" {
227 t.Errorf("scripted seed-531 shape: after the unpinned pass and wake on box0, live %q, build state %+v; want b3 live and R1 completed by it\ntrace:\n%s",
228 w.boxes[0].live, w.state, strings.Join(w.trace, "\n"))
229 }
230 t.Logf("trace:\n%s", strings.Join(w.trace, "\n"))
231}
232
233// runScriptedSim runs a scripted shape's steps, checking every invariant
234// after each; false when one failed (reported).
235func runScriptedSim(t *testing.T, name string, w *simWorld, steps []func() string) bool {
236 t.Helper()
237 for i, step := range steps {
238 w.viols = nil
239 action := step()
240 w.trace = append(w.trace, fmt.Sprintf("%3d %s %s", i+1, action, w.summary()))
241 w.check()
242 for _, v := range w.viols {
243 t.Errorf("INVARIANT %d (%s) violated in %s at step %d (%s): %s\ntrace:\n%s",
244 v.inv, updateSimInvariants[v.inv], name, i+1, action, v.msg, strings.Join(w.trace, "\n"))
245 }
246 if len(w.viols) > 0 {
247 return false
248 }
249 }
250 return true
251}
252
253// testUpdateSimDisagreement gates resolvedFor's order (ruling
254// R-RESOLUTION-STATE-WINS; ruling R-M9-SCRIPTED) on a state built directly:
255// box 0's consumed file resolves the pending R1 to b1 while the build state
256// resolves the same R1 to b3, unpinned and manual. Under the carry fence no
257// graceful path in this model leaves that state behind any more. It is still
258// reachable in production from a box running a pre-fence binary (a racing
259// root pass wrote its record after the cut's carry), or from a registry copy
260// that stays stale for one reconcile without a read error (root resolves R1
261// again from a copy that lacks the state's resolution). Root's rule 2 must
262// install the build state's b3 (through the production Target and
263// NextConsumed), and the wake that runs it must complete R1 (DecideHeldWake,
264// HeldExecStale and NextBuildState). Following the file would run b1, which
265// never completes R1.
266func testUpdateSimDisagreement(t *testing.T) {
267 w := newUpdateSimWorld(0, false)
268 w.scripted = true
269 for i := range w.boxes {
270 w.boxes[i] = newSimBox(fmt.Sprintf("box%d", i))
271 }
272 w.builds = []string{"b1", "b2", "b3"}
273 for i, b := range w.builds {
274 w.tags[b], w.major[b], w.promoted[b] = fmt.Sprintf("1.%d.0", i+1), 1, true
275 }
276 w.head = "b3"
277 for _, b := range w.boxes {
278 b.eligible["b1"], b.eligible["b2"], b.eligible["b3"] = true, true, true
279 }
280 w.state = &BuildState{Schema: 1, Host: updateSimHost, LastExecuted: "b2", Resolved: &ResolvedRequest{ID: 1, Target: "b3"}}
281 w.lastRan, w.replica = "b2", true
282 w.at = 0
283 b0 := w.boxes[0]
284 b0.live, b0.staged["b2"] = "b2", true
285 b0.copy = BuildStateCopy{Known: true, Replica: true, State: cloneSimState(w.state)}
286 b0.consumed = &Consumed{Schema: 1, Host: updateSimHost, Resolved: &ResolvedRequest{ID: 1, Target: "b1"}}
287 w.settings = UpdateSettings{Updates: UpdatesManual, InstallRequest: 1}
288 // R1's resolution as the world records it: the build state's
289 // (R-RESOLUTION-STATE-WINS), so invariant 6 judges installs against b3.
290 w.syncResolutions()
291 steps := []func() string{
292 func() string { return w.rootPass(b0, true) },
293 func() string { return w.wake(b0) },
294 }
295 const name = "the scripted disagreement (file {R1, b1}, build state {R1, b3})"
296 // The outcome is asserted even when an invariant stopped the steps early.
297 runScriptedSim(t, name, w, steps)
298 if st := w.state; b0.live != "b3" || st == nil || st.LastExecuted != "b3" || st.Completed != 1 || st.CompletedFailed {
299 t.Errorf("%s: live %q, build state %+v; want rule 2 to install the build state's b3 and its wake to complete R1\ntrace:\n%s",
300 name, b0.live, st, strings.Join(w.trace, "\n"))
301 }
302 t.Logf("%s, trace:\n%s", name, strings.Join(w.trace, "\n"))
303}
304
305// testUpdateSimCarryFence is Astra round 2 finding 2's shape (ruling
306// R-CARRY-FENCE), scripted both ways. Box 0 resolves R1 to b2 and installs
307// it; b2 then fails on box 0, so root's next pass there records R1
308// completed, failed. That pass races a graceful cut to box 1. Early (its
309// fence first) it publishes, and the cut carries the failed completion: box
310// 1 never selects R1. Late (the cut's fence first) it meets the cut's hold
311// and publishes nothing: R1 is still pending with T b2, which box 1 does not
312// hold as failed, so box 1 installs b2 and its wake completes R1. A late
313// record published past the hold (the fence's re-check removed) is left
314// behind on box 0, and box 1 selects R1 after it completed (invariant 1).
315func testUpdateSimCarryFence(t *testing.T) {
316 for _, late := range []bool{false, true} {
317 name := "the carry fence, root's pass before the hold"
318 if late {
319 name = "the carry fence, root's pass after the carry"
320 }
321 w := newUpdateSimWorld(0, false)
322 w.scripted = true
323 for i := range w.boxes {
324 w.boxes[i] = newSimBox(fmt.Sprintf("box%d", i))
325 }
326 w.builds = []string{"b1", "b2"}
327 for i, b := range w.builds {
328 w.tags[b], w.major[b], w.promoted[b] = fmt.Sprintf("1.%d.0", i+1), 1, true
329 }
330 w.head = "b2"
331 for _, b := range w.boxes {
332 b.eligible["b1"], b.eligible["b2"] = true, true
333 }
334 w.state = &BuildState{Schema: 1, Host: updateSimHost, LastExecuted: "b1"}
335 w.lastRan, w.replica = "b1", true
336 w.at = 0
337 w.boxes[0].live, w.boxes[0].staged["b1"] = "b1", true
338 w.boxes[0].copy = BuildStateCopy{Known: true, Replica: true, State: cloneSimState(w.state)}
339 w.settings = UpdateSettings{Updates: UpdatesManual, InstallRequest: 1}
340 steps := []func() string{
341 func() string { return w.rootPass(w.boxes[0], true) },
342 func() string { w.boxes[0].failed["b2"] = true; return "mark-failed b2 on box0" },
343 func() string {
344 return w.moveToRacing(1, true, func() string { return w.rootPass(w.boxes[0], true) }, late)
345 },
346 func() string { return w.rootPass(w.boxes[1], true) },
347 func() string { return w.wake(w.boxes[1]) },
348 }
349 if !runScriptedSim(t, name, w, steps) {
350 continue
351 }
352 st, c := w.state, w.boxes[0].consumed
353 switch {
354 case !late && (st == nil || st.Completed != 1 || !st.CompletedFailed || w.boxes[1].live == "b2"):
355 t.Errorf("%s: build state %+v, box1 live %q; want R1 carried completed, failed, and b2 never installed on box1\ntrace:\n%s",
356 name, st, w.boxes[1].live, strings.Join(w.trace, "\n"))
357 case late && (c == nil || c.Completed != 0 || st == nil || st.Completed != 1 || st.CompletedFailed || w.boxes[1].live != "b2"):
358 t.Errorf("%s: box0's file %+v, build state %+v, box1 live %q; want nothing published on box0, b2 installed on box1 and R1 completed by its run\ntrace:\n%s",
359 name, c, st, w.boxes[1].live, strings.Join(w.trace, "\n"))
360 }
361 t.Logf("%s, trace:\n%s", name, strings.Join(w.trace, "\n"))
362 }
363}
364
365const (
366 updateSimHost = "blog.example.com"
367 updateSimSteps = 80
368 updateSimBoxes = 3
369)
370
371var updateSimInvariants = map[int]string{
372 0: "model consistency",
373 1: "a completed request never runs again",
374 2: "the build state names the build that last touched the database",
375 3: "no install lacks evidence",
376 4: "failure records outrank",
377 5: "unresolved requests block nothing",
378 6: "a request resolves at its first eligible pass, pin or not",
379 7: "a wake runs only what the rules allow",
380}
381
382func updateSimEnv(t *testing.T, name string, def int) int {
383 v := os.Getenv(name)
384 if v == "" {
385 return def
386 }
387 n, err := strconv.Atoi(v)
388 if err != nil || n < 0 {
389 t.Fatalf("%s=%q: want a count", name, v)
390 }
391 return n
392}
393
394// simBox is one box's view of the instance: root's consumed file, the live
395// link, the failure book, the version store's staged copies, the bake clock
396// (versions whose window has run here) and the agent's registry copy of the
397// build state, which is what root reads.
398type simBox struct {
399 name string
400 // status is the row's status on this box: "" (ready), or "moving" from
401 // the moment a cut holds it until the hand-over.
402 status string
403 consumed *Consumed
404 live string
405 failed map[string]bool
406 staged map[string]bool
407 eligible map[string]bool
408 copy BuildStateCopy
409 // The model's own record of root's last decision on this box (for
410 // invariant 7, never Consumed.Settings): the settings column it decided
411 // for and the head it saw. decided is false until root's first pass.
412 decided bool
413 decidedSettings string
414 decidedHead string
415}
416
417// simWorld is the instance and everything around it. state is the bucket
418// object (nil until the first pre-exec write). replica is whether the
419// instance has a database (a legacy instance has one with no build state).
420type simWorld struct {
421 boxes []*simBox
422 at int
423 state *BuildState
424 replica bool
425 settings UpdateSettings
426 head string
427 builds []string
428 tags map[string]string
429 major map[string]int // 0: the build has no semver tag
430 promoted map[string]bool
431 lastRan string
432 rng *rand.Rand
433 strict bool
434
435 firstEligible map[uint64]string
436 completedByRun map[uint64]bool
437 // carried is the highest failed completion any box had recorded when
438 // the instance left it by a graceful move (ruling R-INV1-2): invariant
439 // 1's watermark includes it. Only a lost box's records are exempt.
440 carried uint64
441 // scripted turns off the random faults (a failed refresh, a wait root
442 // does not answer), for the scripted shapes.
443 scripted bool
444
445 trace []string
446 viols []updateSimViolation
447 stats updateSimStats
448}
449
450type updateSimViolation struct {
451 inv int
452 msg string
453}
454
455type updateSimFailure struct {
456 seed int64
457 step int
458 action string
459 viols []updateSimViolation
460 trace []string
461}
462
463type updateSimResult struct {
464 fail *updateSimFailure
465 stats updateSimStats
466}
467
468// updateSimStats counts the scenarios the invariants need, so a clean run
469// shows they were reached.
470type updateSimStats struct {
471 resolutions, runCompletions, failedCompletions int
472 failedHeadResolutions int // R-TARGET-FAILEDHEAD
473 heldRecoveries int // invariant 5's scenario, repointing onto last_executed
474 heldBakingPasses int // invariant 5's scenario, any
475 unknownWithCompleted int // Known false, the current request already completed (R-TARGET-UNKNOWN)
476 unknownReturning int // Known false on a box whose consumed file names the current request
477 pinnedEligible int // invariant 6 under a pin
478 lostResolutions int
479 pickedUp int // a move or return made another record of R the one in force
480 leftBehind int // a resolution or rule 2 pick strict mode would refuse
481 moves, returns int
482 carriedRequests int // graceful moves whose cut carried a request record
483 carriedFailed int // ... a failed completion among them
484 unreadRefusals int // wakes refused: their refresh failed
485 askRoot int // wakes with no decision from root for the settings
486 askRootRuns int // ... that ran the installed build at once
487 rootWaits int // wakes that asked root and waited
488 heldRuns int // wakes that ran a held target
489 retainedRuns int // ... from a retained copy
490 keptCopies int // returns onto a kept, possibly stale, copy
491 racingEarly int // root passes racing a cut that published before its carry
492 racingFenced int // ... that met the move hold under the fence: nothing published
493}
494
495func (s *updateSimStats) add(o updateSimStats) {
496 s.resolutions += o.resolutions
497 s.runCompletions += o.runCompletions
498 s.failedCompletions += o.failedCompletions
499 s.failedHeadResolutions += o.failedHeadResolutions
500 s.heldRecoveries += o.heldRecoveries
501 s.heldBakingPasses += o.heldBakingPasses
502 s.unknownWithCompleted += o.unknownWithCompleted
503 s.unknownReturning += o.unknownReturning
504 s.pinnedEligible += o.pinnedEligible
505 s.lostResolutions += o.lostResolutions
506 s.pickedUp += o.pickedUp
507 s.leftBehind += o.leftBehind
508 s.moves += o.moves
509 s.returns += o.returns
510 s.carriedRequests += o.carriedRequests
511 s.carriedFailed += o.carriedFailed
512 s.unreadRefusals += o.unreadRefusals
513 s.askRoot += o.askRoot
514 s.askRootRuns += o.askRootRuns
515 s.rootWaits += o.rootWaits
516 s.heldRuns += o.heldRuns
517 s.retainedRuns += o.retainedRuns
518 s.keptCopies += o.keptCopies
519 s.racingEarly += o.racingEarly
520 s.racingFenced += o.racingFenced
521}
522
523func (s updateSimStats) String() string {
524 return fmt.Sprintf("resolutions %d (failed head %d, under a pin %d), run completions %d, failed completions %d, "+
525 "held+baking passes %d (recoveries onto last_executed %d), unread state with the request completed %d, "+
526 "unread state on a returning box %d, lost resolutions %d, records picked up by a move %d, "+
527 "left-behind records acted past %d, moves %d (returns %d, onto a kept copy %d), "+
528 "cuts that carried a request record %d (a failed completion %d), wakes refused unread %d, "+
529 "wakes with no decision for the settings %d (ran the installed build %d), wakes that waited on root %d, "+
530 "held runs %d (from a retained copy %d), root passes racing a cut %d (published before the carry %d, fenced %d)",
531 s.resolutions, s.failedHeadResolutions, s.pinnedEligible, s.runCompletions, s.failedCompletions,
532 s.heldBakingPasses, s.heldRecoveries, s.unknownWithCompleted, s.unknownReturning, s.lostResolutions,
533 s.pickedUp, s.leftBehind, s.moves, s.returns, s.keptCopies, s.carriedRequests, s.carriedFailed,
534 s.unreadRefusals, s.askRoot, s.askRootRuns, s.rootWaits, s.heldRuns, s.retainedRuns,
535 s.racingEarly+s.racingFenced, s.racingEarly, s.racingFenced)
536}
537
538func newUpdateSimWorld(seed int64, strict bool) *simWorld {
539 w := &simWorld{
540 rng: rand.New(rand.NewSource(seed)),
541 strict: strict,
542 settings: UpdateSettings{Updates: UpdatesAuto},
543 tags: map[string]string{},
544 major: map[string]int{},
545 promoted: map[string]bool{},
546 firstEligible: map[uint64]string{},
547 completedByRun: map[uint64]bool{},
548 }
549 for i := 0; i < updateSimBoxes; i++ {
550 w.boxes = append(w.boxes, newSimBox(fmt.Sprintf("box%d", i)))
551 }
552 w.head = "b1"
553 w.builds = []string{"b1"}
554 w.tags["b1"], w.major["b1"], w.promoted["b1"] = "1.1.0", 1, true
555 w.boxes[0].eligible["b1"] = true
556 if w.rng.Intn(100) < 30 {
557 // An instance from before this feature: a database, a live link, no
558 // build state.
559 w.replica = true
560 w.boxes[0].live = "b1"
561 w.boxes[0].staged["b1"] = true
562 }
563 if w.rng.Intn(100) < 25 {
564 w.settings.Updates = UpdatesManual
565 }
566 return w
567}
568
569func newSimBox(name string) *simBox {
570 return &simBox{name: name, failed: map[string]bool{}, staged: map[string]bool{}, eligible: map[string]bool{}}
571}
572
573func runUpdateSim(seed int64, steps int, strict bool) updateSimResult {
574 w := newUpdateSimWorld(seed, strict)
575 for step := 1; step <= steps; step++ {
576 w.viols = nil
577 action := w.act()
578 w.trace = append(w.trace, fmt.Sprintf("%3d %s %s", step, action, w.summary()))
579 w.check()
580 if len(w.viols) > 0 {
581 return updateSimResult{stats: w.stats, fail: &updateSimFailure{seed: seed, step: step, action: action, viols: w.viols, trace: w.trace}}
582 }
583 }
584 return updateSimResult{stats: w.stats}
585}
586
587func (w *simWorld) fail(inv int, format string, args ...any) {
588 w.viols = append(w.viols, updateSimViolation{inv: inv, msg: fmt.Sprintf(format, args...)})
589}
590
591func (w *simWorld) cur() *simBox { return w.boxes[w.at] }
592
593// act picks one action at random and applies it.
594func (w *simWorld) act() string {
595 weights := []int{8, 7, 9, 22, 5, 9, 14, 4, 2, 5, 5, 5, 3}
596 sum := 0
597 for _, x := range weights {
598 sum += x
599 }
600 n := w.rng.Intn(sum)
601 i := 0
602 for ; n >= weights[i]; i++ {
603 n -= weights[i]
604 }
605 switch i {
606 case 0:
607 return w.updateNow()
608 case 1:
609 return w.promote()
610 case 2:
611 return w.expireBake()
612 case 3:
613 return w.rootPass(w.cur(), true)
614 case 4:
615 return w.rootPass(w.cur(), false)
616 case 5:
617 return w.refresh()
618 case 6:
619 return w.wake(w.cur())
620 case 7:
621 return w.move()
622 case 8:
623 return w.loseBox()
624 case 9:
625 return w.markFailed()
626 case 10:
627 return w.toggleManual()
628 case 11:
629 return w.pin()
630 default:
631 return w.setMajor()
632 }
633}
634
635// updateNow is the console's "Update now": a new request id. The console
636// refuses it on a pinned instance (console apiupdates.go); a pin set while a
637// request is pending is allowed, so the model sets pins either way.
638func (w *simWorld) updateNow() string {
639 if w.settings.Pin != "" {
640 return "update-now refused: pinned"
641 }
642 w.settings.InstallRequest++
643 w.settings.InstallFastTrack = w.rng.Intn(100) < 20
644 return fmt.Sprintf("update-now R%d fast=%v", w.settings.InstallRequest, w.settings.InstallFastTrack)
645}
646
647// promote moves the channel head: a new build (no box has baked it yet), or
648// a pull-back to an earlier one, which stays eligible wherever it baked.
649func (w *simWorld) promote() string {
650 if len(w.builds) > 1 && w.rng.Intn(100) < 15 {
651 var older []string
652 for _, b := range w.builds {
653 if b != w.head {
654 older = append(older, b)
655 }
656 }
657 w.head = older[w.rng.Intn(len(older))]
658 return "promote pull-back " + w.head
659 }
660 n := len(w.builds) + 1
661 b := fmt.Sprintf("b%d", n)
662 w.builds = append(w.builds, b)
663 w.head = b
664 w.promoted[b] = w.rng.Intn(100) < 85
665 switch r := w.rng.Intn(100); {
666 case r < 10:
667 w.major[b], w.tags[b] = 0, ""
668 default:
669 m := 1
670 if r >= 75 {
671 m = 2
672 }
673 w.major[b], w.tags[b] = m, fmt.Sprintf("%d.%d.0", m, n)
674 }
675 return fmt.Sprintf("promote %s record=%v tag=%q", b, w.promoted[b], w.tags[b])
676}
677
678func (w *simWorld) expireBake() string {
679 b := w.cur()
680 if w.rng.Intn(100) >= 60 {
681 b = w.boxes[w.rng.Intn(len(w.boxes))]
682 }
683 b.eligible[w.head] = true
684 return fmt.Sprintf("bake-expired %s on %s", w.head, b.name)
685}
686
687// refresh is the agent reading the bucket object into its registry copy.
688// One that fails keeps the last known copy and records ReadErr, as
689// buildStates.refresh does.
690func (w *simWorld) refresh() string {
691 b := w.cur()
692 if w.refreshCopy(b) {
693 return "refresh " + b.name
694 }
695 return "refresh " + b.name + " FAILED (copy kept, read error)"
696}
697
698// refreshCopy is buildStates.refresh on b: true when the read succeeded.
699func (w *simWorld) refreshCopy(b *simBox) bool {
700 if !w.scripted && w.rng.Intn(100) < 15 {
701 b.copy.ReadErr = "s3: timeout"
702 return false
703 }
704 b.copy = BuildStateCopy{Known: true, Replica: w.replica, State: cloneSimState(w.state)}
705 return true
706}
707
708// move hands the instance to another box with its replica and build state:
709// a graceful move (a legacy cut, a Phase 1 cut, a rollback's return). The
710// destination's registry row is new (copy unread) or carries the source's
711// column (registry coldhandover copies build_state); a box the instance
712// returns to may still hold its row from the earlier stay, old copy and all
713// (a rolled-back move's source keeps its row). It still has its old consumed
714// file and live link either way.
715//
716// A third of moves race a root pass on the source that was already running
717// when the cut began (Astra round 2 finding 2). Under the carry fence it
718// either published before the cut's carry, which takes its record, or meets
719// the cut's hold and publishes nothing (moveToRacing).
720func (w *simWorld) move() string {
721 j := w.rng.Intn(len(w.boxes) - 1)
722 if j >= w.at {
723 j++
724 }
725 carried := w.rng.Intn(100) < 50
726 if w.rng.Intn(100) < 33 {
727 src := w.cur()
728 return w.moveToRacing(j, carried, func() string { return w.rootPass(src, true) }, w.rng.Intn(100) < 50)
729 }
730 return w.moveTo(j, carried)
731}
732
733// moveTo moves the instance to box j; carried is whether the destination's
734// registry row carries the source's build-state copy.
735func (w *simWorld) moveTo(j int, carried bool) string {
736 return w.moveToRacing(j, carried, nil, false)
737}
738
739// moveToRacing is moveTo with race, when set, a root pass on the source that
740// was already running when the cut began, modelled through the carry fence
741// (ruling R-CARRY-FENCE). Root's publication and the cut's carry serialize
742// on one lock, the cut takes it only once its hold is effective, and root
743// re-checks the hold under it (publishGate, in rootPass). So the race runs
744// either before the hold (early: its fence came first; it publishes, and
745// the carry below takes the record) or after the carry (late: its fence
746// came second; it meets the hold and publishes nothing). The cut holds the
747// row ("moving"), then carries the source's request record into the build
748// state under the lease (release.CarryRequest; ruling R-SPEC-43A-2), and the
749// source's registry copy follows the write, as buildStates.write sets it.
750// Invariant 1's carried watermark is the source's file at the hand-over,
751// after both (Astra round 2's simulation note: never sampled before a
752// racing callback).
753func (w *simWorld) moveToRacing(j int, carried bool, race func() string, late bool) string {
754 src := w.cur()
755 dst := w.boxes[j]
756 note := ""
757 if race != nil && !late {
758 note += " | racing (before the hold) " + race()
759 w.stats.racingEarly++
760 }
761 src.status = "moving"
762 next := CarryRequest(cloneSimState(w.state), cloneSimConsumed(src.consumed))
763 if !SameRequestState(w.state, &next) {
764 next.Schema, next.Host = 1, updateSimHost
765 w.state = &next
766 src.copy = BuildStateCopy{Known: true, Replica: w.replica, State: cloneSimState(&next)}
767 w.stats.carriedRequests++
768 note += " carried " + simRes(next.Resolved) + fmt.Sprintf(" done %d%s", next.Completed, simFailedMark(next.CompletedFailed))
769 }
770 if race != nil && late {
771 note += " | racing (after the carry) " + race()
772 w.stats.racingFenced++
773 }
774 if c := src.consumed; c != nil && c.CompletedFailed && c.Completed > w.carried {
775 w.carried = c.Completed
776 w.stats.carriedFailed++
777 }
778 src.status = ""
779 kept := false
780 switch {
781 case carried:
782 dst.copy = cloneSimCopy(src.copy)
783 case dst.copy.Known && !w.scripted && w.rng.Intn(100) < 50:
784 kept = true // its row from the earlier stay
785 w.stats.keptCopies++
786 default:
787 dst.copy = BuildStateCopy{}
788 }
789 if w.scripted || w.rng.Intn(100) < 60 {
790 src.copy = BuildStateCopy{} // the route retires here
791 } else if src.copy.Known {
792 // The source keeps its row for a return. Its refreshes while the
793 // instance is away read a location that is not this box's (another
794 // bucket: refused) and fail, so the copy keeps its last state with a
795 // read error; a refresh that succeeds would leave it fresh, which no
796 // rule can mistake.
797 src.copy.ReadErr = "s3: the instance is on another box"
798 }
799 w.at = j
800 w.stats.moves++
801 if dst.consumed != nil || dst.live != "" {
802 w.stats.returns++
803 }
804 w.syncResolutions()
805 return fmt.Sprintf("move %s->%s copy-carried=%v kept=%v%s", src.name, dst.name, carried, kept, note)
806}
807
808// loseBox replaces a box with an empty one: its consumed file, live link,
809// version store, failure book and bake clock are gone. If the instance was
810// on it, its registry row is new too.
811func (w *simWorld) loseBox() string {
812 k := w.rng.Intn(len(w.boxes))
813 name := w.boxes[k].name
814 w.boxes[k] = newSimBox(name)
815 w.syncResolutions()
816 return "lose " + name
817}
818
819// syncResolutions runs after a move or a lost box, for every request with a
820// first eligible build. A resolution the instance can no longer see (no
821// record in the build state or, strict mode aside, its box's consumed file)
822// never ran, since a run completes the request in the build state: spec
823// §4.2 "Lost requests", so the next eligible pass resolves it again. A
824// record it can see is R's resolution from now on (the instance returned to
825// a box holding one); of two, the build state's (R-RESOLUTION-STATE-WINS).
826func (w *simWorld) syncResolutions() {
827 b := w.cur()
828 records := map[uint64]map[string]bool{}
829 note := func(r *ResolvedRequest) {
830 if r == nil {
831 return
832 }
833 if records[r.ID] == nil {
834 records[r.ID] = map[string]bool{}
835 }
836 records[r.ID][r.Target] = true
837 }
838 if w.state != nil {
839 note(w.state.Resolved)
840 }
841 for _, x := range w.boxes {
842 if (x == b || w.strict) && x.consumed != nil {
843 note(x.consumed.Resolved)
844 }
845 }
846 ids := map[uint64]bool{}
847 for r := range w.firstEligible {
848 ids[r] = true
849 }
850 for r := range records {
851 ids[r] = true
852 }
853 for r := range ids {
854 if r <= w.wm(b) {
855 continue
856 }
857 seen := records[r]
858 fe, had := w.firstEligible[r]
859 switch {
860 case len(seen) == 0:
861 delete(w.firstEligible, r)
862 w.stats.lostResolutions++
863 case !w.strict:
864 // One record, or the build state's when both hold one
865 // (R-RESOLUTION-STATE-WINS).
866 t := ""
867 for x := range seen {
868 t = x
869 }
870 if w.state != nil && w.state.Resolved != nil && w.state.Resolved.ID == r {
871 t = w.state.Resolved.Target
872 }
873 if !had || t != fe {
874 w.firstEligible[r] = t
875 w.stats.pickedUp++
876 }
877 }
878 }
879}
880
881func (w *simWorld) markFailed() string {
882 b := w.cur()
883 var cands []string
884 add := func(v string) {
885 if v != "" {
886 cands = append(cands, v)
887 }
888 }
889 add(b.live)
890 add(w.head)
891 add(w.settings.Pin)
892 if w.state != nil {
893 add(w.state.LastExecuted)
894 if w.state.Resolved != nil {
895 add(w.state.Resolved.Target)
896 }
897 }
898 if b.consumed != nil && b.consumed.Resolved != nil {
899 add(b.consumed.Resolved.Target)
900 }
901 v := cands[w.rng.Intn(len(cands))]
902 b.failed[v] = true
903 return fmt.Sprintf("mark-failed %s on %s", v, b.name)
904}
905
906func (w *simWorld) toggleManual() string {
907 if w.settings.Updates == UpdatesManual {
908 w.settings.Updates = UpdatesAuto
909 } else {
910 w.settings.Updates = UpdatesManual
911 }
912 return "updates=" + w.settings.Updates
913}
914
915func (w *simWorld) pin() string {
916 if w.settings.Pin != "" && w.rng.Intn(100) < 50 {
917 w.settings.Pin = ""
918 return "unpin"
919 }
920 w.settings.Pin = w.builds[w.rng.Intn(len(w.builds))]
921 return "pin " + w.settings.Pin
922}
923
924func (w *simWorld) setMajor() string {
925 switch w.rng.Intn(3) {
926 case 0:
927 w.settings.Major = nil
928 return "major=none"
929 default:
930 m := 1 + w.rng.Intn(2)
931 w.settings.Major = &m
932 return fmt.Sprintf("major=%d", m)
933 }
934}
935
936// heldNow is rule 3's condition from the model's own records.
937func (w *simWorld) heldNow() bool {
938 u := w.settings
939 if u.Updates == UpdatesManual {
940 return true
941 }
942 return u.Major != nil && (w.major[w.head] == 0 || w.major[w.head] != *u.Major)
943}
944
945// wm is invariant 1's watermark for a pass or wake on box b: the highest
946// completed id in the bucket's build state or b's consumed file (spec §4.3
947// rule 2), or in every box's consumed file in strict mode.
948func (w *simWorld) wm(b *simBox) uint64 {
949 if w.strict {
950 return w.watermarkAnywhere()
951 }
952 var m uint64
953 if w.state != nil {
954 m = w.state.Completed
955 }
956 if b.consumed != nil && b.consumed.Completed > m {
957 m = b.consumed.Completed
958 }
959 if w.carried > m {
960 m = w.carried
961 }
962 return m
963}
964
965// watermarkAnywhere is the highest completed id any record holds: the
966// build state and every box's consumed file.
967func (w *simWorld) watermarkAnywhere() uint64 {
968 var m uint64
969 if w.state != nil {
970 m = w.state.Completed
971 }
972 for _, b := range w.boxes {
973 if b.consumed != nil && b.consumed.Completed > m {
974 m = b.consumed.Completed
975 }
976 }
977 return m
978}
979
980// boxView is what a pass on b can see of request r: pending (above both
981// sources' completed ids) and the T either source resolved it to, the build
982// state's first (R-RESOLUTION-STATE-WINS).
983func boxView(c *Consumed, st *BuildState, r uint64) (pending bool, t string) {
984 var m uint64
985 if c != nil {
986 m = c.Completed
987 }
988 if st != nil && st.Completed > m {
989 m = st.Completed
990 }
991 if r == 0 || r <= m {
992 return false, ""
993 }
994 if st != nil && st.Resolved != nil && st.Resolved.ID == r {
995 return true, st.Resolved.Target
996 }
997 if c != nil && c.Resolved != nil && c.Resolved.ID == r {
998 return true, c.Resolved.Target
999 }
1000 return true, ""
1001}
1002
1003// rootPass is settingsTarget then adoptHost for the instance on box b.
1004// resolve is root's pass (it writes the consumed file); false is the agent's
1005// pass, which stops when the decision needs root's resolution.
1006func (w *simWorld) rootPass(b *simBox, resolve bool) string {
1007 who := "root"
1008 if !resolve {
1009 who = "agent"
1010 }
1011 u := w.settings
1012 head := w.head
1013 wmBefore := w.wm(b)
1014 held := w.heldNow()
1015
1016 // settingsTarget: a route with default settings and no consumed file is
1017 // today's adoption (no Target, no book, no consumed write).
1018 viaTarget := !(u.Default() && b.consumed == nil)
1019 var dec TargetDecision
1020 var in TargetInput
1021 if !viaTarget {
1022 dec = TargetDecision{Version: head, Reason: ReasonAdopt, Evidence: EvidencePointer, Bake: true, Detail: head}
1023 } else {
1024 in = TargetInput{
1025 Route: registry.Route{Host: updateSimHost, Kind: "instance", UpdateSettings: u.Column()},
1026 Pointer: &ChannelPointer{Channel: "production", Version: head},
1027 HeadTag: w.tags[head],
1028 Settings: u,
1029 Build: cloneSimCopy(b.copy),
1030 Consumed: cloneSimConsumed(b.consumed),
1031 Installed: b.live,
1032 }
1033 if !b.eligible[head] {
1034 in.HeadHeld = "in its supply-chain bake window"
1035 }
1036 // settingsTarget gives Target the failure book only for a route
1037 // with settings (!plain); default settings keep today's adoption,
1038 // which never read it, even with a consumed file (R-T6-BOOK-2).
1039 if !u.Default() {
1040 failed := b.failed
1041 in.Failed = func(v string) bool { return failed[v] }
1042 }
1043 dec = Target(in)
1044 if resolve {
1045 // publishConsumed: root's record is written under the carry
1046 // fence, and only for a row no move holds (ruling
1047 // R-CARRY-FENCE). A refused pass publishes nothing and installs
1048 // nothing for the route: the decision never happened.
1049 if err := publishGate(&registry.Route{Host: updateSimHost, Kind: "instance", Status: b.status}); err != nil {
1050 return fmt.Sprintf("%s@%s %s: fenced: nothing published or installed", who, b.name, simDec(dec))
1051 }
1052 }
1053 w.checkEvidence(dec, head)
1054 w.checkDecision(b, in, dec, resolve, wmBefore, held)
1055 if resolve {
1056 next := NextConsumed(in, dec)
1057 b.consumed = &next
1058 b.decided, b.decidedSettings, b.decidedHead = true, u.Column(), head
1059 // Invariant 6: with the build state read, root's file agrees with
1060 // it on the pending request's T once the pass is written.
1061 if r := u.InstallRequest; in.Build.Read() && r > w.wm(b) && w.state != nil && w.state.Resolved != nil && w.state.Resolved.ID == r &&
1062 next.Resolved != nil && next.Resolved.ID == r && next.Resolved.Target != w.state.Resolved.Target {
1063 w.fail(6, "after root's pass R%d has two resolutions: the build state says %s, %s's consumed file %s",
1064 r, w.state.Resolved.Target, b.name, next.Resolved.Target)
1065 }
1066 } else if dec.Resolve != nil && dec.Reason == ReasonRequest {
1067 return fmt.Sprintf("%s@%s %s: stops, relays to root", who, b.name, simDec(dec))
1068 }
1069 }
1070 desc := fmt.Sprintf("%s@%s %s", who, b.name, simDec(dec))
1071
1072 // Invariant 5's scenario: a held instance, no pin, the build state read
1073 // with a last_executed, an unresolved request whose head bakes here.
1074 recovery := ""
1075 if viaTarget && held && u.Pin == "" && in.Build.Read() && in.Build.State != nil && in.Build.State.LastExecuted != "" {
1076 le := in.Build.State.LastExecuted
1077 pending, t := boxView(in.Consumed, in.Build.State, u.InstallRequest)
1078 if pending && t == "" && in.HeadHeld != "" && !u.InstallFastTrack && !b.failed[le] && (w.promoted[le] || b.staged[le]) {
1079 recovery = le
1080 w.stats.heldBakingPasses++
1081 }
1082 }
1083 defer func() {
1084 if recovery != "" && b.live != recovery {
1085 w.fail(5, "held, request R%d unresolved behind baking head %s, last_executed %s authorized: live is %q after the pass (%s)",
1086 u.InstallRequest, head, recovery, b.live, simDec(dec))
1087 }
1088 }()
1089
1090 // adoptHost.
1091 ver := dec.Version
1092 if ver == "" {
1093 return desc + ": nothing installed"
1094 }
1095 if b.live == ver {
1096 return desc + ": up to date"
1097 }
1098 if (!viaTarget || dec.Bake) && !b.eligible[ver] {
1099 return desc + ": " + ver + " baking"
1100 }
1101 stagedBefore := b.staged[ver]
1102 switch {
1103 case !viaTarget || dec.Evidence == EvidencePointer:
1104 if ver != head {
1105 return desc + ": not the signed head, not staged"
1106 }
1107 case dec.Evidence == EvidenceRecord:
1108 if !w.promoted[ver] && !stagedBefore {
1109 return desc + ": no promotion record, no staged copy: refused"
1110 }
1111 default:
1112 return desc + ": no evidence"
1113 }
1114
1115 // The repoint. Invariant 3's repoint half holds by construction of the
1116 // evidence switch above; it stays as a tripwire for the mirror.
1117 if !(ver == head || w.promoted[ver] || stagedBefore) {
1118 w.fail(3, "repointed onto %s: not the head %s, no promotion record, not staged on %s", ver, head, b.name)
1119 }
1120 if viaTarget && !u.Default() && b.failed[ver] {
1121 w.fail(4, "%s repointed onto %s, which it holds as failed (%s)", b.name, ver, simDec(dec))
1122 }
1123 if viaTarget && held && u.Pin == "" {
1124 ok := !w.replica && ver == head
1125 if w.state != nil && w.state.LastExecuted == ver {
1126 ok = true
1127 }
1128 if r := u.InstallRequest; r > w.wm(b) {
1129 if _, t := boxView(b.consumed, w.state, r); t == ver {
1130 ok = true
1131 }
1132 }
1133 if !ok {
1134 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)",
1135 ver, simLE(w.state), u.InstallRequest, simDec(dec))
1136 }
1137 }
1138 if recovery != "" && ver == recovery {
1139 w.stats.heldRecoveries++
1140 }
1141 prev := b.live
1142 b.staged[ver] = true
1143 b.live = ver
1144 return fmt.Sprintf("%s: repoint %q->%s", desc, prev, ver)
1145}
1146
1147// checkEvidence is invariant 3 at the decision: only the head rests on the
1148// signed pointer, and only the head bakes (§4.1, §4.3: a pin, a resolved T
1149// and a recovery waive bake and need a record or a staged copy).
1150func (w *simWorld) checkEvidence(dec TargetDecision, head string) {
1151 if dec.Version == "" || dec.Version == head {
1152 return
1153 }
1154 if dec.Evidence == EvidencePointer {
1155 w.fail(3, "decision %s rests on the pointer for %s, not the head %s", simDec(dec), dec.Version, head)
1156 }
1157 if dec.Bake {
1158 w.fail(3, "decision %s bakes %s, not the head %s", simDec(dec), dec.Version, head)
1159 }
1160}
1161
1162// checkDecision checks invariants 1 and 6 on one Target decision, before
1163// root writes it.
1164func (w *simWorld) checkDecision(b *simBox, in TargetInput, dec TargetDecision, resolve bool, wmBefore uint64, held bool) {
1165 u := in.Settings
1166 r := u.InstallRequest
1167 head := in.Pointer.Version
1168
1169 if !in.Build.Read() && r != 0 {
1170 if w.state != nil && w.state.Completed >= r {
1171 w.stats.unknownWithCompleted++
1172 }
1173 if in.Consumed != nil && in.Consumed.Resolved != nil && in.Consumed.Resolved.ID == r {
1174 w.stats.unknownReturning++
1175 }
1176 }
1177
1178 if all := w.watermarkAnywhere(); (dec.Reason == ReasonRequest && r <= all && r > wmBefore) ||
1179 (resolve && dec.Resolve != nil && dec.Resolve.ID <= all && dec.Resolve.ID > wmBefore) {
1180 w.stats.leftBehind++
1181 }
1182
1183 // Invariant 1: rule 2 never selects a completed request.
1184 if dec.Reason == ReasonRequest && r <= wmBefore {
1185 w.fail(1, "rule 2 selected R%d (%s), already completed (watermark %d)", r, dec.Version, wmBefore)
1186 }
1187 if !resolve {
1188 return
1189 }
1190 if dec.Resolve != nil && dec.Resolve.ID <= wmBefore {
1191 w.fail(1, "%s resolved R%d again (to %s) after it completed (watermark %d)", b.name, dec.Resolve.ID, dec.Resolve.Target, wmBefore)
1192 }
1193
1194 // Invariant 6: the first eligible pass resolves, pin or not (with the
1195 // build state read: never read, or a refresh that failed, is unread).
1196 if in.Build.Read() && r != 0 {
1197 pending, t := boxView(in.Consumed, in.Build.State, r)
1198 eligible := in.HeadHeld == "" || u.InstallFastTrack
1199 if pending && t == "" && eligible && r > wmBefore {
1200 if _, ok := w.firstEligible[r]; !ok {
1201 w.firstEligible[r] = head
1202 }
1203 if u.Pin != "" {
1204 w.stats.pinnedEligible++
1205 }
1206 want := w.firstEligible[r]
1207 if dec.Resolve == nil || dec.Resolve.ID != r || dec.Resolve.Target != want {
1208 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))
1209 }
1210 }
1211 }
1212 if dec.Resolve != nil {
1213 want, ok := w.firstEligible[dec.Resolve.ID]
1214 if !ok || want != dec.Resolve.Target {
1215 w.fail(6, "%s resolved R%d to %s; first eligible %q", b.name, dec.Resolve.ID, dec.Resolve.Target, want)
1216 }
1217 w.stats.resolutions++
1218 if b.failed[dec.Resolve.Target] {
1219 w.stats.failedHeadResolutions++
1220 }
1221 }
1222 if dec.Reason == ReasonRequest {
1223 if want := w.firstEligible[r]; dec.Version != want {
1224 w.fail(6, "rule 2 installs %s for R%d; first eligible %q", dec.Version, r, want)
1225 }
1226 }
1227 if dec.Fail != 0 {
1228 w.stats.failedCompletions++
1229 }
1230}
1231
1232// wake is the agent's wake on box b, as production runs it with no planner
1233// and an identity it can exec by path:
1234//
1235// - for a route whose settings could hold it, the copy is refreshed first
1236// (buildStates.wakeTarget); a refresh that fails leaves ReadErr in it;
1237// - the held wake check's decision is production's (DecideHeldWake, ruling
1238// R-HELD-PURE), enforced as the activator's wakeCheck does: not held runs
1239// the live link (today's wake); unread, unknown, or a target root reports
1240// failed is refused; a held target runs when it is installed, or from
1241// this box's retained copy; otherwise root is asked and the wake waits
1242// for the install, and a changed answer ends the wait with nothing run.
1243// With no decision from root for the current settings (AskRoot) the
1244// build state's build runs only if it is installed; otherwise the wake
1245// asks root for a pass and waits for its decision, then decides again.
1246// The live link never runs blindly;
1247// - a wait is root's pass, run inline (the stage relay), or, half the
1248// time, no answer within the bound: the wake ends with nothing run;
1249// - then beforeExec: HeldExecStale against the bucket object read under
1250// the lease, and the merge, NextBuildState; then the run.
1251func (w *simWorld) wake(b *simBox) string {
1252 u := w.settings
1253 col := u.Column()
1254 desc := "wake@" + b.name
1255 if !u.Default() {
1256 if !w.refreshCopy(b) {
1257 desc += " (refresh failed)"
1258 }
1259 }
1260 decide := func() HeldWakeDecision {
1261 return DecideHeldWake(HeldWakeInput{Settings: col, Build: cloneSimCopy(b.copy), Consumed: cloneSimConsumed(b.consumed), Installed: b.live})
1262 }
1263 waitRoot := func() bool {
1264 w.stats.rootWaits++
1265 if !w.scripted && w.rng.Intn(100) < 50 {
1266 return false
1267 }
1268 desc += " [waits; " + w.rootPass(b, true) + "]"
1269 return true
1270 }
1271 d := decide()
1272 if d.Held && d.AskRoot && !d.Failed {
1273 w.stats.askRoot++
1274 if d.Target != "" && b.live == d.Target {
1275 w.stats.askRootRuns++
1276 } else {
1277 if !waitRoot() {
1278 return desc + ": no decision from root for its settings within the bound, nothing run"
1279 }
1280 if d = decide(); d.AskRoot && (d.Target == "" || b.live != d.Target) {
1281 return desc + ": root has not decided for its settings, nothing run"
1282 }
1283 }
1284 }
1285 run, retained := "", false
1286 switch {
1287 case !d.Held:
1288 run = b.live // today's wake
1289 if run == "" {
1290 return desc + ": nothing installed"
1291 }
1292 case d.Unread:
1293 w.stats.unreadRefusals++
1294 return desc + ": refused, its build state could not be read"
1295 case d.Unknown || d.Target == "":
1296 return desc + ": refused, build unknown"
1297 case d.Failed:
1298 return desc + ": refused, its target " + d.Target + " failed here"
1299 case b.live == d.Target:
1300 run = d.Target
1301 case !d.AskRoot && b.staged[d.Target]:
1302 run, retained = d.Target, true
1303 default:
1304 if !waitRoot() {
1305 return desc + ": waited for root to install " + d.Target + ", nothing run"
1306 }
1307 if b.live != d.Target {
1308 return desc + ": " + d.Target + " not installed when the wait ended, nothing run"
1309 }
1310 run = d.Target
1311 }
1312 if d.Held {
1313 w.stats.heldRuns++
1314 if retained {
1315 w.stats.retainedRuns++
1316 desc += " (retained copy)"
1317 }
1318 }
1319 // beforeExec: the held target revalidated against the object under the
1320 // lease, then the merge. A refused record runs nothing.
1321 fresh := DecideHeldWake(HeldWakeInput{Settings: col, Build: BuildStateCopy{Known: true, Replica: true, State: cloneSimState(w.state)},
1322 Consumed: cloneSimConsumed(b.consumed), Installed: b.live})
1323 if err := HeldExecStale(fresh, w.state, run, ""); err != nil { // the model's wake has no planner
1324 return desc + ": record refused: " + err.Error()
1325 }
1326 w.checkWakeRun(b, run)
1327 wmBefore := w.wm(b)
1328 cur := cloneSimState(w.state)
1329 next := NextBuildState(cur, cloneSimConsumed(b.consumed), run)
1330 next.Schema, next.Host = 1, updateSimHost
1331
1332 if next.LastExecuted != run {
1333 w.fail(2, "wake ran %s; the build state says last_executed %q", run, next.LastExecuted)
1334 }
1335 var prev uint64
1336 if cur != nil {
1337 prev = cur.Completed
1338 }
1339 // Only the current request: a newer one supersedes an older resolution.
1340 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 {
1341 w.fail(1, "wake ran %s, the build state's T for pending R%d, and R%d stays pending (completed %d)",
1342 run, cur.Resolved.ID, cur.Resolved.ID, next.Completed)
1343 }
1344 if next.Completed > prev && !next.CompletedFailed {
1345 r := next.Completed
1346 if r <= wmBefore || w.completedByRun[r] {
1347 w.fail(1, "wake running %s records R%d newly completed; already completed (watermark %d)", run, r, wmBefore)
1348 }
1349 if next.Resolved == nil || next.Resolved.ID != r || next.Resolved.Target != run {
1350 w.fail(1, "wake running %s records R%d completed, but R%d's T is %s", run, r, r, simRes(next.Resolved))
1351 }
1352 w.completedByRun[r] = true
1353 w.stats.runCompletions++
1354 }
1355 w.state = &next
1356 w.lastRan = run
1357 w.replica = true
1358 b.copy = BuildStateCopy{Known: true, Replica: true, State: cloneSimState(&next)}
1359 return fmt.Sprintf("%s runs %s", desc, run)
1360}
1361
1362// checkWakeRun is invariant 7 on a wake about to run build run on box b, from
1363// the model's own records (never Consumed.Settings or Reason).
1364func (w *simWorld) checkWakeRun(b *simBox, run string) {
1365 u := w.settings
1366 if u.Default() {
1367 return
1368 }
1369 if u.Pin != "" {
1370 if run != u.Pin {
1371 w.fail(7, "pinned on %s, the wake on %s ran %s", u.Pin, b.name, run)
1372 }
1373 return
1374 }
1375 if r := u.InstallRequest; r != 0 && r > w.wm(b) {
1376 t := ""
1377 if w.state != nil && w.state.Resolved != nil && w.state.Resolved.ID == r {
1378 t = w.state.Resolved.Target
1379 } else if b.consumed != nil && b.consumed.Resolved != nil && b.consumed.Resolved.ID == r {
1380 t = b.consumed.Resolved.Target
1381 }
1382 if t != "" {
1383 if run != t {
1384 w.fail(7, "R%d pending with T %s, the wake on %s ran %s", r, t, b.name, run)
1385 }
1386 return
1387 }
1388 }
1389 held := u.Updates == UpdatesManual
1390 if !held && u.Major != nil {
1391 if !b.decided || b.decidedSettings != u.Column() {
1392 held = true // root has not decided for these settings: the wake holds
1393 } else {
1394 m := w.major[b.decidedHead]
1395 held = m == 0 || m != *u.Major
1396 }
1397 }
1398 if le := simLE(w.state); held && le != "" && run != le {
1399 w.fail(7, "held (updates %s, major %v; root decided for these settings: %v), the wake on %s ran %s, not last_executed %s",
1400 u.Updates, simMajor(u.Major), b.decided && b.decidedSettings == u.Column(), b.name, run, le)
1401 }
1402}
1403
1404func simMajor(m *int) string {
1405 if m == nil {
1406 return "-"
1407 }
1408 return strconv.Itoa(*m)
1409}
1410
1411// check is the per-step state check (invariant 2); event checks run inside
1412// the actions. A known copy that differs from the bucket is not a model
1413// error: production keeps one after a failed refresh, and on a box the
1414// instance returns to, until the next refresh (Astra round 1's note on this
1415// simulation). The wake refreshes before it decides and is refused when
1416// that fails; root's passes read the copy as it is.
1417func (w *simWorld) check() {
1418 if w.lastRan != "" && (w.state == nil || w.state.LastExecuted != w.lastRan) {
1419 w.fail(2, "the database last ran %s; the build state says %q", w.lastRan, simLE(w.state))
1420 }
1421}
1422
1423func (w *simWorld) summary() string {
1424 b := w.cur()
1425 u := w.settings
1426 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)
1427 if u.Major != nil {
1428 s += fmt.Sprintf(" major %d", *u.Major)
1429 }
1430 if w.state != nil {
1431 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))
1432 }
1433 if b.consumed != nil {
1434 s += fmt.Sprintf(" | consumed res %s done %d%s", simRes(b.consumed.Resolved), b.consumed.Completed, simFailedMark(b.consumed.CompletedFailed))
1435 }
1436 if !b.copy.Known {
1437 s += " | copy unread"
1438 }
1439 return s + "]"
1440}
1441
1442func simFailedMark(f bool) string {
1443 if f {
1444 return " failed"
1445 }
1446 return ""
1447}
1448
1449func simDec(d TargetDecision) string {
1450 s := fmt.Sprintf("{%s %q", d.Reason, d.Version)
1451 if d.Resolve != nil {
1452 s += " resolve " + simRes(d.Resolve)
1453 }
1454 if d.Fail != 0 {
1455 s += fmt.Sprintf(" fail R%d", d.Fail)
1456 }
1457 return s + "}"
1458}
1459
1460func simRes(r *ResolvedRequest) string {
1461 if r == nil {
1462 return "-"
1463 }
1464 return fmt.Sprintf("R%d->%s", r.ID, r.Target)
1465}
1466
1467func simLE(s *BuildState) string {
1468 if s == nil {
1469 return ""
1470 }
1471 return s.LastExecuted
1472}
1473
1474func simStatesEqual(a, b *BuildState) bool {
1475 if a == nil || b == nil {
1476 return a == nil && b == nil
1477 }
1478 ra, rb := simRes(a.Resolved), simRes(b.Resolved)
1479 return a.LastExecuted == b.LastExecuted && ra == rb && a.Completed == b.Completed && a.CompletedFailed == b.CompletedFailed
1480}
1481
1482func cloneSimState(s *BuildState) *BuildState {
1483 if s == nil {
1484 return nil
1485 }
1486 v := *s
1487 v.Resolved = cloneSimResolved(s.Resolved)
1488 return &v
1489}
1490
1491func cloneSimConsumed(c *Consumed) *Consumed {
1492 if c == nil {
1493 return nil
1494 }
1495 v := *c
1496 v.Resolved = cloneSimResolved(c.Resolved)
1497 return &v
1498}
1499
1500func cloneSimCopy(c BuildStateCopy) BuildStateCopy {
1501 c.State = cloneSimState(c.State)
1502 return c
1503}
1504
1505func cloneSimResolved(r *ResolvedRequest) *ResolvedRequest {
1506 if r == nil {
1507 return nil
1508 }
1509 v := *r
1510 return &v
1511}
1512