| new file mode 100644 |
| index 000000000..842abb56b |
| --- /dev/null |
| +++ b/internal/sim/hostlife/witness_test.go |
| @@ -0,0 +1,738 @@ |
| +package hostlife |
| + |
| +import ( |
| + "fmt" |
| + "os" |
| + "strings" |
| + "testing" |
| +) |
| + |
| +// Witness scenarios (moves spec §14.2, rev 7.3). |
| +// |
| +// The random sweep reaches some interleavings rarely, and every new biased |
| +// schedule reshuffles every seed, so a rare rule's catch can vanish from |
| +// one revision to the next (lost-return-park in rev 7.1, |
| +// generation-conditional in rev 7.2). A witness is one fixed, hand-scheduled |
| +// scenario for one rule: it forces exactly the interleaving the rule |
| +// exists for, as a sequence of protocol steps the witness chooses, with a |
| +// quiet RNG that injects nothing. It must hold (no invariant violated) with |
| +// the rules in place, and violate an invariant when the rule's mutation is |
| +// applied, alone or in the stated combination. |
| +// |
| +// Witnesses never draw from a seed's RNG and never run inside the sweep's |
| +// seeds, so adding one reshuffles nothing. They are the deterministic half |
| +// of the mutation evidence; mutate.sh runs TestWitnesses beside the sweep |
| +// and reports both. |
| + |
| +// quiet is the witness's RNG: every draw takes the branch that injects |
| +// nothing (no fault, no stall, no duplicate, no late completion, no |
| +// second process), so a scenario is exactly the steps the witness scripts. |
| +type quiet struct{} |
| + |
| +func (quiet) Intn(n int) int { |
| + if n <= 1 { |
| + return 0 |
| + } |
| + return 1 |
| +} |
| + |
| +type witness struct { |
| + rule string // the rule it is for |
| + needs string // the mutation set under which it must violate: the rule alone, or a combination the rule belongs to |
| + note string // what it shows |
| + run func(t *testing.T, w *world) |
| +} |
| + |
| +var witnesses = []witness{ |
| + {"generation-conditional", "generation-conditional", |
| + "an earlier push's generation.json PUT completes after a later push's; unconditional, it puts the old generation back and the serving box cannot start", wGenerationConditional}, |
| + {"lost-return-park", "lost-return-park", |
| + "a target stopped after its first return PUT is declared lost; without the park the lane stays in the source region at the release (INV-10)", wLostReturnPark}, |
| + {"declare-lost-compute", "declare-lost-compute", |
| + "a frozen target's lease expires; declared lost on expiry alone, it resumes beside the recovered source (INV-1)", wDeclareLostCompute}, |
| + {"watchdog-independent", "declare-lost-compute,watchdog-independent", |
| + "redundant alone: with compute fencing a paused agent cannot be declared lost; with expiry-based declare-lost, a watchdog inside the paused agent never fences, and the target runs beside the recovered source (INV-1)", wWatchdogIndependent}, |
| + {"lost-quarantine", "lost-quarantine", |
| + "a lost box starts again with its old disk; without the quarantine it keeps a database and files for a host served elsewhere (INV-10)", wLostQuarantine}, |
| + {"markers-last", "markers-last", |
| + "the target's agent crashes between extracting the files and writing the marker; a marker written first vouches for timers that were never installed (INV-2)", wMarkersLast}, |
| + {"rollback-journal", "rollback-journal", |
| + "the source's agent restarts during a dirty rollback's probe; without the journal it restarts at `claimed`, parks the return generation it had replicated into, and a durable write is lost on cold restore (INV-2)", wRollbackJournal}, |
| + {"seal-by-version", "seal-by-version", |
| + "a pre-cut staging round completes after the seal; a landing that copies the current version installs the stale round and loses the writes made after it (INV-2)", wSealByVersion}, |
| + {"staging-quiet", "staging-quiet", |
| + "a staging round completes after the landing's staging park acknowledged; retired at the seal rather than after the writers' horizon, the round is residue at the release (INV-10)", wStagingQuiet}, |
| + {"claim-cas-opid", "claim-cas-opid,revalidate-before-effect", |
| + "redundant alone: a stalled source goroutine with the rollback's last read resumes after a purge claimed the host; revalidation stops it, and so does the op-id condition on its release CAS; with both gone the release overwrites the purge and the store is torn down under a serving host", wClaimCasOpID}, |
| + {"dirty-return", "dirty-return", |
| + "a target that wrote during its probe is rolled back; without the return its writes are lost (INV-2)", wDirtyReturn}, |
| + {"commit-before-open", "commit-before-open,dirty-return", |
| + "redundant alone in this model: a row opened before the commit admits nothing while the claim is uncommitted; the only violation the scenario can show is dirty-return's", wDirtyReturn}, |
| + {"exec-admission", "exec-admission,hold-op-open,start-check-claim-gen", |
| + "one of three admission fences (J2-R2-8): a paused open from an earlier operation makes the old source ready after the commit; hold_op refuses the open, the exec check refuses the wake, the generation check refuses the start; with all three gone the source serves beside the target (INV-1)", wAdmissionTriple}, |
| + {"hold-op-open", "exec-admission,hold-op-open,start-check-claim-gen", "one of three admission fences (see exec-admission)", wAdmissionTriple}, |
| + {"start-check-claim-gen", "exec-admission,hold-op-open,start-check-claim-gen", "one of three admission fences (see exec-admission)", wAdmissionTriple}, |
| + {"start-check", "exec-admission,hold-op-open,start-check", "the whole start check in place of its generation clause (see exec-admission)", wAdmissionTriple}, |
| + {"strict-spawn", "strict-spawn,evidence-whole-tree", |
| + "redundant alone: an escaped descendant is killed by the whole-tree cleanup; with evidence blind to escapees, a non-strict descendant survives the cut and writes beside the target (INV-1)", wStrictSpawn}, |
| + {"touched-incomplete", "touched-incomplete,legacy-discovery", |
| + "redundant alone: discovery at adoption parks the other regions; without discovery, an incomplete touched set must park every region at delete, or a pre-release replica is residue after free (INV-10)", wTouchedIncomplete}, |
| + {"door-reread", "door-reread,location-per-incarnation", |
| + "subsumed by C3a: a listing authorized for the old incarnation selects, after a recreate into the shared location, the new incarnation's object; O2 refuses it", wDoorReread}, |
| + {"door-by-version", "door-by-version,location-per-incarnation", |
| + "subsumed by C3a: a handle signed before the delete opens, after a recreate into the shared location, the key's current object unless bound to the version it selected", wDoorByVersion}, |
| + {"registration-check", "registration-check,fence-etag", |
| + "a cheap extra: a creator paused across a whole purge resumes; the fence and the ETag condition refuse it without the re-read; with the ETag condition gone the re-read is what stops it", wRegistrationCheck}, |
| + {"registration-check", "registration-check,purge-claim-fence", |
| + "the same, with the fence gone instead", wRegistrationCheck}, |
| +} |
| + |
| +// TestWitnesses runs every witness. With no mutation every witness must |
| +// hold. Under HOSTLIFE_MUTATE=m it runs the witnesses of the rules in m |
| +// and reports each as violated or held; a witness whose stated mutation |
| +// set is within m must violate, or the witness is broken and the test |
| +// fails. HOSTLIFE_WITNESS=rule runs one rule's witnesses with their trace. |
| +func TestWitnesses(t *testing.T) { |
| + set := map[string]bool{} |
| + for _, m := range strings.Split(mutated, ",") { |
| + if m != "" { |
| + set[m] = true |
| + } |
| + } |
| + only := os.Getenv("HOSTLIFE_WITNESS") |
| + ran := 0 |
| + for _, x := range witnesses { |
| + if only != "" && x.rule != only { |
| + continue |
| + } |
| + if mutated != "" && !set[x.rule] { |
| + continue |
| + } |
| + ran++ |
| + w := newWitness() |
| + x.run(t, w) |
| + violated := len(w.violations) > 0 |
| + needs := true |
| + for _, m := range strings.Split(x.needs, ",") { |
| + if !set[m] { |
| + needs = false |
| + } |
| + } |
| + tag := "held" |
| + if violated { |
| + tag = "violated: " + w.violations[0] |
| + } |
| + switch { |
| + case mutated == "": |
| + t.Logf("witness %s: %s", x.rule, tag) |
| + if violated { |
| + t.Errorf("witness %s violated with every rule in place", x.rule) |
| + dump(t, w) |
| + } |
| + default: |
| + t.Logf("witness %s under %q (needs %q): %s", x.rule, mutated, x.needs, tag) |
| + if needs && !violated { |
| + t.Errorf("witness %s held under %q, which it must violate", x.rule, mutated) |
| + dump(t, w) |
| + } |
| + } |
| + if only != "" { |
| + dump(t, w) |
| + } |
| + } |
| + if only != "" && ran == 0 { |
| + t.Fatalf("no witness for rule %q", only) |
| + } |
| +} |
| + |
| +func dump(t *testing.T, w *world) { |
| + for _, line := range w.trace { |
| + t.Log(line) |
| + } |
| + t.Logf("state: %s%s", w.state(), w.boxesState()) |
| +} |
| + |
| +// ---------- the fixture ---------- |
| + |
| +// newWitness is a clean world: three boxes with the secrets key, no faults |
| +// armed, no legacy host, the quiet RNG, and the trace kept. |
| +func newWitness() *world { |
| + w := &world{seed: -1, rng: quiet{}, verbose: true, now: 100, |
| + stores: map[string]bool{app0: true, app1: true}, cfgVer: map[string]int{app0: 1, app1: 1}, purgeRes: map[string]bool{}, purgeStep: map[string]int{}, |
| + control: newBucket(), delivered: map[int]bool{}, durable: map[string]map[int]bool{}, writeInc: map[int]int{}, legacyIncs: map[int]bool{}, purgeOp: map[string]string{}, genParent: map[string]string{}, execLease: map[int]execLease{}, fail: map[string]bool{}, stats: map[string]int{}} |
| + for r := 0; r < nRegions; r++ { |
| + w.buckets[r] = newBucket() |
| + b := &box{ID: r, Region: r, HasKey: true} |
| + b.forget() |
| + w.boxes = append(w.boxes, b) |
| + } |
| + w.admit = map[string]*admission{app0: {Reg: map[string]regEntry{}}, app1: {Reg: map[string]regEntry{}}} |
| + return w |
| +} |
| + |
| +// serve installs incarnation inc of app on b as a serving host: claim, |
| +// record, row, local database and files, config rendered, and a replica |
| +// object with its acknowledged writes. |
| +func (w *world) serve(b *box, inc int, app string) { |
| + loc := locationFor(inc, false) |
| + key := 1000 + inc |
| + var writes []int |
| + for i := 0; i < 2; i++ { |
| + w.nextW++ |
| + writes = append(writes, w.nextW) |
| + w.acks = append(w.acks, ack{W: w.nextW, Inc: inc, Box: b.ID, At: w.now, Kind: "write"}) |
| + w.writeInc[w.nextW] = inc |
| + } |
| + if inc > w.nextInc { |
| + w.nextInc = inc |
| + } |
| + w.serial++ |
| + n := &claim{Ver: 1} |
| + if w.claim != nil { |
| + n = w.claim.clone() |
| + n.Ver++ |
| + } |
| + n.Holder = &holder{Inc: inc, App: app, Serial: w.serial, Location: loc} |
| + n.Op = opState{Kind: "serving", Exec: b.ID, Parts: []int{b.ID}} |
| + n.Regions, n.Boxes, n.Complete, n.Obl = []int{b.Region}, []int{b.ID}, true, nil |
| + w.claim = n |
| + w.rec = &record{Inc: inc, App: app, Region: b.Region} |
| + b.Row = &row{Inc: inc, App: app, Status: "ready"} |
| + b.DB = &localDB{Inc: inc, Loc: loc, Key: key, Writes: append([]int(nil), writes...)} |
| + b.Files = &filesDir{Inc: inc, Key: key, Env: key, Done: true} |
| + b.Config, b.CfgVer, b.Live, b.LiveInc = inc, w.cfgVer[app], app, inc |
| + k := dataKey(loc, "", "ltx") |
| + bl := &blob{Kind: "ltx", Inc: inc, Writes: append([]int(nil), writes...), SealKey: key} |
| + w.buckets[b.Region].objs[k] = append(w.buckets[b.Region].objs[k], &version{ID: w.newVer(), B: bl}) |
| + w.markDurable(k, bl) |
| + w.logf("witness: inc %d of app %s serving on box %d", inc, app, b.ID) |
| +} |
| + |
| +// legacy installs a pre-release host: an untagged replica in region r0 |
| +// where it serves with no claim, and a replica an earlier move left in r1. |
| +func (w *world) legacy(b *box, other int) { |
| + w.nextInc++ |
| + inc := w.nextInc |
| + w.rec = &record{Inc: inc, App: app0, Region: b.Region} |
| + w.legacyIncs[inc] = true |
| + key := 7 |
| + var writes []int |
| + for i := 0; i < 2; i++ { |
| + w.nextW++ |
| + writes = append(writes, w.nextW) |
| + w.acks = append(w.acks, ack{W: w.nextW, Inc: inc, Box: b.ID, At: w.now, Kind: "write"}) |
| + w.writeInc[w.nextW] = inc |
| + } |
| + b.Row = &row{Inc: inc, App: app0, Status: "ready"} |
| + b.DB = &localDB{Inc: inc, Loc: locationFor(inc, true), Key: key, Writes: writes} |
| + b.Files = &filesDir{Inc: inc, Key: key, Env: 1, Done: true} |
| + b.Config, b.CfgVer, b.Live, b.LiveInc = inc, 1, app0, inc |
| + k := "instances/" + host + "/ltx" |
| + w.buckets[b.Region].objs[k] = []*version{{ID: w.newVer(), B: &blob{Kind: "ltx", Inc: 0, Writes: writes, SealKey: key}}} |
| + w.markDurable(k, &blob{Writes: writes}) |
| + w.buckets[other].objs[k] = []*version{{ID: w.newVer(), B: &blob{Kind: "ltx", Inc: 0, Writes: writes[:1], SealKey: key}}} |
| +} |
| + |
| +// ---------- the schedule ---------- |
| + |
| +// tick is one step of the witness's own schedule: time, S3 completions, |
| +// paused goroutines, then the actors the witness names, then the per-step |
| +// invariants. |
| +func (w *world) tick(actors ...func()) { |
| + w.now++ |
| + w.completeDue(false) |
| + if p := w.recPend; p != nil && p.at <= w.now { |
| + w.recPend = nil |
| + if w.rec == nil { |
| + w.rec = p.rec |
| + } |
| + } |
| + w.runStalled() |
| + for _, a := range actors { |
| + a() |
| + } |
| + w.checkStep() |
| +} |
| + |
| +// drive ticks until done, a violation, or max steps. |
| +func (w *world) drive(max int, done func() bool, actors ...func()) bool { |
| + for i := 0; i < max; i++ { |
| + if done() { |
| + return true |
| + } |
| + w.tick(actors...) |
| + if len(w.violations) > 0 { |
| + return false |
| + } |
| + } |
| + return done() |
| +} |
| + |
| +// reach drives to a milestone the scenario needs. Not reaching it, with no |
| +// violation to explain why, is a liveness failure and is recorded as one |
| +// (INV-3), so a mutation that leaves the protocol stuck counts as caught |
| +// and an unmutated scenario that stalls fails the test. |
| +func (w *world) reach(t *testing.T, max int, what string, done func() bool, actors ...func()) bool { |
| + if w.drive(max, done, actors...) { |
| + w.logf("witness: reached %s", what) |
| + return true |
| + } |
| + if len(w.violations) == 0 { |
| + w.violate("INV-3 (witness): %s not reached within %d steps: %s", what, max, w.state()) |
| + } |
| + return false |
| +} |
| + |
| +// finish drives to quiescence and runs the final oracle, as runSeed does. |
| +func (w *world) finish(t *testing.T) { |
| + w.drive(2000, w.quiescent, w.actAll(), w.runConsole, w.recoveryPass, w.operator) |
| + if len(w.violations) > 0 { |
| + return |
| + } |
| + w.completeDue(true) |
| + w.final() |
| +} |
| + |
| +func (w *world) act(bs ...*box) func() { |
| + return func() { |
| + for _, b := range bs { |
| + w.worker(b) |
| + w.obligationRunner(b) |
| + w.reconcile(b) |
| + } |
| + } |
| +} |
| + |
| +// actAll runs every live box, replacements included. |
| +func (w *world) actAll() func() { |
| + return func() { |
| + for _, b := range w.liveBoxes() { |
| + w.worker(b) |
| + w.obligationRunner(b) |
| + w.reconcile(b) |
| + } |
| + } |
| +} |
| + |
| +// runConsole runs one step of every console plan, in order: a |
| +// deterministic consoleStep. |
| +func (w *world) runConsole() { |
| + var keep []*consolePlan |
| + for _, p := range w.console { |
| + if p.Stall > w.now || !w.runPlan(p) { |
| + keep = append(keep, p) |
| + } |
| + } |
| + w.console = keep |
| +} |
| + |
| +// stop is the cloud stopping a box: destroyed, nothing on it runs. |
| +func (w *world) stop(b *box) { |
| + b.Destroyed, b.Procs = true, nil |
| + w.logf("witness: box %d stopped", b.ID) |
| +} |
| + |
| +// appWrite is one acknowledged application write by b's main process. |
| +func (w *world) appWrite(b *box) int { |
| + if !hasMain(b) { |
| + panic("appWrite: no main process") |
| + } |
| + p := b.Procs[0] |
| + w.nextW++ |
| + wr := w.nextW |
| + if b.DB != nil && b.DB.Inc == p.Inc { |
| + b.DB.Writes = append(b.DB.Writes, wr) |
| + } |
| + w.acks = append(w.acks, ack{W: wr, Inc: p.Inc, Box: b.ID, At: w.now, Kind: "write"}) |
| + w.writeInc[wr] = p.Inc |
| + w.logf("witness: box %d wrote %d", b.ID, wr) |
| + return wr |
| +} |
| + |
| +// holdKey makes the witness hold every request for key until completeHeld. |
| +func (w *world) holdKey(key string) { |
| + w.hold = func(r *request) bool { return r.key == key } |
| +} |
| + |
| +// completeHeld completes the requests the witness held for key, now. |
| +func (w *world) completeHeld(key string) int { |
| + n := 0 |
| + var keep []*request |
| + for _, r := range w.pending { |
| + if r.key == key && r.doneAt == 1<<30 { |
| + w.complete(r) |
| + w.logf("witness: held %v %s r%d completes now", r.kind, r.key, r.region) |
| + n++ |
| + continue |
| + } |
| + keep = append(keep, r) |
| + } |
| + w.pending = keep |
| + return n |
| +} |
| + |
| +func (w *world) oblOpen(region int, prefix string) bool { |
| + if w.claim == nil { |
| + return false |
| + } |
| + for _, o := range w.claim.Obl { |
| + if o.Region == region && o.Prefix == prefix { |
| + return true |
| + } |
| + } |
| + return false |
| +} |
| + |
| +// landProbed drives a move of the serving host to tgt until the landing's |
| +// probe has passed and the instance runs on tgt, before the settle window |
| +// ends. |
| +func (w *world) landProbed(t *testing.T, src, tgt *box) { |
| + w.moveTo(tgt.Region) |
| + if w.claim.Op.Kind != "moving" { |
| + t.Fatalf("witness: move not started: %s", w.state()) |
| + } |
| + w.reach(t, 600, "landing probed", func() bool { |
| + c := w.claim |
| + return c.Op.Kind == "landing" && c.Op.LandPhase == "probed" && hasMain(tgt) |
| + }, w.act(src, tgt), w.recoveryPass) |
| +} |
| + |
| +// ---------- the scenarios ---------- |
| + |
| +// wGenerationConditional (model 29, §5.1): push p1's first generation.json |
| +// PUT is accepted but its response is lost; the agent publishes again and |
| +// p1 completes. Push p2 completes. Then the stale PUT lands. Conditional on |
| +// the marker it superseded, it is refused (412); unconditional, the marker |
| +// names p1 while the claim names p2, and the serving box cannot start. |
| +func wGenerationConditional(t *testing.T, w *world) { |
| + e := w.boxes[0] |
| + w.serve(e, 1, app0) |
| + loc := w.claim.Holder.Location |
| + push := func(holdMarker bool) { |
| + w.userPush() |
| + id := w.claim.Op.ID |
| + if !w.reach(t, 400, "push "+id+" published", func() bool { return w.claim.Op.ID == id && w.claim.Op.Phase == "published" }, w.act(e)) { |
| + return |
| + } |
| + if holdMarker { |
| + w.holdKey(genMarkerKey(loc)) |
| + w.tick(w.act(e)) // the first publication: accepted, response lost |
| + w.hold = nil |
| + } |
| + w.reach(t, 400, "push "+id+" released", func() bool { return w.claim.Op.Kind == "serving" }, w.act(e)) |
| + w.idleStop(e) |
| + } |
| + push(true) |
| + push(false) |
| + if len(w.violations) > 0 { |
| + return |
| + } |
| + if w.completeHeld(genMarkerKey(loc)) != 1 { |
| + t.Fatalf("witness: no held marker PUT") |
| + } |
| + w.finish(t) |
| +} |
| + |
| +// wLostReturnPark (model 27, §7.10). |
| +func wLostReturnPark(t *testing.T, w *world) { |
| + src, tgt := w.boxes[0], w.boxes[1] |
| + w.serve(src, 1, app0) |
| + w.landProbed(t, src, tgt) |
| + w.appWrite(tgt) // real work in the settle window |
| + w.rollback(w.claim, "settle check failed") |
| + w.reach(t, 50, "target released dirty", func() bool { |
| + c := w.claim |
| + return c.Op.Kind == "restoring" && c.Op.Phase == "released" && c.Op.Dirty |
| + }, w.act(src, tgt), w.recoveryPass) |
| + w.tick(w.act(tgt)) // the first return PUT: moves/<host>/<rb>/db in the source region |
| + if w.claim.Op.ReturnDB.Ver == 0 { |
| + t.Fatalf("witness: the return did not begin: %s", w.state()) |
| + } |
| + w.stop(tgt) // the cloud stops the target mid-return |
| + w.reach(t, 20, "declared lost", func() bool { return contains(w.claim.Lost, tgt.ID) }, w.operator) |
| + w.replaceDestroyed() |
| + w.finish(t) |
| +} |
| + |
| +// wDeclareLostCompute (model 5, §7.10): the target is frozen (a whole-VM |
| +// pause) in its settle window; its execution lease expires. |
| +func wDeclareLostCompute(t *testing.T, w *world) { |
| + src, tgt := w.boxes[0], w.boxes[1] |
| + w.serve(src, 1, app0) |
| + w.landProbed(t, src, tgt) |
| + tgt.Frozen = true |
| + exp := w.execLease[tgt.ID].Expires |
| + w.reach(t, 100, "lease expired", func() bool { return w.now > exp+lostMargin }, w.act(src), w.recoveryPass) |
| + // the operator: refused with compute fencing (the box is not stopped); |
| + // on expiry alone, the rollback and the loss go through and the source |
| + // recovers |
| + w.drive(100, func() bool { return hasMain(src) }, w.act(src), w.recoveryPass, w.operator) |
| + tgt.Frozen = false // the VM resumes: its application runs before its agent does |
| + w.tick() |
| + w.finish(t) |
| +} |
| + |
| +// wWatchdogIndependent (§7.1): as wDeclareLostCompute, with the agent |
| +// alone paused, so the application keeps running and only a watchdog |
| +// outside the agent can fence it. |
| +func wWatchdogIndependent(t *testing.T, w *world) { |
| + src, tgt := w.boxes[0], w.boxes[1] |
| + w.serve(src, 1, app0) |
| + w.landProbed(t, src, tgt) |
| + tgt.AgentPaused = true |
| + exp := w.execLease[tgt.ID].Expires |
| + dog := func() { w.watchdog(tgt) } |
| + w.reach(t, 100, "lease expired", func() bool { return w.now > exp+lostMargin }, w.act(src), w.recoveryPass, dog) |
| + w.drive(100, func() bool { return hasMain(src) }, w.act(src), w.recoveryPass, w.operator, dog) |
| + tgt.AgentPaused = false |
| + w.finish(t) |
| +} |
| + |
| +// wLostQuarantine (claim §7.2, CC12): the target is stopped while landing, |
| +// declared lost, and later started again with its old disk. |
| +func wLostQuarantine(t *testing.T, w *world) { |
| + src, tgt := w.boxes[0], w.boxes[1] |
| + w.serve(src, 1, app0) |
| + w.moveTo(tgt.Region) |
| + w.reach(t, 600, "landing installed", func() bool { |
| + c := w.claim |
| + return c.Op.Kind == "landing" && c.Op.LandPhase == "probing" |
| + }, w.act(src, tgt), w.recoveryPass) |
| + w.stop(tgt) |
| + w.reach(t, 60, "declared lost", func() bool { return contains(w.claim.Lost, tgt.ID) }, w.act(src), w.recoveryPass, w.operator) |
| + tgt.Destroyed = false // started again, with its old disk |
| + tgt.forget() |
| + w.logf("witness: box %d started again", tgt.ID) |
| + w.finish(t) |
| +} |
| + |
| +// wMarkersLast (R2-6): the source has a registered timer; the target's |
| +// agent crashes between extracting the files and writing the marker. |
| +func wMarkersLast(t *testing.T, w *world) { |
| + src, tgt := w.boxes[0], w.boxes[1] |
| + w.serve(src, 1, app0) |
| + w.nextW++ |
| + src.Timers = []int{w.nextW} |
| + w.acks = append(w.acks, ack{W: w.nextW, Inc: 1, Box: src.ID, At: w.now, Kind: "timer"}) |
| + w.moveTo(tgt.Region) |
| + id := w.claim.Op.ID |
| + w.reach(t, 600, "files extracted", func() bool { return tgt.Files != nil && tgt.Files.Gen == id }, w.act(src, tgt), w.recoveryPass) |
| + tgt.Procs = nil |
| + tgt.forget() // the agent crashes and restarts: its memory, the pending timers included, is gone |
| + w.logf("witness: box %d agent crashed between the extraction and the marker", tgt.ID) |
| + w.finish(t) |
| +} |
| + |
| +// wRollbackJournal (R2-3): a dirty rollback; the source's agent restarts |
| +// after its probe spawned the instance, which wrote and replicated. |
| +func wRollbackJournal(t *testing.T, w *world) { |
| + src, tgt := w.boxes[0], w.boxes[1] |
| + w.serve(src, 1, app0) |
| + w.landProbed(t, src, tgt) |
| + w.appWrite(tgt) |
| + w.rollback(w.claim, "settle check failed") |
| + w.reach(t, 2000, "source probed on the return", func() bool { |
| + c := w.claim |
| + return c.Op.Kind == "restoring" && c.Op.SrcPhase == "probed" && hasMain(src) |
| + }, w.act(src, tgt), w.recoveryPass) |
| + w.appWrite(src) |
| + w.replicate(src) // into the return generation: durable there |
| + src.Procs = nil |
| + src.forget() // the agent crashes and restarts |
| + w.logf("witness: box %d agent crashed during the rollback's probe", src.ID) |
| + w.finish(t) |
| +} |
| + |
| +// heldRound drives a move to its first staging round and holds that |
| +// round's db PUT. It returns the staging key. |
| +func (w *world) heldRound(t *testing.T, src, tgt *box) string { |
| + w.moveTo(tgt.Region) |
| + id := w.claim.Op.ID |
| + key := fmt.Sprintf("moves/%s/%s/db", host, id) |
| + w.reach(t, 100, "staging begins", func() bool { |
| + c := w.claim |
| + return c.Op.Phase == "preparing" && contains(c.Regions, tgt.Region) |
| + }, w.act(src, tgt)) |
| + w.holdKey(key) |
| + w.tick(w.act(src)) // this round's db PUT is accepted and completes late |
| + w.hold = nil |
| + return key |
| +} |
| + |
| +// wSealByVersion (J-N2): the held round completes after the seal, so the |
| +// staging key's current version is older than the sealed one. |
| +func wSealByVersion(t *testing.T, w *world) { |
| + src, tgt := w.boxes[0], w.boxes[1] |
| + w.serve(src, 1, app0) |
| + key := w.heldRound(t, src, tgt) |
| + w.wake(src) // the source serves during the move |
| + if !hasMain(src) { |
| + t.Fatalf("witness: source did not wake: %s", w.state()) |
| + } |
| + w.appWrite(src) |
| + w.replicate(src) |
| + w.reach(t, 600, "sealed", func() bool { return w.claim.Op.Phase == "sealed" || w.claim.Op.Kind == "landing" }, w.act(src, tgt), w.recoveryPass) |
| + w.completeHeld(key) |
| + w.finish(t) |
| +} |
| + |
| +// wStagingQuiet (J-N2): the held round completes after the commit, once |
| +// the landing's staging park has acknowledged (if it retired at the seal |
| +// time) and before the release. |
| +func wStagingQuiet(t *testing.T, w *world) { |
| + src, tgt := w.boxes[0], w.boxes[1] |
| + w.serve(src, 1, app0) |
| + key := w.heldRound(t, src, tgt) |
| + prefix := key[:strings.LastIndex(key, "/")+1] |
| + w.reach(t, 600, "committed", func() bool { return w.claim.Op.Committed }, w.act(src, tgt), w.recoveryPass) |
| + w.drive(30, func() bool { return !w.oblOpen(tgt.Region, prefix) }, w.act(src, tgt), w.recoveryPass) |
| + w.completeHeld(key) |
| + w.finish(t) |
| +} |
| + |
| +// wClaimCasOpID (claim C2): a clean rollback; a second goroutine of the |
| +// source read the claim just before the release and stalls; the host is |
| +// released, a purge claims it, and the goroutine resumes. |
| +func wClaimCasOpID(t *testing.T, w *world) { |
| + src, tgt := w.boxes[0], w.boxes[1] |
| + w.serve(src, 1, app0) |
| + w.landProbed(t, src, tgt) |
| + w.rollback(w.claim, "cut deadline") |
| + w.reach(t, 1500, "source about to release", func() bool { |
| + c := w.claim |
| + return c.Op.Kind == "restoring" && c.Op.SrcPhase == "opened" && c.oblFor(c.Op.ID) == 0 |
| + }, w.act(src, tgt), w.recoveryPass) |
| + old := w.claim.clone() // the stalled goroutine's read |
| + w.reach(t, 50, "released", func() bool { return w.claim.Op.Kind == "serving" }, w.act(src, tgt), w.recoveryPass) |
| + pg := &consolePlan{Kind: "purge", App: app0} |
| + w.reach(t, 20, "purge claimed the host", func() bool { return w.claim.Op.Kind == "purging" }, func() { w.runPlan(pg) }) |
| + w.resumeStale(src, old) // the goroutine wakes with the rollback's last read |
| + w.tick() |
| + w.tick(func() { w.runPlan(pg) }) // the purge tears the store down |
| + w.tick(func() { w.runPlan(pg) }) |
| +} |
| + |
| +// wDirtyReturn (INV-2; also commit-before-open's witness): the target |
| +// writes during its probe and is rolled back. |
| +func wDirtyReturn(t *testing.T, w *world) { |
| + src, tgt := w.boxes[0], w.boxes[1] |
| + w.serve(src, 1, app0) |
| + w.landProbed(t, src, tgt) |
| + w.appWrite(tgt) |
| + w.rollback(w.claim, "settle check failed") |
| + w.finish(t) |
| +} |
| + |
| +// wAdmissionTriple (J2-R2-8): an open from an earlier operation paused on |
| +// the source; it lands after the commit, while the source's row is still |
| +// held and before its park-local has run. |
| +func wAdmissionTriple(t *testing.T, w *world) { |
| + src, tgt := w.boxes[0], w.boxes[1] |
| + w.serve(src, 1, app0) |
| + d := &localWrite{kind: "open", holdOp: "p0", epoch: src.Epoch, at: 1 << 30} |
| + src.deferred = append(src.deferred, d) |
| + w.moveTo(tgt.Region) |
| + w.reach(t, 600, "committed", func() bool { return w.claim.Op.Committed }, func() { w.worker(src); w.worker(tgt) }, w.recoveryPass) |
| + d.at = w.now // the paused open lands now |
| + w.tick() |
| + w.wake(src) // a request reaches the old source |
| + w.checkStep() |
| + w.finish(t) |
| +} |
| + |
| +// wStrictSpawn (§6.1): the source runs a main process and a descendant |
| +// placed as its parent was. |
| +func wStrictSpawn(t *testing.T, w *world) { |
| + src, tgt := w.boxes[0], w.boxes[1] |
| + w.serve(src, 1, app0) |
| + w.wake(src) |
| + if !hasMain(src) { |
| + t.Fatalf("witness: source did not wake: %s", w.state()) |
| + } |
| + main := src.Procs[0] |
| + src.Procs = append(src.Procs, &proc{Main: false, Strict: main.Strict, Inc: 1, Box: src.ID}) |
| + w.moveTo(tgt.Region) |
| + w.finish(t) |
| +} |
| + |
| +// wTouchedIncomplete (claim §9, CC4): a legacy host with a pre-release |
| +// replica in another region is adopted, then deleted. |
| +func wTouchedIncomplete(t *testing.T, w *world) { |
| + b0 := w.boxes[0] |
| + w.legacy(b0, 1) |
| + w.tick(func() { w.reconcile(b0) }) // adoption |
| + if w.claim == nil { |
| + t.Fatalf("witness: not adopted") |
| + } |
| + w.reach(t, 400, "adoption settled", func() bool { return w.claim.oblFor("adopt") == 0 }, w.actAll(), w.recoveryPass) |
| + w.userDelete() |
| + w.finish(t) |
| +} |
| + |
| +// recreate deletes and frees the serving host, creates incarnation inc in |
| +// region r, and has it run and replicate. |
| +func (w *world) recreate(t *testing.T, r, inc int) { |
| + w.userDelete() |
| + w.reach(t, 600, "freed", func() bool { |
| + c := w.claim |
| + return c != nil && c.Holder == nil && c.Op.Kind == "" |
| + }, w.actAll(), w.runConsole, w.recoveryPass) |
| + w.console = append(w.console, &consolePlan{Kind: "create", Host: "h", App: app0, OpID: w.newID("cr"), Inc: inc, Region: r}) |
| + b := w.regionBox(r) |
| + w.reach(t, 200, "recreated", func() bool { |
| + c := w.claim |
| + return c.Holder != nil && c.Holder.Inc == inc && c.Op.Kind == "serving" && b.Row != nil |
| + }, w.runConsole, w.actAll(), w.recoveryPass) |
| + b.Config, b.CfgVer, b.Live, b.LiveInc = inc, w.cfgVer[app0], app0, inc // config sync and adoption have run |
| + w.reach(t, 200, "new incarnation running", func() bool { return hasMain(b) }, func() { w.wake(b) }) |
| + w.appWrite(b) |
| + w.replicate(b) |
| +} |
| + |
| +// wDoorReread (claim §6.5 O2): a listing authorized before the delete |
| +// selects after the recreate. |
| +func wDoorReread(t *testing.T, w *world) { |
| + b0 := w.boxes[0] |
| + w.serve(b0, 1, app0) |
| + w.doorAuthorize() // O1 |
| + w.recreate(t, 0, 2) |
| + w.doorOpen() // select and O2 |
| + w.doorOpen() // open |
| +} |
| + |
| +// wDoorByVersion (claim §6.5): a listing selects and signs before the |
| +// delete, and the file request opens after the recreate. |
| +func wDoorByVersion(t *testing.T, w *world) { |
| + b0 := w.boxes[0] |
| + w.serve(b0, 1, app0) |
| + w.doorAuthorize() // O1 |
| + w.tick() |
| + w.tick() |
| + w.doorOpen() // select, O2, sign |
| + if len(w.doorReads) != 1 || !w.doorReads[0].Signed { |
| + t.Fatalf("witness: listing not signed") |
| + } |
| + w.recreate(t, 0, 2) |
| + w.doorOpen() // open |
| +} |
| + |
| +// wRegistrationCheck (CC21, claim §5.3): the first create of a host |
| +// registers and its console pauses; a purge of the app drains the expired |
| +// registration, tears the store down and finishes; the creator resumes. |
| +func wRegistrationCheck(t *testing.T, w *world) { |
| + p := &consolePlan{Kind: "create", Host: "h", App: app0, OpID: w.newID("cr"), Inc: 1, Region: 0} |
| + w.runPlan(p) // registered; the claim is absent |
| + for i := 0; i < 61; i++ { |
| + w.tick() |
| + } |
| + pg := &consolePlan{Kind: "purge", App: app0} |
| + done := false |
| + w.reach(t, 30, "purge done", func() bool { return done }, func() { |
| + if w.runPlan(pg) { |
| + done = true |
| + } |
| + }) |
| + for i := 0; i < 6; i++ { |
| + w.tick(func() { w.runPlan(p) }) // the creator resumes |
| + } |
| +} |
amadan