| 1 | package hostlife |
| 2 | |
| 3 | import ( |
| 4 | "fmt" |
| 5 | "os" |
| 6 | "strings" |
| 7 | "testing" |
| 8 | ) |
| 9 | |
| 10 | // Witness scenarios (moves spec §14.2, rev 7.3). |
| 11 | // |
| 12 | // The random sweep reaches some interleavings rarely, and every new biased |
| 13 | // schedule reshuffles every seed, so a rare rule's catch can vanish from |
| 14 | // one revision to the next (lost-return-park in rev 7.1, |
| 15 | // generation-conditional in rev 7.2). A witness is one fixed, hand-scheduled |
| 16 | // scenario for one rule: it forces exactly the interleaving the rule |
| 17 | // exists for, as a sequence of protocol steps the witness chooses, with a |
| 18 | // quiet RNG that injects nothing. It must hold (no invariant violated) with |
| 19 | // the rules in place, and violate an invariant when the rule's mutation is |
| 20 | // applied, alone or in the stated combination. |
| 21 | // |
| 22 | // Witnesses never draw from a seed's RNG and never run inside the sweep's |
| 23 | // seeds, so adding one reshuffles nothing. They are the deterministic half |
| 24 | // of the mutation evidence; mutate.sh runs TestWitnesses beside the sweep |
| 25 | // and reports both. |
| 26 | |
| 27 | // quiet is the witness's RNG: every draw takes the branch that injects |
| 28 | // nothing (no fault, no stall, no duplicate, no late completion, no |
| 29 | // second process), so a scenario is exactly the steps the witness scripts. |
| 30 | type quiet struct{} |
| 31 | |
| 32 | func (quiet) Intn(n int) int { |
| 33 | if n <= 1 { |
| 34 | return 0 |
| 35 | } |
| 36 | return 1 |
| 37 | } |
| 38 | |
| 39 | type witness struct { |
| 40 | rule string // the rule it is for |
| 41 | needs string // the mutation set under which it must violate: the rule alone, or a combination the rule belongs to |
| 42 | want string // the failure the scenario names: a substring of the first violation (R3 review) |
| 43 | note string // what it shows |
| 44 | run func(t *testing.T, w *world) |
| 45 | } |
| 46 | |
| 47 | var witnesses = []witness{ |
| 48 | {"generation-conditional", "generation-conditional", "cannot start the host", |
| 49 | "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}, |
| 50 | {"fence-converts-moving", "fence-converts-moving", "INV-3", |
| 51 | "the source of a pre-flip move is terminated in a one-box region; the fence converts the move to relocating at pinning with exec none and the lane's park owed, the operator is alerted once, nothing loops while no box exists, and the relocation completes on the replacement box region HA enrolls; without the rule the move never converges", wFenceConvertsMoving}, |
| 52 | {"lost-return-park", "lost-return-park", "ended with residue", |
| 53 | "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}, |
| 54 | {"declare-lost-compute", "declare-lost-compute", "INV-1", |
| 55 | "a frozen target's lease expires; declared lost on expiry alone, it resumes beside the recovered source (INV-1)", wDeclareLostCompute}, |
| 56 | {"watchdog-independent", "declare-lost-compute,watchdog-independent", "INV-1", |
| 57 | "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}, |
| 58 | {"lost-quarantine", "lost-quarantine", "holds local state", |
| 59 | "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}, |
| 60 | {"markers-last", "markers-last", "acknowledged timer", |
| 61 | "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}, |
| 62 | {"rollback-journal", "rollback-journal", "cold restore", |
| 63 | "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}, |
| 64 | {"seal-by-version", "seal-by-version", "cold restore", |
| 65 | "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}, |
| 66 | {"staging-quiet", "staging-quiet", "ended with residue", |
| 67 | "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}, |
| 68 | {"claim-cas-opid", "claim-cas-opid,revalidate-before-effect", "store of app", |
| 69 | "redundant alone: the source closes the rollback's record and stalls before its release (rev 7.23, record first); the recovery pass releases from last_move, a purge claims the host, and the stalled goroutine resumes into its release with the rollback's last read; 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}, |
| 70 | {"dirty-return", "dirty-return", "INV-2", |
| 71 | "the target writes during its probe and replicates; the rollback is dirty and the return lane carries the write to the source; treated as clean with the source's replica covering the stop, the source's admission is covered clean-return, declares nothing, and the serving database lacks the target's write (INV-2 local at the final recovery, rev 7.12; rev 7.11 saw INV-15 at the declaration, rev 7.10 INV-2 on the serving database)", wDirtyReturn}, |
| 72 | {"commit-before-open", "commit-before-open", "INV-5", |
| 73 | "a public request reaches the target's edge while its probe runs; a row opened at the probe routes it before the commit (INV-5, R3-5)", wCommitBeforeOpen}, |
| 74 | {"exec-admission", "exec-admission,hold-op-open,start-check-claim-gen,exec-writer", "INV-1", |
| 75 | "one of four admission fences (J2-R2-8, claim rev 6.8.1): 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, AdmitWriter refuses a box that is not op.exec; with all four gone the source's wake is a cold admission by a non-exec box into a fresh generation restored from its own region's old files, and it serves beside the target (INV-1; its installing CAS also moves holder.stamp under the target, INV-6 a step later)", wAdmissionTriple}, |
| 76 | {"hold-op-open", "exec-admission,hold-op-open,start-check-claim-gen,exec-writer", "INV-1", "one of four admission fences (see exec-admission)", wAdmissionTriple}, |
| 77 | {"start-check-claim-gen", "exec-admission,hold-op-open,start-check-claim-gen,exec-writer", "INV-1", "one of four admission fences (see exec-admission)", wAdmissionTriple}, |
| 78 | {"exec-writer", "exec-admission,hold-op-open,start-check-claim-gen,exec-writer", "INV-1", |
| 79 | "a paused open from an earlier operation lands after the commit while the source's row is still held; the source's AdmitWriter CAS requires op.exec to be the source, which it no longer is, and refuses (claim rev 6.8.1); with the three box-side fences gone as well, the non-exec source is admitted cold and two boxes run the host (INV-1)", wAdmissionTriple}, |
| 80 | {"strict-spawn", "strict-spawn,evidence-whole-tree", "INV-1", |
| 81 | "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}, |
| 82 | {"touched-incomplete", "touched-incomplete,legacy-discovery", "freed with residue", |
| 83 | "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}, |
| 84 | {"registration-check", "registration-check,fence-etag", "store of app", |
| 85 | "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}, |
| 86 | {"registration-check", "registration-check,purge-claim-fence", "store of app", |
| 87 | "the same, with the fence gone instead", wRegistrationCheck}, |
| 88 | // rev 7.4 |
| 89 | {"fence-by-installation", "fence-by-installation", "refused by the box's own installation record", |
| 90 | "a round trip UK→US→UK (R3-3): the second landing replaces the retired marker UK wrote after the first move; a marker for the whole incarnation refuses the probe, the move back rolls back, and the instance never serves on UK again", wRoundTrip}, |
| 91 | {"orphan-order", "orphan-order", "orphan cleanup deleted the record", |
| 92 | "the cleanup reads the claim first and pauses; a create removes the orphan, claims and publishes; the cleanup reads that record, judges it by the stale claim and deletes it (R3-2)", wOrphanOrder}, |
| 93 | {"sweep-namespace", "sweep-namespace", "residue never retired", |
| 94 | "a replication PUT of incarnation 1 completes after 33 recreates dropped it from retired_incarnations; a sweep reading that list never finds it (R3-4)", wSweepNamespace}, |
| 95 | {"recovery-current-inputs", "recovery-current-inputs", "stuck: source could not recover", |
| 96 | "a bundle is published after admission and the target writes; the dirty recovery renders current inputs; gated on move.inputs it never passes its probe (R2-5, §7.8)", wRecoveryInputs}, |
| 97 | // rev 7.5 |
| 98 | {"fence-stamp", "fence-stamp,hostguard", "INV-6", |
| 99 | "a config pass selected under the first installation pauses across a retire-and-reinstall (UK→US→UK) and a bundle change; the host guard's fresh check refuses its stale bundle, the stamp refuses its retired installation; with both gone it writes host state for a retired installation (R4-2)", wStaleWriter}, |
| 100 | {"live-set-region", "live-set-region", "residue never retired", |
| 101 | "a legacy host serving in UK with an earlier replica in US; discovery parks US; an old US replication PUT lands after; the live set is region-qualified, so the US sweep parks it; exempted by key alone it stays for good (R4-3)", wLiveSetRegion}, |
| 102 | {"restore-overlap", "restore-overlap", "INV-3", |
| 103 | "a generation's snapshot ends at TXID 11 and the only continuation is a compacted file [10,15]; litestream's planner takes it and restores through 15; rev 7.4's rule (min == current+1) discards it, the restore stops short of the certificate's max_txid, and the box never starts again (R4-1; since rev 7.10 the certified position is checked before the start, where rev 7.4's rule lost four acknowledged writes)", wRestoreOverlap}, |
| 104 | {"restore-gap-closed", "restore-gap-closed", "INV-2 (cold restore)", |
| 105 | "a generation's snapshot ends at TXID n, the file [n+1,n+1] is missing and [n+2,n+2] is current: a genuine gap; the restore refuses; returning what it has would wake the host without durable transactions (R4-1)", wRestoreGap}, |
| 106 | // rev 7.6 |
| 107 | {"restore-anchor", "restore-anchor", "INV-2", |
| 108 | "a snapshot-only install (a push), then writes and replication, then the disk is lost: without the level-0 anchor litestream's position restarts at 1, the new files sit below the snapshot, and the cold restore loses the writes (R5-1; litestreamfacts TestFact_R5_1_*)", wSnapshotOnlyInstall}, |
| 109 | {"root-advance", "root-advance", "INV-3 (witness): woken cold", |
| 110 | "after a push, four compaction-and-snapshot rotations with retention; the disk is lost; a restore rooted at the pinned snapshot finds its continuation expired and refuses, while one rooted at the newest current successor snapshot succeeds (R5-3; litestreamfacts TestFact_R5_3_SnapshotRetention)", wRootAdvance}, |
| 111 | // rev 7.7 |
| 112 | {"anchor-acked", "anchor-acked", "before its anchor", |
| 113 | "a push installs a snapshot alone and its anchor PUT is slow; litestream reads its position from the remote level-0 listing, so the host must not open replication until the anchor is acknowledged; opened at once it runs from TXID 1 below the snapshot and a cold restore loses the writes (R6-1)", wAnchorHeld}, |
| 114 | {"return-stamp", "return-stamp", "issued for box", |
| 115 | "a dirty rollback whose source lost its local stamp record; the return CAS writes the source installation's stamp back and the source re-initializes from it; left as the target's stamp, the source activates an installation that was never its own (claim rev 6.5, R6-4)", wReturnLostRecord}, |
| 116 | // rev 7.8 |
| 117 | {"recovery-generation", "recovery-generation", "INV-2", |
| 118 | "writer A's level-0 upload [N+1] is in flight when A dies with its disk; B recovers cold into a fresh generation and replicates its own [N+1]; A's upload lands after B's; in the same generation it would replace B's file and the next cold restore loses B's acknowledged write (R7-1, completion order A after B)", wLateUploadAfter}, |
| 119 | {"recovery-generation", "recovery-generation", "INV-2", |
| 120 | "as above, but A's upload lands after B initialized its position and before B's own upload; in the same generation litestream's upload loop takes the remote [N+1] as already uploaded and skips B's, which is then lost (R7-1, the initialization/remote-position race)", wLateUploadRace}, |
| 121 | {"recovery-generation", "recovery-generation", "INV-2", |
| 122 | "A's in-flight write updated K and was declared lost with A's disk; B durably updates K; A's stale upload lands and restores K's old value; coverage by write identity sees B's write missing where a TXID bound and a per-key mask did not (R7-2)", wExemptKeyRestored}, |
| 123 | {"recovery-generation", "recovery-generation", "no cold recovery", |
| 124 | "a clean stop whose uploads all returned, then a crash before closed.json was written: no marker, so the next wake is a cold recovery into a fresh generation (claim rev 6.6 §6.4a)", wCrashBeforeMarker}, |
| 125 | {"closed-marker", "closed-marker", "INV-2", |
| 126 | "a stale closed.json (max_txid behind the remote maximum) beside a dead writer's in-flight upload; the stale marker forces a cold recovery; taken as intact, the box continues in place and the late upload replaces its file (claim rev 6.6 §6.4a, R7-1)", wStaleMarker}, |
| 127 | {"close-waits", "close-waits", "before every upload returned", |
| 128 | "a clean stop with an upload still in flight: closed.json is written only once the upload returned; written at once, the marker vouches for an upload that may still fail or land late (claim rev 6.6 §6.4a)", wCloseWaits}, |
| 129 | {"newest-l0", "newest-l0", "newest level-0", |
| 130 | "the local position runs ahead of the uploads; two compactions and snapshot rotations later, retention below the previous snapshot would remove the newest uploaded level-0 file, which litestream never does (R7-3)", wNewestL0}, |
| 131 | {"evidence-whole-tree", "evidence-whole-tree", "INV-1", |
| 132 | "an adopted legacy host runs a descendant outside the cgroup; the move's stop evidence must cover the whole tree, or the escaped descendant survives the cut and two boxes run the host (§6.1, J-D3)", wEvidenceWholeTree}, |
| 133 | {"timer-freeze", "timer-freeze", "stuck", |
| 134 | "the source has a registered timer; the move stops and holds it; the runner's refused deliveries while held must not advance its bookkeeping, or a clean rollback's digest check finds the timers changed and the source is stuck (J-N14)", wTimerFreeze}, |
| 135 | // rev 7.9 |
| 136 | {"writer-session", "writer-session", "INV-2", |
| 137 | "a dead session's certificate, with a max_txid that still matches the remote maximum because the next writer's upload is in flight: the session moved forward when that writer was admitted, so the certificate authorizes nothing; taken by stamp and TXID alone it readmits a writer into the generation and the late upload replaces that writer's file (claim rev 6.8 §6.4a, R8-1)", wDeadSessionCertificate}, |
| 138 | {"admit-everywhere", "admit-everywhere", "INV-2", |
| 139 | "a committed move's target serves while the claim is still landing; it dies with its disk and an upload in flight; the next wake must be an AdmitWriter within the landing, a cold one into a fresh generation; gated for ordinary wakes only, the target continues the generation and the late upload replaces its file (claim rev 6.8 §6.4a, R8-2)", wCommittedLandingCrash}, |
| 140 | {"admit-everywhere", "admit-everywhere", "INV-2", |
| 141 | "a landing's probe dies with its disk and an upload in flight; the restarted probe must be a cold AdmitWriter within the landing, into a fresh install generation; gated for ordinary wakes only, the restarted probe reuses the generation and the late upload replaces its file (R8-2)", wProbeRestart}, |
| 142 | {"valid-ltx", "valid-ltx", "INV-12", |
| 143 | "a created incarnation's first wake is a cold admission into an empty generation with no LTX file, and a move of the still-empty incarnation installs nothing at position 0; the mutation installs a snapshot [1,0] and an anchor [0,0], files the pinned encoder refuses (R8-3)", wEmptyBootstrap}, |
| 144 | // rev 7.10 |
| 145 | {"remote-baseline", "remote-baseline", "INV-2", |
| 146 | "a session closes cleanly through N+1 and its certificate stands; the box's local database is a cached copy through N (R9-1's clean-close variant); the next wake must purge it and restore the certified remote; keeping it serves a database without an acknowledged write, and its own upload for N+1 is skipped at the remote position (claim rev 6.9)", wStaleLocalAfterClose}, |
| 147 | {"writes-lost", "writes-lost", "INV-2", |
| 148 | "a writer acknowledges a write and crashes before uploading it; the next wake is cold and restores the remote, which lacks the write: the admission must record writes_lost {box, generation, session, remote_max_txid} and alert; silently, the serving database differs from the acknowledged writes (claim rev 6.9, R9-2)", wSilentLoss}, |
| 149 | {"admit-bind-op", "admit-bind-op,claim-cas-opid", "INV-13", |
| 150 | "a wake's admission closure is computed under serving (op.id \"\"); a delete begins, preserving session, generation and executor; the stale closure resumes: bound to the observed op.id, phase and kind it is refused; the model's general CAS condition on op.id (C2, claim-cas-opid) refuses it too, so the two must go together for a writer to be admitted into a host being deleted (claim rev 6.9, R9-4)", wStaleClosureDelete}, |
| 151 | // rev 7.11 |
| 152 | {"admit-before-start", "admit-before-start", "INV-2", |
| 153 | "a background worker acknowledges a write right after the app starts, and the box crashes before replication opens; admitted before the start, the acknowledgement is the session's and the next cold admission declares it; admitted after readiness (rev 7.10's order), it is in a database the next warm admission purges silently (claim rev 6.10, R10-1)", wAckBeforeAdmission}, |
| 154 | {"baseline-live", "baseline-live", "INV-2", |
| 155 | "a cold admission into a fresh generation; the box crashes before the first upload, so the generation is empty and the marker names the predecessor; the predecessor is the unfinished admission's baseline and stays live until the marker names the new generation; with the retire chore queued at the CAS, the predecessor is parked and the recovery restores nothing (claim rev 6.10, R10-2)", wBaselineParked}, |
| 156 | {"clean-return-identity", "clean-return-identity", "INV-16", |
| 157 | "a move's target is probed and writes nothing; the rollback is clean and the seal recorded src_covered; the source's re-admission journals the target's writer as its predecessor and coverage clean-return, declaring nothing; the mutation journals the target's session and box with the source's generation, a writer that never was, and declares a loss (claim rev 6.12, R11-4)", wCleanReturnIdentity}, |
| 158 | {"absent-marker-origin", "absent-marker-origin", "INV-2", |
| 159 | "an adopted host's origin replica holds durable writes and no generation.json; a cold admission into a fresh generation crashes before its first upload; the ordinary serving-time sweep runs before the recovery; with the absent marker read as the origin the chain protects it, and under the mutation (rev 7.11's sweep, which read absence as agreement) the sweep parks the origin and the recovery restores nothing (R11-1; isolated from baseline-live in rev 7.13, R12 evidence)", wOriginSwept}, |
| 160 | {"session-scoped-loss", "session-scoped-loss", "INV-18", |
| 161 | "two writer sessions of one box each acknowledged a write that never uploaded; a writes_lost record for the second session exempts only its own write; matched box-wide (rev 7.12), the record absolves the first session's undeclared write too (R12-1)", wTwoSessionDeclaration}, |
| 162 | {"foreign-region-uncovered", "foreign-region-uncovered", "INV-2", |
| 163 | "a landing's probe publishes the target's generation; the source's generation, in another region, stays uncovered with no chore; a chore queued into the source's region from here parks the rollback's baseline within the horizon, and the clean rollback's return restores an empty database (claim rev 6.14 item 5, R12-3)", wRollbackBaselinePreserved}, |
| 164 | {"cover-at-park", "cover-at-park", "INV-17", |
| 165 | "a committed move: the CAS that queues the source region's whole-location park covers the target's record, whose predecessor is the source's generation there; without CoverRegionPredecessors the record stays uncovered after the park retired its predecessor (claim rev 6.14 item 6, R12-3)", wCommitCoverage}, |
| 166 | {"cover-at-park", "cover-at-park", "INV-17", |
| 167 | "the commit is interrupted between the record's flip and the claim's CAS: every actor pauses past the horizon; whoever follows the record later performs the one CAS, parks and coverage together (R12-3, interruption)", wCommitInterrupted}, |
| 168 | {"cover-at-park", "cover-at-park", "INV-17", |
| 169 | "the commit's CAS is followed again by another reader: the replay is refused, the park is queued once and the coverage stands (R12-3, replay)", wCommitReplayed}, |
| 170 | {"persisted-park-scope", "persisted-park-scope", "INV-9", |
| 171 | "a committed move's source-region park binds its scope, the original evidence time, in the claim; the region's agent restarts mid-park; with the box-local evidence map (rev 7.13) the horizon starts again from the restart and the acknowledgement comes late (claim rev 6.15 §2, R13-4)", wParkScopeSurvivesRestart}, |
| 172 | {"persisted-park-scope", "persisted-park-scope", "INV-9", |
| 173 | "a committed move's staging lane sealed at the cut: its persisted bound is the seal's, deadline seal + lease + H; the target region's cleanup first runs 40 steps after that deadline and its agent restarts as it begins; the acknowledgement must follow at once, since the persisted deadline has passed; bound at cleanup's own clock (rev 7.15) the chore waits a fresh horizon (claim rev 6.23 §2, R15-1)", wStagingScopeDeadline}, |
| 174 | {"scope-membership", "scope-membership", "INV-23", |
| 175 | "incarnation 2 serves after incarnation 1 was deleted; a late object lands under instances/<host>/1/g-old/; the sweep must queue a chore scoped to instances/<host>/1 with archive incarnation 1 and park within it; rev 7.16's sweep scoped the whole prefix as instances/<host> under incarnation 2 and archived the child incarnation's object from there (claim rev 6.24 §2, R16-2)", wSweepScopeMembership}, |
| 176 | {"holderless-park", "holderless-park", "INV-20", |
| 177 | "a deleted host's region keeps late residue; the free host's sweep runs as a holderless parking op and a create requested meanwhile waits for FreeAfterPark; with bare chores on the free claim (rev 7.13) the create claims the host over the outstanding park (claim rev 6.15 §6.2a, R13-4)", wFreeSweepVsCreate}, |
| 178 | {"covered-baseline-refused", "covered-baseline-refused", "INV-2", |
| 179 | "an unfinished run whose link in this region is covered and whose generation was retired; the walk refuses the start and alerts; reading objects alone (rev 7.13) it passes over the empty link and restores the marker's retired generation as an empty database (claim rev 6.22 §6.2a, R13-1)", wCoveredLocalBaseline}, |
| 180 | {"restore-selected-baseline", "restore-selected-baseline", "INV-3", |
| 181 | "the marker names S; R issues its first upload and crashes while it is pending; an empty successor R2 is admitted and crashes before uploading; R's delayed upload lands; the next start selects R from R2 → R → S and must restore it rooted at [1, 1]; restoring through the marker, which names S, refuses it and the valid recovery stalls (R14-1)", wIntermediateBaseline}, |
| 182 | {"unique-declarations", "unique-declarations", "INV-21", |
| 183 | "the target is destroyed after the flip and before its first admission, src_covered is false and the source's cut session is uncertified; the return's admission must declare that session once; rev 7.14's separate source-cut path declared it twice, through writes_lost and again beside it (R14-2)", wNoDuplicateDeclarationEarly}, |
| 184 | {"unique-declarations", "unique-declarations", "INV-21", |
| 185 | "the same with the target lost after its probe was admitted: the predecessor is the target's probe session, the list carries the source's cut session once and no target session twice (R14-2)", wNoDuplicateDeclarationLate}, |
| 186 | {"probe-window", "probe-window", "INV-19", |
| 187 | "a landing probe's launch environment is ready exactly at the 30-step deadline; the deadline is checked before the start, so the attempt fails and a fresh admission follows; unchecked, the expired attempt starts, answers readiness and becomes the probed writer (R12-2)", wProbeWindowAt}, |
| 188 | {"seal-return", "seal-return", "INV-15", |
| 189 | "the source acknowledges a write whose upload is still in flight when the cut stops it: the seal carries the write, the source's replica does not; the landing is rolled back before its probe; the return must carry the seal, and treated as clean the source's cold admission declares the write lost while the landing's built generation holds it (rev 7.11 §7.8)", wSealReturn}, |
| 190 | {"close-evidence", "close-evidence", "certificate while", |
| 191 | "a fresh generation's first upload is held past the client's timeout and its retry lands; the session's clean stop must write no certificate (R10-7)", wFirstUploadRetry}, |
| 192 | {"close-evidence", "close-evidence", "certificate while", |
| 193 | "a warm admission's anchor PUT is held past the client's timeout and its retry lands; the session's clean stop must write no certificate (R10-7)", wAnchorRetry}, |
| 194 | {"close-evidence", "close-evidence", "certificate while", |
| 195 | "a compaction's level-1 PUT is held past the client's timeout; the next compaction pass retries and lands; the original completes afterwards; the session's clean stop must write no certificate, since a request of its lifetime was retried after a timeout; looking at the level-0 queue alone it certifies (R9-5)", wMaintenanceRetry}, |
| 196 | {"close-evidence", "close-evidence", "certificate while", |
| 197 | "a snapshot PUT completes on the server after the client gave up on it, a lost response; the client never observed success, so the session must stay uncertain and certify nothing; counting server completion it certifies (R9-5)", wLostResponse}, |
| 198 | {"close-evidence", "close-evidence", "certificate while", |
| 199 | "an upload times out and its retry succeeds while the original stays unresolved; the writer's clean close must write no certificate, because a request of its lifetime is unaccounted for; looking at the level-0 queue alone it certifies (claim rev 6.8 §6.4a, R8-5)", wRetryUnresolved}, |
| 200 | {"build-completion", "build-completion", "INV-2", |
| 201 | "a push's build with its snapshot, then its anchor, held, the agent crashing in between each; since rev 7.11 the marker is the admission's, so a build completed from its intent gives the probe nothing to restore from its pinned snapshot, and the next session restores an empty generation (INV-2); rev 7.10 caught it at the marker (INV-11)", wBuildCrashes}, |
| 202 | // region HA, two boxes per region (L18; plan 2026-10-07-region-ha-hostlife-two-box rev 2) |
| 203 | {"reloc-release-first", "reloc-release-first", "INV-1", |
| 204 | "a drain: the target's worker pins while the source still runs the host, and the target's probe starts beside it", wRelocReleaseFirst}, |
| 205 | {"reloc-install-receipt", "reloc-install-receipt,reloc-ensure-local", "INV-4", |
| 206 | "the target is terminated at installed, after its receipt; its replacement inherits the receipt and skips its local install, and with EnsureLocal gone too (it restores the install otherwise: 1b-next rev 14's 'each covers the other') it starts over data sealed with the old key", wRelocInstallReceipt}, |
| 207 | {"reloc-no-reinstall", "reloc-no-reinstall", "acknowledged timer", |
| 208 | "the first probe admitted P and registered a timer; the agent restarts and re-applies the pinned wake state over it", wRelocNoReinstall}, |
| 209 | {"reloc-released-coverage", "reloc-released-coverage", "INV-2", |
| 210 | "a failover: the executor is terminated with an acknowledged write whose upload is still in flight; the first admission of P takes released coverage and the write is neither restored nor declared", wRelocReleasedCoverage}, |
| 211 | {"reloc-source-loss", "reloc-source-loss", "INV-2", |
| 212 | "a drain whose source is terminated in releasing before its release is journaled, with an unuploaded write; taken as released at what the remote holds, the write goes undeclared", wRelocSourceLoss}, |
| 213 | {"reloc-row-cases", "reloc-row-cases,exec-admission,exec-writer", "INV-6", |
| 214 | "a stale edges file: after the source's release a paused duplicate open makes its row ready again; reconcile holds it, and with the row case, the exec check and AdmitWriter's op.exec check gone a request admits the released source as a writer, and the stamp its admission issued is activated under the target (INV-6). Since L18 finding 2 no relocating phase admits a non-probe writer, so the admission lands just after the completion, and the target's cold first serving wake activates it (joint round 2 finding 1)", wRelocRowCases}, |
| 215 | {"fence-discharge-qualified", "fence-discharge-qualified", "INV-26", |
| 216 | "a terminated box with a volume that was not DeleteOnTermination has its park-local chores discharged automatically", wFenceDischargeQualified}, |
| 217 | {"fence-declares-timers", "fence-declares-timers", "acknowledged timer", |
| 218 | "the executor registers a timer whose manifest never lands and is terminated; the fence drops the timer silently", wFenceDeclaresTimers}, |
| 219 | {"reloc-enrolled-only", "reloc-enrolled-only", "INV-27", |
| 220 | "the only other box of the region holds no key and a replacement has launched unenrolled; the failover names the unenrolled reference", wRelocEnrolledOnly}, |
| 221 | {"files-live-set", "files-live-set", "INV-30", |
| 222 | "the chain's live manifest is the origin generation's, which a cold admission superseded without publishing (nothing changed: 1b-next rev 12's unchanged file); the origin's park-generation archives it, and the failover finds no manifest carrying instance.key: stuck, never served (rev 3: 1b-next ruling 25 makes the loss fail safe; with files-pin-needs-key also gone it is INV-4)", wFilesLiveSet}, |
| 223 | {"reloc-pin-claim-gen", "reloc-pin-claim-gen", "INV-3", |
| 224 | "a pinner observed the first round after the source's release and stalled; after the target wrote into P and died, its stale selection of generation_from is journaled for the nested pinning, and the build waits forever for objects generation_from's own park retired", wRelocPinClaimGen}, |
| 225 | {"reloc-release-deadline", "reloc-release-deadline", "INV-3", |
| 226 | "a drain whose source can never flush: with the deadline the operation is stuck and the operator's resolve returns the host to the source; without it the drain waits forever", wRelocReleaseDeadline}, |
| 227 | {"reloc-ensure-local", "reloc-ensure-local", "INV-4", |
| 228 | "the target freezes past its lease after its receipt; the scoped cleanup retires the unopened local install, and without EnsureLocal P's first admission starts over data sealed with a key no files directory carries", wRelocEnsureLocal}, |
| 229 | {"reloc-verify-receipt", "reloc-verify-receipt", "INV-4", |
| 230 | "after P opened the target's volume is replaced and its agent restarts; without VerifyReceipt the next attempt is admitted with no install and starts over data sealed with the old key", wRelocVerifyReceipt}, |
| 231 | {"reloc-prepared-opened-journal", "reloc-prepared-opened-journal", "acknowledged timer", |
| 232 | "P opened, a timer registered, a second attempt admitted, and P's admission trimmed from holder.admissions; read from the list alone, P looks unopened after the next restart and the local install is remade over the timer", wRelocPreparedOpenedJournal}, |
| 233 | {"fence-reassigns-regional", "fence-reassigns-regional", "INV-3", |
| 234 | "the terminated executor owns a park-generation chore in the legacy box:<b> form; without the reassignment nothing ever runs it", wFenceReassignsRegional}, |
| 235 | {"reloc-replace-not-owing", "reloc-replace-not-owing", "INV-3", |
| 236 | "the only spare owes a park-local for the host when the target dies at installing; named anyway, its pending retirement retires the new installation's stamp under it, and the operation never converges", wRelocReplaceNotOwing}, |
| 237 | {"reloc-exhausted-fence", "reloc-exhausted-fence", "INV-1", |
| 238 | "three targets die while the live source is still op.exec in starting; with rev 8's exhausted fence op.exec goes to none, the operator's replay installs a spare, and it runs beside the source", wRelocExhaustedFence}, |
| 239 | {"reloc-pin-evidenced-empty", "reloc-pin-evidenced-empty", "INV-2", |
| 240 | "a failover whose listing finds nothing although the writes are durable: with the rule the operation is stuck until an operator resolves it on a listing that shows them; without it the pin is empty and the install loses the durable writes", wRelocPinEvidencedEmpty}, |
| 241 | {"files-prepared-seq-zero", "files-prepared-seq-zero", "INV-28", |
| 242 | "the source's manifests reach sequence 3; P's prepared manifest keeps 3, the probe session publishes its timer at 1, and the nested failover pins and declares from the stale prepared manifest", wFilesPreparedSeqZero}, |
| 243 | // rev 3: 1b-next rev 17 to 19's fixes for the model's findings, and the L21 window |
| 244 | // rev 4: Astra's round 1 and claim §11's additional witnesses |
| 245 | {"files-objects-region-bound", "files-objects-region-bound", "INV-3", |
| 246 | "claim §11: the host moves to region 1 with a file unchanged since region 0 published it, the source region is cleaned up, then the target dies; the failover pins an object in region 1's bucket, or, without the region binding, can never pin region 0's", wMoveUnchangedFile}, |
| 247 | {"files-origins-referenced", "files-origins-referenced", "INV-3", |
| 248 | "R11-1: a file unchanged through ten cold admissions, holder.admissions trimmed past its origin; the failover pins the origin's object, or, authorized from the trimmed list, is refused for ever", wOriginsAfterTrim}, |
| 249 | {"reloc-clear-after-cleanup", "reloc-clear-after-cleanup", "INV-29", |
| 250 | "claim §11: the former source's scoped cleanup fails after the drain; its controller record stays and root refuses an executable update until the cleanup succeeds; without the rule the update runs over the unfinished cleanup", wClearAfterCleanup}, |
| 251 | {"fence-converts-committed-landing", "fence-converts-committed-landing", "INV-3", |
| 252 | "claim §11, F5: the record commits a landing and its target dies before the claim follows; the fence makes it a failover in the target's region, or nothing ever finishes it", wCommittedLandingTargetLost}, |
| 253 | {"files-live-set-moves-parks", "files-live-set-moves-parks", "INV-30", |
| 254 | "F4: a push parks the whole location; the files live set survives, so the later failover pins the live object, or can never pin the host's files", wPushKeepsLiveFiles}, |
| 255 | {"files-pin-needs-key", "files-pin-needs-key", "INV-4", |
| 256 | "L21, explicit: the pre-start manifest copy landed without instance.key, the app minted the key after starting and replicated rows sealed with it, and the box died before the keyed manifest landed; with the rule recovery is stuck and installs nothing, without it the keyless pin installs a fresh key over the sealed rows", wL21Window}, |
| 257 | {"reloc-no-spare-bound", "reloc-no-spare-bound", "INV-3", |
| 258 | "F1: a drain's target fails its probe in a two-box region with no spare; with the bound the operation is stuck and the operator's resolve returns the host to the source, without it it waits for ever", wNoSpareBound}, |
| 259 | {"reloc-dead-target-bound", "reloc-dead-target-bound", "INV-3", |
| 260 | "rev 18 finding 2: the target dies at installing and no spare is launched; with the bound the fence is consumed into stuck and the operator's replay serves on the source, without it nothing moves", wDeadTargetBound}, |
| 261 | // the final review's fixes |
| 262 | {"park-evidence-every-box", "park-evidence-every-box", "freed with residue", |
| 263 | "two-box seed 819: a delete's regional park-replica is run by the writer's sibling while the writer's replicator still runs; with the rule it waits for the writer's own stop evidence, without it the region is parked and the writer's next shipment is residue when the host is freed (INV-10)", wParkEvidenceEveryBox}, |
| 264 | // joint round 1 |
| 265 | {"files-live-region", "files-live-region", "residue never retired", |
| 266 | "joint round 1 finding 1: the source's manifest PUT is held while the host moves to region 1 and region 0 is cleaned up, then lands in region 0; the files live set is region-qualified, so the at-rest sweep retires it there; read in every region, the chain's newest manifest protects itself and is never retired (INV-10)", wLateManifestAfterMove}, |
| 267 | {"files-home-move-phases", "files-home-move-phases", "INV-30", |
| 268 | "joint round 1 review I1: a park-generation the source's restart queues during a move runs in the move's stopped phase, op.exec none; region 0 is still authoritative (moves §5.1), so the live manifest survives and the failover the source's termination converts the move into pins it and serves; with the files home read from op.exec alone it is archived and the failover is stuck for ever (INV-3)", wMoveStoppedKeepsLiveFiles}, |
| 269 | {"files-home-move-phases", "files-home-move-phases", "INV-30", |
| 270 | "Astra joint round 2: the same park waits until the target's probe is admitted, runs before the commit, and the landing rolls back cleanly; the source region stays the files home until the commit, so the source's failover after the return pins the keyed manifest and serves; home only until the probe's admission, or never, it is archived and the failover is stuck for ever (INV-3)", wRollbackKeepsSourceFiles}, |
| 271 | // L18 joint round findings 2 and 3 (regionha_completion_witness_test.go) |
| 272 | {"reloc-probe-stop", "reloc-probe-stop", "INV-31", |
| 273 | "a drain completes: the probe's session is stopped with root's receipt before the serving CAS, and the host wakes on the target afterwards; completed over the running probe, its session outlives the kind change on a box whose participation is not discharged", wProbeStopBeforeServing}, |
| 274 | {"reloc-probe-fence-owner", "reloc-probe-fence-owner", "INV-32", |
| 275 | "another operation fences the host on the target after its probe passed: the probe stop refuses with nothing stopped and ruling 67 makes the relocation stuck; installed over that fence, the stop later lifts it as its own and the serving wake starts the host under it", wProbeStopMeetsAnotherFence}, |
| 276 | {"reloc-probe-fence-owner", "reloc-probe-fence-owner", "INV-32", |
| 277 | "a crash: the target's agent restarts while the discharge fails, emptying the activator's fences, and another operation fences the host; the completion lifts only its own fence and the serving wake waits; lifting any fence opens the host under the other", wLiftAfterRestartMeetsAnotherFence}, |
| 278 | {"reloc-completion-discharge-first", "reloc-completion-discharge-first", "INV-31", |
| 279 | "C10's discharge fails for thirty steps: the hold and the fence stay and no wake moves the holder; then it succeeds, the agent crashes after the hold's release, and the next pass resumes and marks; with the hold released and the fence lifted first, a request admits a writer before the discharge", wDischargeFailsHoldsTheRow}, |
| 280 | {"reloc-completion-mark-last", "reloc-completion-mark-last", "INV-31", |
| 281 | "the discharge fails and a drain from the completion box is asked for: with the mark last the barrier refuses it until the discharge succeeds; marked first, the drain names the box while its participation is still the completed op's, and the discharge is never retried", wMarkLastAfterAFailedDischarge}, |
| 282 | {"reloc-completion-from-claim", "reloc-completion-from-claim", "INV-3", |
| 283 | "the mark fails once after the hold's release and the lift, and a second completion crashes after the lift: each next pass finds the unmarked completion from the claim and marks it; found from the row's hold, which the release removed, it is never marked and nothing starts from the host again", wFailedMarkRetriedFromTheClaim}, |
| 284 | {"reloc-completion-barrier", "reloc-completion-barrier", "INV-31", |
| 285 | "while the completion's discharge fails a drain, a move and a push from the completion box are refused; once marked the drain starts and completes; without the barrier the drain names the box while its participation is still the completed op's", wSuccessorWaitsForTheDischarge}, |
| 286 | {"reloc-completion-claim-mode", "reloc-completion-claim-mode", "INV-3", |
| 287 | "ruling 82: the discharge fails, region HA is turned off and the target's agent restarts; the completion-only pass still discharges, releases, lifts and marks, and the host serves; run with region HA on only, the completion never finishes", wCompletionWithRegionHAOff}, |
| 288 | {"reloc-completed-handover", "reloc-completed-handover", "INV-3", |
| 289 | "N6: the first serving wake after the completion hands over from the probe's receipt and the host runs; routed to main's stop, its serving-shaped fence replaces the probe's and the handover refuses for good", wServingWakeHandsOver}, |
| 290 | {"reloc-completed-catchup-hold", "reloc-completed-catchup-hold", "INV-33", |
| 291 | "finding 3, ruling 85: the source releases, its reconcile is delayed until the target completed, and its next reconcile holds its row for the completed op until its park-local retires it; without the catch-up hold the row its release left ready stays ready", wDelayedSourceHoldsItsRow}, |
| 292 | {"reloc-probe-stop-flush", "reloc-probe-stop-flush", "INV-34", |
| 293 | "ruling 87: the probe session acknowledges a write its replicator has not shipped; the probe stop flushes it before root's stop, so the first serving wake, cold, declares nothing the probe session acknowledged; stopped with nothing flushed, that wake declares the write lost", wProbeStopFlushes}, |
| 294 | {"dirty-return-needs-admission", "dirty-return-needs-admission", "INV-30", |
| 295 | "Astra joint round 4: the source's unreplicated write makes the seal src_covered false and the target stalls before its probe, so the landing rolls back dirty with no target admission; the source keeps the files home and its install parks nothing; without the admission check the install park retires the manifest the source's next install would pin", wDirtyReturnWithoutAdmission}, |
| 296 | {"reloc-completion-fenced-exempt", "reloc-completion-fenced-exempt", "INV-3", |
| 297 | "ruling 86, seed 2224: a purge closes the app's admission and the completion box is terminated before its discharge; once its fence record exists the purge verifies it, starts over the unmarked completion and frees the host; without the exemption the barrier refuses the purge and the closed admission the failover, for ever", wPurgeOverAFencedCompletionBox}, |
| 298 | } |
| 299 | |
| 300 | // TestWitnesses is the deterministic half of the mutation evidence. |
| 301 | // |
| 302 | // With no mutation (the gate) it proves every witness's claim in full: |
| 303 | // the scenario holds with every rule in place, holds under every proper |
| 304 | // subset of its stated mutation set (so a rule a combination names is |
| 305 | // shown necessary, not assumed), and under the whole set violates the |
| 306 | // failure the scenario names, not merely some invariant. |
| 307 | // |
| 308 | // Under HOSTLIFE_MUTATE=m (the harness) it runs the witnesses of the |
| 309 | // rules in m and reports each as violated or held; a witness whose set is |
| 310 | // within m must violate with its named failure, or the test fails (the |
| 311 | // witness is broken, not the rule). HOSTLIFE_WITNESS=rule runs one rule's |
| 312 | // witnesses with their trace. |
| 313 | func TestWitnesses(t *testing.T) { |
| 314 | only := os.Getenv("HOSTLIFE_WITNESS") |
| 315 | if mutated == "" { |
| 316 | ran := 0 |
| 317 | for _, x := range witnesses { |
| 318 | if only != "" && x.rule != only { |
| 319 | continue |
| 320 | } |
| 321 | ran++ |
| 322 | check(t, x, "", false, only != "") |
| 323 | for _, s := range properSubsets(x.needs) { |
| 324 | check(t, x, s, false, only != "") |
| 325 | } |
| 326 | check(t, x, x.needs, true, only != "") |
| 327 | } |
| 328 | if only != "" && ran == 0 { |
| 329 | t.Fatalf("no witness for rule %q", only) |
| 330 | } |
| 331 | return |
| 332 | } |
| 333 | set := mutationSet(mutated) |
| 334 | for _, x := range witnesses { |
| 335 | if only != "" && x.rule != only { |
| 336 | continue |
| 337 | } |
| 338 | if !set[x.rule] { |
| 339 | continue |
| 340 | } |
| 341 | needs := true |
| 342 | for _, m := range strings.Split(x.needs, ",") { |
| 343 | if !set[m] { |
| 344 | needs = false |
| 345 | } |
| 346 | } |
| 347 | if needs { |
| 348 | check(t, x, mutated, true, only != "") |
| 349 | continue |
| 350 | } |
| 351 | // the mutation set is not the witness's: report, enforce nothing. |
| 352 | // A wider combination may well violate it (the whole start check |
| 353 | // in place of its generation clause, either registration-check |
| 354 | // partner); the proper-subset proofs live in the gate |
| 355 | report(t, x, mutated, only != "") |
| 356 | } |
| 357 | } |
| 358 | |
| 359 | func report(t *testing.T, x witness, m string, trace bool) { |
| 360 | saved := mutated |
| 361 | mutated = m |
| 362 | defer func() { mutated = saved }() |
| 363 | w := newWitness() |
| 364 | x.run(t, w) |
| 365 | tag := "held" |
| 366 | if len(w.violations) > 0 { |
| 367 | tag = "violated: " + w.violations[0] |
| 368 | } |
| 369 | t.Logf("witness %s under %q (needs %q): %s", x.rule, m, x.needs, tag) |
| 370 | if trace { |
| 371 | dump(t, w) |
| 372 | } |
| 373 | } |
| 374 | |
| 375 | // check runs one witness under mutation m, reports it, and fails the |
| 376 | // test if the outcome is not the stated one: held when no violation is |
| 377 | // expected, the named failure when one is. |
| 378 | func check(t *testing.T, x witness, m string, expectViolation bool, trace bool) { |
| 379 | saved := mutated |
| 380 | mutated = m |
| 381 | defer func() { mutated = saved }() |
| 382 | w := newWitness() |
| 383 | x.run(t, w) |
| 384 | violated := len(w.violations) > 0 |
| 385 | tag := "held" |
| 386 | if violated { |
| 387 | tag = "violated: " + w.violations[0] |
| 388 | } |
| 389 | t.Logf("witness %s under %q (needs %q): %s", x.rule, m, x.needs, tag) |
| 390 | switch { |
| 391 | case expectViolation && !violated: |
| 392 | t.Errorf("witness %s held under %q, which it must violate", x.rule, m) |
| 393 | dump(t, w) |
| 394 | case expectViolation && !namedFailure(w.violations[0], x.want): |
| 395 | t.Errorf("witness %s under %q violated, but not its named failure %q", x.rule, m, x.want) |
| 396 | dump(t, w) |
| 397 | case !expectViolation && violated: |
| 398 | t.Errorf("witness %s violated under %q, where it must hold", x.rule, m) |
| 399 | dump(t, w) |
| 400 | } |
| 401 | if trace { |
| 402 | dump(t, w) |
| 403 | } |
| 404 | } |
| 405 | |
| 406 | // namedFailure: the violation names the witness's failure. want is one |
| 407 | // failure or several separated by "|" (any of them); a failure that ends |
| 408 | // in a digit must not run on into another (INV-3 is not INV-30). |
| 409 | func namedFailure(v, want string) bool { |
| 410 | for _, f := range strings.Split(want, "|") { |
| 411 | for i := 0; ; { |
| 412 | j := strings.Index(v[i:], f) |
| 413 | if j < 0 { |
| 414 | break |
| 415 | } |
| 416 | end := i + j + len(f) |
| 417 | last := f[len(f)-1] |
| 418 | if !(last >= '0' && last <= '9') || end == len(v) || v[end] < '0' || v[end] > '9' { |
| 419 | return true |
| 420 | } |
| 421 | i = i + j + 1 |
| 422 | } |
| 423 | } |
| 424 | return false |
| 425 | } |
| 426 | |
| 427 | func mutationSet(m string) map[string]bool { |
| 428 | set := map[string]bool{} |
| 429 | for _, x := range strings.Split(m, ",") { |
| 430 | if x != "" { |
| 431 | set[x] = true |
| 432 | } |
| 433 | } |
| 434 | return set |
| 435 | } |
| 436 | |
| 437 | // properSubsets: every non-empty proper subset of a comma-separated set. |
| 438 | func properSubsets(needs string) []string { |
| 439 | xs := strings.Split(needs, ",") |
| 440 | var out []string |
| 441 | for mask := 1; mask < (1<<len(xs))-1; mask++ { |
| 442 | var sub []string |
| 443 | for i, x := range xs { |
| 444 | if mask&(1<<i) != 0 { |
| 445 | sub = append(sub, x) |
| 446 | } |
| 447 | } |
| 448 | out = append(out, strings.Join(sub, ",")) |
| 449 | } |
| 450 | return out |
| 451 | } |
| 452 | |
| 453 | func dump(t *testing.T, w *world) { |
| 454 | for _, line := range w.trace { |
| 455 | t.Log(line) |
| 456 | } |
| 457 | t.Logf("state: %s%s", w.state(), w.boxesState()) |
| 458 | } |
| 459 | |
| 460 | // ---------- the fixture ---------- |
| 461 | |
| 462 | // newWitness is a clean world: three boxes with the secrets key, no faults |
| 463 | // armed, no legacy host, the quiet RNG, and the trace kept. |
| 464 | func newWitness() *world { |
| 465 | w := &world{seed: -1, rng: quiet{}, verbose: true, now: 100, perRegion: 1, |
| 466 | stores: map[string]bool{app0: true, app1: true}, cfgVer: map[string]int{app0: 1, app1: 1}, purgeRes: map[string]bool{}, purgeStep: map[string]int{}, |
| 467 | 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{}} |
| 468 | for r := 0; r < nRegions; r++ { |
| 469 | w.buckets[r] = newBucket() |
| 470 | b := &box{ID: r, Region: r, HasKey: true, Enrolled: true, DeleteOnTermination: true} |
| 471 | b.forget() |
| 472 | w.boxes = append(w.boxes, b) |
| 473 | } |
| 474 | w.admit = map[string]*admission{app0: {Reg: map[string]regEntry{}}, app1: {Reg: map[string]regEntry{}}} |
| 475 | return w |
| 476 | } |
| 477 | |
| 478 | // serve installs incarnation inc of app on b as a serving host: claim, |
| 479 | // record, row, local database and files, config rendered, and a replica |
| 480 | // object with its acknowledged writes. |
| 481 | func (w *world) serve(b *box, inc int, app string) { |
| 482 | loc := locationFor(inc, false) |
| 483 | key := 1000 + inc |
| 484 | db := &localDB{Inc: inc, Loc: loc, Key: key, State: map[string]int{}, Epoch: b.Epoch} |
| 485 | for i := 0; i < 2; i++ { |
| 486 | w.nextW++ |
| 487 | w.acks = append(w.acks, ack{W: w.nextW, Inc: inc, Box: b.ID, Session: -1, At: w.now, Kind: "write"}) // the session is the holder's below |
| 488 | w.writeInc[w.nextW] = inc |
| 489 | w.commit(db, w.nextW) |
| 490 | } |
| 491 | if inc > w.nextInc { |
| 492 | w.nextInc = inc |
| 493 | } |
| 494 | w.serial++ |
| 495 | n := &claim{Ver: 1} |
| 496 | if w.claim != nil { |
| 497 | n = w.claim.clone() |
| 498 | n.Ver++ |
| 499 | } |
| 500 | n.Holder = &holder{Inc: inc, App: app, Serial: w.serial, Location: loc, Stamp: n.Ver, Session: n.Ver, WriterBox: b.ID} // the serving CAS wrote holder.stamp; one writer session so far |
| 501 | n.Op = opState{Kind: "serving", Exec: b.ID, Parts: []int{b.ID}} |
| 502 | n.Regions, n.Boxes, n.Complete, n.Obl = []int{b.Region}, []int{b.ID}, true, nil |
| 503 | w.claim = n |
| 504 | for i := range w.acks { |
| 505 | if w.acks[i].Session == -1 { |
| 506 | w.acks[i].Session = n.Holder.Session // the one writer session so far acknowledged them |
| 507 | } |
| 508 | } |
| 509 | db.Session = n.Holder.Session |
| 510 | w.rec = &record{Ver: w.newVer(), Inc: inc, App: app, Region: b.Region} |
| 511 | b.Row = &row{Inc: inc, App: app, Status: "ready"} |
| 512 | b.DB = db |
| 513 | b.Files = &filesDir{Inc: inc, Key: key, Env: key, Done: true} |
| 514 | b.Config, b.CfgVer, b.Live, b.LiveInc = inc, w.cfgVer[app], app, inc |
| 515 | b.install(inc, n.Ver) // the create's installation stamp, initialized from holder.stamp |
| 516 | db.Stamp = n.Ver |
| 517 | bl := w.deltaOf(db, inc) |
| 518 | db.Pos, db.Pending = 1, nil |
| 519 | k := ltxKey(loc, "", 0, bl.Min, bl.Max) |
| 520 | w.buckets[b.Region].objs[k] = append(w.buckets[b.Region].objs[k], &version{ID: w.newVer(), B: bl}) |
| 521 | w.markDurable(k, bl) |
| 522 | // the generation is intact: its last writer session closed cleanly at |
| 523 | // position 1 on this box (claim rev 6.8 §6.4a) |
| 524 | w.buckets[b.Region].objs[closedKey(loc, "", n.Ver)] = []*version{{ID: w.newVer(), B: &blob{Kind: "closed", Inc: inc, Stamp: n.Ver, Seq: b.ID, Session: n.Ver, TX: 1}}} |
| 525 | w.logf("witness: inc %d of app %s serving on box %d", inc, app, b.ID) |
| 526 | } |
| 527 | |
| 528 | // legacy installs a pre-release host: an untagged replica in region r0 |
| 529 | // where it serves with no claim, and a replica an earlier move left in r1. |
| 530 | func (w *world) legacy(b *box, other int) { |
| 531 | w.nextInc++ |
| 532 | inc := w.nextInc |
| 533 | w.rec = &record{Ver: w.newVer(), Inc: inc, App: app0, Region: b.Region} |
| 534 | w.legacyIncs[inc] = true |
| 535 | key := 7 |
| 536 | b.Row = &row{Inc: inc, App: app0, Status: "ready"} |
| 537 | b.DB = &localDB{Inc: inc, Loc: locationFor(inc, true), Key: key, State: map[string]int{}, Epoch: b.Epoch} |
| 538 | for i := 0; i < 2; i++ { |
| 539 | w.nextW++ |
| 540 | w.acks = append(w.acks, ack{W: w.nextW, Inc: inc, Box: b.ID, Session: 0, At: w.now, Kind: "write"}) // the pre-release writer: the legacy identity, session 0 (claim rev 6.24) |
| 541 | w.writeInc[w.nextW] = inc |
| 542 | w.commit(b.DB, w.nextW) |
| 543 | } |
| 544 | b.DB.Session = 0 |
| 545 | b.Files = &filesDir{Inc: inc, Key: key, Env: 1, Done: true} |
| 546 | b.Config, b.CfgVer, b.Live, b.LiveInc = inc, 1, app0, inc |
| 547 | full := w.deltaOf(b.DB, 0) |
| 548 | b.DB.Pos, b.DB.Pending = 1, nil |
| 549 | k := ltxKey(b.DB.Loc, "", 0, 1, 1) |
| 550 | w.buckets[b.Region].objs[k] = []*version{{ID: w.newVer(), B: full}} |
| 551 | w.markDurable(k, full) |
| 552 | // the pre-release writer closed cleanly on this box (a fixture for a |
| 553 | // warm first wake; the real pre-release writer leaves no certificate, |
| 554 | // so a real first wake is cold); adoption's stamp is 1 and the legacy |
| 555 | // identity's session 0 (claim rev 6.24) |
| 556 | w.buckets[b.Region].objs[closedKey(b.DB.Loc, "", 0)] = []*version{{ID: w.newVer(), B: &blob{Kind: "closed", Inc: inc, Stamp: 1, Seq: b.ID, Session: 0, TX: 1}}} |
| 557 | first := w.txs[b.DB.Log[0]] |
| 558 | 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}} |
| 559 | w.buckets[other].objs[ltxKey(b.DB.Loc, "", 0, 1, 1)] = []*version{{ID: w.newVer(), B: part}} |
| 560 | } |
| 561 | |
| 562 | // ---------- the schedule ---------- |
| 563 | |
| 564 | // tick is one step of the witness's own schedule: time, S3 completions, |
| 565 | // paused goroutines, then the actors the witness names, then the per-step |
| 566 | // invariants. |
| 567 | func (w *world) tick(actors ...func()) { |
| 568 | w.now++ |
| 569 | w.completeDue(false) |
| 570 | if p := w.recPend; p != nil && p.at <= w.now { |
| 571 | w.recPend = nil |
| 572 | if w.rec == nil { |
| 573 | w.rec = p.rec |
| 574 | } |
| 575 | } |
| 576 | w.runStalled() |
| 577 | if w.perRegion > 1 { |
| 578 | w.twoBoxStep() // replacements launch and enroll, the publisher runs; the quiet source terminates and drains nothing |
| 579 | } |
| 580 | for _, a := range actors { |
| 581 | a() |
| 582 | } |
| 583 | w.checkStep() |
| 584 | } |
| 585 | |
| 586 | // drive ticks until done, a violation, or max steps. |
| 587 | func (w *world) drive(max int, done func() bool, actors ...func()) bool { |
| 588 | for i := 0; i < max; i++ { |
| 589 | if done() { |
| 590 | return true |
| 591 | } |
| 592 | w.tick(actors...) |
| 593 | if len(w.violations) > 0 { |
| 594 | return false |
| 595 | } |
| 596 | } |
| 597 | return done() |
| 598 | } |
| 599 | |
| 600 | // reach drives to a milestone the scenario needs. Not reaching it, with no |
| 601 | // violation to explain why, is a liveness failure and is recorded as one |
| 602 | // (INV-3), so a mutation that leaves the protocol stuck counts as caught |
| 603 | // and an unmutated scenario that stalls fails the test. |
| 604 | func (w *world) reach(t *testing.T, max int, what string, done func() bool, actors ...func()) bool { |
| 605 | if w.drive(max, done, actors...) { |
| 606 | w.logf("witness: reached %s", what) |
| 607 | return true |
| 608 | } |
| 609 | if len(w.violations) == 0 { |
| 610 | w.violate("INV-3 (witness): %s not reached within %d steps: %s", what, max, w.state()) |
| 611 | } |
| 612 | return false |
| 613 | } |
| 614 | |
| 615 | // finish drives to quiescence and runs the final oracle, as runSeed does. |
| 616 | func (w *world) finish(t *testing.T) { |
| 617 | w.drive(2000, w.quiescent, w.actAll(), w.runConsole, w.recoveryPass, w.operator) |
| 618 | if len(w.violations) > 0 { |
| 619 | return |
| 620 | } |
| 621 | w.completeDue(true) |
| 622 | w.final() |
| 623 | } |
| 624 | |
| 625 | func (w *world) act(bs ...*box) func() { |
| 626 | return func() { |
| 627 | for _, b := range bs { |
| 628 | w.worker(b) |
| 629 | w.obligationRunner(b) |
| 630 | w.reconcile(b) |
| 631 | } |
| 632 | } |
| 633 | } |
| 634 | |
| 635 | // actAll runs every live box, replacements included: its worker, |
| 636 | // obligation runner and reconcile, and the config-sync and adoption |
| 637 | // passes a serving row needs before the host is at rest. |
| 638 | func (w *world) actAll() func() { |
| 639 | return func() { |
| 640 | for _, b := range w.liveBoxes() { |
| 641 | w.worker(b) |
| 642 | w.obligationRunner(b) |
| 643 | w.reconcile(b) |
| 644 | if len(b.plans) == 0 { |
| 645 | w.passPlan(b, "config") |
| 646 | w.passPlan(b, "adopt") |
| 647 | } |
| 648 | w.passExec(b) |
| 649 | } |
| 650 | } |
| 651 | } |
| 652 | |
| 653 | // runConsole runs one step of every console plan, in order: a |
| 654 | // deterministic consoleStep. |
| 655 | func (w *world) runConsole() { w.runPlans(nil) } |
| 656 | |
| 657 | // runPlans runs one step of every console plan but skip. A plan may add |
| 658 | // another (a create's orphan cleanup); the new one is kept for the next |
| 659 | // step. |
| 660 | func (w *world) runPlans(skip *consolePlan) { |
| 661 | plans := append([]*consolePlan(nil), w.console...) |
| 662 | done := map[*consolePlan]bool{} |
| 663 | for _, p := range plans { |
| 664 | if p == skip || p.Stall > w.now { |
| 665 | continue |
| 666 | } |
| 667 | if w.runPlan(p) { |
| 668 | done[p] = true |
| 669 | } |
| 670 | } |
| 671 | var keep []*consolePlan |
| 672 | for _, p := range w.console { |
| 673 | if !done[p] { |
| 674 | keep = append(keep, p) |
| 675 | } |
| 676 | } |
| 677 | w.console = keep |
| 678 | } |
| 679 | |
| 680 | // stop is the cloud stopping a box: destroyed, nothing on it runs. |
| 681 | func (w *world) stop(b *box) { |
| 682 | b.Destroyed, b.Procs = true, nil |
| 683 | w.logf("witness: box %d stopped", b.ID) |
| 684 | } |
| 685 | |
| 686 | // appWrite is one acknowledged application write by b's main process. |
| 687 | func (w *world) appWrite(b *box) int { |
| 688 | if !hasMain(b) { |
| 689 | panic("appWrite: no main process") |
| 690 | } |
| 691 | p := b.Procs[0] |
| 692 | w.nextW++ |
| 693 | wr := w.nextW |
| 694 | if b.DB != nil && b.DB.Inc == p.Inc { |
| 695 | w.commit(b.DB, wr) |
| 696 | } else { |
| 697 | w.txs[wr] = tx{W: wr} |
| 698 | } |
| 699 | sess, gen := w.sessionOf(b) |
| 700 | w.acks = append(w.acks, ack{W: wr, Inc: p.Inc, Box: b.ID, Session: sess, Gen: gen, At: w.now, Kind: "write"}) |
| 701 | w.writeInc[wr] = p.Inc |
| 702 | w.logf("witness: box %d wrote %d", b.ID, wr) |
| 703 | return wr |
| 704 | } |
| 705 | |
| 706 | // holdKey makes the witness hold every request for key, or under a prefix |
| 707 | // ending in "/", until completeHeld. |
| 708 | func (w *world) holdKey(key string) { |
| 709 | w.hold = func(r *request) bool { |
| 710 | return r.key == key || strings.HasSuffix(key, "/") && strings.HasPrefix(r.key, key) |
| 711 | } |
| 712 | } |
| 713 | |
| 714 | // completeHeld completes the requests the witness held for key (or |
| 715 | // prefix), now. |
| 716 | func (w *world) completeHeld(key string) int { |
| 717 | n := 0 |
| 718 | var keep []*request |
| 719 | for _, r := range w.pending { |
| 720 | if (r.key == key || strings.HasSuffix(key, "/") && strings.HasPrefix(r.key, key)) && r.doneAt == 1<<30 { |
| 721 | r.doneAt = w.now // the response arrives now (the close's evidence reads the completion time, R9-5) |
| 722 | if w.now-r.at > horizonH { |
| 723 | r.beyond = true // a completion past the horizon: the sweep's, as the biased schedule's are (§6.4) |
| 724 | } |
| 725 | w.complete(r) |
| 726 | w.logf("witness: held %v %s r%d completes now", r.kind, r.key, r.region) |
| 727 | n++ |
| 728 | continue |
| 729 | } |
| 730 | keep = append(keep, r) |
| 731 | } |
| 732 | w.pending = keep |
| 733 | return n |
| 734 | } |
| 735 | |
| 736 | func (w *world) oblOpen(region int, prefix string) bool { |
| 737 | if w.claim == nil { |
| 738 | return false |
| 739 | } |
| 740 | for _, o := range w.claim.Obl { |
| 741 | if o.Region == region && o.Prefix == prefix { |
| 742 | return true |
| 743 | } |
| 744 | } |
| 745 | return false |
| 746 | } |
| 747 | |
| 748 | // landProbed drives a move of the serving host to tgt until the landing's |
| 749 | // probe has passed and the instance runs on tgt, before the settle window |
| 750 | // ends. |
| 751 | func (w *world) landProbed(t *testing.T, src, tgt *box) { |
| 752 | w.moveTo(tgt.Region) |
| 753 | if w.claim.Op.Kind != "moving" { |
| 754 | t.Fatalf("witness: move not started: %s", w.state()) |
| 755 | } |
| 756 | w.reach(t, 600, "landing probed", func() bool { |
| 757 | c := w.claim |
| 758 | return c.Op.Kind == "landing" && c.Op.LandPhase == "probed" && hasMain(tgt) |
| 759 | }, w.act(src, tgt), w.recoveryPass) |
| 760 | } |
| 761 | |
| 762 | // ---------- the scenarios ---------- |
| 763 | |
| 764 | // wGenerationConditional (model 29, §5.1): push p1's first generation.json |
| 765 | // PUT is accepted but its response is lost; the agent publishes again and |
| 766 | // p1 completes. Push p2 completes. Then the stale PUT lands. Conditional on |
| 767 | // the marker it superseded, it is refused (412); unconditional, the marker |
| 768 | // names p1 while the claim names p2, and the serving box cannot start. |
| 769 | func wGenerationConditional(t *testing.T, w *world) { |
| 770 | e := w.boxes[0] |
| 771 | w.serve(e, 1, app0) |
| 772 | loc := w.claim.Holder.Location |
| 773 | push := func(holdMarker bool) { |
| 774 | // the previous push's publication queued the predecessor's |
| 775 | // park-generation chore (claim rev 6.14 item 5: a prepared |
| 776 | // generation publishes too); an obligation in the region blocks a |
| 777 | // new operation until it runs (rule obligations-block-ops) |
| 778 | w.reach(t, 400, "obligations clear", func() bool { return len(w.claim.Obl) == 0 }, w.act(e)) |
| 779 | w.userPush() |
| 780 | id := w.claim.Op.ID |
| 781 | if !w.reach(t, 400, "push "+id+" probing", func() bool { return w.claim.Op.ID == id && w.claim.Op.Phase == "probing" }, w.act(e)) { |
| 782 | return |
| 783 | } |
| 784 | if holdMarker { |
| 785 | // the probe's cold admission publishes generation.json for the |
| 786 | // prepared generation (rev 7.10): accepted, response lost; the |
| 787 | // writer does not start, and the next attempt publishes again |
| 788 | w.holdKey(genMarkerKey(loc)) |
| 789 | w.tick(w.act(e)) |
| 790 | w.hold = nil |
| 791 | } |
| 792 | w.reach(t, 400, "push "+id+" released", func() bool { return w.claim.Op.Kind == "serving" }, w.act(e)) |
| 793 | w.idleStop(e) |
| 794 | } |
| 795 | push(true) |
| 796 | push(false) |
| 797 | if len(w.violations) > 0 { |
| 798 | return |
| 799 | } |
| 800 | if w.completeHeld(genMarkerKey(loc)) != 1 { |
| 801 | t.Fatalf("witness: no held marker PUT") |
| 802 | } |
| 803 | w.finish(t) |
| 804 | } |
| 805 | |
| 806 | // wLostReturnPark (model 27, §7.10). |
| 807 | func wLostReturnPark(t *testing.T, w *world) { |
| 808 | src, tgt := w.boxes[0], w.boxes[1] |
| 809 | w.serve(src, 1, app0) |
| 810 | w.landProbed(t, src, tgt) |
| 811 | w.appWrite(tgt) // real work in the settle window |
| 812 | w.rollback(w.claim, "settle check failed") |
| 813 | w.reach(t, 50, "target released dirty", func() bool { |
| 814 | c := w.claim |
| 815 | return c.Op.Kind == "restoring" && c.Op.Phase == "released" && c.Op.Dirty |
| 816 | }, w.act(src, tgt), w.recoveryPass) |
| 817 | w.tick(w.act(tgt)) // the first return PUT: moves/<host>/<rb>/db in the source region |
| 818 | if w.claim.Op.ReturnDB.Ver == 0 { |
| 819 | t.Fatalf("witness: the return did not begin: %s", w.state()) |
| 820 | } |
| 821 | w.stop(tgt) // the cloud stops the target mid-return |
| 822 | w.reach(t, 20, "declared lost", func() bool { return contains(w.claim.Lost, tgt.ID) }, w.operator) |
| 823 | w.replaceDestroyed() |
| 824 | w.finish(t) |
| 825 | } |
| 826 | |
| 827 | // wFenceConvertsMoving (moves rev 7.20 §7.10, claim rev 6.28 §4): the |
| 828 | // source of a move that has not flipped is terminated, in a one-box |
| 829 | // region. The termination fence converts the move to relocating at |
| 830 | // pinning: exec none, the stamp and generation kept, the lane's park owed |
| 831 | // to the target region. No box exists in the source region, so the |
| 832 | // relocation holds there, safely (no writer, the data pinned), the |
| 833 | // operator is told once, and the claim does not churn. Once region HA |
| 834 | // enrolls a replacement box (the model's replacement mechanism), the |
| 835 | // relocation completes on it and the host serves again in its region. |
| 836 | func wFenceConvertsMoving(t *testing.T, w *world) { |
| 837 | src, tgt := w.boxes[0], w.boxes[1] |
| 838 | w.serve(src, 1, app0) |
| 839 | w.moveTo(tgt.Region) |
| 840 | w.reach(t, 100, "staging begins", func() bool { |
| 841 | c := w.claim |
| 842 | return c.Op.Kind == "moving" && c.Op.Phase == "preparing" && contains(c.Regions, tgt.Region) |
| 843 | }, w.act(src, tgt)) |
| 844 | w.stop(src) // the cloud terminates the source; the regional worker's read is the fence |
| 845 | if !w.reach(t, 50, "converted to relocating at pinning", func() bool { |
| 846 | c := w.claim |
| 847 | return c.Op.Kind == "relocating" && c.Op.Phase == "pinning" && c.Op.Exec == -1 |
| 848 | }, w.act(tgt), w.recoveryPass) { |
| 849 | return // under the mutation the move never converges: reach recorded INV-3 |
| 850 | } |
| 851 | c := w.claim |
| 852 | if !contains(c.Lost, src.ID) || c.Op.FenceBox != src.ID || c.oblFor(c.Op.ID) == 0 { |
| 853 | t.Fatalf("witness: the conversion did not record the fence and the lane's park: %s", w.state()) |
| 854 | } |
| 855 | // it waits: no box in region 0. Nothing runs, nothing loops; the only |
| 856 | // claim writes are the lane park's own steps and the one alert |
| 857 | ver, alerts := c.Ver, w.alerts |
| 858 | w.drive(200, func() bool { return false }, w.act(tgt), w.recoveryPass, w.operator) |
| 859 | c = w.claim |
| 860 | if c.Op.Kind != "relocating" || c.Op.Phase != "pinning" || c.Op.Exec != -1 { |
| 861 | t.Fatalf("witness: the relocation did not hold at pinning: %s", w.state()) |
| 862 | } |
| 863 | if w.alerts <= alerts { |
| 864 | t.Fatalf("witness: no alert for a relocation with no box in its region") |
| 865 | } |
| 866 | if c.Ver-ver > 8 { |
| 867 | t.Fatalf("witness: the claim churned %d times while waiting: %s", c.Ver-ver, w.state()) |
| 868 | } |
| 869 | for _, b := range w.liveBoxes() { |
| 870 | if len(b.Procs) > 0 { |
| 871 | t.Fatalf("witness: box %d runs the host while the relocation waits", b.ID) |
| 872 | } |
| 873 | } |
| 874 | w.replaceDestroyed() // region HA enrolls a replacement box (H16, H17) |
| 875 | w.finish(t) |
| 876 | if len(w.violations) > 0 { |
| 877 | return |
| 878 | } |
| 879 | if w.stats["relocation"] != 1 { |
| 880 | t.Fatalf("witness: the relocation did not complete: %s", w.state()) |
| 881 | } |
| 882 | nb := w.regionBox(src.Region) |
| 883 | if e := w.execBox(w.claim); e == nil || nb == nil || e.ID != nb.ID || w.claim.Op.Kind != "serving" { |
| 884 | t.Fatalf("witness: the host does not serve on the replacement box: %s", w.state()) |
| 885 | } |
| 886 | } |
| 887 | |
| 888 | // wDeclareLostCompute (model 5, §7.10): the target is frozen (a whole-VM |
| 889 | // pause) in its settle window; its execution lease expires. |
| 890 | func wDeclareLostCompute(t *testing.T, w *world) { |
| 891 | src, tgt := w.boxes[0], w.boxes[1] |
| 892 | w.serve(src, 1, app0) |
| 893 | w.landProbed(t, src, tgt) |
| 894 | tgt.Frozen = true |
| 895 | exp := w.execLease[tgt.ID].Expires |
| 896 | w.reach(t, 100, "lease expired", func() bool { return w.now > exp+lostMargin }, w.act(src), w.recoveryPass) |
| 897 | // the operator: refused with compute fencing (the box is not stopped); |
| 898 | // on expiry alone, the rollback and the loss go through and the source |
| 899 | // recovers |
| 900 | w.drive(100, func() bool { return hasMain(src) }, w.act(src), w.recoveryPass, w.operator) |
| 901 | tgt.Frozen = false // the VM resumes: its application runs before its agent does |
| 902 | w.tick() |
| 903 | w.finish(t) |
| 904 | } |
| 905 | |
| 906 | // wWatchdogIndependent (§7.1): as wDeclareLostCompute, with the agent |
| 907 | // alone paused, so the application keeps running and only a watchdog |
| 908 | // outside the agent can fence it. |
| 909 | func wWatchdogIndependent(t *testing.T, w *world) { |
| 910 | src, tgt := w.boxes[0], w.boxes[1] |
| 911 | w.serve(src, 1, app0) |
| 912 | w.landProbed(t, src, tgt) |
| 913 | tgt.AgentPaused = true |
| 914 | exp := w.execLease[tgt.ID].Expires |
| 915 | dog := func() { w.watchdog(tgt) } |
| 916 | w.reach(t, 100, "lease expired", func() bool { return w.now > exp+lostMargin }, w.act(src), w.recoveryPass, dog) |
| 917 | w.drive(100, func() bool { return hasMain(src) }, w.act(src), w.recoveryPass, w.operator, dog) |
| 918 | tgt.AgentPaused = false |
| 919 | w.finish(t) |
| 920 | } |
| 921 | |
| 922 | // wLostQuarantine (claim §7.2, CC12): the target is stopped while landing, |
| 923 | // declared lost, and later started again with its old disk. |
| 924 | func wLostQuarantine(t *testing.T, w *world) { |
| 925 | src, tgt := w.boxes[0], w.boxes[1] |
| 926 | w.serve(src, 1, app0) |
| 927 | w.moveTo(tgt.Region) |
| 928 | w.reach(t, 600, "landing installed", func() bool { |
| 929 | c := w.claim |
| 930 | return c.Op.Kind == "landing" && c.Op.LandPhase == "probing" |
| 931 | }, w.act(src, tgt), w.recoveryPass) |
| 932 | w.stop(tgt) |
| 933 | w.reach(t, 60, "declared lost", func() bool { return contains(w.claim.Lost, tgt.ID) }, w.act(src), w.recoveryPass, w.operator) |
| 934 | tgt.Destroyed = false // started again, with its old disk |
| 935 | tgt.forget() |
| 936 | w.logf("witness: box %d started again", tgt.ID) |
| 937 | w.finish(t) |
| 938 | } |
| 939 | |
| 940 | // wMarkersLast (R2-6): the source has a registered timer; the target's |
| 941 | // agent crashes between extracting the files and writing the marker. |
| 942 | func wMarkersLast(t *testing.T, w *world) { |
| 943 | src, tgt := w.boxes[0], w.boxes[1] |
| 944 | w.serve(src, 1, app0) |
| 945 | w.nextW++ |
| 946 | src.Timers = []int{w.nextW} |
| 947 | w.acks = append(w.acks, ack{W: w.nextW, Inc: 1, Box: src.ID, Session: src.DB.Session, Gen: src.DB.Gen, At: w.now, Kind: "timer"}) |
| 948 | w.moveTo(tgt.Region) |
| 949 | id := w.claim.Op.ID |
| 950 | w.reach(t, 600, "files extracted", func() bool { return tgt.Files != nil && tgt.Files.Gen == id }, w.act(src, tgt), w.recoveryPass) |
| 951 | tgt.Procs = nil |
| 952 | tgt.forget() // the agent crashes and restarts: its memory, the pending timers included, is gone |
| 953 | w.logf("witness: box %d agent crashed between the extraction and the marker", tgt.ID) |
| 954 | w.finish(t) |
| 955 | } |
| 956 | |
| 957 | // wRollbackJournal (R2-3): a dirty rollback; the source's agent restarts |
| 958 | // after its probe spawned the instance, which wrote and replicated. |
| 959 | func wRollbackJournal(t *testing.T, w *world) { |
| 960 | src, tgt := w.boxes[0], w.boxes[1] |
| 961 | w.serve(src, 1, app0) |
| 962 | w.landProbed(t, src, tgt) |
| 963 | w.appWrite(tgt) |
| 964 | w.rollback(w.claim, "settle check failed") |
| 965 | w.reach(t, 2000, "source probed on the return", func() bool { |
| 966 | c := w.claim |
| 967 | return c.Op.Kind == "restoring" && c.Op.SrcPhase == "probed" && hasMain(src) |
| 968 | }, w.act(src, tgt), w.recoveryPass) |
| 969 | if !hasMain(src) { |
| 970 | w.violate("INV-3 (witness): the source's probe did not run on the return: %s%s", w.state(), w.boxesState()) |
| 971 | return |
| 972 | } |
| 973 | w.appWrite(src) |
| 974 | w.replicate(src) // into the return generation: durable there |
| 975 | src.Procs = nil |
| 976 | src.forget() // the agent crashes and restarts |
| 977 | w.logf("witness: box %d agent crashed during the rollback's probe", src.ID) |
| 978 | w.finish(t) |
| 979 | } |
| 980 | |
| 981 | // heldRound drives a move to its first staging round and holds that |
| 982 | // round's db PUT. It returns the staging key. |
| 983 | func (w *world) heldRound(t *testing.T, src, tgt *box) string { |
| 984 | w.moveTo(tgt.Region) |
| 985 | id := w.claim.Op.ID |
| 986 | key := fmt.Sprintf("moves/%s/%s/db", host, id) |
| 987 | w.reach(t, 100, "staging begins", func() bool { |
| 988 | c := w.claim |
| 989 | return c.Op.Phase == "preparing" && contains(c.Regions, tgt.Region) |
| 990 | }, w.act(src, tgt)) |
| 991 | w.holdKey(key) |
| 992 | w.tick(w.act(src)) // this round's db PUT is accepted and completes late |
| 993 | w.hold = nil |
| 994 | return key |
| 995 | } |
| 996 | |
| 997 | // wSealByVersion (J-N2): the held round completes after the seal, so the |
| 998 | // staging key's current version is older than the sealed one. |
| 999 | func wSealByVersion(t *testing.T, w *world) { |
| 1000 | src, tgt := w.boxes[0], w.boxes[1] |
| 1001 | w.serve(src, 1, app0) |
| 1002 | key := w.heldRound(t, src, tgt) |
| 1003 | w.wake(src) // the source serves during the move |
| 1004 | if !hasMain(src) { |
| 1005 | t.Fatalf("witness: source did not wake: %s", w.state()) |
| 1006 | } |
| 1007 | w.appWrite(src) |
| 1008 | w.replicate(src) |
| 1009 | w.reach(t, 600, "sealed", func() bool { return w.claim.Op.Phase == "sealed" || w.claim.Op.Kind == "landing" }, w.act(src, tgt), w.recoveryPass) |
| 1010 | w.completeHeld(key) |
| 1011 | w.finish(t) |
| 1012 | } |
| 1013 | |
| 1014 | // wStagingQuiet (J-N2): the held round completes after the commit, once |
| 1015 | // the landing's staging park has acknowledged (if it retired at the seal |
| 1016 | // time) and before the release. |
| 1017 | func wStagingQuiet(t *testing.T, w *world) { |
| 1018 | src, tgt := w.boxes[0], w.boxes[1] |
| 1019 | w.serve(src, 1, app0) |
| 1020 | key := w.heldRound(t, src, tgt) |
| 1021 | prefix := key[:strings.LastIndex(key, "/")+1] |
| 1022 | w.reach(t, 600, "committed", func() bool { return w.claim.Op.Committed }, w.act(src, tgt), w.recoveryPass) |
| 1023 | w.drive(30, func() bool { return !w.oblOpen(tgt.Region, prefix) }, w.act(src, tgt), w.recoveryPass) |
| 1024 | w.completeHeld(key) |
| 1025 | w.finish(t) |
| 1026 | } |
| 1027 | |
| 1028 | // wClaimCasOpID (claim C2): a clean rollback; the source's close writes the |
| 1029 | // record (record first, rev 7.23) and its goroutine stalls before the |
| 1030 | // release, holding the claim it read; the recovery pass releases from |
| 1031 | // last_move, a purge claims the host, and the goroutine resumes into its |
| 1032 | // release. |
| 1033 | func wClaimCasOpID(t *testing.T, w *world) { |
| 1034 | src, tgt := w.boxes[0], w.boxes[1] |
| 1035 | w.serve(src, 1, app0) |
| 1036 | w.landProbed(t, src, tgt) |
| 1037 | w.rollback(w.claim, "cut deadline") |
| 1038 | w.reach(t, 1500, "source about to close", func() bool { |
| 1039 | c := w.claim |
| 1040 | return c.Op.Kind == "restoring" && c.Op.SrcPhase == "opened" && c.oblFor(c.Op.ID) == 0 |
| 1041 | }, w.act(src, tgt), w.recoveryPass) |
| 1042 | old := w.claim.clone() // the stalled goroutine's read |
| 1043 | if !w.closeRecord(old, src.ID) { |
| 1044 | t.Fatalf("witness: the record did not close: %s", w.state()) |
| 1045 | } |
| 1046 | w.reach(t, 50, "released from last_move", func() bool { return w.claim.Op.Kind == "serving" }, w.recoveryPass) |
| 1047 | pg := &consolePlan{Kind: "purge", App: app0} |
| 1048 | w.reach(t, 20, "purge claimed the host", func() bool { return w.claim.Op.Kind == "purging" }, func() { w.runPlan(pg) }) |
| 1049 | w.resumeStaleRelease(src, old) // the goroutine wakes into its release |
| 1050 | w.tick() |
| 1051 | w.tick(func() { w.runPlan(pg) }) // the purge tears the store down |
| 1052 | w.tick(func() { w.runPlan(pg) }) |
| 1053 | } |
| 1054 | |
| 1055 | // resumeStaleRelease is a close's goroutine that stalled between the |
| 1056 | // record's close and the claim's release, resuming with the claim it read: |
| 1057 | // it revalidates (claim C3), then writes the release half. |
| 1058 | func (w *world) resumeStaleRelease(b *box, old *claim) { |
| 1059 | c, ok := w.readClaim(b) |
| 1060 | if !ok { |
| 1061 | return |
| 1062 | } |
| 1063 | if on("revalidate-before-effect") && !sameStep(old, c) { |
| 1064 | return |
| 1065 | } |
| 1066 | w.release(old, closeExec(old.Op)) |
| 1067 | } |
| 1068 | |
| 1069 | // wDirtyReturn (INV-2; also commit-before-open's witness): the target |
| 1070 | // writes during its probe and is rolled back. |
| 1071 | func wDirtyReturn(t *testing.T, w *world) { |
| 1072 | src, tgt := w.boxes[0], w.boxes[1] |
| 1073 | w.serve(src, 1, app0) |
| 1074 | w.landProbed(t, src, tgt) |
| 1075 | w.appWrite(tgt) |
| 1076 | w.replicate(tgt) // durable in the target's generation: no writes_lost declaration can cover it (rev 7.10) |
| 1077 | w.rollback(w.claim, "settle check failed") |
| 1078 | w.finish(t) |
| 1079 | } |
| 1080 | |
| 1081 | // wAdmissionTriple (J2-R2-8): an open from an earlier operation paused on |
| 1082 | // the source; it lands after the commit, while the source's row is still |
| 1083 | // held and before its park-local has run. |
| 1084 | func wAdmissionTriple(t *testing.T, w *world) { |
| 1085 | src, tgt := w.boxes[0], w.boxes[1] |
| 1086 | w.serve(src, 1, app0) |
| 1087 | d := &localWrite{kind: "open", holdOp: "p0", epoch: src.Epoch, at: 1 << 30} |
| 1088 | src.deferred = append(src.deferred, d) |
| 1089 | w.moveTo(tgt.Region) |
| 1090 | w.reach(t, 600, "committed", func() bool { return w.claim.Op.Committed }, func() { w.worker(src); w.worker(tgt) }, w.recoveryPass) |
| 1091 | d.at = w.now // the paused open lands now |
| 1092 | w.tick() |
| 1093 | w.wake(src) // a request reaches the old source |
| 1094 | w.checkStep() |
| 1095 | w.finish(t) |
| 1096 | } |
| 1097 | |
| 1098 | // wStrictSpawn (§6.1): the source runs a main process and a descendant |
| 1099 | // placed as its parent was. |
| 1100 | func wStrictSpawn(t *testing.T, w *world) { |
| 1101 | src, tgt := w.boxes[0], w.boxes[1] |
| 1102 | w.serve(src, 1, app0) |
| 1103 | w.wake(src) |
| 1104 | if !hasMain(src) { |
| 1105 | t.Fatalf("witness: source did not wake: %s", w.state()) |
| 1106 | } |
| 1107 | main := src.Procs[0] |
| 1108 | src.Procs = append(src.Procs, &proc{Main: false, Strict: main.Strict, Inc: 1, Gen: main.Gen, Session: main.Session, Box: src.ID}) |
| 1109 | w.moveTo(tgt.Region) |
| 1110 | w.finish(t) |
| 1111 | } |
| 1112 | |
| 1113 | // wTouchedIncomplete (claim §9, CC4): a legacy host with a pre-release |
| 1114 | // replica in another region is adopted, then deleted. |
| 1115 | func wTouchedIncomplete(t *testing.T, w *world) { |
| 1116 | b0 := w.boxes[0] |
| 1117 | w.legacy(b0, 1) |
| 1118 | w.tick(func() { w.reconcile(b0) }) // adoption |
| 1119 | if w.claim == nil { |
| 1120 | t.Fatalf("witness: not adopted") |
| 1121 | } |
| 1122 | w.reach(t, 400, "adoption settled", func() bool { return w.claim.oblFor("adopt") == 0 }, w.actAll(), w.recoveryPass) |
| 1123 | w.userDelete() |
| 1124 | w.finish(t) |
| 1125 | } |
| 1126 | |
| 1127 | // recreate deletes and frees the serving host, creates incarnation inc in |
| 1128 | // region r, and has it run and replicate. |
| 1129 | func (w *world) recreate(t *testing.T, r, inc int) { |
| 1130 | w.userDelete() |
| 1131 | w.reach(t, 600, "freed", func() bool { |
| 1132 | c := w.claim |
| 1133 | return c != nil && c.Holder == nil && c.Op.Kind == "" |
| 1134 | }, w.actAll(), w.runConsole, w.recoveryPass) |
| 1135 | w.console = append(w.console, &consolePlan{Kind: "create", Host: "h", App: app0, OpID: w.newID("cr"), Inc: inc, Region: r}) |
| 1136 | b := w.regionBox(r) |
| 1137 | w.reach(t, 200, "recreated", func() bool { |
| 1138 | c := w.claim |
| 1139 | return c.Holder != nil && c.Holder.Inc == inc && c.Op.Kind == "serving" && b.Row != nil |
| 1140 | }, w.runConsole, w.actAll(), w.recoveryPass) |
| 1141 | b.Config, b.CfgVer, b.Live, b.LiveInc = inc, w.cfgVer[app0], app0, inc // config sync and adoption have run |
| 1142 | // the first wake of the new incarnation's empty generation is a cold |
| 1143 | // recovery (claim rev 6.6 §6.4a): the box's role runs it, then the wake |
| 1144 | // admits the writer into the recovered generation |
| 1145 | if !w.reach(t, 400, "new incarnation running", func() bool { return hasMain(b) }, w.actAll(), func() { w.wake(b) }) { |
| 1146 | t.Fatalf("witness: the new incarnation did not run: %s", w.state()) |
| 1147 | } |
| 1148 | w.appWrite(b) |
| 1149 | w.appWrite(b) // two transactions: its first LTX file has the same key as the fixture's |
| 1150 | w.replicate(b) |
| 1151 | } |
| 1152 | |
| 1153 | // wDoorReread (claim §6.5 O2): a listing authorized before the delete |
| 1154 | // selects after the recreate. Retired from the table in rev 7.8: under |
| 1155 | // claim rev 6.6's writer epochs a recreated incarnation's first wake is a |
| 1156 | // cold recovery into a fresh generation, which a listing scoped to the |
| 1157 | // generation it was authorized for never selects, so the scenario holds |
| 1158 | // with C3a dropped too; C3a stays as defence in depth (§14.2.5). |
| 1159 | func wDoorReread(t *testing.T, w *world) { |
| 1160 | b0 := w.boxes[0] |
| 1161 | w.serve(b0, 1, app0) |
| 1162 | w.doorAuthorize() // O1 |
| 1163 | w.recreate(t, 0, 2) |
| 1164 | w.doorOpen() // select and O2 |
| 1165 | w.doorOpen() // open |
| 1166 | } |
| 1167 | |
| 1168 | // wDoorByVersion (claim §6.5): a listing selects and signs before the |
| 1169 | // delete, and the file request opens after the recreate. |
| 1170 | func wDoorByVersion(t *testing.T, w *world) { |
| 1171 | b0 := w.boxes[0] |
| 1172 | w.serve(b0, 1, app0) |
| 1173 | w.doorAuthorize() // O1 |
| 1174 | w.tick() |
| 1175 | w.tick() |
| 1176 | w.doorOpen() // select, O2, sign |
| 1177 | if len(w.doorReads) != 1 || !w.doorReads[0].Signed { |
| 1178 | t.Fatalf("witness: listing not signed") |
| 1179 | } |
| 1180 | w.recreate(t, 0, 2) |
| 1181 | w.doorOpen() // open |
| 1182 | } |
| 1183 | |
| 1184 | // wRegistrationCheck (CC21, claim §5.3): the first create of a host |
| 1185 | // registers and its console pauses; a purge of the app drains the expired |
| 1186 | // registration, tears the store down and finishes; the creator resumes. |
| 1187 | func wRegistrationCheck(t *testing.T, w *world) { |
| 1188 | p := &consolePlan{Kind: "create", Host: "h", App: app0, OpID: w.newID("cr"), Inc: 1, Region: 0} |
| 1189 | w.runPlan(p) // registered; the claim is absent |
| 1190 | for i := 0; i < 61; i++ { |
| 1191 | w.tick() |
| 1192 | } |
| 1193 | pg := &consolePlan{Kind: "purge", App: app0} |
| 1194 | done := false |
| 1195 | w.reach(t, 30, "purge done", func() bool { return done }, func() { |
| 1196 | if w.runPlan(pg) { |
| 1197 | done = true |
| 1198 | } |
| 1199 | }) |
| 1200 | for i := 0; i < 6; i++ { |
| 1201 | w.tick(func() { w.runPlan(p) }) // the creator resumes |
| 1202 | } |
| 1203 | } |
| 1204 | |
| 1205 | // ---------- rev 7.4 ---------- |
| 1206 | |
| 1207 | // wRoundTrip (claim rev 6 §6.4, R3-3): UK→US, then US→UK. The first |
| 1208 | // move's retirement wrote UK's local marker for the incarnation; the |
| 1209 | // second landing must replace it. Unmutated, the instance must serve on |
| 1210 | // UK again, running. |
| 1211 | func wRoundTrip(t *testing.T, w *world) { |
| 1212 | uk, us := w.boxes[0], w.boxes[1] |
| 1213 | w.serve(uk, 1, app0) |
| 1214 | w.moveTo(us.Region) |
| 1215 | w.reach(t, 1500, "serving on box 1 after the first move", func() bool { |
| 1216 | c := w.claim |
| 1217 | return c.Op.Kind == "serving" && c.Op.Exec == us.ID && w.rec != nil && w.rec.MoveID == "" && len(c.Obl) == 0 |
| 1218 | }, w.act(uk, us), w.recoveryPass) |
| 1219 | if st := uk.Stamps[1]; st == nil || st.Active != 0 || len(st.Retired) == 0 { |
| 1220 | t.Fatalf("witness: box 0 did not retire its installation: %+v %s%s", st, w.state(), w.boxesState()) |
| 1221 | } |
| 1222 | w.moveTo(uk.Region) |
| 1223 | if w.claim.Op.Kind != "moving" { |
| 1224 | t.Fatalf("witness: the move back did not start: %s", w.state()) |
| 1225 | } |
| 1226 | w.reach(t, 1500, "instance back on box 0, running", func() bool { |
| 1227 | c := w.claim |
| 1228 | return c.Op.Kind == "serving" && c.Op.Exec == uk.ID && hasMain(uk) |
| 1229 | }, w.act(uk, us), w.recoveryPass, w.operator) |
| 1230 | w.finish(t) |
| 1231 | } |
| 1232 | |
| 1233 | // runOthers runs every console plan but skip, one step each, removing |
| 1234 | // the finished ones. |
| 1235 | func (w *world) runOthers(skip *consolePlan) func() { |
| 1236 | return func() { w.runPlans(skip) } |
| 1237 | } |
| 1238 | |
| 1239 | // wOrphanOrder (claim rev 6 §5.1 step 5, R3-2): a cancelled create's |
| 1240 | // record lands late; the recovery pass starts its cleanup and pauses |
| 1241 | // after its first observation; a create of the next incarnation removes |
| 1242 | // the orphan itself, claims and publishes; the paused cleanup resumes. |
| 1243 | func wOrphanOrder(t *testing.T, w *world) { |
| 1244 | w.claim = &claim{Ver: w.newVer(), Retired: []int{1}, Cancelled: []cancelledCreate{{Inc: 1, Until: w.now + 1000}}} |
| 1245 | w.nextInc = 1 |
| 1246 | w.rec = &record{Ver: w.newVer(), Inc: 1, App: app0, Region: 0} |
| 1247 | w.logf("witness: the record of cancelled incarnation 1 landed") |
| 1248 | w.recoveryPass() |
| 1249 | var p1 *consolePlan |
| 1250 | for _, p := range w.console { |
| 1251 | if p.Kind == "orphan" { |
| 1252 | p1 = p |
| 1253 | } |
| 1254 | } |
| 1255 | if p1 == nil { |
| 1256 | t.Fatalf("witness: the recovery pass started no cleanup: %s", w.state()) |
| 1257 | } |
| 1258 | w.tick(func() { w.runPlan(p1) }) // the first observation; then the console pauses |
| 1259 | cr := &consolePlan{Kind: "create", Host: "h", App: app0, OpID: w.newID("cr"), Inc: 2, Region: 0} |
| 1260 | w.console = append(w.console, cr) |
| 1261 | w.reach(t, 50, "incarnation 2 claimed and published", func() bool { |
| 1262 | return w.rec != nil && w.rec.Inc == 2 |
| 1263 | }, w.runOthers(p1)) |
| 1264 | w.tick(func() { w.runPlan(p1) }) // the paused cleanup resumes |
| 1265 | w.tick(func() { w.runPlan(p1) }) |
| 1266 | w.finish(t) |
| 1267 | } |
| 1268 | |
| 1269 | // wSweepNamespace (claim rev 6 §6.2a, R3-4): a replication PUT of |
| 1270 | // incarnation 1 is accepted and completes after 33 delete-and-recreate |
| 1271 | // cycles, by which time retired_incarnations no longer lists 1. |
| 1272 | func wSweepNamespace(t *testing.T, w *world) { |
| 1273 | b := w.boxes[0] |
| 1274 | w.serve(b, 1, app0) |
| 1275 | w.wake(b) |
| 1276 | if !hasMain(b) { |
| 1277 | t.Fatalf("witness: the host did not wake: %s", w.state()) |
| 1278 | } |
| 1279 | w.appWrite(b) |
| 1280 | key := dataKey(w.claim.Holder.Location, "", "") + "0000/" |
| 1281 | w.holdKey(key) |
| 1282 | w.replicate(b) |
| 1283 | w.hold = nil |
| 1284 | for inc := 2; inc <= retiredCap+2; inc++ { |
| 1285 | w.recreate(t, 0, inc) |
| 1286 | if len(w.violations) > 0 { |
| 1287 | return |
| 1288 | } |
| 1289 | } |
| 1290 | if contains(w.claim.Retired, 1) { |
| 1291 | t.Fatalf("witness: incarnation 1 is still in retired_incarnations after %d recreates", retiredCap+1) |
| 1292 | } |
| 1293 | if w.completeHeld(key) != 1 { |
| 1294 | t.Fatalf("witness: no held replication PUT") |
| 1295 | } |
| 1296 | w.finish(t) |
| 1297 | } |
| 1298 | |
| 1299 | // wCommitBeforeOpen (INV-5, R3-5): a public request reaches the target's |
| 1300 | // edge while its probe runs. The edge routes on the row. |
| 1301 | func wCommitBeforeOpen(t *testing.T, w *world) { |
| 1302 | src, tgt := w.boxes[0], w.boxes[1] |
| 1303 | w.serve(src, 1, app0) |
| 1304 | w.landProbed(t, src, tgt) |
| 1305 | w.wake(tgt) |
| 1306 | w.checkStep() |
| 1307 | w.finish(t) |
| 1308 | } |
| 1309 | |
| 1310 | // wRecoveryInputs (§7.8, R2-5): a config bundle is published after the |
| 1311 | // move was admitted; the target does real work and the rollback is |
| 1312 | // dirty; the source's recovery install must render current inputs, not |
| 1313 | // the inputs the move pinned. |
| 1314 | func wRecoveryInputs(t *testing.T, w *world) { |
| 1315 | src, tgt := w.boxes[0], w.boxes[1] |
| 1316 | w.serve(src, 1, app0) |
| 1317 | w.landProbed(t, src, tgt) |
| 1318 | w.cfgVer[app0]++ |
| 1319 | w.logf("witness: config bundle %s v%d published during the settle window", app0, w.cfgVer[app0]) |
| 1320 | w.appWrite(tgt) |
| 1321 | w.rollback(w.claim, "settle check failed") |
| 1322 | w.finish(t) |
| 1323 | } |
| 1324 | |
| 1325 | // ---------- rev 7.5 ---------- |
| 1326 | |
| 1327 | // roundTrip moves the host UK→US→UK and requires it to serve on UK again, |
| 1328 | // running. |
| 1329 | func (w *world) roundTrip(t *testing.T, uk, us *box) { |
| 1330 | w.moveTo(us.Region) |
| 1331 | w.reach(t, 1500, "serving on box 1 after the first move", func() bool { |
| 1332 | c := w.claim |
| 1333 | return c.Op.Kind == "serving" && c.Op.Exec == us.ID && w.rec != nil && w.rec.MoveID == "" && len(c.Obl) == 0 |
| 1334 | }, w.act(uk, us), w.recoveryPass) |
| 1335 | w.moveTo(uk.Region) |
| 1336 | if w.claim.Op.Kind != "moving" { |
| 1337 | t.Fatalf("witness: the move back did not start: %s", w.state()) |
| 1338 | } |
| 1339 | w.reach(t, 1500, "instance back on box 0, running", func() bool { |
| 1340 | c := w.claim |
| 1341 | return c.Op.Kind == "serving" && c.Op.Exec == uk.ID && hasMain(uk) |
| 1342 | }, w.act(uk, us), w.recoveryPass, w.operator) |
| 1343 | } |
| 1344 | |
| 1345 | // wStaleWriter (claim rev 6.5 §6.4, R4-2): a config-sync pass selects the |
| 1346 | // row under the first installation and pauses; the host moves away and |
| 1347 | // back; a new bundle is published; the pass takes the guard. |
| 1348 | func wStaleWriter(t *testing.T, w *world) { |
| 1349 | uk, us := w.boxes[0], w.boxes[1] |
| 1350 | w.serve(uk, 1, app0) |
| 1351 | w.passPlan(uk, "config") |
| 1352 | if len(uk.plans) != 1 { |
| 1353 | t.Fatalf("witness: no plan") |
| 1354 | } |
| 1355 | p := uk.plans[0] |
| 1356 | p.At = 1 << 30 // paused |
| 1357 | w.roundTrip(t, uk, us) |
| 1358 | if len(w.violations) > 0 { |
| 1359 | return |
| 1360 | } |
| 1361 | w.cfgVer[app0]++ |
| 1362 | p.At = w.now // the pass resumes and takes the guard |
| 1363 | w.tick(func() { w.passExec(uk) }) |
| 1364 | w.finish(t) |
| 1365 | } |
| 1366 | |
| 1367 | // wLiveSetRegion (claim rev 6.5 §6.2a, R4-3): a legacy host serves in UK |
| 1368 | // (box 0) with a pre-release replica in US (box 1). Adoption's discovery |
| 1369 | // parks US. A replication PUT the old US executor issued before the |
| 1370 | // retirement completes after it. |
| 1371 | func wLiveSetRegion(t *testing.T, w *world) { |
| 1372 | uk, us := w.boxes[0], w.boxes[1] |
| 1373 | w.legacy(uk, us.Region) |
| 1374 | // the old US executor's last replication PUT, accepted, completing late |
| 1375 | late := &blob{Kind: "ltx", Level: 0, Min: 2, Max: 2, Inc: 0, SealKey: 7, Pages: cloneState(uk.DB.State)} |
| 1376 | w.pending = append(w.pending, &request{kind: rPut, region: us.Region, key: ltxKey("instances/"+host+"/", "", 0, 2, 2), b: late, doneAt: 1 << 30, by: "box:1"}) |
| 1377 | w.tick(func() { w.reconcile(uk) }) // adoption |
| 1378 | if w.claim == nil { |
| 1379 | t.Fatalf("witness: not adopted") |
| 1380 | } |
| 1381 | w.reach(t, 400, "discovery settled", func() bool { return w.claim.oblFor("adopt") == 0 }, w.actAll(), w.recoveryPass) |
| 1382 | if w.completeHeld(ltxKey("instances/"+host+"/", "", 0, 2, 2)) != 1 { |
| 1383 | t.Fatalf("witness: no held PUT") |
| 1384 | } |
| 1385 | w.finish(t) |
| 1386 | } |
| 1387 | |
| 1388 | // pushed installs a push generation on b: the host serves from a snapshot |
| 1389 | // at its current TXID, then runs again, so the witness can shape the |
| 1390 | // generation's LTX files by hand. |
| 1391 | func (w *world) pushed(t *testing.T, b *box) (loc, gen string) { |
| 1392 | w.userPush() |
| 1393 | gen = w.claim.Op.ID |
| 1394 | w.reach(t, 400, "push released", func() bool { return w.claim.Op.Kind == "serving" }, w.act(b)) |
| 1395 | w.idleStop(b) |
| 1396 | // the wake after the push: under a mutation it may be a cold recovery |
| 1397 | // first (claim rev 6.6 §6.4a), which the box's role runs |
| 1398 | if !w.reach(t, 60, "woken after the push", func() bool { return hasMain(b) }, w.act(b), func() { w.wake(b) }) { |
| 1399 | t.Fatalf("witness: the host did not wake after the push: %s%s", w.state(), w.boxesState()) |
| 1400 | } |
| 1401 | return w.claim.Holder.Location, gen |
| 1402 | } |
| 1403 | |
| 1404 | // compactedPending builds the level-1 file [min, max], in replication |
| 1405 | // numbering, that compaction would have left for b's pending writes: the |
| 1406 | // final image of every key they touched. The witness places it where |
| 1407 | // compaction would and advances the position past it. |
| 1408 | func (w *world) compactedPending(b *box, min, max int) *blob { |
| 1409 | db := b.DB |
| 1410 | out := &blob{Kind: "ltx", Level: 1, Min: min, Max: max, Inc: db.Inc, Gen: db.Gen, SealKey: db.Key, Pages: map[string]int{}} |
| 1411 | for _, wr := range db.Pending { |
| 1412 | t := w.txs[wr] |
| 1413 | out.Pages[t.Key] = db.State[t.Key] |
| 1414 | out.TXs = append(out.TXs, wr) |
| 1415 | } |
| 1416 | db.Pos, db.Pending = max, nil |
| 1417 | return out |
| 1418 | } |
| 1419 | |
| 1420 | // wRestoreOverlap (R4-1): after a push the generation's snapshot ends at |
| 1421 | // TXID 11 (two writes, eight more, the push's mark). The host writes four |
| 1422 | // more; compaction has left one current file [10,15] and no level-0 |
| 1423 | // files. The disk is lost and the host wakes cold. |
| 1424 | func wRestoreOverlap(t *testing.T, w *world) { |
| 1425 | b := w.boxes[0] |
| 1426 | w.serve(b, 1, app0) |
| 1427 | w.wake(b) |
| 1428 | for i := 0; i < 8; i++ { |
| 1429 | w.appWrite(b) |
| 1430 | } |
| 1431 | w.replicate(b) |
| 1432 | loc, gen := w.pushed(t, b) |
| 1433 | if len(w.violations) > 0 { |
| 1434 | return |
| 1435 | } |
| 1436 | n := b.DB.Pos // the snapshot's TXID after the push, in replication numbering |
| 1437 | for i := 0; i < 4; i++ { |
| 1438 | w.appWrite(b) |
| 1439 | } |
| 1440 | // compaction has left one file [n-1, n+2] overlapping the snapshot |
| 1441 | f := w.compactedPending(b, n-1, n+2) |
| 1442 | w.buckets[b.Region].objs[ltxKey(loc, gen, 1, n-1, n+2)] = []*version{{ID: w.newVer(), B: f}} |
| 1443 | w.markDurable(ltxKey(loc, gen, 1, n-1, n+2), f) |
| 1444 | w.idleStop(b) |
| 1445 | b.DB = nil // the disk is lost; the next wake restores cold |
| 1446 | w.logf("witness: box %d lost its database; the generation holds the snapshot at %d and [%d,%d]", b.ID, n, n-1, n+2) |
| 1447 | w.reach(t, 60, "woken cold", func() bool { return hasMain(b) }, w.act(b), func() { w.wake(b) }) |
| 1448 | w.finish(t) |
| 1449 | } |
| 1450 | |
| 1451 | // wRestoreGap (R4-1): the same generation with a genuine gap: the file |
| 1452 | // [12,12] never landed and [13,13] is current. The restore must refuse. |
| 1453 | func wRestoreGap(t *testing.T, w *world) { |
| 1454 | b := w.boxes[0] |
| 1455 | w.serve(b, 1, app0) |
| 1456 | w.wake(b) |
| 1457 | for i := 0; i < 8; i++ { |
| 1458 | w.appWrite(b) |
| 1459 | } |
| 1460 | w.replicate(b) |
| 1461 | loc, gen := w.pushed(t, b) |
| 1462 | if len(w.violations) > 0 { |
| 1463 | return |
| 1464 | } |
| 1465 | n := b.DB.Pos |
| 1466 | w.appWrite(b) // its file, [n+1, n+1], never lands |
| 1467 | b.DB.Pos, b.DB.Pending = n+1, nil |
| 1468 | w.appWrite(b) |
| 1469 | f := w.compactedPending(b, n+2, n+2) // [n+2, n+2] is current |
| 1470 | w.buckets[b.Region].objs[ltxKey(loc, gen, 0, n+2, n+2)] = []*version{{ID: w.newVer(), B: f}} |
| 1471 | w.idleStop(b) |
| 1472 | db := w.restoreCalc(b.Region, 1, loc, gen) |
| 1473 | if db != nil { |
| 1474 | w.violate("INV-2 (cold restore): a restore across the gap after TXID %d returned a database at position %d", n, db.Pos) |
| 1475 | } |
| 1476 | } |
| 1477 | |
| 1478 | // ---------- rev 7.6 ---------- |
| 1479 | |
| 1480 | // wSnapshotOnlyInstall (R5-1): the push installs a snapshot; the host |
| 1481 | // wakes, writes, replicates, loses its disk and wakes cold. |
| 1482 | func wSnapshotOnlyInstall(t *testing.T, w *world) { |
| 1483 | b := w.boxes[0] |
| 1484 | w.serve(b, 1, app0) |
| 1485 | w.wake(b) |
| 1486 | for i := 0; i < 3; i++ { |
| 1487 | w.appWrite(b) |
| 1488 | } |
| 1489 | w.replicate(b) |
| 1490 | // the push's probe process goes on serving after the release (no |
| 1491 | // clean close in between: a clean close would write a marker whose |
| 1492 | // max_txid betrays the missing anchor and force a recovery first) |
| 1493 | w.userPush() |
| 1494 | w.reach(t, 400, "push released", func() bool { return w.claim.Op.Kind == "serving" }, w.act(b)) |
| 1495 | if len(w.violations) > 0 || !hasMain(b) { |
| 1496 | return |
| 1497 | } |
| 1498 | for i := 0; i < 2; i++ { |
| 1499 | w.appWrite(b) |
| 1500 | w.replicate(b) |
| 1501 | } |
| 1502 | // the writer dies with its disk (a clean close would write a marker |
| 1503 | // whose max_txid, 2, is behind the snapshot's 3 and force a cold |
| 1504 | // recovery from the warm database, which hides the missing anchor) |
| 1505 | w.crash(b) |
| 1506 | w.loseDisk(b) |
| 1507 | w.logf("witness: box %d lost its database after replicating past the push's snapshot", b.ID) |
| 1508 | w.reach(t, 60, "woken cold", func() bool { return hasMain(b) }, w.act(b), func() { w.wake(b) }) |
| 1509 | w.finish(t) |
| 1510 | } |
| 1511 | |
| 1512 | // wRootAdvance (R5-3): after the push, enough writes and replication for |
| 1513 | // compaction to rotate snapshots four times, retention expiring the files |
| 1514 | // that continued from the pinned snapshot; then the disk is lost. |
| 1515 | func wRootAdvance(t *testing.T, w *world) { |
| 1516 | b := w.boxes[0] |
| 1517 | w.serve(b, 1, app0) |
| 1518 | w.wake(b) |
| 1519 | w.appWrite(b) |
| 1520 | w.replicate(b) |
| 1521 | loc, gen := w.pushed(t, b) |
| 1522 | if len(w.violations) > 0 { |
| 1523 | return |
| 1524 | } |
| 1525 | for round := 0; round < 4; round++ { |
| 1526 | for i := 0; i < 3; i++ { |
| 1527 | w.appWrite(b) |
| 1528 | w.replicate(b) |
| 1529 | } |
| 1530 | } |
| 1531 | snaps := w.currentLTX(w.buckets[b.Region], dataKey(loc, gen, ""), 9) |
| 1532 | if len(snaps) == 0 || snaps[len(snaps)-1].B.Max <= w.buckets[b.Region].current(genMarkerKey(loc)).B.TX { |
| 1533 | t.Fatalf("witness: no successor snapshot rotated in: %d snapshots", len(snaps)) |
| 1534 | } |
| 1535 | w.idleStop(b) |
| 1536 | b.DB = nil // the disk is lost |
| 1537 | w.logf("witness: box %d lost its database after four rotations", b.ID) |
| 1538 | w.reach(t, 60, "woken cold", func() bool { return hasMain(b) }, w.act(b), func() { w.wake(b) }) |
| 1539 | w.finish(t) |
| 1540 | } |
| 1541 | |
| 1542 | // ---------- rev 7.7 ---------- |
| 1543 | |
| 1544 | // wAnchorHeld (R6-1): the push's install writes its anchor and the PUT is |
| 1545 | // slow. Until it is acknowledged the host must not open replication: the |
| 1546 | // position litestream would read from the listing is 0. |
| 1547 | func wAnchorHeld(t *testing.T, w *world) { |
| 1548 | b := w.boxes[0] |
| 1549 | w.serve(b, 1, app0) |
| 1550 | w.wake(b) |
| 1551 | for i := 0; i < 3; i++ { |
| 1552 | w.appWrite(b) |
| 1553 | } |
| 1554 | w.replicate(b) |
| 1555 | w.userPush() |
| 1556 | gen := w.claim.Op.ID |
| 1557 | loc := w.claim.Holder.Location |
| 1558 | // the build (R7-4): the snapshot is acknowledged, the anchor is next; |
| 1559 | // the witness holds the anchor PUT there |
| 1560 | w.reach(t, 400, "push building its anchor", func() bool { |
| 1561 | return w.claim.Op.Kind == "pushing" && w.claim.Op.Phase == "install-anchor" |
| 1562 | }, w.act(b)) |
| 1563 | n := w.claim.Op.BaseTX |
| 1564 | anchor := ltxKey(loc, gen, 0, n, n) |
| 1565 | w.holdKey(anchor) |
| 1566 | prefix := dataKey(loc, gen, "") |
| 1567 | for i := 0; i < 40; i++ { |
| 1568 | w.tick(w.act(b)) |
| 1569 | if len(w.violations) > 0 { |
| 1570 | return // INV-11: published before the anchor landed |
| 1571 | } |
| 1572 | for _, f := range w.currentLTX(w.buckets[b.Region], prefix, 0) { |
| 1573 | if f.B.Min != n { |
| 1574 | w.violate("INV-2 (witness): box %d replicated [%d,%d] before its anchor [%d,%d] was acknowledged", b.ID, f.B.Min, f.B.Max, n, n) |
| 1575 | return |
| 1576 | } |
| 1577 | } |
| 1578 | if hasMain(b) { |
| 1579 | w.violate("INV-2 (witness): box %d opened replication before its anchor [%d,%d] was acknowledged; litestream's position would be %d", b.ID, n, n, w.maxL0(w.buckets[b.Region], prefix)) |
| 1580 | return |
| 1581 | } |
| 1582 | } |
| 1583 | w.hold = nil |
| 1584 | if w.completeHeld(anchor) == 0 { |
| 1585 | t.Fatalf("witness: no anchor PUT was held: %s", w.state()) |
| 1586 | } |
| 1587 | w.reach(t, 400, "push released", func() bool { return w.claim.Op.Kind == "serving" }, w.act(b)) |
| 1588 | w.idleStop(b) |
| 1589 | w.reach(t, 60, "woken after the push", func() bool { return hasMain(b) }, w.act(b), func() { w.wake(b) }) |
| 1590 | for i := 0; i < 2; i++ { |
| 1591 | w.appWrite(b) |
| 1592 | w.replicate(b) |
| 1593 | } |
| 1594 | w.idleStop(b) |
| 1595 | b.DB = nil // the disk is lost |
| 1596 | w.reach(t, 60, "woken cold", func() bool { return hasMain(b) }, w.act(b), func() { w.wake(b) }) |
| 1597 | w.finish(t) |
| 1598 | } |
| 1599 | |
| 1600 | // wReturnLostRecord (claim rev 6.5, R6-4): a dirty rollback; the source's |
| 1601 | // local stamp record is lost before the return. The return CAS writes the |
| 1602 | // source installation's stamp back into holder.stamp, the source |
| 1603 | // re-initializes from it, installs the return generation under it, and its |
| 1604 | // probe CAS issues the new stamp, which retires it. |
| 1605 | func wReturnLostRecord(t *testing.T, w *world) { |
| 1606 | src, tgt := w.boxes[0], w.boxes[1] |
| 1607 | w.serve(src, 1, app0) |
| 1608 | s := src.stampOf(1) |
| 1609 | w.landProbed(t, src, tgt) |
| 1610 | w.appWrite(tgt) |
| 1611 | w.rollback(w.claim, "settle check failed") |
| 1612 | w.reach(t, 400, "target returned", func() bool { return w.claim.Op.Phase == "returned" }, w.act(tgt)) |
| 1613 | src.Stamps = nil |
| 1614 | w.logf("witness: box %d lost its local stamp record", src.ID) |
| 1615 | w.finish(t) |
| 1616 | if len(w.violations) > 0 { |
| 1617 | return |
| 1618 | } |
| 1619 | c := w.claim |
| 1620 | if c == nil || c.Holder == nil || c.Op.Exec != src.ID { |
| 1621 | t.Fatalf("witness: the source does not serve after the rollback: %s", w.state()) |
| 1622 | } |
| 1623 | act := src.stampOf(1) |
| 1624 | switch { |
| 1625 | case act != c.Holder.Stamp: |
| 1626 | w.violate("INV-6 (witness): box %d active stamp %d, holder.stamp %d", src.ID, act, c.Holder.Stamp) |
| 1627 | case src.DB == nil || src.DB.Stamp != act: |
| 1628 | w.violate("INV-6 (witness): box %d database tagged %d, active %d", src.ID, dbStamp(src.DB), act) |
| 1629 | case act == s || !contains(src.Stamps[1].Retired, s): |
| 1630 | w.violate("INV-6 (witness): the pre-move stamp %d did not retire when %d activated on box %d", s, act, src.ID) |
| 1631 | } |
| 1632 | } |
| 1633 | |
| 1634 | // ---------- rev 7.8 ---------- |
| 1635 | |
| 1636 | // crash is the agent dying with its processes (an OOM kill, a crash): what |
| 1637 | // it had in flight is unaccounted for, and the restarted agent knows |
| 1638 | // nothing of it (forget). Nothing cleans up, so no closed.json. |
| 1639 | func (w *world) crash(b *box) { |
| 1640 | b.Procs = nil |
| 1641 | b.forget() |
| 1642 | w.logf("witness: box %d's agent crashed", b.ID) |
| 1643 | } |
| 1644 | |
| 1645 | // loseDisk is the disk-loss fault: the database file is gone, and every |
| 1646 | // acknowledged write not yet durable anywhere is declared lost (exempt). |
| 1647 | func (w *world) loseDisk(b *box) { |
| 1648 | if b.DB == nil { |
| 1649 | return |
| 1650 | } |
| 1651 | // physical loss only (R10-6): the next admission declares the writes |
| 1652 | b.DB = nil |
| 1653 | w.logf("witness: box %d lost its database file", b.ID) |
| 1654 | } |
| 1655 | |
| 1656 | // appWriteKey is one acknowledged application write of key = val (0 is a |
| 1657 | // delete) by b's main process. |
| 1658 | func (w *world) appWriteKey(b *box, key string, val int) int { |
| 1659 | if !hasMain(b) { |
| 1660 | panic("appWriteKey: no main process") |
| 1661 | } |
| 1662 | p := b.Procs[0] |
| 1663 | w.nextW++ |
| 1664 | wr := w.nextW |
| 1665 | db := b.DB |
| 1666 | t := tx{W: wr, Key: key, Val: val} |
| 1667 | if val == 0 { |
| 1668 | delete(db.State, key) |
| 1669 | } else { |
| 1670 | db.State[key] = val |
| 1671 | } |
| 1672 | db.TX++ |
| 1673 | t.TX = db.TX |
| 1674 | db.Pending = append(db.Pending, wr) |
| 1675 | db.Log = append(db.Log, wr) |
| 1676 | w.txs[wr] = t |
| 1677 | sess, gen := w.sessionOf(b) |
| 1678 | w.acks = append(w.acks, ack{W: wr, Inc: p.Inc, Box: b.ID, Session: sess, Gen: gen, At: w.now, Kind: "write"}) |
| 1679 | w.writeInc[wr] = p.Inc |
| 1680 | w.logf("witness: box %d wrote %d: %s = %d", b.ID, wr, key, val) |
| 1681 | return wr |
| 1682 | } |
| 1683 | |
| 1684 | // recovered drives the box until it runs again: a cold recovery first, |
| 1685 | // when its replication state was lost, then the wake. |
| 1686 | // sessionOf is the writer session and generation b's database was admitted |
| 1687 | // under: what its acknowledgements carry (rev 7.13, R12-1). |
| 1688 | func (w *world) sessionOf(b *box) (int, string) { |
| 1689 | if b.DB == nil { |
| 1690 | return 0, "" |
| 1691 | } |
| 1692 | return b.DB.Session, b.DB.Gen |
| 1693 | } |
| 1694 | |
| 1695 | func (w *world) recovered(t *testing.T, b *box, what string) { |
| 1696 | if !w.reach(t, 120, what, func() bool { return hasMain(b) }, w.act(b), w.recoveryPass, func() { w.wake(b) }) { |
| 1697 | t.Fatalf("witness: %s: the host did not run again: %s%s", what, w.state(), w.boxesState()) |
| 1698 | } |
| 1699 | } |
| 1700 | |
| 1701 | // deadWriter is the common opening of the R7-1 witnesses: the serving box |
| 1702 | // writes once more, its level-0 upload for that write is held in flight, |
| 1703 | // and the box dies with its disk. It returns the held key. |
| 1704 | func (w *world) deadWriter(t *testing.T, b *box) string { |
| 1705 | w.serve(b, 1, app0) |
| 1706 | w.wake(b) |
| 1707 | loc := w.claim.Holder.Location |
| 1708 | w.appWrite(b) |
| 1709 | key := ltxKey(loc, "", 0, b.DB.Pos+1, b.DB.Pos+1) |
| 1710 | w.holdKey(key) |
| 1711 | w.replicate(b) // A's upload: accepted, outstanding |
| 1712 | w.hold = nil |
| 1713 | w.crash(b) |
| 1714 | w.loseDisk(b) |
| 1715 | return key |
| 1716 | } |
| 1717 | |
| 1718 | // wLateUploadAfter (R7-1): A's outstanding upload lands after B uploaded |
| 1719 | // its own file for the same TXID. |
| 1720 | func wLateUploadAfter(t *testing.T, w *world) { |
| 1721 | b := w.boxes[0] |
| 1722 | key := w.deadWriter(t, b) |
| 1723 | w.recovered(t, b, "B running after A's death") |
| 1724 | w.appWrite(b) |
| 1725 | w.replicate(b) // B's upload |
| 1726 | if w.completeHeld(key) == 0 { |
| 1727 | t.Fatalf("witness: A's upload was not held") |
| 1728 | } |
| 1729 | w.checkDurable(w.claim, "after A's late upload landed") // before any snapshot of the warm database repairs the replica |
| 1730 | w.finish(t) |
| 1731 | } |
| 1732 | |
| 1733 | // wLateUploadRace (R7-1): A's outstanding upload lands after B |
| 1734 | // initialized its position and before B's own upload for that TXID. |
| 1735 | func wLateUploadRace(t *testing.T, w *world) { |
| 1736 | b := w.boxes[0] |
| 1737 | key := w.deadWriter(t, b) |
| 1738 | w.recovered(t, b, "B running after A's death") |
| 1739 | if w.completeHeld(key) == 0 { |
| 1740 | t.Fatalf("witness: A's upload was not held") |
| 1741 | } |
| 1742 | w.appWrite(b) |
| 1743 | w.replicate(b) // B's upload, or litestream's skip at the remote position |
| 1744 | w.checkDurable(w.claim, "after B's upload") |
| 1745 | w.finish(t) |
| 1746 | } |
| 1747 | |
| 1748 | // wExemptKeyRestored (R7-2): A's in-flight write updated K; B durably |
| 1749 | // updates K; A's stale upload lands and restores A's value. |
| 1750 | func wExemptKeyRestored(t *testing.T, w *world) { |
| 1751 | b := w.boxes[0] |
| 1752 | w.serve(b, 1, app0) |
| 1753 | w.wake(b) |
| 1754 | loc := w.claim.Holder.Location |
| 1755 | k := fmt.Sprintf("k%d", b.DB.Log[0]) // a key the fixture wrote |
| 1756 | w.appWriteKey(b, k, 99) |
| 1757 | key := ltxKey(loc, "", 0, b.DB.Pos+1, b.DB.Pos+1) |
| 1758 | w.holdKey(key) |
| 1759 | w.replicate(b) |
| 1760 | w.hold = nil |
| 1761 | w.crash(b) |
| 1762 | w.loseDisk(b) // A's update of K is declared lost |
| 1763 | w.recovered(t, b, "B running after A's death") |
| 1764 | w.appWriteKey(b, k, 77) // B's durable update of K |
| 1765 | w.replicate(b) |
| 1766 | if w.completeHeld(key) == 0 { |
| 1767 | t.Fatalf("witness: A's upload was not held") |
| 1768 | } |
| 1769 | w.checkDurable(w.claim, "after A's stale upload landed") |
| 1770 | w.finish(t) |
| 1771 | } |
| 1772 | |
| 1773 | // wCrashBeforeMarker (claim rev 6.6 §6.4a): a clean stop drains its |
| 1774 | // uploads, then the agent crashes before closed.json is written; the next |
| 1775 | // wake must be a cold recovery. |
| 1776 | func wCrashBeforeMarker(t *testing.T, w *world) { |
| 1777 | b := w.boxes[0] |
| 1778 | w.serve(b, 1, app0) |
| 1779 | w.wake(b) |
| 1780 | gen := w.claim.Holder.Gen |
| 1781 | w.appWrite(b) |
| 1782 | key := ltxKey(w.claim.Holder.Location, "", 0, b.DB.Pos+1, b.DB.Pos+1) |
| 1783 | w.holdKey(key) |
| 1784 | w.idleStop(b) // closing: the upload is outstanding, no marker yet |
| 1785 | w.hold = nil |
| 1786 | w.completeHeld(key) // the upload returns |
| 1787 | w.crash(b) // before closeStep ran again: no closed.json |
| 1788 | if on("recovery-generation") && w.buckets[b.Region].current(closedKey(w.claim.Holder.Location, gen, w.claim.Holder.Session)) != nil { |
| 1789 | t.Fatalf("witness: a certificate exists after the crash") |
| 1790 | } |
| 1791 | w.recovered(t, b, "running after the crash") |
| 1792 | if w.claim.Holder.Gen == gen { |
| 1793 | w.violate("INV-2 (witness): no cold recovery after a crash left generation %q without closed.json; box %d continued it", gen, b.ID) |
| 1794 | return |
| 1795 | } |
| 1796 | w.finish(t) |
| 1797 | } |
| 1798 | |
| 1799 | // wStaleMarker (claim rev 6.6 §6.4a): a closed.json whose max_txid is |
| 1800 | // behind the remote maximum, beside a dead writer's outstanding upload. |
| 1801 | func wStaleMarker(t *testing.T, w *world) { |
| 1802 | b := w.boxes[0] |
| 1803 | w.serve(b, 1, app0) |
| 1804 | w.wake(b) // consumes the fixture's marker as it opens |
| 1805 | loc := w.claim.Holder.Location |
| 1806 | key := w.deadWriterContinues(b, loc) // [2,2] in flight; the remote maximum is 1 |
| 1807 | // a stale certificate for the current session: a late PUT of a close |
| 1808 | // that said 0, behind the remote maximum, beside the dead writer's |
| 1809 | // outstanding upload |
| 1810 | sk := closedKey(loc, "", w.claim.Holder.Session) |
| 1811 | w.buckets[b.Region].objs[sk] = append(w.buckets[b.Region].objs[sk], |
| 1812 | &version{ID: w.newVer(), B: &blob{Kind: "closed", Inc: 1, Stamp: b.stampOf(1), Seq: b.ID, Session: w.claim.Holder.Session, TX: 0}}) |
| 1813 | w.recovered(t, b, "B running after A's death") |
| 1814 | w.appWrite(b) |
| 1815 | w.replicate(b) |
| 1816 | if w.completeHeld(key) == 0 { |
| 1817 | t.Fatalf("witness: A's upload was not held") |
| 1818 | } |
| 1819 | w.checkDurable(w.claim, "after A's late upload landed") |
| 1820 | w.finish(t) |
| 1821 | } |
| 1822 | |
| 1823 | // deadWriterContinues: the running writer writes once more with its |
| 1824 | // upload held, then dies with its disk; the held key is returned. |
| 1825 | func (w *world) deadWriterContinues(b *box, loc string) string { |
| 1826 | w.appWrite(b) |
| 1827 | key := ltxKey(loc, b.DB.Gen, 0, b.DB.Pos+1, b.DB.Pos+1) |
| 1828 | w.holdKey(key) |
| 1829 | w.replicate(b) |
| 1830 | w.hold = nil |
| 1831 | w.crash(b) |
| 1832 | w.loseDisk(b) |
| 1833 | return key |
| 1834 | } |
| 1835 | |
| 1836 | // wCloseWaits (claim rev 6.6 §6.4a): a clean stop with an upload in |
| 1837 | // flight writes no closed.json until the upload returned. |
| 1838 | func wCloseWaits(t *testing.T, w *world) { |
| 1839 | b := w.boxes[0] |
| 1840 | w.serve(b, 1, app0) |
| 1841 | w.wake(b) |
| 1842 | loc := w.claim.Holder.Location |
| 1843 | w.appWrite(b) |
| 1844 | key := ltxKey(loc, "", 0, b.DB.Pos+1, b.DB.Pos+1) |
| 1845 | w.holdKey(key) |
| 1846 | w.idleStop(b) |
| 1847 | sk := closedKey(loc, "", b.DB.Session) |
| 1848 | for i := 0; i < uploadTimeout-2; i++ { // short of the client's timeout: a retry would make this session uncertain for good (R8-5) |
| 1849 | w.tick(func() { w.replicate(b) }) |
| 1850 | if w.buckets[b.Region].current(sk) != nil { |
| 1851 | w.violate("INV-2 (witness): box %d wrote its certificate before every upload returned (%s is in flight)", b.ID, key) |
| 1852 | return |
| 1853 | } |
| 1854 | } |
| 1855 | w.hold = nil |
| 1856 | if w.completeHeld(key) == 0 { |
| 1857 | t.Fatalf("witness: the upload was not held") |
| 1858 | } |
| 1859 | w.tick(func() { w.replicate(b) }) |
| 1860 | if w.buckets[b.Region].current(sk) == nil { |
| 1861 | t.Fatalf("witness: no certificate after the uploads returned") |
| 1862 | } |
| 1863 | // the writer continues the generation: no upload of its previous run |
| 1864 | // can be outstanding, every one returned before the marker |
| 1865 | w.recovered(t, b, "continued after the clean close") |
| 1866 | if w.claim.Holder.Gen != "" { |
| 1867 | t.Fatalf("witness: a cold recovery after a clean close") |
| 1868 | } |
| 1869 | w.appWrite(b) |
| 1870 | w.replicate(b) |
| 1871 | w.finish(t) |
| 1872 | } |
| 1873 | |
| 1874 | // wNewestL0 (R7-3): the local position runs ahead of the uploads across |
| 1875 | // two compactions and snapshot rotations. |
| 1876 | func wNewestL0(t *testing.T, w *world) { |
| 1877 | b := w.boxes[0] |
| 1878 | w.serve(b, 1, app0) |
| 1879 | w.wake(b) |
| 1880 | loc := w.claim.Holder.Location |
| 1881 | prefix := dataKey(loc, "", "") |
| 1882 | held := map[string]bool{} |
| 1883 | w.hold = func(r *request) bool { return held[r.key] } |
| 1884 | k := func(n int) string { return ltxKey(loc, "", 0, n, n) } |
| 1885 | // position 2 is already uploaded (the fixture at 1, one write at 2) |
| 1886 | w.appWrite(b) |
| 1887 | w.replicate(b) |
| 1888 | // uploads from 3 on are held; the writer reaches position 10 |
| 1889 | held[k(3)] = true |
| 1890 | for i := 3; i <= 10; i++ { |
| 1891 | w.appWrite(b) |
| 1892 | w.replicate(b) |
| 1893 | } |
| 1894 | // 3 lands; 4 and 5 ship; 6 is held: compaction sees {2,3,4,5}, keeps 5, |
| 1895 | // rotates a snapshot at the local position 10 |
| 1896 | held[k(6)] = true |
| 1897 | delete(held, k(3)) |
| 1898 | w.completeHeld(k(3)) |
| 1899 | w.replicate(b) |
| 1900 | if got := w.maxL0(w.buckets[b.Region], prefix); got == 0 { |
| 1901 | w.violate("INV-2 (witness): compaction removed the newest level-0 file of %s; litestream keeps it, and a fresh box reads its position there (%s)", prefix, w.ltxShape(b.Region, prefix)) |
| 1902 | return |
| 1903 | } else if got != 5 { |
| 1904 | t.Fatalf("witness: newest uploaded level-0 file is %d, want 5 (%s)", got, w.ltxShape(b.Region, prefix)) |
| 1905 | } |
| 1906 | // the writer goes on to 11; 6 lands and 7 to 11 ship but 12 is held: |
| 1907 | // compaction sees {5,6,...}, rotates a snapshot at 11 and expires |
| 1908 | // below the previous snapshot, 10 |
| 1909 | w.appWrite(b) |
| 1910 | w.replicate(b) |
| 1911 | held[k(12)] = true |
| 1912 | delete(held, k(6)) |
| 1913 | w.completeHeld(k(6)) |
| 1914 | w.replicate(b) |
| 1915 | w.appWrite(b) |
| 1916 | w.replicate(b) |
| 1917 | w.hold = nil |
| 1918 | newest := w.maxL0(w.buckets[b.Region], prefix) |
| 1919 | snaps := w.currentLTX(w.buckets[b.Region], prefix, 9) |
| 1920 | if len(snaps) == 0 { |
| 1921 | t.Fatalf("witness: no snapshot rotated: %s", w.ltxShape(b.Region, prefix)) |
| 1922 | } |
| 1923 | if newest == 0 { |
| 1924 | w.violate("INV-2 (witness): retention removed the newest level-0 file of %s; litestream keeps it, and a fresh box reads its position there (%s)", prefix, w.ltxShape(b.Region, prefix)) |
| 1925 | return |
| 1926 | } |
| 1927 | w.completeHeld(k(12)) |
| 1928 | w.finish(t) |
| 1929 | } |
| 1930 | |
| 1931 | // wBuildCrashes (R7-4): a push's build with its snapshot PUT, then its |
| 1932 | // anchor PUT, held, the agent crashing in between each. |
| 1933 | func wBuildCrashes(t *testing.T, w *world) { |
| 1934 | b := w.boxes[0] |
| 1935 | w.serve(b, 1, app0) |
| 1936 | w.wake(b) |
| 1937 | for i := 0; i < 2; i++ { |
| 1938 | w.appWrite(b) |
| 1939 | } |
| 1940 | w.replicate(b) |
| 1941 | w.userPush() |
| 1942 | gen := w.claim.Op.ID |
| 1943 | loc := w.claim.Holder.Location |
| 1944 | w.reach(t, 400, "push installing", func() bool { |
| 1945 | return w.claim.Op.Kind == "pushing" && w.claim.Op.Phase == "install" |
| 1946 | }, w.act(b)) |
| 1947 | n := w.claim.Op.PushSnap.Max |
| 1948 | snap := snapKey(loc, gen, n) |
| 1949 | anchor := ltxKey(loc, gen, 0, n, n) |
| 1950 | published := func() bool { |
| 1951 | m := w.buckets[b.Region].current(genMarkerKey(loc)) |
| 1952 | return m != nil && m.B.Gen == gen |
| 1953 | } |
| 1954 | w.holdKey(snap) |
| 1955 | for i := 0; i < 12; i++ { |
| 1956 | w.tick(w.act(b)) |
| 1957 | if len(w.violations) > 0 { |
| 1958 | return // INV-11 |
| 1959 | } |
| 1960 | if i == 5 { |
| 1961 | w.crash(b) // between the intent and the snapshot's acknowledgement |
| 1962 | } |
| 1963 | if published() { |
| 1964 | w.violate("INV-11 (witness): generation.json names %s before its snapshot %s landed", gen, snap) |
| 1965 | return |
| 1966 | } |
| 1967 | } |
| 1968 | w.hold = nil |
| 1969 | w.completeHeld(snap) |
| 1970 | w.reach(t, 100, "push building its anchor", func() bool { return w.claim.Op.Phase == "install-anchor" }, w.act(b)) |
| 1971 | w.holdKey(anchor) |
| 1972 | for i := 0; i < 12; i++ { |
| 1973 | w.tick(w.act(b)) |
| 1974 | if len(w.violations) > 0 { |
| 1975 | return |
| 1976 | } |
| 1977 | if i == 5 { |
| 1978 | w.crash(b) // between the snapshot's and the anchor's acknowledgement |
| 1979 | } |
| 1980 | if published() { |
| 1981 | w.violate("INV-11 (witness): generation.json names %s before its anchor %s landed", gen, anchor) |
| 1982 | return |
| 1983 | } |
| 1984 | } |
| 1985 | w.hold = nil |
| 1986 | w.completeHeld(anchor) |
| 1987 | w.reach(t, 400, "push released", func() bool { return w.claim.Op.Kind == "serving" }, w.act(b)) |
| 1988 | w.crash(b) // after completion: the marker stands, the generation is complete |
| 1989 | w.recovered(t, b, "running after the push") |
| 1990 | w.appWrite(b) |
| 1991 | w.replicate(b) |
| 1992 | w.finish(t) |
| 1993 | } |
| 1994 | |
| 1995 | // wEvidenceWholeTree (§6.1): a legacy host adopted with a descendant that |
| 1996 | // escaped the cgroup; the move cuts. |
| 1997 | func wEvidenceWholeTree(t *testing.T, w *world) { |
| 1998 | b0, b1 := w.boxes[0], w.boxes[1] |
| 1999 | w.legacy(b0, 1) |
| 2000 | w.tick(func() { w.reconcile(b0) }) // adoption |
| 2001 | if w.claim == nil { |
| 2002 | t.Fatalf("witness: not adopted") |
| 2003 | } |
| 2004 | w.reach(t, 400, "adoption settled", func() bool { return w.claim.oblFor("adopt") == 0 }, w.actAll(), w.recoveryPass) |
| 2005 | if !hasMain(b0) { |
| 2006 | w.recovered(t, b0, "running after adoption") |
| 2007 | } |
| 2008 | b0.Procs = append(b0.Procs, &proc{Main: false, Strict: false, Inc: 1, Gen: b0.Procs[0].Gen, Session: b0.Procs[0].Session, Box: b0.ID}) // an escaped descendant |
| 2009 | w.moveTo(b1.Region) |
| 2010 | w.finish(t) |
| 2011 | } |
| 2012 | |
| 2013 | // wTimerFreeze (J-N14): a timer registered on the source, a move that |
| 2014 | // holds the row, refused deliveries, then a clean rollback whose verify |
| 2015 | // compares the timer digest with the one recorded at the stop. |
| 2016 | func wTimerFreeze(t *testing.T, w *world) { |
| 2017 | src, tgt := w.boxes[0], w.boxes[1] |
| 2018 | w.serve(src, 1, app0) |
| 2019 | w.nextW++ |
| 2020 | src.Timers = []int{w.nextW} |
| 2021 | w.acks = append(w.acks, ack{W: w.nextW, Inc: 1, Box: src.ID, Session: src.DB.Session, Gen: src.DB.Gen, At: w.now, Kind: "timer"}) |
| 2022 | w.landProbed(t, src, tgt) // the source is stopped and its row held |
| 2023 | for i := 0; i < 3; i++ { |
| 2024 | w.runner(src) // deliveries refused while the row is held |
| 2025 | } |
| 2026 | w.rollback(w.claim, "settle check failed") // clean: the target wrote nothing |
| 2027 | w.finish(t) |
| 2028 | } |
| 2029 | |
| 2030 | // ---------- rev 7.9 ---------- |
| 2031 | |
| 2032 | // wDeadSessionCertificate (claim rev 6.8 §6.4a, R8-1): a certificate of a |
| 2033 | // dead session whose max_txid still matches the remote maximum. |
| 2034 | func wDeadSessionCertificate(t *testing.T, w *world) { |
| 2035 | b := w.boxes[0] |
| 2036 | w.serve(b, 1, app0) |
| 2037 | w.wake(b) // warm: session 2 |
| 2038 | loc := w.claim.Holder.Location |
| 2039 | w.idleStop(b) // session 2 certifies {max 1}, the generation's position |
| 2040 | w.recovered(t, b, "warm continuation") // session 3; the certificates of 1 and 2 are dead |
| 2041 | key := w.deadWriterContinues(b, loc) // [2,2] in flight; A dies with its disk |
| 2042 | // the dead certificates are still there, never deleted, and session 2's |
| 2043 | // max_txid 1 equals the remote maximum, since [2,2] has not landed; |
| 2044 | // holder.session is 3, for which no certificate exists |
| 2045 | w.recovered(t, b, "B running after A's death") |
| 2046 | w.appWrite(b) |
| 2047 | w.replicate(b) // B's [2,2] |
| 2048 | if w.completeHeld(key) == 0 { |
| 2049 | t.Fatalf("witness: A's upload was not held") |
| 2050 | } |
| 2051 | w.checkDurable(w.claim, "after A's late upload landed") // two level-0 files: nothing compacted or snapshotted over A's |
| 2052 | w.finish(t) |
| 2053 | } |
| 2054 | |
| 2055 | // wCommittedLandingCrash (R8-2): the committed move's target dies with its |
| 2056 | // disk and an upload in flight while the claim is still landing. |
| 2057 | func wCommittedLandingCrash(t *testing.T, w *world) { |
| 2058 | src, tgt := w.boxes[0], w.boxes[1] |
| 2059 | w.serve(src, 1, app0) |
| 2060 | w.moveTo(tgt.Region) |
| 2061 | w.reach(t, 600, "committed and serving on the target", func() bool { |
| 2062 | return w.claim.Op.Kind == "landing" && w.claim.Op.Committed && hasMain(tgt) |
| 2063 | }, w.act(src, tgt), w.recoveryPass) |
| 2064 | if w.claim.Op.Kind != "landing" { |
| 2065 | t.Fatalf("witness: the move finalized before the target could crash: %s", w.state()) |
| 2066 | } |
| 2067 | loc := w.claim.Holder.Location |
| 2068 | key := w.deadWriterContinues(tgt, loc) // the target's upload in flight; it dies with its disk |
| 2069 | w.recovered(t, tgt, "target running again while the claim is still landing") |
| 2070 | w.appWrite(tgt) |
| 2071 | w.replicate(tgt) |
| 2072 | if w.completeHeld(key) == 0 { |
| 2073 | t.Fatalf("witness: the target's upload was not held") |
| 2074 | } |
| 2075 | w.checkDurable(w.claim, "after the dead target's late upload landed") |
| 2076 | w.finish(t) |
| 2077 | } |
| 2078 | |
| 2079 | // wProbeRestart (R8-2): the landing's probe dies with its disk and an |
| 2080 | // upload in flight; the landing restarts its probe. |
| 2081 | func wProbeRestart(t *testing.T, w *world) { |
| 2082 | src, tgt := w.boxes[0], w.boxes[1] |
| 2083 | w.serve(src, 1, app0) |
| 2084 | w.landProbed(t, src, tgt) |
| 2085 | loc := w.claim.Holder.Location |
| 2086 | w.appWrite(tgt) // the probe writes |
| 2087 | key := ltxKey(loc, tgt.DB.Gen, 0, tgt.DB.Pos+1, tgt.DB.Pos+1) |
| 2088 | w.holdKey(key) |
| 2089 | w.replicate(tgt) |
| 2090 | w.hold = nil |
| 2091 | w.crash(tgt) |
| 2092 | w.loseDisk(tgt) |
| 2093 | w.reach(t, 400, "probe restarted", func() bool { return hasMain(tgt) }, w.act(src, tgt), w.recoveryPass) |
| 2094 | if !hasMain(tgt) { |
| 2095 | t.Fatalf("witness: the probe did not restart: %s", w.state()) |
| 2096 | } |
| 2097 | wr := w.appWrite(tgt) |
| 2098 | w.replicate(tgt) |
| 2099 | if w.completeHeld(key) == 0 { |
| 2100 | t.Fatalf("witness: the dead probe's upload was not held") |
| 2101 | } |
| 2102 | // the landing's generation, holder.generation since the probe's cold |
| 2103 | // admission (claim rev 6.9), as its planner would restore it now |
| 2104 | gen := w.claim.Holder.Gen |
| 2105 | db := w.restoreCalc(tgt.Region, 1, loc, gen) |
| 2106 | if db == nil || !contains(db.Log, wr) { |
| 2107 | w.violate("INV-2 (witness): the landing's generation %q lost the restarted probe's write %d after the dead probe's upload landed", gen, wr) |
| 2108 | return |
| 2109 | } |
| 2110 | w.finish(t) |
| 2111 | } |
| 2112 | |
| 2113 | // wEmptyBootstrap (R8-3): a created incarnation's first wake. |
| 2114 | func wEmptyBootstrap(t *testing.T, w *world) { |
| 2115 | w.console = append(w.console, &consolePlan{Kind: "create", Host: "h", App: app0, OpID: w.newID("cr"), Inc: 1, Region: 0}) |
| 2116 | b := w.regionBox(0) |
| 2117 | w.reach(t, 200, "created", func() bool { |
| 2118 | c := w.claim |
| 2119 | return c != nil && c.Holder != nil && c.Holder.Inc == 1 && c.Op.Kind == "serving" && b.Row != nil |
| 2120 | }, w.runConsole, w.actAll(), w.recoveryPass) |
| 2121 | b.Config, b.CfgVer, b.Live, b.LiveInc = 1, w.cfgVer[app0], app0, 1 |
| 2122 | // the first wake: a cold admission into an empty generation (claim rev |
| 2123 | // 6.9), no LTX file at all |
| 2124 | w.reach(t, 120, "first wake", func() bool { return hasMain(b) }, w.act(b), w.recoveryPass, func() { w.wake(b) }) |
| 2125 | if len(w.violations) > 0 { |
| 2126 | return |
| 2127 | } |
| 2128 | if !hasMain(b) { |
| 2129 | t.Fatalf("witness: the created incarnation did not run: %s", w.state()) |
| 2130 | } |
| 2131 | loc := w.claim.Holder.Location |
| 2132 | gen := w.claim.Holder.Gen |
| 2133 | if n := len(w.currentLTX(w.buckets[b.Region], dataKey(loc, gen, ""), 0)) + len(w.currentLTX(w.buckets[b.Region], dataKey(loc, gen, ""), 9)); n != 0 { |
| 2134 | t.Fatalf("witness: an empty generation has %d LTX files before the first transaction", n) |
| 2135 | } |
| 2136 | // a move of the empty incarnation: its seal at the cut is at position 0 |
| 2137 | // with no transaction, and the landing installs nothing; the mutation |
| 2138 | // installs a snapshot [1,0] and an anchor [0,0], which the encoder |
| 2139 | // refuses (INV-12 at the PUT). A push cannot be empty: its seal carries |
| 2140 | // the push's own mark |
| 2141 | w.idleStop(b) |
| 2142 | w.reach(t, 400, "the first wake's chores done", func() bool { return len(w.claim.Obl) == 0 }, w.act(b), w.recoveryPass) |
| 2143 | tgt := w.regionBox(1) |
| 2144 | w.moveTo(tgt.Region) |
| 2145 | if w.claim.Op.Kind != "moving" { |
| 2146 | t.Fatalf("witness: the move of the empty incarnation did not start: %s", w.state()) |
| 2147 | } |
| 2148 | w.reach(t, 800, "move of the empty incarnation finalized", func() bool { return w.claim.Op.Kind == "serving" && w.claim.Op.Exec == tgt.ID }, w.act(b, tgt), w.recoveryPass) |
| 2149 | if len(w.violations) > 0 { |
| 2150 | return |
| 2151 | } |
| 2152 | w.recovered(t, tgt, "woken after the move") |
| 2153 | w.appWrite(tgt) |
| 2154 | w.replicate(tgt) // the first transaction is the first upload, [1,1] |
| 2155 | w.idleStop(tgt) |
| 2156 | w.loseDisk(tgt) |
| 2157 | w.recovered(t, tgt, "woken cold") |
| 2158 | w.finish(t) |
| 2159 | } |
| 2160 | |
| 2161 | // wRetryUnresolved (R8-5): an upload times out, its retry succeeds, the |
| 2162 | // original stays unresolved. |
| 2163 | func wRetryUnresolved(t *testing.T, w *world) { |
| 2164 | b := w.boxes[0] |
| 2165 | w.serve(b, 1, app0) |
| 2166 | w.wake(b) |
| 2167 | loc := w.claim.Holder.Location |
| 2168 | w.appWrite(b) |
| 2169 | key := ltxKey(loc, "", 0, b.DB.Pos+1, b.DB.Pos+1) |
| 2170 | var original *request |
| 2171 | w.hold = func(r *request) bool { |
| 2172 | if r.key == key && original == nil { |
| 2173 | original = r |
| 2174 | return true // the first attempt alone is held |
| 2175 | } |
| 2176 | return r == original |
| 2177 | } |
| 2178 | w.replicate(b) |
| 2179 | for i := 0; i <= uploadTimeout; i++ { |
| 2180 | w.tick(func() { w.replicate(b) }) // the client times out and retries the same bytes; the retry lands |
| 2181 | } |
| 2182 | if original == nil || w.buckets[b.Region].current(key) == nil { |
| 2183 | t.Fatalf("witness: the retry did not land: %s", w.ltxShape(b.Region, dataKey(loc, "", ""))) |
| 2184 | } |
| 2185 | w.idleStop(b) |
| 2186 | sk := closedKey(loc, "", b.DB.Session) |
| 2187 | for i := 0; i < 10; i++ { |
| 2188 | w.tick(func() { w.replicate(b) }) |
| 2189 | if w.buckets[b.Region].current(sk) != nil { |
| 2190 | w.violate("INV-2 (witness): box %d wrote its certificate while its original upload %s was unresolved (R8-5)", b.ID, key) |
| 2191 | return |
| 2192 | } |
| 2193 | } |
| 2194 | w.hold = nil |
| 2195 | w.completeHeld(key) |
| 2196 | w.finish(t) |
| 2197 | } |
| 2198 | |
| 2199 | // ---------- rev 7.10 ---------- |
| 2200 | |
| 2201 | // wStaleLocalAfterClose (claim rev 6.9, R9-1): a valid certificate and a |
| 2202 | // stale local database. |
| 2203 | func wStaleLocalAfterClose(t *testing.T, w *world) { |
| 2204 | b := w.boxes[0] |
| 2205 | w.serve(b, 1, app0) |
| 2206 | w.wake(b) |
| 2207 | stale := b.DB.clone() // a cached copy through N |
| 2208 | w.appWrite(b) |
| 2209 | w.replicate(b) // N+1, durable |
| 2210 | w.idleStop(b) // the certificate names N+1 as the remote maximum |
| 2211 | loc := w.claim.Holder.Location |
| 2212 | if w.buckets[b.Region].current(closedKey(loc, w.claim.Holder.Gen, b.DB.Session)) == nil { |
| 2213 | t.Fatalf("witness: no certificate after the clean close") |
| 2214 | } |
| 2215 | b.DB = stale |
| 2216 | w.logf("witness: box %d's local database is a cached copy without the last acknowledged write", b.ID) |
| 2217 | w.recovered(t, b, "woken on the certificate") |
| 2218 | w.appWrite(b) |
| 2219 | w.replicate(b) // the next upload: skipped at the remote position if the stale copy was kept |
| 2220 | w.checkLocal(w.claim, b, b.DB) |
| 2221 | w.checkDurable(w.claim, "after the wake on the stale copy") |
| 2222 | w.finish(t) |
| 2223 | } |
| 2224 | |
| 2225 | // wSilentLoss (claim rev 6.9, R9-2): an acknowledged, unuploaded write and |
| 2226 | // a crash; the next admission declares the loss. |
| 2227 | func wSilentLoss(t *testing.T, w *world) { |
| 2228 | b := w.boxes[0] |
| 2229 | w.serve(b, 1, app0) |
| 2230 | w.wake(b) |
| 2231 | w.appWrite(b) // acknowledged, never uploaded |
| 2232 | w.crash(b) |
| 2233 | w.recovered(t, b, "woken after the crash") |
| 2234 | if w.stats["writes_lost declared"] == 0 && on("writes-lost") { |
| 2235 | t.Fatalf("witness: no writes_lost record after the crash") |
| 2236 | } |
| 2237 | w.checkLocal(w.claim, b, b.DB) |
| 2238 | w.finish(t) |
| 2239 | } |
| 2240 | |
| 2241 | // wStaleClosureDelete (claim rev 6.9, R9-4): an admission closure computed |
| 2242 | // under serving resumes after a delete began. |
| 2243 | func wStaleClosureDelete(t *testing.T, w *world) { |
| 2244 | b := w.boxes[0] |
| 2245 | w.serve(b, 1, app0) |
| 2246 | w.wake(b) |
| 2247 | w.idleStop(b) |
| 2248 | stale := w.claim.clone() // the wake's read, under serving |
| 2249 | w.userDelete() |
| 2250 | if w.claim.Op.Kind != "deleting" { |
| 2251 | t.Fatalf("witness: the delete did not begin: %s", w.state()) |
| 2252 | } |
| 2253 | // the claim library's BeginDelete preserves session, generation and the |
| 2254 | // executor (R9-4); this model's delete names no executor, so the |
| 2255 | // witness keeps the serving box as op.exec, as the library does |
| 2256 | w.cas(w.claim, func(n *claim) bool { n.Op.Exec = b.ID; return true }) |
| 2257 | w.logf("witness: a stalled wake resumes with its serving-time read of the claim") |
| 2258 | if w.spawn(b, stale, stale.Holder.Gen, false) { |
| 2259 | w.logf("witness: the stale closure admitted a writer during the delete") |
| 2260 | } |
| 2261 | w.finish(t) |
| 2262 | } |
| 2263 | |
| 2264 | // wMaintenanceRetry (R9-5): a compaction PUT retried after a timeout. |
| 2265 | func wMaintenanceRetry(t *testing.T, w *world) { |
| 2266 | b := w.boxes[0] |
| 2267 | w.serve(b, 1, app0) |
| 2268 | w.wake(b) |
| 2269 | loc := w.claim.Holder.Location |
| 2270 | gen := w.claim.Holder.Gen |
| 2271 | var original *request |
| 2272 | w.hold = func(r *request) bool { |
| 2273 | if r.kind == rPut && r.b != nil && r.b.Level == 1 && original == nil { |
| 2274 | original = r |
| 2275 | return true // the first compaction attempt alone is held |
| 2276 | } |
| 2277 | return r == original |
| 2278 | } |
| 2279 | for i := 0; i < 3; i++ { |
| 2280 | w.appWrite(b) |
| 2281 | w.replicate(b) // three level-0 files: compaction issues its level-1 PUT, held |
| 2282 | } |
| 2283 | if original == nil { |
| 2284 | t.Fatalf("witness: no compaction PUT was issued: %s", w.ltxShape(b.Region, dataKey(loc, gen, ""))) |
| 2285 | } |
| 2286 | for i := 0; i <= uploadTimeout; i++ { |
| 2287 | w.tick(func() { w.replicate(b) }) // the client times out; the next compaction pass retries and lands |
| 2288 | } |
| 2289 | if len(w.currentLTX(w.buckets[b.Region], dataKey(loc, gen, ""), 1)) == 0 { |
| 2290 | // the retry may compact a wider range than the original, under its own key |
| 2291 | t.Fatalf("witness: the compaction retry did not land: %s", w.ltxShape(b.Region, dataKey(loc, gen, ""))) |
| 2292 | } |
| 2293 | w.idleStop(b) |
| 2294 | sk := closedKey(loc, gen, b.DB.Session) |
| 2295 | for i := 0; i < 10; i++ { |
| 2296 | w.tick(func() { w.replicate(b) }) |
| 2297 | if w.buckets[b.Region].current(sk) != nil { |
| 2298 | w.violate("INV-2 (witness): box %d wrote its certificate while its original compaction PUT %s was unresolved (R9-5)", b.ID, original.key) |
| 2299 | return |
| 2300 | } |
| 2301 | } |
| 2302 | w.hold = nil |
| 2303 | w.completeHeld(original.key) |
| 2304 | w.finish(t) |
| 2305 | } |
| 2306 | |
| 2307 | // wLostResponse (R9-5): a snapshot PUT whose response is lost. |
| 2308 | func wLostResponse(t *testing.T, w *world) { |
| 2309 | b := w.boxes[0] |
| 2310 | w.serve(b, 1, app0) |
| 2311 | w.wake(b) |
| 2312 | loc := w.claim.Holder.Location |
| 2313 | gen := w.claim.Holder.Gen |
| 2314 | var original *request |
| 2315 | w.hold = func(r *request) bool { |
| 2316 | if r.kind == rPut && r.b != nil && r.b.Level == 9 && original == nil { |
| 2317 | original = r |
| 2318 | return true // the snapshot PUT alone is held |
| 2319 | } |
| 2320 | return r == original |
| 2321 | } |
| 2322 | for i := 0; i < 3; i++ { |
| 2323 | w.appWrite(b) |
| 2324 | w.replicate(b) // compaction rotates a snapshot, whose PUT is held |
| 2325 | } |
| 2326 | if original == nil { |
| 2327 | t.Fatalf("witness: no snapshot PUT was issued: %s", w.ltxShape(b.Region, dataKey(loc, gen, ""))) |
| 2328 | } |
| 2329 | for i := 0; i <= uploadTimeout; i++ { |
| 2330 | w.tick(func() { w.replicate(b) }) // the client gives up on it |
| 2331 | } |
| 2332 | w.hold = nil |
| 2333 | w.completeHeld(original.key) // the server completes it after the client gave up: a lost response |
| 2334 | w.idleStop(b) |
| 2335 | sk := closedKey(loc, gen, b.DB.Session) |
| 2336 | for i := 0; i < 10; i++ { |
| 2337 | w.tick(func() { w.replicate(b) }) |
| 2338 | if w.buckets[b.Region].current(sk) != nil { |
| 2339 | w.violate("INV-2 (witness): box %d wrote its certificate while the response to its snapshot PUT %s was lost (R9-5)", b.ID, original.key) |
| 2340 | return |
| 2341 | } |
| 2342 | } |
| 2343 | w.finish(t) |
| 2344 | } |
| 2345 | |
| 2346 | // ---------- rev 7.11 ---------- |
| 2347 | |
| 2348 | // ackInto acknowledges one write into b's database without a main process: |
| 2349 | // a background worker's work (R10-1). |
| 2350 | func (w *world) ackInto(b *box, inc int) int { |
| 2351 | db := b.DB |
| 2352 | w.nextW++ |
| 2353 | wr := w.nextW |
| 2354 | w.commit(db, wr) |
| 2355 | sess, gen := w.sessionOf(b) |
| 2356 | w.acks = append(w.acks, ack{W: wr, Inc: inc, Box: b.ID, Session: sess, Gen: gen, At: w.now, Kind: "write"}) |
| 2357 | w.writeInc[wr] = inc |
| 2358 | w.logf("witness: a background worker on box %d acknowledged %d", b.ID, wr) |
| 2359 | return wr |
| 2360 | } |
| 2361 | |
| 2362 | // wAckBeforeAdmission (claim rev 6.10, R10-1): a background acknowledgement |
| 2363 | // right after the app starts, then a crash before replication opens. |
| 2364 | func wAckBeforeAdmission(t *testing.T, w *world) { |
| 2365 | b := w.boxes[0] |
| 2366 | w.serve(b, 1, app0) |
| 2367 | w.wake(b) |
| 2368 | w.idleStop(b) // a certified close: the next admission is warm |
| 2369 | armed := true |
| 2370 | w.startHook = func(x *box) bool { |
| 2371 | if x != b || !armed || x.DB == nil { |
| 2372 | return false |
| 2373 | } |
| 2374 | armed = false |
| 2375 | w.ackInto(x, 1) |
| 2376 | w.crash(x) |
| 2377 | return true |
| 2378 | } |
| 2379 | w.wake(b) |
| 2380 | w.startHook = nil |
| 2381 | w.recovered(t, b, "woken after the crash") |
| 2382 | w.checkLocal(w.claim, b, b.DB) |
| 2383 | w.finish(t) |
| 2384 | } |
| 2385 | |
| 2386 | // wBaselineParked (claim rev 6.10, R10-2): a crash between the admitting |
| 2387 | // CAS and the first upload, then the predecessor's retirement. |
| 2388 | func wBaselineParked(t *testing.T, w *world) { |
| 2389 | b := w.boxes[0] |
| 2390 | w.serve(b, 1, app0) |
| 2391 | w.wake(b) |
| 2392 | w.appWrite(b) |
| 2393 | w.replicate(b) |
| 2394 | w.crash(b) // no certificate: the next admission is cold, into a fresh generation |
| 2395 | armed := true |
| 2396 | w.startHook = func(x *box) bool { |
| 2397 | if x != b || !armed { |
| 2398 | return false |
| 2399 | } |
| 2400 | armed = false |
| 2401 | w.crash(x) // before the first upload: the new generation stays empty |
| 2402 | return true |
| 2403 | } |
| 2404 | w.wake(b) |
| 2405 | w.startHook = nil |
| 2406 | if g := w.claim.Holder.Gen; g == "" || len(w.buckets[b.Region].keys(dataKey(w.claim.Holder.Location, g, ""))) != 0 { |
| 2407 | t.Fatalf("witness: expected an empty fresh generation, have %q: %s", g, w.state()) |
| 2408 | } |
| 2409 | // the predecessor's retirement, queued at the CAS under the mutation, |
| 2410 | // runs out its quiet time |
| 2411 | w.reach(t, 200, "chores settled", func() bool { return len(w.claim.Obl) == 0 }, w.act(b), w.recoveryPass) |
| 2412 | w.recovered(t, b, "woken after the crash") |
| 2413 | w.checkLocal(w.claim, b, b.DB) |
| 2414 | w.checkDurable(w.claim, "after the recovery") |
| 2415 | w.finish(t) |
| 2416 | } |
| 2417 | |
| 2418 | // wFirstUploadRetry (R10-7): the fresh generation's first upload retried. |
| 2419 | func wFirstUploadRetry(t *testing.T, w *world) { |
| 2420 | b := w.boxes[0] |
| 2421 | w.serve(b, 1, app0) |
| 2422 | w.wake(b) |
| 2423 | w.appWrite(b) |
| 2424 | w.replicate(b) |
| 2425 | w.crash(b) |
| 2426 | var original *request |
| 2427 | w.hold = func(r *request) bool { |
| 2428 | if r.kind == rPut && r.b != nil && r.b.Level == 0 && r.b.Min == 1 && r.b.Max == 1 && r.b.Gen != "" && original == nil { |
| 2429 | original = r |
| 2430 | return true // the first upload's first attempt alone is held |
| 2431 | } |
| 2432 | return r == original |
| 2433 | } |
| 2434 | w.wake(b) |
| 2435 | for i := 0; i <= uploadTimeout+1; i++ { |
| 2436 | w.tick(w.act(b)) // the client times out; the retry lands and the start completes |
| 2437 | } |
| 2438 | if original == nil { |
| 2439 | t.Fatalf("witness: no first upload was issued: %s", w.state()) |
| 2440 | } |
| 2441 | if !hasMain(b) { |
| 2442 | t.Fatalf("witness: the writer did not start after the retry: %s", w.state()) |
| 2443 | } |
| 2444 | loc, gen := w.claim.Holder.Location, w.claim.Holder.Gen |
| 2445 | w.idleStop(b) |
| 2446 | sk := closedKey(loc, gen, b.DB.Session) |
| 2447 | for i := 0; i < 10; i++ { |
| 2448 | w.tick(func() { w.replicate(b) }) |
| 2449 | if w.buckets[b.Region].current(sk) != nil { |
| 2450 | w.violate("INV-2 (witness): box %d wrote its certificate while its first upload %s was unresolved (R10-7)", b.ID, original.key) |
| 2451 | return |
| 2452 | } |
| 2453 | } |
| 2454 | w.hold = nil |
| 2455 | w.completeHeld(original.key) |
| 2456 | w.finish(t) |
| 2457 | } |
| 2458 | |
| 2459 | // wAnchorRetry (R10-7): a warm admission's anchor retried. |
| 2460 | func wAnchorRetry(t *testing.T, w *world) { |
| 2461 | b := w.boxes[0] |
| 2462 | w.serve(b, 1, app0) |
| 2463 | loc := w.claim.Holder.Location |
| 2464 | // the generation's newest snapshot stands above its level-0 maximum |
| 2465 | // (retention expired the files above it): a warm restore lands at the |
| 2466 | // snapshot's position and needs the anchor there |
| 2467 | snap := snapshotOf(b.DB, 1) |
| 2468 | snap.Max = 2 |
| 2469 | w.nextW++ |
| 2470 | wr := w.nextW |
| 2471 | sess, gen := w.sessionOf(b) |
| 2472 | w.acks = append(w.acks, ack{W: wr, Inc: 1, Box: b.ID, Session: sess, Gen: gen, At: w.now, Kind: "write"}) |
| 2473 | w.writeInc[wr] = 1 |
| 2474 | w.txs[wr] = tx{W: wr, TX: 3, Key: fmt.Sprintf("k%d", wr), Val: wr} |
| 2475 | snap.Pages[fmt.Sprintf("k%d", wr)] = wr |
| 2476 | snap.TXs = append(snap.TXs, wr) |
| 2477 | k := snapKey(loc, "", 2) |
| 2478 | w.buckets[b.Region].objs[k] = append(w.buckets[b.Region].objs[k], &version{ID: w.newVer(), B: snap}) |
| 2479 | w.markDurable(k, snap) |
| 2480 | w.buckets[b.Region].objs[closedKey(loc, "", w.claim.Holder.Session)][0].B.TX = 2 // the certificate names the snapshot's position (the serving fixture's session, not the legacy identity) |
| 2481 | var original *request |
| 2482 | w.hold = func(r *request) bool { |
| 2483 | if r.kind == rPut && r.b != nil && r.b.Level == 0 && r.b.Min == 2 && r.b.Max == 2 && original == nil { |
| 2484 | original = r |
| 2485 | return true // the anchor's first attempt alone is held |
| 2486 | } |
| 2487 | return r == original |
| 2488 | } |
| 2489 | w.wake(b) |
| 2490 | for i := 0; i <= uploadTimeout+1; i++ { |
| 2491 | w.tick(w.act(b)) |
| 2492 | } |
| 2493 | if original == nil { |
| 2494 | t.Fatalf("witness: no anchor PUT was issued: %s%s", w.state(), w.boxesState()) |
| 2495 | } |
| 2496 | if !hasMain(b) { |
| 2497 | t.Fatalf("witness: the writer did not start after the anchor retry: %s", w.state()) |
| 2498 | } |
| 2499 | w.idleStop(b) |
| 2500 | sk := closedKey(loc, "", b.DB.Session) |
| 2501 | for i := 0; i < 10; i++ { |
| 2502 | w.tick(func() { w.replicate(b) }) |
| 2503 | if w.buckets[b.Region].current(sk) != nil { |
| 2504 | w.violate("INV-2 (witness): box %d wrote its certificate while its anchor %s was unresolved (R10-7)", b.ID, original.key) |
| 2505 | return |
| 2506 | } |
| 2507 | } |
| 2508 | w.hold = nil |
| 2509 | w.completeHeld(original.key) |
| 2510 | w.finish(t) |
| 2511 | } |
| 2512 | |
| 2513 | // wSealReturn (rev 7.11 §7.8): the source's last upload is in flight at |
| 2514 | // the cut; the rollback's return must carry the seal. |
| 2515 | func wSealReturn(t *testing.T, w *world) { |
| 2516 | src, tgt := w.boxes[0], w.boxes[1] |
| 2517 | w.serve(src, 1, app0) |
| 2518 | w.wake(src) |
| 2519 | loc, gen0 := w.claim.Holder.Location, w.claim.Holder.Gen |
| 2520 | w.hold = func(r *request) bool { |
| 2521 | // every level-0 upload of the source's own generation is held: its |
| 2522 | // replica stops short of the stopped database |
| 2523 | return r.kind == rPut && r.region == src.Region && r.b != nil && r.b.Level == 0 && genOf(loc, r.key) == gen0 |
| 2524 | } |
| 2525 | w.appWrite(src) |
| 2526 | w.replicate(src) |
| 2527 | w.moveTo(tgt.Region) |
| 2528 | if !w.reach(t, 600, "landing built", func() bool { |
| 2529 | c := w.claim |
| 2530 | return c.Op.Kind == "landing" && (c.Op.LandPhase == "local" || c.Op.LandPhase == "config" || c.Op.LandPhase == "probing") |
| 2531 | }, w.act(src, tgt), w.recoveryPass) { |
| 2532 | return |
| 2533 | } |
| 2534 | if w.claim.Op.SrcCovered { |
| 2535 | t.Fatalf("witness: the seal found the source's replica complete; the held upload was not held: %s", w.state()) |
| 2536 | } |
| 2537 | w.rollback(w.claim, "configuration changed during the move") |
| 2538 | // the source's recovery admission decides with the replica still short |
| 2539 | w.reach(t, 800, "source admitted after the rollback", func() bool { |
| 2540 | c := w.claim |
| 2541 | return len(w.violations) > 0 || c.Op.Kind == "serving" || c.Op.Kind == "restoring" && (c.Op.SrcPhase == "probed" || c.Op.SrcPhase == "opened") |
| 2542 | }, w.act(src, tgt), w.recoveryPass, w.runConsole) |
| 2543 | w.hold = nil |
| 2544 | w.completeHeld(dataKey(loc, gen0, "")) |
| 2545 | w.finish(t) |
| 2546 | } |
| 2547 | |
| 2548 | // ---------- rev 7.12 ---------- |
| 2549 | |
| 2550 | // wCleanReturnIdentity (claim rev 6.12, R11-4): a clean rollback's return |
| 2551 | // and the identity the source's re-admission journals. |
| 2552 | func wCleanReturnIdentity(t *testing.T, w *world) { |
| 2553 | src, tgt := w.boxes[0], w.boxes[1] |
| 2554 | w.serve(src, 1, app0) |
| 2555 | w.wake(src) |
| 2556 | w.appWrite(src) |
| 2557 | w.replicate(src) // the source's replica covers everything it acknowledged: src_covered at the seal |
| 2558 | w.landProbed(t, src, tgt) |
| 2559 | tl := lastAdmission(w.claim.Holder) |
| 2560 | if tl == nil || tl.Box != tgt.ID { |
| 2561 | t.Fatalf("witness: the target's probe is not the last admission: %s", w.state()) |
| 2562 | } |
| 2563 | tgtSession, tgtGen := tl.Session, tl.Gen |
| 2564 | if !w.claim.Op.SrcCovered { |
| 2565 | t.Fatalf("witness: the seal did not record src_covered: %s", w.state()) |
| 2566 | } |
| 2567 | w.rollback(w.claim, "settle check failed") // the target wrote nothing: a clean rollback |
| 2568 | before := w.stats["writes_lost declared"] |
| 2569 | w.reach(t, 800, "source re-admitted", func() bool { |
| 2570 | c := w.claim |
| 2571 | return len(w.violations) > 0 || c.Op.Kind == "serving" || c.Op.Kind == "restoring" && (c.Op.SrcPhase == "probed" || c.Op.SrcPhase == "opened") |
| 2572 | }, w.act(src, tgt), w.recoveryPass, w.runConsole) |
| 2573 | if len(w.violations) > 0 { |
| 2574 | return |
| 2575 | } |
| 2576 | e := lastAdmission(w.claim.Holder) |
| 2577 | if e == nil || e.Box != src.ID { |
| 2578 | t.Fatalf("witness: the source's re-admission is not the last admission: %s", w.state()) |
| 2579 | } |
| 2580 | if e.Predecessor.Session != tgtSession || e.Predecessor.Box != tgt.ID || e.Predecessor.Gen != tgtGen { |
| 2581 | w.violate("INV-16 (witness): the source journalled predecessor {session %d, box %d, generation %q}; the target's writer was {session %d, box %d, generation %q}", e.Predecessor.Session, e.Predecessor.Box, e.Predecessor.Gen, tgtSession, tgt.ID, tgtGen) |
| 2582 | return |
| 2583 | } |
| 2584 | if e.Coverage != "clean-return" || w.stats["writes_lost declared"] != before { |
| 2585 | w.violate("INV-16 (witness): a clean return with src_covered declared a loss (coverage %q, %d records)", e.Coverage, w.stats["writes_lost declared"]-before) |
| 2586 | return |
| 2587 | } |
| 2588 | w.finish(t) |
| 2589 | } |
| 2590 | |
| 2591 | // wOriginSwept (R11-1): origin, an unfinished admission, the ordinary |
| 2592 | // sweep, then the recovery. |
| 2593 | func wOriginSwept(t *testing.T, w *world) { |
| 2594 | b0 := w.boxes[0] |
| 2595 | w.legacy(b0, 1) |
| 2596 | w.tick(func() { w.reconcile(b0) }) // adoption |
| 2597 | if w.claim == nil { |
| 2598 | t.Fatalf("witness: not adopted") |
| 2599 | } |
| 2600 | w.reach(t, 400, "adoption settled", func() bool { return w.claim.oblFor("adopt") == 0 }, w.actAll(), w.recoveryPass) |
| 2601 | if len(w.violations) > 0 { |
| 2602 | return |
| 2603 | } |
| 2604 | // the pre-release writer left no certificate (the helper's is for a |
| 2605 | // warm first wake): the first wake is cold, from the origin |
| 2606 | delete(w.buckets[b0.Region].objs, closedKey(w.claim.Holder.Location, "", 0)) |
| 2607 | armed := true |
| 2608 | w.startHook = func(x *box) bool { |
| 2609 | if x != b0 || !armed { |
| 2610 | return false |
| 2611 | } |
| 2612 | armed = false |
| 2613 | w.crash(x) // before the first upload: the new generation is empty, the marker absent, the origin the baseline |
| 2614 | return true |
| 2615 | } |
| 2616 | w.wake(b0) // the first cold admission from the origin |
| 2617 | w.startHook = nil |
| 2618 | if g := w.claim.Holder.Gen; g == "" { |
| 2619 | t.Fatalf("witness: no cold admission happened: %s", w.state()) |
| 2620 | } |
| 2621 | // the ordinary sweep runs before any recovery: every box's obligation |
| 2622 | // runner, no wakes |
| 2623 | for i := 0; i < 3*horizonH; i++ { |
| 2624 | w.tick(func() { |
| 2625 | for _, b := range w.liveBoxes() { |
| 2626 | w.obligationRunner(b) |
| 2627 | } |
| 2628 | }) |
| 2629 | if len(w.violations) > 0 { |
| 2630 | return |
| 2631 | } |
| 2632 | } |
| 2633 | // the recovery: under the mutation the swept origin is a covered local |
| 2634 | // baseline since rev 7.14 (claim rev 6.22 §6.2a), and the start refuses |
| 2635 | // with an alert rather than restoring nothing; either way the data is |
| 2636 | // unreachable, which is the failure the witness names |
| 2637 | if !w.drive(120, func() bool { return hasMain(b0) }, w.act(b0), w.recoveryPass, func() { w.wake(b0) }) { |
| 2638 | if len(w.violations) == 0 { |
| 2639 | w.violate("INV-2 (witness): the recovery cannot start, its origin baseline was retired under the unfinished admission (%d starts refused as a covered local baseline)", w.stats["start refused: covered local baseline"]) |
| 2640 | } |
| 2641 | return |
| 2642 | } |
| 2643 | w.checkLocal(w.claim, b0, b0.DB) |
| 2644 | w.checkDurable(w.claim, "after the recovery") |
| 2645 | w.finish(t) |
| 2646 | } |
| 2647 | |
| 2648 | // ---------- rev 7.14 ---------- |
| 2649 | |
| 2650 | // wParkScopeSurvivesRestart (claim rev 6.15 §2, R13-4): a committed move's |
| 2651 | // source-region park binds its scope, with the evidence time, in the |
| 2652 | // claim; the region's agent restarts mid-park; the acknowledgement comes |
| 2653 | // at the original evidence time plus the horizon, not the restart's. |
| 2654 | func wParkScopeSurvivesRestart(t *testing.T, w *world) { |
| 2655 | src, tgt := w.boxes[0], w.boxes[1] |
| 2656 | w.serve(src, 1, app0) |
| 2657 | w.wake(src) |
| 2658 | w.appWrite(src) |
| 2659 | w.commitLanding(t, src, tgt) |
| 2660 | if len(w.violations) > 0 { |
| 2661 | return |
| 2662 | } |
| 2663 | t0 := w.now |
| 2664 | var id string |
| 2665 | deadline := w.claim.Op.StopAt + horizonH // the cut's stop evidence plus H (claim rev 6.23: the persisted original bound) |
| 2666 | for _, o := range w.claim.Obl { |
| 2667 | if o.Kind == "park-superseded" && o.Region == src.Region { |
| 2668 | id = o.ID |
| 2669 | if o.Scope != nil { |
| 2670 | deadline = o.Scope.deadline() |
| 2671 | } |
| 2672 | } |
| 2673 | } |
| 2674 | if id == "" { |
| 2675 | t.Fatalf("witness: no park-superseded for the source region after the commit: %s", w.state()) |
| 2676 | } |
| 2677 | // the park runs for a while, then the source region's agent restarts |
| 2678 | // before the deadline |
| 2679 | restart := deadline - 20 |
| 2680 | if restart < t0+5 { |
| 2681 | restart = t0 + 5 |
| 2682 | } |
| 2683 | for w.now < restart { |
| 2684 | w.tick(w.act(src, tgt), w.runConsole, w.recoveryPass) |
| 2685 | if len(w.violations) > 0 { |
| 2686 | return |
| 2687 | } |
| 2688 | } |
| 2689 | if !hasObl(w.claim.Obl, id) { |
| 2690 | t.Fatalf("witness: the park %s acknowledged before the restart, at %d (commit at %d, deadline %d): the horizon did not hold", id, w.now, t0, deadline) |
| 2691 | } |
| 2692 | w.crash(src) // a new agent process: the box-local evidence map is gone |
| 2693 | w.reach(t, 400, "the source region's park acknowledged", func() bool { return !hasObl(w.claim.Obl, id) }, w.act(src, tgt), w.runConsole, w.recoveryPass) |
| 2694 | if len(w.violations) > 0 { |
| 2695 | return |
| 2696 | } |
| 2697 | if w.now > deadline+30 { |
| 2698 | w.violate("INV-9 (witness): the park %s was acknowledged at %d, after its persisted deadline %d and slack: the restart at %d started the horizon again from the restart's clock", id, w.now, deadline, restart) |
| 2699 | return |
| 2700 | } |
| 2701 | w.finish(t) |
| 2702 | } |
| 2703 | |
| 2704 | // wStagingScopeDeadline (claim rev 6.23 §2, R15-1): a staging lane's scope |
| 2705 | // persists the seal bound, and its deadline is that bound plus H; a |
| 2706 | // cleanup that first runs after the deadline, through an agent restart, |
| 2707 | // acknowledges at once rather than waiting a fresh horizon from its own |
| 2708 | // clock (the round's example: sealed at 100, deadline 560, cleanup at 600 |
| 2709 | // must not wait until 660). |
| 2710 | func wStagingScopeDeadline(t *testing.T, w *world) { |
| 2711 | src, tgt := w.boxes[0], w.boxes[1] |
| 2712 | w.serve(src, 1, app0) |
| 2713 | w.wake(src) |
| 2714 | w.appWrite(src) |
| 2715 | w.commitLanding(t, src, tgt) |
| 2716 | if len(w.violations) > 0 { |
| 2717 | return |
| 2718 | } |
| 2719 | var id string |
| 2720 | deadline := w.claim.Op.SealQuiet |
| 2721 | for _, o := range w.claim.Obl { |
| 2722 | if o.Kind == "park-staging" && o.Region == tgt.Region { |
| 2723 | id = o.ID |
| 2724 | if o.Scope != nil { |
| 2725 | deadline = o.Scope.deadline() |
| 2726 | } |
| 2727 | } |
| 2728 | } |
| 2729 | if id == "" { |
| 2730 | t.Fatalf("witness: no staging park for the target region after the commit: %s", w.state()) |
| 2731 | } |
| 2732 | // the target region's cleanup is delayed: its obligation runner does |
| 2733 | // not run until 40 steps past the deadline (the target's worker and |
| 2734 | // the source run as usual) |
| 2735 | for w.now < deadline+40 { |
| 2736 | w.tick(func() { w.worker(src); w.obligationRunner(src); w.worker(tgt) }, w.runConsole, w.recoveryPass) |
| 2737 | if len(w.violations) > 0 { |
| 2738 | return |
| 2739 | } |
| 2740 | } |
| 2741 | if !hasObl(w.claim.Obl, id) { |
| 2742 | t.Fatalf("witness: the staging park %s was acknowledged before its cleanup ran: %s", id, w.state()) |
| 2743 | } |
| 2744 | w.crash(tgt) // the cleanup begins under a new agent process |
| 2745 | start := w.now |
| 2746 | w.reach(t, 200, "the staging lane parked", func() bool { return !hasObl(w.claim.Obl, id) }, w.act(src, tgt), w.runConsole, w.recoveryPass) |
| 2747 | if len(w.violations) > 0 { |
| 2748 | return |
| 2749 | } |
| 2750 | if w.now < deadline { |
| 2751 | w.violate("INV-9 (witness): the staging park %s was acknowledged at %d, before its persisted deadline %d", id, w.now, deadline) |
| 2752 | return |
| 2753 | } |
| 2754 | if w.now > start+20 { |
| 2755 | w.violate("INV-9 (witness): the staging park %s was acknowledged at %d; its persisted deadline %d had passed when the cleanup began at %d, yet it waited a fresh horizon (bound at the cleanup's clock, until %d)", id, w.now, deadline, start, start+horizonH) |
| 2756 | return |
| 2757 | } |
| 2758 | w.finish(t) |
| 2759 | } |
| 2760 | |
| 2761 | // ---------- rev 7.17 ---------- |
| 2762 | |
| 2763 | // recreated drives a delete of the serving host and a create of the next |
| 2764 | // incarnation in region r, and returns once it serves. |
| 2765 | func (w *world) recreated(t *testing.T, r int) { |
| 2766 | w.userDelete() |
| 2767 | w.reach(t, 800, "host deleted and free", func() bool { |
| 2768 | c := w.claim |
| 2769 | return c != nil && c.Holder == nil && c.Op.Kind == "" && len(c.Obl) == 0 && w.rec == nil |
| 2770 | }, w.actAll(), w.runConsole, w.recoveryPass) |
| 2771 | if len(w.violations) > 0 { |
| 2772 | return |
| 2773 | } |
| 2774 | w.nextInc++ |
| 2775 | w.console = append(w.console, &consolePlan{Kind: "create", Host: "h", App: app0, OpID: w.newID("cr"), Inc: w.nextInc, Region: r}) |
| 2776 | w.reach(t, 800, "the next incarnation serves", func() bool { |
| 2777 | c := w.claim |
| 2778 | return len(w.violations) > 0 || c != nil && c.Holder != nil && c.Op.Kind == "serving" && c.Holder.Inc == w.nextInc |
| 2779 | }, w.actAll(), w.runConsole, w.recoveryPass) |
| 2780 | } |
| 2781 | |
| 2782 | // wSweepScopeMembership (claim rev 6.24 §2, R16-2): the serving |
| 2783 | // incarnation's sweep finds a late object of a deleted incarnation; the |
| 2784 | // chore that parks it is scoped to that incarnation's own location and |
| 2785 | // archives under its incarnation, never under the serving one's legacy |
| 2786 | // scope. |
| 2787 | func wSweepScopeMembership(t *testing.T, w *world) { |
| 2788 | b0 := w.boxes[0] |
| 2789 | w.serve(b0, 1, app0) |
| 2790 | w.wake(b0) |
| 2791 | w.appWrite(b0) |
| 2792 | w.recreated(t, b0.Region) |
| 2793 | if len(w.violations) > 0 { |
| 2794 | return |
| 2795 | } |
| 2796 | if w.claim.Holder.Inc != 2 { |
| 2797 | t.Fatalf("witness: incarnation %d serves, want 2: %s", w.claim.Holder.Inc, w.state()) |
| 2798 | } |
| 2799 | // a late object of incarnation 1 lands under its own location |
| 2800 | old := locationFor(1, false) |
| 2801 | k := ltxKey(old, "old", 0, 3, 3) |
| 2802 | w.buckets[b0.Region].objs[k] = append(w.buckets[b0.Region].objs[k], &version{ID: w.newVer(), B: &blob{Kind: "ltx", Level: 0, Min: 3, Max: 3, Inc: 1, Pages: map[string]int{}}}) |
| 2803 | var scope *parkScope |
| 2804 | w.reach(t, 600, "the late object parked", func() bool { |
| 2805 | for _, o := range w.claim.Obl { |
| 2806 | if o.Kind == "park-sweep" && o.Region == b0.Region && o.Scope != nil && strings.HasPrefix(k, o.Prefix) { |
| 2807 | cp := *o.Scope |
| 2808 | scope = &cp |
| 2809 | } |
| 2810 | } |
| 2811 | return len(w.violations) > 0 || w.buckets[b0.Region].current(k) == nil |
| 2812 | }, w.actAll(), w.recoveryPass) |
| 2813 | if len(w.violations) > 0 { |
| 2814 | return |
| 2815 | } |
| 2816 | if scope == nil { |
| 2817 | t.Fatalf("witness: no scoped sweep chore covered %s: %s", k, w.state()) |
| 2818 | } |
| 2819 | if scope.Location != scopeLocation(old) || scope.Inc != 1 { |
| 2820 | w.violate("INV-23 (witness): the sweep parked %s under scope %s (incarnation %d); the object's own location is %s, incarnation 1", k, scope.Location, scope.Inc, scopeLocation(old)) |
| 2821 | return |
| 2822 | } |
| 2823 | w.finish(t) |
| 2824 | } |
| 2825 | |
| 2826 | // TestLegacyLostTargetReturn (claim rev 6.24, R16-3) is the legacy |
| 2827 | // identity through a lost-target return: an adopted host whose pre-claim |
| 2828 | // writer (session 0, generation "") left a write its replica never got; |
| 2829 | // no wake before the move, so the cut session is 0 and src_covered is |
| 2830 | // false; the target is admitted cold and declared lost; the source's |
| 2831 | // return declares the target's session and the source's cut session 0, in |
| 2832 | // additional_writes_lost, and INV-24 accepts the legacy identity. |
| 2833 | func TestLegacyLostTargetReturn(t *testing.T) { |
| 2834 | w := newWitness() |
| 2835 | defer func() { |
| 2836 | if t.Failed() { |
| 2837 | dump(t, w) |
| 2838 | } |
| 2839 | }() |
| 2840 | b0, b1 := w.boxes[0], w.boxes[1] |
| 2841 | w.legacy(b0, 1) |
| 2842 | w.tick(func() { w.reconcile(b0) }) // adoption |
| 2843 | if w.claim == nil || w.claim.Holder.Session != 0 { |
| 2844 | t.Fatalf("not adopted with the legacy identity: %s", w.state()) |
| 2845 | } |
| 2846 | w.reach(t, 400, "adoption settled", func() bool { return w.claim.oblFor("adopt") == 0 }, w.actAll(), w.recoveryPass) |
| 2847 | // the pre-claim writer's last write, acknowledged, never uploaded: the |
| 2848 | // origin's level-0 uploads are held, so the cut's flush cannot land it |
| 2849 | loc := w.claim.Holder.Location |
| 2850 | w.hold = func(r *request) bool { |
| 2851 | return r.kind == rPut && r.region == b0.Region && r.b != nil && r.b.Level == 0 && genOf(loc, r.key) == "" |
| 2852 | } |
| 2853 | w.nextW++ |
| 2854 | w.commit(b0.DB, w.nextW) |
| 2855 | w.acks = append(w.acks, ack{W: w.nextW, Inc: 1, Box: b0.ID, Session: 0, Gen: "", At: w.now, Kind: "write"}) |
| 2856 | w.writeInc[w.nextW] = 1 |
| 2857 | w.moveTo(b1.Region) |
| 2858 | w.reach(t, 600, "landing probed", func() bool { |
| 2859 | c := w.claim |
| 2860 | return len(w.violations) > 0 || c.Op.Kind == "landing" && c.Op.LandPhase == "probed" && hasMain(b1) |
| 2861 | }, w.act(b0, b1), w.recoveryPass) |
| 2862 | if len(w.violations) > 0 { |
| 2863 | t.Fatalf("%s", w.violations[0]) |
| 2864 | } |
| 2865 | if w.claim.Op.SrcCovered || w.claim.Op.CutSession != 0 { |
| 2866 | t.Fatalf("the cut must be session 0 with src_covered false: covered=%v cut=%d", w.claim.Op.SrcCovered, w.claim.Op.CutSession) |
| 2867 | } |
| 2868 | tgtSession := lastAdmission(w.claim.Holder).Session |
| 2869 | w.stop(b1) |
| 2870 | w.reach(t, 400, "declared lost", func() bool { return contains(w.claim.Lost, b1.ID) }, w.act(b0), w.recoveryPass, w.operator) |
| 2871 | w.replaceDestroyed() |
| 2872 | w.reach(t, 800, "the source's return admitted", func() bool { |
| 2873 | c := w.claim |
| 2874 | l := lastAdmission(c.Holder) |
| 2875 | return len(w.violations) > 0 || c.Op.Kind == "serving" || c.Op.Kind == "restoring" && l != nil && l.Box == b0.ID && l.Session > tgtSession |
| 2876 | }, w.act(b0), w.recoveryPass, w.runConsole, w.operator) |
| 2877 | w.hold = nil |
| 2878 | w.completeHeld(dataKey(loc, "", "")) |
| 2879 | if len(w.violations) > 0 { |
| 2880 | t.Fatalf("%s", w.violations[0]) |
| 2881 | } |
| 2882 | e := lastAdmission(w.claim.Holder) |
| 2883 | seen := map[[2]int]int{} |
| 2884 | for _, x := range declarationsOf(e) { |
| 2885 | seen[[2]int{x.Box, x.Session}]++ |
| 2886 | } |
| 2887 | if seen[[2]int{b1.ID, tgtSession}] != 1 || seen[[2]int{b0.ID, 0}] != 1 { |
| 2888 | t.Fatalf("the return must declare the target's session %d and the source's cut session 0 once each: %v (record %+v)", tgtSession, seen, *e) |
| 2889 | } |
| 2890 | t.Logf("declared %v at %s; legacy declarations %d", seen, loc, w.stats["writes_lost: the legacy identity (session 0)"]) |
| 2891 | w.finish(t) |
| 2892 | if len(w.violations) > 0 { |
| 2893 | t.Fatalf("%s", w.violations[0]) |
| 2894 | } |
| 2895 | } |
| 2896 | |
| 2897 | // TestForeignManifestReplayRefused (R17-1): a persisted manifest naming |
| 2898 | // another incarnation's keys, replayed under a valid scope, is refused by |
| 2899 | // INV-23 and nothing it names is deleted. The state is constructed: no |
| 2900 | // schedule of the model produces such a manifest. |
| 2901 | func TestForeignManifestReplayRefused(t *testing.T) { |
| 2902 | w := newWitness() |
| 2903 | defer func() { |
| 2904 | if t.Failed() { |
| 2905 | dump(t, w) |
| 2906 | } |
| 2907 | }() |
| 2908 | b0 := w.boxes[0] |
| 2909 | w.serve(b0, 1, app0) |
| 2910 | w.wake(b0) |
| 2911 | w.appWrite(b0) |
| 2912 | w.recreated(t, b0.Region) |
| 2913 | if len(w.violations) > 0 || w.claim.Holder == nil || w.claim.Holder.Inc != 2 { |
| 2914 | t.Fatalf("incarnation 2 does not serve: %s", w.state()) |
| 2915 | } |
| 2916 | // a late object of incarnation 1, and a sweep chore of incarnation 2's |
| 2917 | // own location whose persisted manifest wrongly names it |
| 2918 | foreign := ltxKey(locationFor(1, false), "old", 0, 3, 3) |
| 2919 | w.buckets[b0.Region].objs[foreign] = append(w.buckets[b0.Region].objs[foreign], &version{ID: w.newVer(), B: &blob{Kind: "ltx", Level: 0, Min: 3, Max: 3, Inc: 1, Pages: map[string]int{}}}) |
| 2920 | fv := w.buckets[b0.Region].current(foreign).ID |
| 2921 | o := obligation{ID: "obx", Op: fmt.Sprintf("session:%d", w.claim.Holder.Session), Kind: "park-sweep", Region: b0.Region, Box: -1, Prefix: locationFor(2, false), Ret: "sweep", |
| 2922 | Scope: &parkScope{Location: scopeLocation(locationFor(2, false)), Inc: 2, EvidenceAt: w.now - horizonH, RequestLimit: requestLimitH}} |
| 2923 | man := &blob{Kind: "manifest", Refs: []ref{{Region: b0.Region, Key: foreign, Ver: fv}}, Dels: []ref{{Region: b0.Region, Key: foreign, Ver: fv}}} |
| 2924 | w.buckets[b0.Region].objs[o.Dest()+"manifest"] = []*version{{ID: w.newVer(), B: man}} |
| 2925 | w.cas(w.claim, func(n *claim) bool { n.Obl = append(n.Obl, o); return true }) |
| 2926 | // one step of the chore: the replay of its persisted manifest (a later |
| 2927 | // at-rest sweep may park the object legitimately under incarnation 1's |
| 2928 | // own scope, which is not in question here) |
| 2929 | w.tick(func() { w.obligationRunner(b0) }) |
| 2930 | found := false |
| 2931 | for _, v := range w.violations { |
| 2932 | if strings.Contains(v, "INV-23") && strings.Contains(v, foreign) { |
| 2933 | found = true |
| 2934 | } |
| 2935 | } |
| 2936 | if !found { |
| 2937 | t.Fatalf("the replayed foreign manifest was not refused by INV-23: %v", w.violations) |
| 2938 | } |
| 2939 | w.completeDue(true) |
| 2940 | if w.buckets[b0.Region].byID(foreign, fv) == nil { |
| 2941 | t.Fatalf("the foreign object %s@%d was deleted by the replay", foreign, fv) |
| 2942 | } |
| 2943 | t.Logf("refused: %s", w.violations[0]) |
| 2944 | } |
| 2945 | |
| 2946 | // TestStagingSurvivesLegacyPark (claim rev 6.24 §2, R16-1): a legacy host's |
| 2947 | // earlier stay in the target region is parked by the landing's install |
| 2948 | // phase while the move's sealed staging sits beside it under moves/; the |
| 2949 | // park is scoped to the legacy instance location and the staging survives |
| 2950 | // for the build. |
| 2951 | func TestStagingSurvivesLegacyPark(t *testing.T) { |
| 2952 | w := newWitness() |
| 2953 | defer func() { |
| 2954 | if t.Failed() { |
| 2955 | dump(t, w) |
| 2956 | } |
| 2957 | }() |
| 2958 | b0, b1 := w.boxes[0], w.boxes[1] |
| 2959 | w.legacy(b0, 1) // the fixture leaves an earlier stay's replica part in region 1 |
| 2960 | w.tick(func() { w.reconcile(b0) }) |
| 2961 | w.reach(t, 400, "adoption settled", func() bool { return w.claim.oblFor("adopt") == 0 }, w.actAll(), w.recoveryPass) |
| 2962 | w.recovered(t, b0, "running after adoption") |
| 2963 | w.appWrite(b0) |
| 2964 | w.moveTo(b1.Region) |
| 2965 | w.reach(t, 600, "landing probed", func() bool { |
| 2966 | c := w.claim |
| 2967 | return len(w.violations) > 0 || c.Op.Kind == "landing" && c.Op.LandPhase == "probed" && hasMain(b1) |
| 2968 | }, w.act(b0, b1), w.recoveryPass) |
| 2969 | if len(w.violations) > 0 { |
| 2970 | t.Fatalf("%s", w.violations[0]) |
| 2971 | } |
| 2972 | op := w.claim.Op |
| 2973 | for _, r := range []ref{op.SealDB, op.SealFiles} { |
| 2974 | if w.buckets[r.Region].byID(r.Key, r.Ver) == nil || w.buckets[r.Region].current(r.Key) == nil { |
| 2975 | t.Fatalf("the sealed staging %s@%d is gone from region %d after the install park", r.Key, r.Ver, r.Region) |
| 2976 | } |
| 2977 | } |
| 2978 | t.Logf("staging %s and %s survived the legacy instance park; landing probed", op.SealDB.Key, op.SealFiles.Key) |
| 2979 | w.finish(t) |
| 2980 | if len(w.violations) > 0 { |
| 2981 | t.Fatalf("%s", w.violations[0]) |
| 2982 | } |
| 2983 | } |
| 2984 | |
| 2985 | // wFreeSweepVsCreate (claim rev 6.15 §6.2a, R13-4): a deleted host's |
| 2986 | // region keeps late residue; the free host's sweep runs as a holderless |
| 2987 | // parking op, and a create requested meanwhile waits for FreeAfterPark. |
| 2988 | // Without the op the create claims the host over the outstanding park |
| 2989 | // (INV-20). |
| 2990 | func wFreeSweepVsCreate(t *testing.T, w *world) { |
| 2991 | b0 := w.boxes[0] |
| 2992 | w.serve(b0, 1, app0) |
| 2993 | w.wake(b0) |
| 2994 | w.appWrite(b0) |
| 2995 | loc := w.claim.Holder.Location |
| 2996 | w.userDelete() |
| 2997 | w.reach(t, 800, "host deleted and free", func() bool { |
| 2998 | c := w.claim |
| 2999 | return c != nil && c.Holder == nil && c.Op.Kind == "" && len(c.Obl) == 0 && w.rec == nil |
| 3000 | }, w.actAll(), w.runConsole, w.recoveryPass) |
| 3001 | if len(w.violations) > 0 { |
| 3002 | return |
| 3003 | } |
| 3004 | // a replica PUT accepted before the delete's park lands now |
| 3005 | k := ltxKey(loc, "", 0, 7, 7) |
| 3006 | w.buckets[b0.Region].objs[k] = append(w.buckets[b0.Region].objs[k], &version{ID: w.newVer(), B: &blob{Kind: "ltx", Level: 0, Min: 7, Max: 7, Inc: 1, Pages: map[string]int{}}}) |
| 3007 | // the create is requested at once; the sweep finds the residue on its |
| 3008 | // next pass |
| 3009 | w.nextInc++ |
| 3010 | w.console = append(w.console, &consolePlan{Kind: "create", Host: "h", App: app0, OpID: w.newID("cr"), Inc: w.nextInc, Region: 1}) |
| 3011 | w.reach(t, 800, "the create completed", func() bool { |
| 3012 | c := w.claim |
| 3013 | return len(w.violations) > 0 || c != nil && c.Holder != nil && c.Op.Kind == "serving" |
| 3014 | }, w.actAll(), w.runConsole, w.recoveryPass) |
| 3015 | if len(w.violations) > 0 { |
| 3016 | return |
| 3017 | } |
| 3018 | if w.stats["holderless sweeps"] == 0 && on("holderless-park") { |
| 3019 | t.Fatalf("witness: no holderless sweep ran before the create: %s", w.state()) |
| 3020 | } |
| 3021 | w.finish(t) |
| 3022 | } |
| 3023 | |
| 3024 | // wCoveredLocalBaseline (claim rev 6.22 §6.2a, R13-1): an unfinished run |
| 3025 | // whose link in this region is covered, its generation retired. The walk |
| 3026 | // must refuse the start and alert; reading objects alone, as rev 7.13 |
| 3027 | // did, it passes over the empty link and restores the marker's generation, |
| 3028 | // retired too, as an empty database (INV-2). |
| 3029 | func wCoveredLocalBaseline(t *testing.T, w *world) { |
| 3030 | b0 := w.boxes[0] |
| 3031 | w.serve(b0, 1, app0) |
| 3032 | w.wake(b0) |
| 3033 | w.appWrite(b0) |
| 3034 | w.replicate(b0) |
| 3035 | loc := w.claim.Holder.Location |
| 3036 | // a cold admission into a fresh generation g1 that runs and publishes: |
| 3037 | // the serving session closes cleanly, its certificate is removed, the |
| 3038 | // next wake is cold |
| 3039 | w.idleStop(b0) |
| 3040 | w.reach(t, 200, "closed", func() bool { return !hasMain(b0) && (b0.DB == nil || !b0.DB.Closing) }, w.act(b0)) |
| 3041 | delete(w.buckets[b0.Region].objs, closedKey(loc, "", w.claim.Holder.Session)) |
| 3042 | w.wake(b0) |
| 3043 | g1 := w.claim.Holder.Gen |
| 3044 | if g1 == "" { |
| 3045 | t.Fatalf("witness: no cold admission after the certificate was removed: %s", w.state()) |
| 3046 | } |
| 3047 | w.reach(t, 200, "g1 published", func() bool { bg, _ := w.bucketGen(b0, loc); return bg == g1 }, w.act(b0)) |
| 3048 | w.idleStop(b0) |
| 3049 | w.reach(t, 200, "g1 closed", func() bool { return !hasMain(b0) && (b0.DB == nil || !b0.DB.Closing) }, w.act(b0)) |
| 3050 | // a second cold admission, g2, that dies before its first upload: the |
| 3051 | // marker still names g1, the run is g2 -> g1 |
| 3052 | delete(w.buckets[b0.Region].objs, closedKey(loc, g1, w.claim.Holder.Session)) |
| 3053 | armed := true |
| 3054 | w.startHook = func(x *box) bool { |
| 3055 | if x != b0 || !armed { |
| 3056 | return false |
| 3057 | } |
| 3058 | armed = false |
| 3059 | w.crash(x) |
| 3060 | return true |
| 3061 | } |
| 3062 | w.wake(b0) |
| 3063 | w.startHook = nil |
| 3064 | g2 := w.claim.Holder.Gen |
| 3065 | if g2 == g1 || g2 == "" { |
| 3066 | t.Fatalf("witness: no second cold admission: %s", w.state()) |
| 3067 | } |
| 3068 | // the constructed state: g2's record is covered and g1 is retired in |
| 3069 | // this region (an operator parked it, or a chore it should not have had) |
| 3070 | w.cas(w.claim, func(n *claim) bool { |
| 3071 | for i := range n.Holder.Admissions { |
| 3072 | if n.Holder.Admissions[i].Gen == g2 { |
| 3073 | n.Holder.Admissions[i].Covered = true |
| 3074 | } |
| 3075 | } |
| 3076 | return true |
| 3077 | }) |
| 3078 | bk := w.buckets[b0.Region] |
| 3079 | for _, k := range bk.keys(dataKey(loc, g1, "")) { |
| 3080 | if genOf(loc, k) == g1 { |
| 3081 | bk.objs[k] = nil // parked: the key keeps its entry with no version |
| 3082 | } |
| 3083 | } |
| 3084 | for i := 0; i < 80; i++ { |
| 3085 | w.tick(w.act(b0), w.recoveryPass, func() { w.wake(b0) }) |
| 3086 | if len(w.violations) > 0 || hasMain(b0) { |
| 3087 | break |
| 3088 | } |
| 3089 | } |
| 3090 | if hasMain(b0) { |
| 3091 | w.checkLocal(w.claim, b0, b0.DB) // started on nothing: INV-2 |
| 3092 | return |
| 3093 | } |
| 3094 | if w.stats["start refused: covered local baseline"] == 0 { |
| 3095 | t.Fatalf("witness: the host neither started nor refused a covered local baseline: %s", w.state()) |
| 3096 | } |
| 3097 | } |
| 3098 | |
| 3099 | // ---------- rev 7.15 ---------- |
| 3100 | |
| 3101 | // wIntermediateBaseline (R14-1): the run walk selects a generation of the |
| 3102 | // run that holds an object while the marker still names the run's |
| 3103 | // baseline; the start must restore what the walk selected, rooted at |
| 3104 | // [1, 1], as the oracle does. |
| 3105 | func wIntermediateBaseline(t *testing.T, w *world) { |
| 3106 | b0 := w.boxes[0] |
| 3107 | w.serve(b0, 1, app0) |
| 3108 | w.wake(b0) |
| 3109 | w.appWrite(b0) |
| 3110 | w.replicate(b0) |
| 3111 | loc := w.claim.Holder.Location |
| 3112 | w.idleStop(b0) |
| 3113 | w.reach(t, 200, "closed", func() bool { return !hasMain(b0) && (b0.DB == nil || !b0.DB.Closing) }, w.act(b0)) |
| 3114 | delete(w.buckets[b0.Region].objs, closedKey(loc, "", w.claim.Holder.Session)) |
| 3115 | // R: a cold admission whose first upload is held in flight |
| 3116 | w.hold = func(r *request) bool { |
| 3117 | g := genOf(loc, r.key) |
| 3118 | return r.kind == rPut && r.region == b0.Region && r.b != nil && r.b.Level == 0 && g != "" && g != "-" |
| 3119 | } |
| 3120 | w.wake(b0) |
| 3121 | gR := w.claim.Holder.Gen |
| 3122 | if gR == "" { |
| 3123 | t.Fatalf("witness: no cold admission R: %s", w.state()) |
| 3124 | } |
| 3125 | w.reach(t, 30, "R's first upload issued", func() bool { return b0.open != nil && b0.open.req != nil }, w.act(b0)) |
| 3126 | w.crash(b0) // R dies with its upload pending; the marker still names S |
| 3127 | w.hold = nil |
| 3128 | // R2: admitted over the empty R, dies before uploading |
| 3129 | armed := true |
| 3130 | w.startHook = func(x *box) bool { |
| 3131 | if x != b0 || !armed { |
| 3132 | return false |
| 3133 | } |
| 3134 | armed = false |
| 3135 | w.crash(x) |
| 3136 | return true |
| 3137 | } |
| 3138 | w.wake(b0) |
| 3139 | w.startHook = nil |
| 3140 | gR2 := w.claim.Holder.Gen |
| 3141 | if gR2 == gR || gR2 == "" { |
| 3142 | t.Fatalf("witness: no second cold admission R2: %s", w.state()) |
| 3143 | } |
| 3144 | // R's delayed upload lands: R holds an object, R2 none, the marker names S |
| 3145 | if w.completeHeld(dataKey(loc, gR, "")) == 0 { |
| 3146 | t.Fatalf("witness: R's upload was not held: %s", w.state()) |
| 3147 | } |
| 3148 | // the next start: R2 -> R -> S selects R |
| 3149 | if !w.drive(120, func() bool { return hasMain(b0) }, w.act(b0), w.recoveryPass, func() { w.wake(b0) }) { |
| 3150 | if len(w.violations) == 0 { |
| 3151 | w.violate("INV-3 (witness): the start cannot restore %q, the baseline the run walk selected, while the marker names %q (%d restores refused)", gR, "", w.stats["restore refused"]) |
| 3152 | } |
| 3153 | return |
| 3154 | } |
| 3155 | if w.stats["restore: run generation rooted"] == 0 { |
| 3156 | t.Fatalf("witness: the start did not restore the selected run generation: %v", w.stats) |
| 3157 | } |
| 3158 | w.checkLocal(w.claim, b0, b0.DB) |
| 3159 | w.checkDurable(w.claim, "after the recovery") |
| 3160 | w.finish(t) |
| 3161 | } |
| 3162 | |
| 3163 | // lostTargetReturn is the common opening of the R14-2 witnesses: the |
| 3164 | // source's level-0 uploads are held so src_covered is false and its cut |
| 3165 | // session is uncertified; the landing proceeds to the given point; the |
| 3166 | // target is destroyed and declared lost; the source's return is admitted. |
| 3167 | // It returns the source's return record. |
| 3168 | func (w *world) lostTargetReturn(t *testing.T, probed bool) *admissionRecord { |
| 3169 | src, tgt := w.boxes[0], w.boxes[1] |
| 3170 | w.serve(src, 1, app0) |
| 3171 | w.wake(src) |
| 3172 | loc, gen0 := w.claim.Holder.Location, w.claim.Holder.Gen |
| 3173 | w.hold = func(r *request) bool { |
| 3174 | return r.kind == rPut && r.region == src.Region && r.b != nil && r.b.Level == 0 && genOf(loc, r.key) == gen0 |
| 3175 | } |
| 3176 | w.appWrite(src) |
| 3177 | w.replicate(src) |
| 3178 | w.moveTo(tgt.Region) |
| 3179 | if probed { |
| 3180 | w.reach(t, 600, "landing probed", func() bool { |
| 3181 | c := w.claim |
| 3182 | return c.Op.Kind == "landing" && c.Op.LandPhase == "probed" && hasMain(tgt) |
| 3183 | }, w.act(src, tgt), w.recoveryPass) |
| 3184 | } else { |
| 3185 | w.reach(t, 600, "landing built, no admission yet", func() bool { |
| 3186 | c := w.claim |
| 3187 | return c.Op.Kind == "landing" && (c.Op.LandPhase == "local" || c.Op.LandPhase == "config" || c.Op.LandPhase == "probing") && tgt.open == nil |
| 3188 | }, w.act(src, tgt), w.recoveryPass) |
| 3189 | } |
| 3190 | if len(w.violations) > 0 { |
| 3191 | return nil |
| 3192 | } |
| 3193 | if w.claim.Op.SrcCovered { |
| 3194 | t.Fatalf("witness: the seal found the source's replica complete; the held upload was not held: %s", w.state()) |
| 3195 | } |
| 3196 | w.stop(tgt) // the cloud destroys the target |
| 3197 | w.reach(t, 400, "declared lost", func() bool { return contains(w.claim.Lost, tgt.ID) }, w.act(src), w.recoveryPass, w.operator) |
| 3198 | w.replaceDestroyed() |
| 3199 | w.reach(t, 800, "the source's return admitted", func() bool { |
| 3200 | c := w.claim |
| 3201 | if len(w.violations) > 0 || c.Op.Kind == "serving" { |
| 3202 | return true |
| 3203 | } |
| 3204 | l := lastAdmission(c.Holder) |
| 3205 | return c.Op.Kind == "restoring" && l != nil && l.Box == src.ID && l.Session > c.Op.CutSession |
| 3206 | }, w.act(src), w.recoveryPass, w.runConsole, w.operator) |
| 3207 | w.hold = nil |
| 3208 | w.completeHeld(dataKey(loc, gen0, "")) |
| 3209 | if len(w.violations) > 0 { |
| 3210 | return nil |
| 3211 | } |
| 3212 | l := lastAdmission(w.claim.Holder) |
| 3213 | if l == nil || l.Box != src.ID { |
| 3214 | t.Fatalf("witness: the source's return is not the last admission: %s", w.state()) |
| 3215 | } |
| 3216 | return l |
| 3217 | } |
| 3218 | |
| 3219 | // declarationsOf is a record's declarations, the ordinary one and the list. |
| 3220 | func declarationsOf(e *admissionRecord) []*writesLost { |
| 3221 | var out []*writesLost |
| 3222 | if e.Lost != nil { |
| 3223 | out = append(out, e.Lost) |
| 3224 | } |
| 3225 | return append(out, e.AdditionalWritesLost...) |
| 3226 | } |
| 3227 | |
| 3228 | // wNoDuplicateDeclarationEarly (R14-2): the target is destroyed before its |
| 3229 | // first admission, so the source's cut session is the predecessor itself; |
| 3230 | // it is declared once, as writes_lost, and never again in the list. |
| 3231 | func wNoDuplicateDeclarationEarly(t *testing.T, w *world) { |
| 3232 | e := w.lostTargetReturn(t, false) |
| 3233 | if e == nil { |
| 3234 | return |
| 3235 | } |
| 3236 | cut := w.claim.Op.CutSession |
| 3237 | n := 0 |
| 3238 | for _, x := range declarationsOf(e) { |
| 3239 | if x.Box == w.boxes[0].ID && x.Session == cut { |
| 3240 | n++ |
| 3241 | } |
| 3242 | } |
| 3243 | if n != 1 && len(w.violations) == 0 { |
| 3244 | w.violate("INV-21 (witness): the source's cut session %d was declared %d times by its return admission", cut, n) |
| 3245 | return |
| 3246 | } |
| 3247 | w.finish(t) |
| 3248 | } |
| 3249 | |
| 3250 | // wNoDuplicateDeclarationLate (R14-2): the target was admitted (its probe |
| 3251 | // session is the predecessor); the list carries the source's cut session |
| 3252 | // once and no target session twice. |
| 3253 | func wNoDuplicateDeclarationLate(t *testing.T, w *world) { |
| 3254 | e := w.lostTargetReturn(t, true) |
| 3255 | if e == nil { |
| 3256 | return |
| 3257 | } |
| 3258 | cut := w.claim.Op.CutSession |
| 3259 | seen := map[[2]int]int{} |
| 3260 | for _, x := range declarationsOf(e) { |
| 3261 | seen[[2]int{x.Box, x.Session}]++ |
| 3262 | } |
| 3263 | if seen[[2]int{w.boxes[0].ID, cut}] != 1 && len(w.violations) == 0 { |
| 3264 | w.violate("INV-21 (witness): the source's cut session %d was declared %d times behind the lost target", cut, seen[[2]int{w.boxes[0].ID, cut}]) |
| 3265 | return |
| 3266 | } |
| 3267 | for k, c := range seen { |
| 3268 | if c > 1 && len(w.violations) == 0 { |
| 3269 | w.violate("INV-21 (witness): {box %d, session %d} declared %d times", k[0], k[1], c) |
| 3270 | return |
| 3271 | } |
| 3272 | } |
| 3273 | if e.Predecessor.Box != w.boxes[1].ID { |
| 3274 | t.Fatalf("witness: the predecessor is not the target's probe session: %s", w.state()) |
| 3275 | } |
| 3276 | w.finish(t) |
| 3277 | } |
| 3278 | |
| 3279 | // TestJoinHolderlessSweep (R14-4) is the positive case of rev 7.14 note 1: |
| 3280 | // a deleted host keeps late residue in two regions; the first region's |
| 3281 | // sweep starts the holderless parking op and the second region's joins |
| 3282 | // it with its own scoped chores under the same op id. |
| 3283 | func TestJoinHolderlessSweep(t *testing.T) { |
| 3284 | w := newWitness() |
| 3285 | defer func() { |
| 3286 | if t.Failed() { |
| 3287 | dump(t, w) |
| 3288 | } |
| 3289 | }() |
| 3290 | b0 := w.boxes[0] |
| 3291 | w.serve(b0, 1, app0) |
| 3292 | w.wake(b0) |
| 3293 | w.appWrite(b0) |
| 3294 | loc := w.claim.Holder.Location |
| 3295 | w.userDelete() |
| 3296 | w.reach(t, 800, "host deleted and free", func() bool { |
| 3297 | c := w.claim |
| 3298 | return c != nil && c.Holder == nil && c.Op.Kind == "" && len(c.Obl) == 0 && w.rec == nil |
| 3299 | }, w.actAll(), w.runConsole, w.recoveryPass) |
| 3300 | if len(w.violations) > 0 { |
| 3301 | t.Fatalf("%s", w.violations[0]) |
| 3302 | } |
| 3303 | for _, r := range []int{0, 1} { |
| 3304 | k := ltxKey(loc, "", 0, 7, 7) |
| 3305 | w.buckets[r].objs[k] = append(w.buckets[r].objs[k], &version{ID: w.newVer(), B: &blob{Kind: "ltx", Level: 0, Min: 7, Max: 7, Inc: 1, Pages: map[string]int{}}}) |
| 3306 | } |
| 3307 | // region 0's box sweeps first, then region 1's joins the running op |
| 3308 | joined := false |
| 3309 | w.tick(w.act(w.boxes[0])) |
| 3310 | if c := w.claim; c.Op.Kind != "parking" || c.Op.ParkSweep == "" { |
| 3311 | t.Fatalf("no holderless sweep started: %s", w.state()) |
| 3312 | } |
| 3313 | id := w.claim.Op.ID |
| 3314 | w.tick(w.act(w.boxes[1])) |
| 3315 | regions := map[int]bool{} |
| 3316 | for _, o := range w.claim.Obl { |
| 3317 | if o.Kind == "park-sweep" && o.Op == id { |
| 3318 | regions[o.Region] = true |
| 3319 | } |
| 3320 | } |
| 3321 | joined = regions[0] && regions[1] && w.claim.Op.ID == id |
| 3322 | if !joined { |
| 3323 | t.Fatalf("region 1 did not join op %s: %s", id, w.state()) |
| 3324 | } |
| 3325 | w.reach(t, 800, "freed after the park", func() bool { c := w.claim; return c != nil && c.Holder == nil && c.Op.Kind == "" && len(c.Obl) == 0 }, w.actAll(), w.recoveryPass) |
| 3326 | if len(w.violations) > 0 { |
| 3327 | t.Fatalf("%s", w.violations[0]) |
| 3328 | } |
| 3329 | if w.stats["holderless sweeps"] != 1 || w.stats["sweep joined a running holderless op"] < 1 || w.stats["free after park"] != 1 { |
| 3330 | t.Fatalf("one op, one join, one free expected: %v", w.stats) |
| 3331 | } |
| 3332 | t.Logf("op %s: regions %v joined, freed once", id, regions) |
| 3333 | w.finish(t) |
| 3334 | if len(w.violations) > 0 { |
| 3335 | t.Fatalf("%s", w.violations[0]) |
| 3336 | } |
| 3337 | } |
| 3338 | |
| 3339 | // TestInterruptedCleanReturn (R13-1) is the positive case of claim rev |
| 3340 | // 6.22's run walk across regions: a clean rollback's fresh source |
| 3341 | // admission dies before its first upload, so the run is R -> T -> S with T, |
| 3342 | // the target's generation, in the other region and covered under its park; |
| 3343 | // the walk passes T over and restores S; then one more interrupted |
| 3344 | // admission afterward, R2 -> R -> T -> S. |
| 3345 | func TestInterruptedCleanReturn(t *testing.T) { |
| 3346 | w := newWitness() |
| 3347 | defer func() { |
| 3348 | if t.Failed() { |
| 3349 | dump(t, w) |
| 3350 | } |
| 3351 | }() |
| 3352 | src, tgt := w.boxes[0], w.boxes[1] |
| 3353 | w.serve(src, 1, app0) |
| 3354 | w.wake(src) |
| 3355 | w.appWrite(src) |
| 3356 | w.replicate(src) |
| 3357 | w.landProbed(t, src, tgt) |
| 3358 | loc, gen0 := w.claim.Holder.Location, w.claim.Op.SrcGen |
| 3359 | w.rollback(w.claim, "settle check failed") // the target wrote nothing: a clean rollback |
| 3360 | crashes := 0 |
| 3361 | w.startHook = func(x *box) bool { |
| 3362 | if x != src || crashes >= 2 || w.claim.Op.Kind != "restoring" && w.claim.Op.Kind != "serving" { |
| 3363 | return false |
| 3364 | } |
| 3365 | crashes++ |
| 3366 | w.crash(x) // before the first upload: the fresh generation is empty |
| 3367 | return true |
| 3368 | } |
| 3369 | w.reach(t, 800, "the source's return admission crashed", func() bool { return crashes >= 1 }, w.act(src, tgt), w.recoveryPass, w.runConsole) |
| 3370 | if len(w.violations) > 0 { |
| 3371 | t.Fatalf("%s", w.violations[0]) |
| 3372 | } |
| 3373 | // the recovery: R is empty, T is the other region's, S holds the data |
| 3374 | w.recovered(t, src, "source recovered across the interrupted return") |
| 3375 | if w.stats["abandoned empty generation skipped"] < 1 { |
| 3376 | t.Fatalf("the recovery did not walk the run: %v", w.stats) |
| 3377 | } |
| 3378 | w.checkLocal(w.claim, src, src.DB) |
| 3379 | if len(w.violations) > 0 { |
| 3380 | t.Fatalf("%s", w.violations[0]) |
| 3381 | } |
| 3382 | // one more interrupted admission afterward: R2 -> R -> T -> S |
| 3383 | w.reach(t, 1500, "the rollback finished", func() bool { return w.claim.Op.Kind == "serving" }, w.act(src, tgt), w.recoveryPass, w.runConsole) |
| 3384 | if len(w.violations) > 0 { |
| 3385 | t.Fatalf("%s", w.violations[0]) |
| 3386 | } |
| 3387 | w.idleStop(src) |
| 3388 | w.reach(t, 200, "closed", func() bool { return !hasMain(src) }, w.act(src)) |
| 3389 | delete(w.buckets[src.Region].objs, closedKey(loc, w.claim.Holder.Gen, w.claim.Holder.Session)) |
| 3390 | w.wake(src) // cold, and the hook crashes it before its upload |
| 3391 | w.startHook = nil |
| 3392 | if crashes != 2 { |
| 3393 | t.Fatalf("the second admission did not crash (%d crashes): %s", crashes, w.state()) |
| 3394 | } |
| 3395 | w.recovered(t, src, "source recovered across two interrupted admissions") |
| 3396 | w.checkLocal(w.claim, src, src.DB) |
| 3397 | w.checkDurable(w.claim, "after the second recovery") |
| 3398 | if len(w.violations) > 0 { |
| 3399 | t.Fatalf("%s", w.violations[0]) |
| 3400 | } |
| 3401 | t.Logf("run walked twice from %q: %d empty generations skipped, %d starts refused", gen0, w.stats["abandoned empty generation skipped"], w.stats["start refused: covered local baseline"]) |
| 3402 | w.finish(t) |
| 3403 | if len(w.violations) > 0 { |
| 3404 | t.Fatalf("%s", w.violations[0]) |
| 3405 | } |
| 3406 | } |
| 3407 | |
| 3408 | // wTwoSessionDeclaration (R12-1) is a constructed-state oracle test: the |
| 3409 | // loss oracle's exemption, applied to acknowledgements of two sessions. |
| 3410 | // A box's first session acknowledged a write that never uploaded; so did |
| 3411 | // its second. A writes_lost record naming the second session exempts the |
| 3412 | // second write only (INV-18): the first stays an undeclared loss for the |
| 3413 | // oracles to report. Rev 7.12's match by box and incarnation absolved it. |
| 3414 | func wTwoSessionDeclaration(t *testing.T, w *world) { |
| 3415 | b := w.boxes[0] |
| 3416 | w.serve(b, 1, app0) |
| 3417 | h := w.claim.Holder |
| 3418 | s1 := h.Session |
| 3419 | w1 := w.ackInto(b, 1) // session 1's write, never uploaded |
| 3420 | s2 := s1 + 1 |
| 3421 | b.DB.Session = s2 // the constructed second session on the same box, same generation |
| 3422 | w2 := w.ackInto(b, 1) |
| 3423 | rec := &writesLost{Box: b.ID, Gen: h.Gen, Session: s2} |
| 3424 | n := w.exemptDeclared(b, rec, h, h.Gen, false) |
| 3425 | var x1, x2 *ack |
| 3426 | for i := range w.acks { |
| 3427 | switch w.acks[i].W { |
| 3428 | case w1: |
| 3429 | x1 = &w.acks[i] |
| 3430 | case w2: |
| 3431 | x2 = &w.acks[i] |
| 3432 | } |
| 3433 | } |
| 3434 | if x2 == nil || !x2.Exempt { |
| 3435 | t.Fatalf("witness: the declared session's write %d was not exempted", w2) |
| 3436 | } |
| 3437 | if x1 != nil && x1.Exempt { |
| 3438 | w.violate("INV-18 (witness): the writes_lost record for session %d exempted write %d, which session %d acknowledged and no record declares (%d exempted)", s2, w1, s1, n) |
| 3439 | } |
| 3440 | } |
| 3441 | |
| 3442 | // wRollbackBaselinePreserved (claim rev 6.14 item 5, R12-3): the target's |
| 3443 | // publication leaves the source's generation uncovered, with no chore, in |
| 3444 | // the source's region. Under the mutation a park-generation chore for it |
| 3445 | // is queued into the source's region from the target's publication; the |
| 3446 | // witness brings the chore's quiet time forward to now (the schedule |
| 3447 | // seeds 1036 and 1296 / rev 7.12 found with a landing open past the |
| 3448 | // horizon), lets the source's obligation runner work within the settle |
| 3449 | // window, then rolls the landing back cleanly: the return restores from |
| 3450 | // the source's generation. |
| 3451 | func wRollbackBaselinePreserved(t *testing.T, w *world) { |
| 3452 | src, tgt := w.boxes[0], w.boxes[1] |
| 3453 | w.serve(src, 1, app0) |
| 3454 | w.wake(src) |
| 3455 | w.appWrite(src) |
| 3456 | w.replicate(src) |
| 3457 | w.landProbed(t, src, tgt) |
| 3458 | loc, gen0 := w.claim.Holder.Location, w.claim.Op.SrcGen |
| 3459 | chores := 0 |
| 3460 | w.cas(w.claim, func(n *claim) bool { |
| 3461 | for i := range n.Obl { |
| 3462 | if n.Obl[i].Kind == "park-generation" && n.Obl[i].Region == src.Region { |
| 3463 | n.Obl[i].Quiet = w.now // the horizon has passed |
| 3464 | chores++ |
| 3465 | } |
| 3466 | } |
| 3467 | return true |
| 3468 | }) |
| 3469 | w.logf("witness: %d park-generation chores in the source's region after the target's publication", chores) |
| 3470 | // within the settle window, before the target's commit: the source |
| 3471 | // region's runner works the chore, if any |
| 3472 | w.drive(12, func() bool { return !w.hasFilesIn(src.Region, loc, gen0) }, w.act(src, tgt)) |
| 3473 | if len(w.violations) > 0 { |
| 3474 | return |
| 3475 | } |
| 3476 | if !w.hasFilesIn(src.Region, loc, gen0) { |
| 3477 | w.logf("witness: the source's generation %q is gone from region %d before the rollback", gen0, src.Region) |
| 3478 | } |
| 3479 | w.rollback(w.claim, "settle check failed") // the target wrote nothing: a clean rollback |
| 3480 | w.reach(t, 800, "source re-admitted after the rollback", func() bool { |
| 3481 | c := w.claim |
| 3482 | return len(w.violations) > 0 || c.Op.Kind == "serving" || c.Op.Kind == "restoring" && (c.Op.SrcPhase == "probed" || c.Op.SrcPhase == "opened" || c.Op.SrcPhase == "stuck") |
| 3483 | }, w.act(src, tgt), w.recoveryPass, w.runConsole) |
| 3484 | if len(w.violations) > 0 { |
| 3485 | return |
| 3486 | } |
| 3487 | if w.claim.Op.Kind == "restoring" && w.claim.Op.SrcPhase == "stuck" { |
| 3488 | w.violate("stuck: source could not recover %s: its generation %q was parked while the landing was still open", w.claim.Op.ID, gen0) |
| 3489 | return |
| 3490 | } |
| 3491 | w.recovered(t, src, "source serving again") |
| 3492 | w.checkLocal(w.claim, src, src.DB) |
| 3493 | w.checkDurable(w.claim, "after the rollback") |
| 3494 | w.finish(t) |
| 3495 | } |
| 3496 | |
| 3497 | // commitLanding drives a probed landing through its commit: the record |
| 3498 | // flips first, then whoever reads both follows it with the claim's CAS. |
| 3499 | // It returns the target's admission record, whose predecessor is the |
| 3500 | // source's generation in the source's region. |
| 3501 | func (w *world) commitLanding(t *testing.T, src, tgt *box) *admissionRecord { |
| 3502 | w.landProbed(t, src, tgt) |
| 3503 | var target *admissionRecord |
| 3504 | for i := range w.claim.Holder.Admissions { |
| 3505 | e := &w.claim.Holder.Admissions[i] |
| 3506 | if e.Box == tgt.ID && e.Mode == "cold" { |
| 3507 | target = e |
| 3508 | } |
| 3509 | } |
| 3510 | if target == nil || target.PredRegion != src.Region || target.Predecessor.Gen != w.claim.Op.SrcGen { |
| 3511 | t.Fatalf("witness: the target's record does not name the source's generation in the source's region: %s", w.state()) |
| 3512 | } |
| 3513 | if target.Covered { |
| 3514 | t.Fatalf("witness: the target's record was covered by its own publication, with its predecessor in another region: %s", w.state()) |
| 3515 | } |
| 3516 | w.reach(t, 400, "landing committed", func() bool { return w.claim.Op.Kind == "landing" && w.claim.Op.Committed }, w.act(src, tgt), w.recoveryPass, w.runConsole) |
| 3517 | return target |
| 3518 | } |
| 3519 | |
| 3520 | // targetRecord finds the target's cold admission record in the claim now. |
| 3521 | func (w *world) targetRecord(tgt *box) *admissionRecord { |
| 3522 | var out *admissionRecord |
| 3523 | for i := range w.claim.Holder.Admissions { |
| 3524 | e := &w.claim.Holder.Admissions[i] |
| 3525 | if e.Box == tgt.ID && e.Mode == "cold" { |
| 3526 | out = e |
| 3527 | } |
| 3528 | } |
| 3529 | return out |
| 3530 | } |
| 3531 | |
| 3532 | // wCommitCoverage (claim rev 6.14 item 6, R12-3): the commit's CAS queues |
| 3533 | // the source region's whole-location park and covers the target's record |
| 3534 | // in the same CAS. |
| 3535 | func wCommitCoverage(t *testing.T, w *world) { |
| 3536 | src, tgt := w.boxes[0], w.boxes[1] |
| 3537 | w.serve(src, 1, app0) |
| 3538 | w.wake(src) |
| 3539 | w.appWrite(src) |
| 3540 | w.commitLanding(t, src, tgt) |
| 3541 | if len(w.violations) > 0 { |
| 3542 | return |
| 3543 | } |
| 3544 | e := w.targetRecord(tgt) |
| 3545 | if e == nil { |
| 3546 | t.Fatalf("witness: the target's record is gone after the commit: %s", w.state()) |
| 3547 | } |
| 3548 | parks := 0 |
| 3549 | for _, o := range w.claim.Obl { |
| 3550 | if o.Kind == "park-superseded" && o.Region == src.Region { |
| 3551 | parks++ |
| 3552 | } |
| 3553 | } |
| 3554 | if parks != 1 { |
| 3555 | t.Fatalf("witness: %d park-superseded obligations for the source region after the commit: %s", parks, w.state()) |
| 3556 | } |
| 3557 | if !e.Covered { |
| 3558 | w.logf("witness: the target's record is uncovered after the commit's CAS queued the source region's park") |
| 3559 | } |
| 3560 | w.finish(t) // INV-17 at the end: an uncovered record whose predecessor's objects the park retired |
| 3561 | } |
| 3562 | |
| 3563 | // wCommitInterrupted (R12-3, interruption): the record flips to committed |
| 3564 | // and nothing follows it for longer than the horizon; the claim's CAS, |
| 3565 | // parks and coverage in one, is performed by whoever reads both later. |
| 3566 | func wCommitInterrupted(t *testing.T, w *world) { |
| 3567 | src, tgt := w.boxes[0], w.boxes[1] |
| 3568 | w.serve(src, 1, app0) |
| 3569 | w.wake(src) |
| 3570 | w.appWrite(src) |
| 3571 | w.landProbed(t, src, tgt) |
| 3572 | // the record commits (the target's settle check passed) with no claim CAS following |
| 3573 | w.reach(t, 400, "record committed", func() bool { return w.rec != nil && w.rec.MoveState == "committed" }, func() { w.worker(tgt) }) |
| 3574 | if w.claim.Op.Committed { |
| 3575 | t.Fatalf("witness: the claim followed the record in the same step; the interruption needs a gap: %s", w.state()) |
| 3576 | } |
| 3577 | for i := 0; i < horizonH+10; i++ { |
| 3578 | w.tick() // every actor paused: nobody follows the record |
| 3579 | } |
| 3580 | if w.claim.Op.Committed { |
| 3581 | t.Fatalf("witness: the claim committed while every actor was paused: %s", w.state()) |
| 3582 | } |
| 3583 | w.reach(t, 400, "landing committed after the interruption", func() bool { return w.claim.Op.Kind == "landing" && w.claim.Op.Committed }, w.act(src, tgt), w.recoveryPass, w.runConsole) |
| 3584 | if len(w.violations) > 0 { |
| 3585 | return |
| 3586 | } |
| 3587 | if e := w.targetRecord(tgt); e != nil && !e.Covered { |
| 3588 | w.logf("witness: the target's record is uncovered after the replayed commit") |
| 3589 | } |
| 3590 | w.finish(t) |
| 3591 | } |
| 3592 | |
| 3593 | // wCommitReplayed (R12-3, replay): after the commit's CAS another reader |
| 3594 | // follows the record again; the replay is refused, the source region's |
| 3595 | // park is queued once and the coverage stands. |
| 3596 | func wCommitReplayed(t *testing.T, w *world) { |
| 3597 | src, tgt := w.boxes[0], w.boxes[1] |
| 3598 | w.serve(src, 1, app0) |
| 3599 | w.wake(src) |
| 3600 | w.appWrite(src) |
| 3601 | w.commitLanding(t, src, tgt) |
| 3602 | if len(w.violations) > 0 { |
| 3603 | return |
| 3604 | } |
| 3605 | before := w.claim.Ver |
| 3606 | if w.followRecord(w.claim) || w.claim.Ver != before { |
| 3607 | w.violate("INV-17 (witness): the commit's CAS was replayed after it committed (claim %d, now %d)", before, w.claim.Ver) |
| 3608 | return |
| 3609 | } |
| 3610 | parks := 0 |
| 3611 | for _, o := range w.claim.Obl { |
| 3612 | if o.Kind == "park-superseded" && o.Region == src.Region { |
| 3613 | parks++ |
| 3614 | } |
| 3615 | } |
| 3616 | if parks != 1 { |
| 3617 | w.violate("INV-17 (witness): %d park-superseded obligations for the source region after the replay", parks) |
| 3618 | return |
| 3619 | } |
| 3620 | w.finish(t) |
| 3621 | } |
| 3622 | |
| 3623 | // wProbeWindowAt (R12-2): the landing probe's environment is ready exactly |
| 3624 | // at the deadline. Under the rule the attempt fails before the start and |
| 3625 | // the next admission's probe is accepted; without the check before the |
| 3626 | // start, the expired attempt starts and is accepted (INV-19). |
| 3627 | func wProbeWindowAt(t *testing.T, w *world) { |
| 3628 | w.probeWindow(t, probeStartWindow) |
| 3629 | if len(w.violations) > 0 { |
| 3630 | return |
| 3631 | } |
| 3632 | w.finish(t) |
| 3633 | } |
| 3634 | |
| 3635 | // probeWindow runs a landing whose target's launch environment is ready k |
| 3636 | // steps after the probe attempt's app stage first runs, and reports how |
| 3637 | // the first attempt ended. The knob is released once the first attempt |
| 3638 | // has been counted, so the next attempt proceeds at once. |
| 3639 | func (w *world) probeWindow(t *testing.T, k int) (accepted bool) { |
| 3640 | src, tgt := w.boxes[0], w.boxes[1] |
| 3641 | w.serve(src, 1, app0) |
| 3642 | w.wake(src) |
| 3643 | tgt.envUnreadyFor = k |
| 3644 | w.moveTo(tgt.Region) |
| 3645 | id := w.claim.Op.ID |
| 3646 | w.reach(t, 800, "landing probed", func() bool { |
| 3647 | c := w.claim |
| 3648 | if c.Op.ID == id && c.Op.ProbeTries > 0 { |
| 3649 | tgt.envUnreadyFor = 0 |
| 3650 | } |
| 3651 | return len(w.violations) > 0 || c.Op.ID != id || c.Op.Kind == "landing" && c.Op.LandPhase == "probed" && hasMain(tgt) |
| 3652 | }, w.act(src, tgt), w.recoveryPass) |
| 3653 | if w.claim.Op.ID != id { |
| 3654 | t.Fatalf("witness: the move %s ended before its probe: %s", id, w.state()) |
| 3655 | } |
| 3656 | return w.claim.Op.ProbeTries == 0 |
| 3657 | } |
| 3658 | |
| 3659 | // TestProbeWindow (R12-2) walks the boundary: readiness k steps after the |
| 3660 | // attempt's first app stage, for k just before, at and after the window. |
| 3661 | func TestProbeWindow(t *testing.T) { |
| 3662 | for _, k := range []int{probeStartWindow - 1, probeStartWindow, probeStartWindow + 1} { |
| 3663 | w := newWitness() |
| 3664 | accepted := w.probeWindow(t, k) |
| 3665 | if len(w.violations) > 0 { |
| 3666 | t.Fatalf("k=%d: %s", k, w.violations[0]) |
| 3667 | } |
| 3668 | p := w.boxes[1].lastProbe |
| 3669 | tries := w.claim.Op.ProbeTries |
| 3670 | beforeStart, atEnv := w.stats["probe attempt failed: deadline before the start"], w.stats["probe attempt failed: environment"] |
| 3671 | switch { |
| 3672 | case k < probeStartWindow && !accepted: |
| 3673 | t.Errorf("k=%d: the attempt within the window was not accepted (tries %d)", k, tries) |
| 3674 | case k < probeStartWindow && p.readyAt-p.startedAt != k: |
| 3675 | t.Errorf("k=%d: the accepted attempt answered %d steps after its first start", k, p.readyAt-p.startedAt) |
| 3676 | case k >= probeStartWindow && accepted: |
| 3677 | t.Errorf("k=%d: an attempt at or beyond the deadline was accepted", k) |
| 3678 | case k == probeStartWindow && beforeStart != 1: |
| 3679 | // ready exactly at the deadline: the check before the start |
| 3680 | t.Errorf("k=%d: the deadline check before the start did not fail the attempt (stats %v)", k, w.stats) |
| 3681 | case k > probeStartWindow && atEnv != 1: |
| 3682 | // still unready at the deadline: the attempt fails there |
| 3683 | t.Errorf("k=%d: the deadline did not fail the attempt while the environment was unready (stats %v)", k, w.stats) |
| 3684 | case k >= probeStartWindow && tries != 1: |
| 3685 | t.Errorf("k=%d: %d probe tries counted, want 1", k, tries) |
| 3686 | } |
| 3687 | w.finish(t) |
| 3688 | if len(w.violations) > 0 { |
| 3689 | t.Fatalf("k=%d: %s", k, w.violations[0]) |
| 3690 | } |
| 3691 | t.Logf("k=%d: accepted=%v tries=%d probe start %d ready %d (failed before the start %d, at the deadline unready %d)", k, accepted, tries, p.startedAt, p.readyAt, beforeStart, atEnv) |
| 3692 | } |
| 3693 | } |
| 3694 | |
| 3695 | // TestK8JudgesOnlyASucceededRelease (Task 7 fix round 2): the K8 oracle |
| 3696 | // judges a release CAS that succeeded, never one the op-id guard refused. |
| 3697 | // The source closes a clean rollback's record and its goroutine stalls |
| 3698 | // before the release; the recovery pass releases from last_move; a purge |
| 3699 | // runs to the end and removes the record; the stalled release resumes with |
| 3700 | // only revalidate-before-effect dropped. Its CAS is conditional on the |
| 3701 | // rollback's op, which the claim no longer holds: refused, the claim is |
| 3702 | // untouched, and nothing is violated. |
| 3703 | func TestK8JudgesOnlyASucceededRelease(t *testing.T) { |
| 3704 | saved := mutated |
| 3705 | mutated = "revalidate-before-effect" |
| 3706 | defer func() { mutated = saved }() |
| 3707 | w := newWitness() |
| 3708 | src, tgt := w.boxes[0], w.boxes[1] |
| 3709 | w.serve(src, 1, app0) |
| 3710 | w.landProbed(t, src, tgt) |
| 3711 | w.rollback(w.claim, "cut deadline") |
| 3712 | w.reach(t, 1500, "source about to close", func() bool { |
| 3713 | c := w.claim |
| 3714 | return c.Op.Kind == "restoring" && c.Op.SrcPhase == "opened" && c.oblFor(c.Op.ID) == 0 |
| 3715 | }, w.act(src, tgt), w.recoveryPass) |
| 3716 | old := w.claim.clone() // the stalled goroutine's read |
| 3717 | if !w.closeRecord(old, src.ID) { |
| 3718 | t.Fatalf("the record did not close: %s", w.state()) |
| 3719 | } |
| 3720 | w.reach(t, 50, "released from last_move", func() bool { return w.claim.Op.Kind == "serving" }, w.recoveryPass) |
| 3721 | pg := &consolePlan{Kind: "purge", App: app0} |
| 3722 | w.reach(t, 2000, "the purge removed the record", func() bool { return w.rec == nil }, func() { w.runPlan(pg) }, w.actAll(), w.recoveryPass) |
| 3723 | before := w.claim.clone() |
| 3724 | w.resumeStaleRelease(src, old) |
| 3725 | if len(w.violations) > 0 { |
| 3726 | dump(t, w) |
| 3727 | t.Fatalf("a refused stale release was judged: %v", w.violations) |
| 3728 | } |
| 3729 | if w.claim.Ver != before.Ver || w.claim.Op.Kind == "serving" && w.claim.Op.Exec == src.ID && w.claim.Holder != nil { |
| 3730 | t.Fatalf("the stale release was not refused: before %s after %s", before.Op.Kind, w.state()) |
| 3731 | } |
| 3732 | } |
| 3733 | |
amadan