| 1 | package hostlife |
| 2 | |
| 3 | import ( |
| 4 | "encoding/json" |
| 5 | "fmt" |
| 6 | "math/rand" |
| 7 | "os" |
| 8 | "strconv" |
| 9 | "strings" |
| 10 | "testing" |
| 11 | ) |
| 12 | |
| 13 | const ( |
| 14 | chaosSteps = 2000 |
| 15 | calmSteps = 6000 |
| 16 | ) |
| 17 | |
| 18 | func newWorld(seed int64, verbose bool) *world { |
| 19 | w := &world{seed: seed, rng: &counting{r: rand.New(rand.NewSource(seed))}, verbose: verbose, perRegion: boxesPerRegion, |
| 20 | stores: map[string]bool{app0: true, app1: true}, cfgVer: map[string]int{app0: 1, app1: 1}, purgeRes: map[string]bool{}, purgeStep: map[string]int{}, |
| 21 | control: newBucket(), delivered: map[int]bool{}, durable: map[string]map[int]bool{}, writeInc: map[int]int{}, txs: map[int]tx{}, legacyIncs: map[int]bool{}, purgeOp: map[string]string{}, genParent: map[string]string{}, markerAlerted: map[string]bool{}, execLease: map[int]execLease{}, fail: map[string]bool{}, stats: map[string]int{}} |
| 22 | for r := 0; r < nRegions; r++ { |
| 23 | w.buckets[r] = newBucket() |
| 24 | } |
| 25 | w.admit = map[string]*admission{app0: {Reg: map[string]regEntry{}}, app1: {Reg: map[string]regEntry{}}} |
| 26 | for _, f := range []string{"partition", "freeze", "pause", "destroy", "disk", "recreate", "pausecreate", "lostreturn", "markerhold", "freezetgt", "retention"} { |
| 27 | w.fail[f] = w.rng.Intn(2) == 0 |
| 28 | } |
| 29 | for r := 0; r < nRegions; r++ { |
| 30 | b := &box{ID: r, Region: r, HasKey: r == 0 || w.rng.Intn(4) != 0, Skew: w.rng.Intn(3) - 1, Nested: w.rng.Intn(2) == 0, Enrolled: true} |
| 31 | if r != 0 && w.rng.Intn(4) == 0 { |
| 32 | b.FailApp = true |
| 33 | } |
| 34 | if w.rng.Intn(10) == 0 { |
| 35 | b.FailArchive = true |
| 36 | } |
| 37 | if r != 0 && w.rng.Intn(2) == 0 { |
| 38 | b.FailSettle = true |
| 39 | } |
| 40 | b.forget() |
| 41 | w.boxes = append(w.boxes, b) |
| 42 | } |
| 43 | if w.rng.Intn(3) == 0 { |
| 44 | w.legacyStart() |
| 45 | } else if w.fail["retention"] { |
| 46 | w.retentionStart() |
| 47 | } |
| 48 | // the two-box shape (region HA L18): a second enrolled box in every |
| 49 | // region, drawn after every one-box draw of this world, so the one-box |
| 50 | // stream is untouched; id nRegions+r, as addBox gives a witness |
| 51 | for r := 0; r < nRegions && w.perRegion > 1; r++ { |
| 52 | b := &box{ID: nRegions + r, Region: r, HasKey: w.rng.Intn(4) != 0, Skew: w.rng.Intn(3) - 1, Nested: w.rng.Intn(2) == 0, Enrolled: true} |
| 53 | if w.rng.Intn(4) == 0 { |
| 54 | b.FailApp = true |
| 55 | } |
| 56 | if w.rng.Intn(10) == 0 { |
| 57 | b.FailArchive = true |
| 58 | } |
| 59 | if w.rng.Intn(2) == 0 { |
| 60 | b.FailSettle = true |
| 61 | } |
| 62 | b.forget() |
| 63 | w.boxes = append(w.boxes, b) |
| 64 | } |
| 65 | if w.perRegion > 1 { |
| 66 | w.fail["terminate"] = w.rng.Intn(2) == 0 |
| 67 | for _, b := range w.boxes { |
| 68 | b.DeleteOnTermination = w.rng.Intn(8) != 0 // one box in eight has a volume without the flag (§5.9, H19) |
| 69 | } |
| 70 | } |
| 71 | return w |
| 72 | } |
| 73 | |
| 74 | // retentionStart: the host has been recreated more times than |
| 75 | // retired_incarnations remembers (claim rev 6.5 §2 caps it at 32), and a |
| 76 | // replication object of an incarnation the list forgot is still in a |
| 77 | // bucket (rev 7.5, R4 §3: the retention-boundary fixture). Only a sweep |
| 78 | // that discovers locations from the namespace parks it. |
| 79 | func (w *world) retentionStart() { |
| 80 | w.claim = &claim{Ver: w.newVer()} |
| 81 | old := 1 // an incarnation older than every one the list remembers |
| 82 | w.nextInc = old |
| 83 | for i := 0; i < retiredCap+1; i++ { |
| 84 | w.nextInc++ |
| 85 | w.claim.Retired = retire(w.claim.Retired, w.nextInc) // 2 to 33: the cap drops nothing but 1 was never listed |
| 86 | } |
| 87 | if contains(w.claim.Retired, old) || len(w.claim.Retired) != retiredCap { |
| 88 | panic("retention fixture: the injected incarnation must be absent from a full list (R5-6)") |
| 89 | } |
| 90 | r := w.rng.Intn(nRegions) |
| 91 | k := ltxKey(locationFor(old, false), "", 0, 1, 1) |
| 92 | // a request that completed long after its incarnation was retired: a |
| 93 | // straggler, which only the sweep retires (INV-10 at an operation's end |
| 94 | // exempts it, as it exempts every completion after H) |
| 95 | w.buckets[r].objs[k] = []*version{{ID: w.newVer(), Straggler: true, B: &blob{Kind: "ltx", Level: 0, Min: 1, Max: 1, Inc: old, Pages: map[string]int{"k0": 1}}}} |
| 96 | w.logf("retention fixture: incarnation %d's replica in region %d, past the cap", old, r) |
| 97 | } |
| 98 | |
| 99 | // legacyStart: a host that exists before the release. Its data is untagged, |
| 100 | // a best-effort-placed descendant may be running, and an earlier |
| 101 | // (pre-release) move left a replica in another region. |
| 102 | func (w *world) legacyStart() { |
| 103 | r := w.rng.Intn(nRegions) |
| 104 | b := w.regionBox(r) |
| 105 | w.nextInc++ |
| 106 | inc := w.nextInc |
| 107 | w.rec = &record{Ver: w.newVer(), Inc: inc, App: app0, Region: r} |
| 108 | w.legacyIncs[inc] = true |
| 109 | key := 7 |
| 110 | b.Row = &row{Inc: inc, App: app0, Status: "ready"} |
| 111 | b.DB = &localDB{Inc: inc, Loc: locationFor(inc, true), Key: key, State: map[string]int{}, Epoch: b.Epoch} |
| 112 | for i := 0; i < 3; i++ { |
| 113 | w.nextW++ |
| 114 | w.acks = append(w.acks, ack{W: w.nextW, Inc: inc, Box: b.ID, Session: 0, Gen: "", At: 0, Kind: "write"}) // the pre-release writer: the legacy identity, session 0 (claim rev 6.24) |
| 115 | w.writeInc[w.nextW] = inc |
| 116 | w.commit(b.DB, w.nextW) |
| 117 | } |
| 118 | b.Files = &filesDir{Inc: inc, Key: key, Env: 1, Done: true} |
| 119 | b.Config, b.CfgVer, b.Live, b.LiveInc = inc, 1, app0, inc |
| 120 | // the pre-release replica: one level-0 file of everything, untagged |
| 121 | full := w.deltaOf(b.DB, 0) |
| 122 | full.Inc = 0 |
| 123 | b.DB.Pos, b.DB.Pending = 1, nil |
| 124 | k := ltxKey(b.DB.Loc, "", 0, 1, 1) |
| 125 | w.buckets[r].objs[k] = []*version{{ID: w.newVer(), B: full}} |
| 126 | w.markDurable(k, full) |
| 127 | // an earlier move's replica in another region: the first transaction only |
| 128 | first := w.txs[b.DB.Log[0]] |
| 129 | part := &blob{Kind: "ltx", Level: 0, Min: 1, Max: 1, Inc: 0, SealKey: key, Pages: map[string]int{first.Key: first.Val}, TXs: []int{first.W}} |
| 130 | other := (r + 1 + w.rng.Intn(nRegions-1)) % nRegions |
| 131 | w.buckets[other].objs[ltxKey(b.DB.Loc, "", 0, 1, 1)] = []*version{{ID: w.newVer(), B: part}} |
| 132 | if w.rng.Intn(2) == 0 { |
| 133 | // the pre-release processes: the legacy identity, session 0 in the origin generation (claim rev 6.24; rev 7.13's seed 44450 found them acknowledging under no identity at all) |
| 134 | b.Procs = []*proc{{Main: true, Strict: false, Inc: inc, Session: 0, Box: b.ID}, {Main: false, Strict: false, Inc: inc, Session: 0, Box: b.ID}} |
| 135 | } |
| 136 | if w.rng.Intn(2) == 0 { |
| 137 | // that earlier move also left the old box's local state behind: |
| 138 | // a database, a files directory and env files, and no row |
| 139 | ob := w.regionBox(other) |
| 140 | ob.DB = &localDB{Inc: inc, Loc: locationFor(inc, true), Key: key, State: cloneState(part.Pages), TX: 1, Pos: 1, Epoch: ob.Epoch} |
| 141 | ob.Files = &filesDir{Inc: inc, Key: key, Env: 1, Done: true} |
| 142 | } |
| 143 | } |
| 144 | |
| 145 | // ---------- the scheduler ---------- |
| 146 | |
| 147 | func (w *world) step() { |
| 148 | w.now++ |
| 149 | w.completeDue(false) |
| 150 | if p := w.recPend; p != nil && p.at <= w.now { |
| 151 | w.recPend = nil |
| 152 | if w.rec == nil { // create-only: it lands only where no record is |
| 153 | w.rec = p.rec |
| 154 | w.logf("a late record PUT for inc %d landed", p.rec.Inc) |
| 155 | } |
| 156 | } |
| 157 | w.runStalled() |
| 158 | if w.perRegion > 1 { |
| 159 | w.twoBoxStep() // the two-box shape's own draws, after the one-box ones (ruling 1) |
| 160 | } |
| 161 | bs := w.liveBoxes() |
| 162 | b := bs[w.rng.Intn(len(bs))] |
| 163 | n := w.rng.Intn(100) |
| 164 | switch { |
| 165 | case !w.calm && n < 6: |
| 166 | switch w.rng.Intn(10) { |
| 167 | case 9: |
| 168 | // a config or secrets update publishes a new bundle version |
| 169 | app := []string{app0, app1}[w.rng.Intn(2)] |
| 170 | w.cfgVer[app]++ |
| 171 | w.logf("config bundle %s v%d published", app, w.cfgVer[app]) |
| 172 | case 0, 1: |
| 173 | w.userCreate() |
| 174 | case 2, 7, 8: |
| 175 | w.userMove() |
| 176 | case 3: |
| 177 | w.userDelete() |
| 178 | case 4: |
| 179 | w.userPush() |
| 180 | case 5: |
| 181 | if w.rng.Intn(3) == 0 { |
| 182 | w.userPurge() |
| 183 | } |
| 184 | default: |
| 185 | w.doorAuthorize() |
| 186 | } |
| 187 | case !w.calm && n < 12: |
| 188 | w.fault() |
| 189 | case n < 20: |
| 190 | w.consoleStep() |
| 191 | case n < 24: |
| 192 | w.recoveryPass() |
| 193 | case n < 25: |
| 194 | w.doorOpen() |
| 195 | case n < 26: |
| 196 | if !w.calm { |
| 197 | w.doorAuthorize() |
| 198 | } |
| 199 | case n < 28: |
| 200 | if w.calm || w.rng.Intn(4) == 0 { |
| 201 | w.operator() // operators act during the incident too, not only after |
| 202 | } |
| 203 | case n < 56: |
| 204 | w.worker(b) |
| 205 | case n < 62: |
| 206 | w.obligationRunner(b) |
| 207 | case n < 67: |
| 208 | w.reconcile(b) |
| 209 | case n < 73: |
| 210 | w.traffic(b) |
| 211 | w.wake(b) |
| 212 | case n < 77: |
| 213 | w.replicate(b) |
| 214 | case n < 78: |
| 215 | w.idleStop(b) |
| 216 | case n < 81: |
| 217 | w.passPlan(b, "config") |
| 218 | case n < 84: |
| 219 | w.passPlan(b, "adopt") |
| 220 | case n < 89: |
| 221 | w.passExec(b) |
| 222 | case n < 94: |
| 223 | w.runner(b) |
| 224 | default: |
| 225 | w.watchdog(b) |
| 226 | } |
| 227 | w.checkStep() |
| 228 | } |
| 229 | |
| 230 | // heal ends the chaos. On the first call some faults linger, so the |
| 231 | // operator meets a frozen, paused or partitioned participant, and destroyed |
| 232 | // boxes stay down; on the final call everything heals, and each stopped box |
| 233 | // either comes back (an instance stopped, then started) or is replaced. |
| 234 | func (w *world) heal(final bool) { |
| 235 | w.calm = true |
| 236 | c := w.claim |
| 237 | for _, b := range w.boxes { |
| 238 | linger := !final && c != nil && (c.Op.Kind == "landing" || c.Op.Kind == "restoring") && b.ID == c.Op.Tgt && w.rng.Intn(2) == 0 |
| 239 | if linger { |
| 240 | continue |
| 241 | } |
| 242 | b.Partitioned, b.Frozen, b.AgentPaused, b.AgentDown, b.PurgeFails = false, false, false, false, false |
| 243 | if b.hostFailed { |
| 244 | b.hostFailed, b.failCounted, b.startFails, b.nextStart = false, false, 0, 0 // the operator cleared the failed host |
| 245 | w.stats["failed hosts cleared"]++ |
| 246 | } |
| 247 | } |
| 248 | if final { |
| 249 | for _, b := range w.boxes { |
| 250 | if b.Destroyed && !b.Terminated && w.regionBox(b.Region) == nil && w.rng.Intn(2) == 0 { |
| 251 | b.Destroyed = false // started again, with its old disk |
| 252 | b.forget() |
| 253 | w.logf("stopped box %d started again", b.ID) |
| 254 | } |
| 255 | } |
| 256 | w.replaceDestroyed() |
| 257 | } |
| 258 | // a box with no key gets one: ops distributes it (the approved fix) |
| 259 | for _, b := range w.boxes { |
| 260 | b.HasKey = true |
| 261 | b.FailArchive = false |
| 262 | } |
| 263 | } |
| 264 | |
| 265 | func (w *world) quiescent() bool { |
| 266 | if len(w.pending) > 0 || len(w.console) > 0 || w.recPend != nil || !w.atRest() { |
| 267 | return false |
| 268 | } |
| 269 | return len(w.residue()) == 0 |
| 270 | } |
| 271 | |
| 272 | // whyNotQuiescent names, for a non-convergence report, what quiescent() |
| 273 | // found unfinished. |
| 274 | func (w *world) whyNotQuiescent() string { |
| 275 | var out []string |
| 276 | for _, r := range w.pending { |
| 277 | out = append(out, fmt.Sprintf("pending %v %s r%d by %s issued %d due %d beyond=%v", r.kind, r.key, r.region, r.by, r.at, r.doneAt, r.beyond)) |
| 278 | } |
| 279 | if len(w.console) > 0 { |
| 280 | out = append(out, fmt.Sprintf("%d console plans", len(w.console))) |
| 281 | } |
| 282 | if w.recPend != nil { |
| 283 | out = append(out, "a record PUT pending") |
| 284 | } |
| 285 | if w.h2.Kind != "" { |
| 286 | out = append(out, "h2 "+w.h2.Kind) |
| 287 | } |
| 288 | for app, ad := range w.admit { |
| 289 | if ad.Closed { |
| 290 | out = append(out, "admission closed for "+app) |
| 291 | } |
| 292 | for id, e := range ad.Reg { |
| 293 | if w.now <= e.Until || !on("registration-recovery") { |
| 294 | out = append(out, fmt.Sprintf("registration %s of %s live until %d", id, app, e.Until)) |
| 295 | } |
| 296 | } |
| 297 | } |
| 298 | if c := w.claim; c != nil && c.Holder != nil { |
| 299 | if c.Op.Kind != "serving" { |
| 300 | out = append(out, "op "+c.Op.Kind) |
| 301 | } |
| 302 | for _, o := range c.Obl { |
| 303 | out = append(out, fmt.Sprintf("obligation %s %s %s", o.ID, o.Kind, o.Prefix)) |
| 304 | } |
| 305 | if e := w.execBox(c); e != nil && (e.Config != c.Holder.Inc || e.Live != c.Holder.App || e.LiveInc != c.Holder.Inc) { |
| 306 | out = append(out, "config or adoption owed") |
| 307 | } |
| 308 | for _, b := range w.liveBoxes() { |
| 309 | if e := w.execBox(c); b != e && (b.Row != nil || len(b.Procs) > 0) { |
| 310 | out = append(out, fmt.Sprintf("box %d has a row or processes", b.ID)) |
| 311 | } |
| 312 | if b.open != nil { |
| 313 | out = append(out, fmt.Sprintf("box %d admitted into %q, start in progress at stage %s", b.ID, b.open.Gen, b.open.stage)) |
| 314 | } |
| 315 | } |
| 316 | } |
| 317 | if r := w.residue(); len(r) > 0 { |
| 318 | out = append(out, fmt.Sprintf("residue %v", r)) |
| 319 | } |
| 320 | if len(out) == 0 { |
| 321 | return "quiescent" |
| 322 | } |
| 323 | return strings.Join(out, "; ") |
| 324 | } |
| 325 | |
| 326 | // atRest: the claim, record and boxes have converged. |
| 327 | func (w *world) atRest() bool { |
| 328 | if w.h2.Kind == "creating" || w.h2.Kind == "purging" || w.h2.Kind == "fenced" { |
| 329 | return false |
| 330 | } |
| 331 | for _, ad := range w.admit { |
| 332 | if ad.Closed { |
| 333 | return false |
| 334 | } |
| 335 | for _, e := range ad.Reg { |
| 336 | if w.now <= e.Until || !on("registration-recovery") { |
| 337 | return false // a live registration: its create is still in flight |
| 338 | } |
| 339 | } |
| 340 | } |
| 341 | c := w.claim |
| 342 | if c == nil { |
| 343 | return w.rec == nil |
| 344 | } |
| 345 | if c.Holder == nil { |
| 346 | return c.Op.Kind == "" && w.rec == nil && len(c.Obl) == 0 |
| 347 | } |
| 348 | if c.Op.Kind != "serving" || len(c.Obl) > 0 || w.rec == nil || w.rec.Inc != c.Holder.Inc || w.rec.MoveID != "" { |
| 349 | return false |
| 350 | } |
| 351 | e := w.execBox(c) |
| 352 | if e == nil || e.Row == nil || e.Row.Status != "ready" { |
| 353 | return false |
| 354 | } |
| 355 | if d := c.Op.Completed; d != nil && !d.Discharged || e.actFence != "" { |
| 356 | return false // a completion not yet marked, or a fence not yet lifted (L18 finding 2) |
| 357 | } |
| 358 | if e.Config != c.Holder.Inc || e.Live != c.Holder.App || e.LiveInc != c.Holder.Inc { |
| 359 | return false // config sync and adoption still owe this incarnation |
| 360 | } |
| 361 | for _, b := range w.liveBoxes() { |
| 362 | if b != e && (b.Row != nil || len(b.Procs) > 0) { |
| 363 | return false |
| 364 | } |
| 365 | if b.open != nil { |
| 366 | return false // an admitted writer still finishing its start |
| 367 | } |
| 368 | } |
| 369 | return true |
| 370 | } |
| 371 | |
| 372 | // ---------- invariants ---------- |
| 373 | |
| 374 | // checkStep runs after every step. |
| 375 | func (w *world) checkStep() { |
| 376 | // one writer per host, across every region |
| 377 | var writers []int |
| 378 | for _, b := range w.boxes { |
| 379 | if !b.Destroyed && !b.Frozen && len(b.Procs) > 0 { |
| 380 | writers = append(writers, b.ID) |
| 381 | } |
| 382 | } |
| 383 | if len(writers) > 1 { |
| 384 | w.violate("INV-1: boxes %v run the host at once", writers) |
| 385 | } |
| 386 | // an app store exists while any instance of the app is held for serving |
| 387 | if w.h2.Kind == "serving" && !w.stores[w.h2.App] { |
| 388 | w.violate("purge: store of app %s destroyed while its second host serves", w.h2.App) |
| 389 | } |
| 390 | if c := w.claim; c != nil && c.Holder != nil && !w.stores[c.Holder.App] { |
| 391 | switch c.Op.Kind { |
| 392 | case "purging", "deleting", "parking": |
| 393 | default: |
| 394 | w.violate("purge: store of app %s destroyed while its host is %s", c.Holder.App, c.Op.Kind) |
| 395 | } |
| 396 | } |
| 397 | if c := w.claim; c != nil && c.Op.Kind == "restoring" && c.Op.SrcPhase == "stuck" { |
| 398 | w.violate("stuck: source could not recover %s", c.Op.ID) |
| 399 | } |
| 400 | if c := w.claim; c != nil && c.Op.Kind == "reverting" && c.Op.RevPhase == "stuck" { |
| 401 | w.violate("stuck: source could not revert %s", c.Op.ID) |
| 402 | } |
| 403 | // INV-27 (region HA HA1, HA7): while relocating, op.exec is none or an |
| 404 | // enrolled box that is not on lost; execution authority never names a |
| 405 | // fenced or unenrolled reference |
| 406 | if c := w.claim; c != nil && c.Op.Kind == "relocating" && c.Op.Exec >= 0 { |
| 407 | released := c.Op.Release != nil && c.Op.Release.Box == c.Op.Exec // a released executor fenced before PinAfterRelease (FenceSource after the release, rev 4) |
| 408 | if e := w.boxByID(c.Op.Exec); e == nil || !e.Enrolled || contains(c.Lost, e.ID) && !released { |
| 409 | w.violate("INV-27: relocation %s names box %d as op.exec, which is unenrolled or lost", c.Op.ID, c.Op.Exec) |
| 410 | } |
| 411 | } |
| 412 | w.checkCompletion() // INV-31 (L18 finding 2): only a relocation sets owedDischarge |
| 413 | if w.perRegion > 1 && !w.noPinWatch { |
| 414 | w.checkFilesPreserved() // INV-30 (joint round 2): only the two-box shape has files keys |
| 415 | } |
| 416 | } |
| 417 | |
| 418 | func (w *world) boxesState() string { |
| 419 | s := "" |
| 420 | for _, b := range w.liveBoxes() { |
| 421 | s += fmt.Sprintf(" [box %d r%d row=%+v procs=%d db=%v files=%v cfg=%d live=%s/%d old=%v]", b.ID, b.Region, b.Row, len(b.Procs), b.DB != nil, b.Files != nil, b.Config, b.Live, b.LiveInc, b.Old) |
| 422 | } |
| 423 | return s |
| 424 | } |
| 425 | |
| 426 | // residue lists live-namespace data that should not exist: everything |
| 427 | // under the host's namespace in a region the host does not serve from, and |
| 428 | // in the serving region anything but the claim's location and generation |
| 429 | // (and the parkers' own locks). Nothing here writes. |
| 430 | func (w *world) residue() []string { return w.residueOf(false) } |
| 431 | |
| 432 | // residueAtEnd is INV-10 as the spec states it, checked when an operation |
| 433 | // ends (a release to serving, a free): no copy outside the live set, except |
| 434 | // a straggler that completed after H, which only the sweep can retire. |
| 435 | func (w *world) residueAtEnd() []string { return w.residueOf(true) } |
| 436 | |
| 437 | func (w *world) residueOf(exceptStragglers bool) []string { |
| 438 | var out []string |
| 439 | c := w.claim |
| 440 | live := map[string]bool{} |
| 441 | serving := -1 |
| 442 | if c != nil && c.Holder != nil { |
| 443 | if e := w.execBox(c); e != nil { |
| 444 | serving = e.Region |
| 445 | loc, gen := c.Holder.Location, c.Holder.Gen |
| 446 | live[dataKey(loc, gen, "")] = true // the generation's prefix: every LTX file of the generation |
| 447 | live[genMarkerKey(loc)] = true |
| 448 | live[dataKey(loc, gen, "closed/")] = true // the live generation's certificates, every session's (claim rev 6.8 §6.4a) |
| 449 | // an unfinished admission's predecessor is its baseline until the |
| 450 | // marker names the new generation (claim rev 6.10, R10-2) |
| 451 | if bg, _ := w.bucketGen(e, loc); bg != gen { |
| 452 | if chain, ok := w.unfinishedChain(c, bg); ok { |
| 453 | for _, g := range append(chain, bg) { |
| 454 | live[dataKey(loc, g, "")] = true |
| 455 | live[dataKey(loc, g, "closed/")] = true |
| 456 | } |
| 457 | } |
| 458 | } |
| 459 | } |
| 460 | } |
| 461 | for r := 0; r < nRegions; r++ { |
| 462 | bk := w.buckets[r] |
| 463 | for _, p := range []string{"instances/" + host + "/", "moves/" + host + "/"} { |
| 464 | for _, k := range bk.keys(p) { |
| 465 | if strings.HasSuffix(k, "lock.json") || (r == serving && (live[k] || isDataKey(k) && live[genPrefixOf(k)] || isClosedKey(k) && live[k[:strings.LastIndex(k, "closed/")+7]] || w.filesLiveSet(c, r, k))) { |
| 466 | continue |
| 467 | } |
| 468 | if exceptStragglers && w.owed(r, k) { |
| 469 | continue // a pending chore of another operation covers it |
| 470 | } |
| 471 | for _, v := range bk.objs[k] { |
| 472 | if !v.Marker && !(exceptStragglers && (v.Straggler || v.SweepOwed)) { |
| 473 | out = append(out, fmt.Sprintf("r%d:%s", r, k)) |
| 474 | break |
| 475 | } |
| 476 | } |
| 477 | } |
| 478 | } |
| 479 | } |
| 480 | return out |
| 481 | } |
| 482 | |
| 483 | // owed: an open park obligation names this region and a prefix of k. |
| 484 | func (w *world) owed(r int, k string) bool { |
| 485 | c := w.claim |
| 486 | if c == nil { |
| 487 | return false |
| 488 | } |
| 489 | for _, o := range c.Obl { |
| 490 | if o.Region == r && o.Prefix != "" && strings.HasPrefix(k, o.Prefix) { |
| 491 | return true |
| 492 | } |
| 493 | } |
| 494 | // a cold admission whose writer died after its marker landed and before |
| 495 | // it queued the retire chores (rev 7.11): the writers journal still |
| 496 | // shows its predecessor uncovered, and the next admission's marker |
| 497 | // retires it (§5.1 step 9); until then the predecessor is owed, as a |
| 498 | // pending chore's keys are (seeds 4159, 26817, 34163 / 100,000) |
| 499 | if h := c.Holder; h != nil && strings.HasPrefix(k, h.Location) { |
| 500 | g := genOf(h.Location, k) |
| 501 | for i := range c.Holder.Admissions { |
| 502 | if e := &c.Holder.Admissions[i]; e.Mode == "cold" && !e.Covered && e.Predecessor.Gen == g { |
| 503 | return true |
| 504 | } |
| 505 | } |
| 506 | } |
| 507 | return false |
| 508 | } |
| 509 | |
| 510 | func hasNonMarker(vs []*version) bool { |
| 511 | for _, v := range vs { |
| 512 | if !v.Marker { |
| 513 | return true |
| 514 | } |
| 515 | } |
| 516 | return false |
| 517 | } |
| 518 | |
| 519 | // canStart is the start check and admission, computed without starting |
| 520 | // anything: the final oracle never writes. |
| 521 | func (w *world) canStart(e *box, c *claim) string { |
| 522 | c = c.clone() |
| 523 | // the wake's first step is the record's initialization from this fresh |
| 524 | // read (claim rev 6.5 §6.4): a box with no record for the incarnation |
| 525 | // that the claim names as op.exec takes holder.stamp. On a copy of the |
| 526 | // box: the oracle never writes (R6-1) |
| 527 | eb := *e |
| 528 | eb.Stamps = map[int]*stamps{} |
| 529 | for k, v := range e.Stamps { |
| 530 | cp := *v |
| 531 | cp.Retired = append([]int(nil), v.Retired...) |
| 532 | eb.Stamps[k] = &cp |
| 533 | } |
| 534 | inc := c.Holder.Inc |
| 535 | if eb.stampOf(inc) == 0 && c.Holder.Stamp != 0 && c.Op.Exec == eb.ID && !(eb.Stamps[inc] != nil && contains(eb.Stamps[inc].Retired, c.Holder.Stamp)) { |
| 536 | eb.install(inc, c.Holder.Stamp) |
| 537 | } |
| 538 | c.readStamp = eb.stampOf(inc) // as a fresh read by e would carry it |
| 539 | if !w.admits(&eb, c, "") { |
| 540 | return "not admitted" |
| 541 | } |
| 542 | h := c.Holder |
| 543 | bg, binc := w.bucketGen(e, h.Location) |
| 544 | if bg != h.Gen || (bg != "" && binc != h.Inc) { |
| 545 | return fmt.Sprintf("generation.json %q, claim %q", bg, h.Gen) |
| 546 | } |
| 547 | if e.Files != nil && (e.Files.Gen != bg || e.Files.Inc != h.Inc) { |
| 548 | return fmt.Sprintf(".files-gen %q inc %d", e.Files.Gen, e.Files.Inc) |
| 549 | } |
| 550 | return "" |
| 551 | } |
| 552 | |
| 553 | // finalFreed is the end state of a freed host: no record, and no box holds |
| 554 | // local state for it. |
| 555 | func (w *world) finalFreed() { |
| 556 | if w.rec != nil { |
| 557 | w.violate("claim/record: claim free but record inc %d exists", w.rec.Inc) |
| 558 | } |
| 559 | for _, b := range w.liveBoxes() { |
| 560 | if b.DB != nil || b.Files != nil { |
| 561 | w.violate("INV-10: box %d still holds local state for a freed host", b.ID) |
| 562 | } |
| 563 | } |
| 564 | } |
| 565 | |
| 566 | func (w *world) final() { |
| 567 | if !w.quiescent() { |
| 568 | if len(w.pending) == 0 && len(w.console) == 0 && w.atRest() { |
| 569 | w.violate("INV-10: residue never retired: %v", w.residue()) |
| 570 | return |
| 571 | } |
| 572 | w.violate("INV-3: no convergence after %d calm steps: %s; %s%s", calmSteps, w.whyNotQuiescent(), w.state(), w.boxesState()) |
| 573 | return |
| 574 | } |
| 575 | c := w.claim |
| 576 | if c == nil || c.Holder == nil { |
| 577 | w.finalFreed() |
| 578 | return |
| 579 | } |
| 580 | e := w.execBox(c) |
| 581 | if !hasMain(e) && c.Op.Kind == "serving" && w.certificate(e, c) == nil { |
| 582 | // the host is at rest after a session that did not certify: its |
| 583 | // next wake is a cold admission that declares the acknowledged, |
| 584 | // unuploaded writes (R10-6). Rev 7.11's oracle exempted them as a |
| 585 | // prospective declaration, recording and alerting nothing; the |
| 586 | // recovery admission is run for real now, then everything it |
| 587 | // queued, and the writes are judged by what it declared |
| 588 | w.stats["final: recovery admission run"]++ |
| 589 | w.drive(400, func() bool { return hasMain(e) && e.open == nil }, func() { w.wake(e) }, w.actAll(), w.runConsole, w.recoveryPass, w.operator) |
| 590 | if len(w.violations) > 0 { |
| 591 | return |
| 592 | } |
| 593 | if !(hasMain(e) && e.open == nil) { |
| 594 | w.stats["final: unverified prospective declaration"]++ |
| 595 | w.logf("final: the recovery admission on box %d did not complete; its declaration is unverified", e.ID) |
| 596 | } else { |
| 597 | w.drive(calmSteps, w.quiescent, w.actAll(), w.runConsole, w.recoveryPass, w.operator) |
| 598 | if len(w.violations) > 0 { |
| 599 | return |
| 600 | } |
| 601 | if !w.quiescent() { |
| 602 | w.violate("INV-3: no convergence after the final recovery admission: %s; %s%s", w.whyNotQuiescent(), w.state(), w.boxesState()) |
| 603 | return |
| 604 | } |
| 605 | } |
| 606 | c = w.claim |
| 607 | if c == nil || c.Holder == nil { |
| 608 | // the final drive ran the console too: a purge may have freed |
| 609 | // the host (seed 2547 / 3,000 under admission-registration) |
| 610 | w.finalFreed() |
| 611 | return |
| 612 | } |
| 613 | e = w.execBox(c) |
| 614 | } |
| 615 | if e == nil || w.rec == nil { |
| 616 | w.violate("claim/record: the claim's holder has no record or no executing box at the end: %s", w.state()) |
| 617 | return |
| 618 | } |
| 619 | if w.rec.Region != e.Region { |
| 620 | w.violate("claim/record: record region %d, claim serves from box %d in region %d", w.rec.Region, e.ID, e.Region) |
| 621 | } |
| 622 | for _, b := range w.liveBoxes() { |
| 623 | if b != e && (b.DB != nil || b.Files != nil) { |
| 624 | w.violate("INV-10: box %d holds local state; the host serves from box %d", b.ID, e.ID) |
| 625 | } |
| 626 | } |
| 627 | if !hasMain(e) { |
| 628 | if why := w.canStart(e, c); why != "" { |
| 629 | w.violate("final: the serving box %d cannot start the host: %s (%s)", e.ID, why, w.state()) |
| 630 | return |
| 631 | } |
| 632 | } |
| 633 | // the serving box's database as it stands, or, if it has none, the |
| 634 | // cold restore it would do: computed, never written |
| 635 | before := w.fingerprint() |
| 636 | defer w.pure("final oracle", before) |
| 637 | local := e.DB |
| 638 | if local == nil { |
| 639 | local = w.restoreAsNext(e, c) |
| 640 | } |
| 641 | if local == nil { |
| 642 | w.violate("final: the serving box %d has no database and nothing to restore", e.ID) |
| 643 | return |
| 644 | } |
| 645 | if w.stats["final: unverified prospective declaration"] == 0 || w.certificate(e, c) != nil { |
| 646 | w.checkLocal(c, e, local) |
| 647 | } |
| 648 | w.checkDurable(c, "final") |
| 649 | if w.lostAlert != w.stats["writes_lost declared"] { |
| 650 | w.violate("INV-14: %d writes_lost records, %d alerts delivered (R10-6)", w.stats["writes_lost declared"], w.lostAlert) |
| 651 | } |
| 652 | } |
| 653 | |
| 654 | // checkDurable is the cold-restore promise, checked at every release to |
| 655 | // serving and at the end: a restore of the claim's location and generation |
| 656 | // in the serving region holds the effect of every acknowledged write that |
| 657 | // a completed replica object ever covered, and equals the database the |
| 658 | // acknowledged writes up to its TXID produce. It reads the bucket and |
| 659 | // writes nothing. |
| 660 | func (w *world) checkDurable(c *claim, when string) { |
| 661 | if c == nil || c.Holder == nil { |
| 662 | return |
| 663 | } |
| 664 | e := w.execBox(c) |
| 665 | if e == nil { |
| 666 | return |
| 667 | } |
| 668 | before := w.fingerprint() |
| 669 | defer w.pure("INV-2 oracle", before) |
| 670 | db := w.restoreAsNext(e, c) |
| 671 | need := map[int]bool{} |
| 672 | seen := map[string]bool{} |
| 673 | for p := dataKey(c.Holder.Location, c.Holder.Gen, ""); p != "" && !seen[p]; p = w.genParent[p] { |
| 674 | seen[p] = true |
| 675 | for x := range w.durable[p] { |
| 676 | need[x] = true |
| 677 | } |
| 678 | } |
| 679 | have := map[int]bool{} |
| 680 | if db != nil { |
| 681 | for _, x := range db.Log { |
| 682 | have[x] = true |
| 683 | } |
| 684 | } |
| 685 | for _, a := range w.acks { |
| 686 | if a.Inc != c.Holder.Inc || a.Exempt || a.Kind != "write" || !need[a.W] { |
| 687 | continue |
| 688 | } |
| 689 | // coverage by write identity (R7-2): a required write is present |
| 690 | // only if a file the restore applied carried it; a maximum TXID |
| 691 | // says nothing after a fork |
| 692 | if db == nil || !have[a.W] { |
| 693 | w.violate("INV-2 (cold restore, %s): durable write %d (box %d, t=%d) lost (%s)", when, a.W, a.Box, a.At, w.ltxShape(e.Region, dataKey(c.Holder.Location, c.Holder.Gen, ""))) |
| 694 | return |
| 695 | } |
| 696 | } |
| 697 | if db == nil { |
| 698 | return |
| 699 | } |
| 700 | w.foreignWrites(db, c.Holder.Inc, "cold restore, "+when) |
| 701 | // the restored state must be the replay, in acknowledgement order, of |
| 702 | // exactly the writes its files carried (R7-2): a write declared lost |
| 703 | // with a disk that landed anyway is replayed because it is there, a |
| 704 | // required write that is missing was caught above, and no key is ever |
| 705 | // masked; a later required write re-establishes its key's value |
| 706 | if why, ok := statesEqual(w.expectFrom(c.Holder.Inc, have), db.State); !ok { |
| 707 | w.violate("INV-2 (cold restore, %s): the restored database differs from the replay of the writes it carries: %s (restored TXID %d; %s; %s; %s)", when, why, db.TX, w.keyHistory(c.Holder.Inc, why, have), w.ltxShape(e.Region, dataKey(c.Holder.Location, c.Holder.Gen, "")), w.fileDetail(e.Region, dataKey(c.Holder.Location, c.Holder.Gen, ""), why)) |
| 708 | } |
| 709 | } |
| 710 | |
| 711 | // fileDetail lists, for diagnosis, each current file of the generation |
| 712 | // with its kind, range, TXs and the page it holds for the key named in a |
| 713 | // statesEqual message. |
| 714 | func (w *world) fileDetail(r int, prefix, why string) string { |
| 715 | key := "" |
| 716 | if i := strings.Index(why, "key "); i >= 0 { |
| 717 | rest := why[i+4:] |
| 718 | if j := strings.Index(rest, " "); j > 0 { |
| 719 | key = rest[:j] |
| 720 | } |
| 721 | } |
| 722 | bk := w.buckets[r] |
| 723 | var out []string |
| 724 | for _, k := range bk.keys(prefix) { |
| 725 | v := bk.current(k) |
| 726 | if v == nil || v.B == nil || !isDataKey(k) { |
| 727 | continue |
| 728 | } |
| 729 | val, ok := v.B.Pages[key] |
| 730 | out = append(out, fmt.Sprintf("%s{full=%v txs=%v %s=%d/%v}", strings.TrimPrefix(k, prefix), v.B.Full, v.B.TXs, key, val, ok)) |
| 731 | } |
| 732 | return "detail " + strings.Join(out, " ") |
| 733 | } |
| 734 | |
| 735 | // keyHistory lists, for diagnosis, the acknowledged writes of inc that |
| 736 | // touched the key named in a statesEqual message: W, lineage TXID, value, |
| 737 | // whether the restored files carried it, whether it is exempt. |
| 738 | func (w *world) keyHistory(inc int, why string, have map[int]bool) string { |
| 739 | key := "" |
| 740 | if i := strings.Index(why, "key "); i >= 0 { |
| 741 | rest := why[i+4:] |
| 742 | if j := strings.Index(rest, " "); j > 0 { |
| 743 | key = rest[:j] |
| 744 | } |
| 745 | } |
| 746 | var out []string |
| 747 | for _, a := range w.acks { |
| 748 | if a.Inc != inc || a.Kind != "write" { |
| 749 | continue |
| 750 | } |
| 751 | t := w.txs[a.W] |
| 752 | k := t.Key |
| 753 | if k == "" { |
| 754 | k = fmt.Sprintf("k%d", a.W) |
| 755 | } |
| 756 | if k != key { |
| 757 | continue |
| 758 | } |
| 759 | out = append(out, fmt.Sprintf("W%d:TX%d=%d have=%v exempt=%v session=%d gen=%q", a.W, t.TX, t.Val, have[a.W], a.Exempt, a.Session, a.Gen)) |
| 760 | } |
| 761 | return "history of " + key + ": " + strings.Join(out, " ") |
| 762 | } |
| 763 | |
| 764 | // expectFrom replays, in acknowledgement order, the acknowledged writes of |
| 765 | // inc that the restored files carried (have), into the state a correct |
| 766 | // restore of those files must equal. |
| 767 | func (w *world) expectFrom(inc int, have map[int]bool) map[string]int { |
| 768 | state := map[string]int{} |
| 769 | for _, a := range w.acks { |
| 770 | if a.Inc != inc || a.Kind != "write" || !have[a.W] { |
| 771 | continue |
| 772 | } |
| 773 | t := w.txs[a.W] |
| 774 | if t.Key == "" { |
| 775 | t.Key, t.Val = fmt.Sprintf("k%d", a.W), a.W |
| 776 | } |
| 777 | if t.Val == 0 { |
| 778 | delete(state, t.Key) |
| 779 | } else { |
| 780 | state[t.Key] = t.Val |
| 781 | } |
| 782 | } |
| 783 | return state |
| 784 | } |
| 785 | |
| 786 | // counting is the sweep's random source, counting its draws so the oracle |
| 787 | // purity check can show an oracle consumed none (R6-1). |
| 788 | type counting struct { |
| 789 | r *rand.Rand |
| 790 | n int |
| 791 | } |
| 792 | |
| 793 | func (c *counting) Intn(n int) int { |
| 794 | c.n++ |
| 795 | return c.r.Intn(n) |
| 796 | } |
| 797 | |
| 798 | // fingerprint is everything an oracle must leave alone: the buckets (the |
| 799 | // version counter and every version), the pending requests, the boxes' |
| 800 | // upload queues and anchors, the console's plans and the random source's |
| 801 | // position (R6-1). An oracle that changes any of it is repairing or |
| 802 | // disturbing the system it checks. |
| 803 | func (w *world) fingerprint() string { |
| 804 | objs := 0 |
| 805 | for _, bk := range w.buckets { |
| 806 | for _, vs := range bk.objs { |
| 807 | objs += len(vs) |
| 808 | } |
| 809 | } |
| 810 | queue, anchors := 0, 0 |
| 811 | for _, b := range w.boxes { |
| 812 | if b.DB != nil { |
| 813 | queue += len(b.DB.Queue) |
| 814 | } |
| 815 | for _, rs := range b.anchors { |
| 816 | anchors += len(rs) |
| 817 | } |
| 818 | } |
| 819 | draws := -1 |
| 820 | if c, ok := w.rng.(*counting); ok { |
| 821 | draws = c.n |
| 822 | } |
| 823 | return fmt.Sprintf("ver=%d objs=%d pending=%d queue=%d anchors=%d console=%d draws=%d", w.ver, objs, len(w.pending), queue, anchors, len(w.console), draws) |
| 824 | } |
| 825 | |
| 826 | // pure records a violation if an oracle changed the system (R6-1): the |
| 827 | // fingerprint taken before it must equal the one after. |
| 828 | func (w *world) pure(what, before string) { |
| 829 | if after := w.fingerprint(); after != before { |
| 830 | w.violate("oracle purity: the %s changed the system: before %s, after %s", what, before, after) |
| 831 | } |
| 832 | } |
| 833 | |
| 834 | // ltxShape describes the current LTX files under prefix, for diagnosis. |
| 835 | func (w *world) ltxShape(r int, prefix string) string { |
| 836 | var parts []string |
| 837 | bk := w.buckets[r] |
| 838 | for _, k := range bk.keys(prefix) { |
| 839 | if !isDataKey(k) { |
| 840 | continue |
| 841 | } |
| 842 | var vs []string |
| 843 | for _, v := range bk.objs[k] { |
| 844 | if v.Marker { |
| 845 | vs = append(vs, "M") |
| 846 | } else { |
| 847 | vs = append(vs, fmt.Sprintf("v%d", v.ID)) |
| 848 | } |
| 849 | } |
| 850 | parts = append(parts, strings.TrimPrefix(k, prefix)+":"+strings.Join(vs, ",")) |
| 851 | } |
| 852 | return "files " + strings.Join(parts, " ") |
| 853 | } |
| 854 | |
| 855 | // foreignWrites: a database restored or started for incarnation inc holds |
| 856 | // no key another incarnation wrote (C1, INV-4, claim C3a). |
| 857 | func (w *world) foreignWrites(db *localDB, inc int, how string) { |
| 858 | for k, v := range db.State { |
| 859 | if v == 0 { |
| 860 | continue |
| 861 | } |
| 862 | if i, ok := w.writeInc[keyID(k)]; ok && i != inc { |
| 863 | w.violate("C3a (%s): incarnation %d's database holds key %s of incarnation %d", how, inc, k, i) |
| 864 | return |
| 865 | } |
| 866 | } |
| 867 | } |
| 868 | |
| 869 | // checkLocal: the serving box's database holds the effect of every |
| 870 | // acknowledged, non-exempt write of the incarnation (INV-2), and every |
| 871 | // acknowledged timer is delivered or still registered. |
| 872 | func (w *world) checkLocal(c *claim, e *box, db *localDB) { |
| 873 | // the serving database is the replay of every acknowledged write that |
| 874 | // was never declared lost, and of every write declared lost that came |
| 875 | // back: an upload in flight at a lost disk that landed anyway, which a |
| 876 | // later cold admission's remote baseline carried (R7-2's identity rule, |
| 877 | // as checkDurable applies it; seed 5863 / 30,000) |
| 878 | have := map[int]bool{} |
| 879 | for _, x := range db.Log { |
| 880 | have[x] = true |
| 881 | } |
| 882 | want := map[int]bool{} |
| 883 | for _, a := range w.acks { |
| 884 | if a.Inc == c.Holder.Inc && a.Kind == "write" && (!a.Exempt || have[a.W]) { |
| 885 | want[a.W] = true |
| 886 | } |
| 887 | } |
| 888 | if why, ok := statesEqual(w.expectFrom(c.Holder.Inc, want), db.State); !ok { |
| 889 | w.violate("INV-2 (local): the serving database differs from the acknowledged writes: %s (%s)", why, w.keyHistory(c.Holder.Inc, why, have)) |
| 890 | return |
| 891 | } |
| 892 | timers := map[int]bool{} |
| 893 | for _, x := range e.Timers { |
| 894 | timers[x] = true |
| 895 | } |
| 896 | for _, a := range w.acks { |
| 897 | if a.Inc != c.Holder.Inc || a.Exempt || a.Kind != "timer" { |
| 898 | continue |
| 899 | } |
| 900 | if !w.delivered[a.W] && !timers[a.W] { |
| 901 | w.violate("INV-2: acknowledged timer %d (box %d, t=%d) lost", a.W, a.Box, a.At) |
| 902 | return |
| 903 | } |
| 904 | } |
| 905 | } |
| 906 | |
| 907 | func (w *world) state() string { |
| 908 | c := w.claim |
| 909 | if c == nil { |
| 910 | return fmt.Sprintf("claim absent, record %+v", w.rec) |
| 911 | } |
| 912 | obl := "" |
| 913 | for _, o := range c.Obl { |
| 914 | obl += fmt.Sprintf(" %s:%s/r%d/b%d/%s", o.ID, o.Kind, o.Region, o.Box, o.Prefix) |
| 915 | } |
| 916 | adm := "" |
| 917 | for app, ad := range w.admit { |
| 918 | adm += fmt.Sprintf(" %s:closed=%v/reg=%d", app, ad.Closed, len(ad.Reg)) |
| 919 | } |
| 920 | return fmt.Sprintf("op=%s/%s phase=%s land=%s src=%s rev=%s exec=%d obl=%d holder=%+v rec=%+v pending=%d console=%d obls=[%s] quiet=%v h2=%+v admission=[%s] residue=%v", |
| 921 | c.Op.Kind, c.Op.ID, c.Op.Phase, c.Op.LandPhase, c.Op.SrcPhase, c.Op.RevPhase, c.Op.Exec, len(c.Obl), c.Holder, w.rec, len(w.pending), len(w.console), obl, c.Quiet, w.h2, adm, w.residue()) |
| 922 | } |
| 923 | |
| 924 | // ---------- running ---------- |
| 925 | |
| 926 | func runSeed(seed int64, verbose bool) *world { |
| 927 | w := newWorld(seed, verbose) |
| 928 | for i := 0; i < chaosSteps; i++ { |
| 929 | w.step() |
| 930 | } |
| 931 | w.heal(false) |
| 932 | for i := 0; i < calmSteps && !w.quiescent(); i++ { |
| 933 | w.step() |
| 934 | if i == 400 || i%400 == 399 { |
| 935 | w.heal(true) |
| 936 | if w.verbose { |
| 937 | w.logf("calm step %d: %s", i, w.whyNotQuiescent()) |
| 938 | } |
| 939 | } |
| 940 | } |
| 941 | w.completeDue(true) |
| 942 | w.final() |
| 943 | return w |
| 944 | } |
| 945 | |
| 946 | func seedsFromEnv(def int) int { |
| 947 | if s := os.Getenv("HOSTLIFE_SEEDS"); s != "" { |
| 948 | if n, err := strconv.Atoi(s); err == nil { |
| 949 | return n |
| 950 | } |
| 951 | } |
| 952 | return def |
| 953 | } |
| 954 | |
| 955 | // TestHostLifecycle runs the joint model. HOSTLIFE_SEEDS sets the seed |
| 956 | // count (the gate's default is short); HOSTLIFE_SEED=n runs one seed and |
| 957 | // prints its trace; HOSTLIFE_BOXES=2 runs the two-box shape (region HA |
| 958 | // L18) in place of the one-box one. |
| 959 | func TestHostLifecycle(t *testing.T) { |
| 960 | sweep(t) |
| 961 | } |
| 962 | |
| 963 | // TestHostLifecycleTwoBox runs the joint model with two boxes per region |
| 964 | // (region HA L18) beside the one-box sweep, so the gate covers both |
| 965 | // shapes. With HOSTLIFE_BOXES set, TestHostLifecycle runs that shape and |
| 966 | // this test stands aside. |
| 967 | func TestHostLifecycleTwoBox(t *testing.T) { |
| 968 | if os.Getenv("HOSTLIFE_BOXES") != "" { |
| 969 | t.Skip("HOSTLIFE_BOXES is set: TestHostLifecycle runs that shape") |
| 970 | } |
| 971 | saved := boxesPerRegion |
| 972 | boxesPerRegion = 2 |
| 973 | defer func() { boxesPerRegion = saved }() |
| 974 | sweep(t) |
| 975 | } |
| 976 | |
| 977 | func sweep(t *testing.T) { |
| 978 | if s := os.Getenv("HOSTLIFE_SEED"); s != "" { |
| 979 | seed, _ := strconv.ParseInt(s, 10, 64) |
| 980 | w := runSeed(seed, true) |
| 981 | for _, line := range w.trace { |
| 982 | t.Log(line) |
| 983 | } |
| 984 | for _, v := range w.violations { |
| 985 | t.Errorf("seed %d: %s", seed, v) |
| 986 | } |
| 987 | return |
| 988 | } |
| 989 | n := seedsFromEnv(300) |
| 990 | failed := 0 |
| 991 | kinds := map[string]int{} |
| 992 | firstSeed := map[string]int64{} |
| 993 | ops := 0 |
| 994 | stats := map[string]int{} |
| 995 | for seed := int64(1); seed <= int64(n); seed++ { |
| 996 | w := runSeed(seed, false) |
| 997 | ops += w.opsDone |
| 998 | for k, v := range w.stats { |
| 999 | stats[k] += v |
| 1000 | } |
| 1001 | if len(w.violations) > 0 { |
| 1002 | failed++ |
| 1003 | k := kind(w.violations[0]) |
| 1004 | kinds[k]++ |
| 1005 | if _, ok := firstSeed[k]; !ok { |
| 1006 | firstSeed[k] = seed |
| 1007 | t.Logf("seed %d: %s", seed, w.violations[0]) |
| 1008 | } |
| 1009 | } |
| 1010 | } |
| 1011 | t.Logf("%d seeds, %d failed, %d completed operations; mutated=%q boxes=%d", n, failed, ops, mutated, boxesPerRegion) |
| 1012 | t.Logf("outcomes: %v", stats) |
| 1013 | if js, err := json.Marshal(stats); err == nil { |
| 1014 | t.Logf("COUNTERS %s", js) // structured, for the spec's generator (R10-9) |
| 1015 | } |
| 1016 | for k, c := range kinds { |
| 1017 | t.Logf(" %4d × %s (first seed %d)", c, k, firstSeed[k]) |
| 1018 | } |
| 1019 | if failed > 0 { |
| 1020 | t.Fatalf("%d of %d seeds violated an invariant", failed, n) |
| 1021 | } |
| 1022 | } |
| 1023 | |
| 1024 | func kind(v string) string { |
| 1025 | if i := strings.Index(v, ": "); i >= 0 { |
| 1026 | v = v[i+2:] |
| 1027 | } |
| 1028 | // strip ids and numbers so a family groups together |
| 1029 | var b strings.Builder |
| 1030 | skip := false |
| 1031 | for _, r := range v { |
| 1032 | if r >= '0' && r <= '9' { |
| 1033 | if !skip { |
| 1034 | b.WriteByte('#') |
| 1035 | } |
| 1036 | skip = true |
| 1037 | continue |
| 1038 | } |
| 1039 | skip = false |
| 1040 | b.WriteRune(r) |
| 1041 | } |
| 1042 | v = b.String() |
| 1043 | if i := strings.Index(v, " holder="); i >= 0 { |
| 1044 | v = v[:i] |
| 1045 | } |
| 1046 | if len(v) > 110 { |
| 1047 | v = v[:110] |
| 1048 | } |
| 1049 | return v |
| 1050 | } |
| 1051 | |
amadan