| 1 | // Package hostlife is a deterministic, randomized model of the host |
| 2 | // lifecycle claim (docs/superpowers/specs/2026-10-02-host-lifecycle-claim-design.md, |
| 3 | // rev 6.5, d36adcfa) and Phase 1 of move-any-app |
| 4 | // (docs/superpowers/specs/2026-10-02-move-any-app-design.md, rev 7.7). |
| 5 | // |
| 6 | // Since joint round 2 the model encodes what the specs say and nothing |
| 7 | // stronger: restore reads the holder's location and the generation the |
| 8 | // claim names, the start check compares markers, every multi-object step |
| 9 | // is split at its real write boundaries, and the final oracle only reads. |
| 10 | // |
| 11 | // It is test-only. Nothing here is product code: every file is a _test.go |
| 12 | // file, so `go build ./...` never sees it. It exists to find interleavings |
| 13 | // that prose review rounds kept missing, and to prove each protocol rule is |
| 14 | // load-bearing by mutation (see rules_test.go and README in the spec §14.2). |
| 15 | // |
| 16 | // The model is an abstraction. What it keeps, and what it drops, is listed |
| 17 | // in the spec's §14.2; the short version: |
| 18 | // |
| 19 | // - one host, three regions, one box per region (plus replacement boxes); |
| 20 | // - every bucket is versioned, with the real IAM split: a box has full |
| 21 | // rights on its own data bucket, and only Put/Delete/CopyInto on another |
| 22 | // region's moves/* (no Get, no ListVersions, no DeleteVersion); |
| 23 | // - every S3 request may complete late, after the client gave up; |
| 24 | // - boxes crash (agent restart: flat children die, memory lost), reboot, |
| 25 | // freeze (whole-VM pause), pause (agent only), partition from the |
| 26 | // control bucket, are destroyed, or boot-recover an old executable; |
| 27 | // - the application writes and registers timers on its own, through |
| 28 | // descendants that may outlive the main process. |
| 29 | package hostlife |
| 30 | |
| 31 | import ( |
| 32 | "fmt" |
| 33 | "sort" |
| 34 | "strings" |
| 35 | ) |
| 36 | |
| 37 | const ( |
| 38 | nRegions = 3 |
| 39 | app0 = "A" |
| 40 | app1 = "B" |
| 41 | |
| 42 | // Time is in model steps. |
| 43 | // H, the late-completion horizon (claim §6.2a): a request may complete |
| 44 | // up to H steps after issue. It is the signature-age limit plus the |
| 45 | // request bound, request_limit_ns (claim rev 6.15 §2); the park scope |
| 46 | // persists the request bound and the horizon is computed from it (R14-3) |
| 47 | horizonH = sigAgeH + requestLimitH |
| 48 | sigAgeH = 45 // the signature-age allowance (the 15 minutes) |
| 49 | requestLimitH = 15 // request_limit_ns: the longest request, added to the signature age |
| 50 | execTTL = 40 // exec lease TTL |
| 51 | execRenew = 15 // renew when this close to expiry |
| 52 | lostMargin = 10 // declare-lost margin past expiry |
| 53 | cutBudget = 320 // absolute cut deadline after admission |
| 54 | stagingTTL = 400 // staging-work lease TTL: longer than the cut budget, as in production |
| 55 | probeTries = 3 |
| 56 | // probeStartWindow is a probe attempt's readiness window in steps (the |
| 57 | // budget's 30 s, §7.3): the retry policy's app restarts within one |
| 58 | // admitted session share it, and when it passes the attempt fails and |
| 59 | // the operation counts one of its budgeted tries (rev 7.12 §7.7) |
| 60 | probeStartWindow = 30 |
| 61 | readyWait = 800 // abort a move whose readiness never comes |
| 62 | maxSkew = 1 // a box clock is within this of true time |
| 63 | maxPause = 3 // a typical pause between a check and the act (a VM freeze is longer) |
| 64 | sigAge = 30 // S3's signature-age limit; H covers it plus the longest request |
| 65 | beyondH = 20 // one long-tail request in this many completes after H (R2-1) |
| 66 | retiredCap = 32 // retired_incarnations keeps this many (claim rev 6 §2) |
| 67 | ) |
| 68 | |
| 69 | // retire adds inc to retired_incarnations, dropping the oldest past the cap. |
| 70 | func retire(xs []int, inc int) []int { |
| 71 | xs = addUniq(xs, inc) |
| 72 | if len(xs) > retiredCap { |
| 73 | xs = append([]int(nil), xs[len(xs)-retiredCap:]...) |
| 74 | } |
| 75 | return xs |
| 76 | } |
| 77 | |
| 78 | // ---------- storage ---------- |
| 79 | |
| 80 | type blob struct { |
| 81 | Kind string // "ltx", "base", "files", "snap", "lock", "manifest", "lease", "report", "gen" |
| 82 | Inc int // incarnation tag; 0 = untagged legacy |
| 83 | Gen string // lineage that wrote it |
| 84 | Seq int |
| 85 | SealKey int // the instance.key the data is sealed with |
| 86 | // an LTX file (ltx_test.go, R4-1, R5-2): its level (0 and 1, 9 for a |
| 87 | // snapshot), its range in replication numbering, the final image of |
| 88 | // every key it touches (0 is a delete), and, for the oracle only, the |
| 89 | // writes it covers. No database checksum: the pinned writers put none |
| 90 | // in a file (litestreamfacts, R5-2) |
| 91 | Level int |
| 92 | Min int |
| 93 | Max int |
| 94 | Pages map[string]int |
| 95 | TXs []int |
| 96 | // Full: the file carries every page (a snapshot, an anchor, litestream's |
| 97 | // first sync after a cold initialization, a compaction of one of those), |
| 98 | // so applying it replaces the state; a key absent from it is gone |
| 99 | Full bool |
| 100 | // a "gen" marker (R3-1, R4-1): the generation's snapshot by key, version |
| 101 | // id and TXID |
| 102 | Base int |
| 103 | SnapKey string |
| 104 | TX int |
| 105 | // a "closed" certificate (claim rev 6.8 §6.4a): the writer's stamp and |
| 106 | // session; Seq is its box and TX its max_txid |
| 107 | Stamp int |
| 108 | Session int |
| 109 | Files *filesDir |
| 110 | Timers []int |
| 111 | Refs []ref // a park manifest's archive set |
| 112 | Dels []ref // a park manifest's deletion set, delete markers included |
| 113 | Text string |
| 114 | } |
| 115 | |
| 116 | type ref struct { |
| 117 | Region int // -1 = control bucket |
| 118 | Key string |
| 119 | Ver int |
| 120 | } |
| 121 | |
| 122 | type version struct { |
| 123 | ID int |
| 124 | B *blob |
| 125 | Marker bool |
| 126 | Straggler bool // created by a request that completed after H |
| 127 | SweepOwed bool // a dead generation's files key its park kept while live: the at-rest sweep's once obsolete (claim §6.2a) |
| 128 | } |
| 129 | |
| 130 | type bucket struct { |
| 131 | objs map[string][]*version |
| 132 | } |
| 133 | |
| 134 | func newBucket() *bucket { return &bucket{objs: map[string][]*version{}} } |
| 135 | |
| 136 | func (b *bucket) keys(prefix string) []string { |
| 137 | var out []string |
| 138 | for k := range b.objs { |
| 139 | if strings.HasPrefix(k, prefix) { |
| 140 | out = append(out, k) |
| 141 | } |
| 142 | } |
| 143 | sort.Strings(out) |
| 144 | return out |
| 145 | } |
| 146 | |
| 147 | func (b *bucket) current(key string) *version { |
| 148 | vs := b.objs[key] |
| 149 | if len(vs) == 0 { |
| 150 | return nil |
| 151 | } |
| 152 | v := vs[len(vs)-1] |
| 153 | if v.Marker { |
| 154 | return nil |
| 155 | } |
| 156 | return v |
| 157 | } |
| 158 | |
| 159 | func (b *bucket) byID(key string, id int) *version { |
| 160 | for _, v := range b.objs[key] { |
| 161 | if v.ID == id { |
| 162 | return v |
| 163 | } |
| 164 | } |
| 165 | return nil |
| 166 | } |
| 167 | |
| 168 | // dataVersions are every non-marker version under prefix. |
| 169 | func (b *bucket) dataVersions(prefix string) []ref { |
| 170 | var out []ref |
| 171 | for _, k := range b.keys(prefix) { |
| 172 | for _, v := range b.objs[k] { |
| 173 | if !v.Marker { |
| 174 | out = append(out, ref{Key: k, Ver: v.ID}) |
| 175 | } |
| 176 | } |
| 177 | } |
| 178 | return out |
| 179 | } |
| 180 | |
| 181 | func (b *bucket) hasData(prefix string, skipLock bool) bool { |
| 182 | for _, k := range b.keys(prefix) { |
| 183 | if skipLock && strings.HasSuffix(k, "lock.json") { |
| 184 | continue |
| 185 | } |
| 186 | for _, v := range b.objs[k] { |
| 187 | if !v.Marker { |
| 188 | return true |
| 189 | } |
| 190 | } |
| 191 | } |
| 192 | return false |
| 193 | } |
| 194 | |
| 195 | // ---------- locations and generations (claim C3a, moves rev 6 §5.1) ---------- |
| 196 | |
| 197 | // locationFor is holder.location for an incarnation. |
| 198 | func locationFor(inc int, legacy bool) string { |
| 199 | if legacy || !on("location-per-incarnation") { |
| 200 | return "instances/" + host + "/" |
| 201 | } |
| 202 | return fmt.Sprintf("instances/%s/%d/", host, inc) |
| 203 | } |
| 204 | |
| 205 | // dataKey is a replica object of generation gen within location loc. The |
| 206 | // origin generation keeps the bare layout; every later generation has its |
| 207 | // own operation-scoped prefix, so a request from one generation that lands |
| 208 | // late can only ever add an object to that generation. |
| 209 | func dataKey(loc, gen, kind string) string { |
| 210 | if gen == "" { |
| 211 | return loc + kind |
| 212 | } |
| 213 | return loc + "g-" + gen + "/" + kind |
| 214 | } |
| 215 | |
| 216 | func genMarkerKey(loc string) string { return loc + "generation.json" } |
| 217 | |
| 218 | func isDataKey(k string) bool { |
| 219 | return strings.HasPrefix(k, "instances/") && ltxKeyRe.MatchString(k) |
| 220 | } |
| 221 | |
| 222 | // ---------- requests (late completion) ---------- |
| 223 | |
| 224 | type reqKind int |
| 225 | |
| 226 | const ( |
| 227 | rPut reqKind = iota |
| 228 | rDelVer |
| 229 | rDelKey // bare-key delete: forbidden on host prefixes (mutation only) |
| 230 | rCopy // copy srcRegion/srcKey?versionId=srcVer -> region/key |
| 231 | ) |
| 232 | |
| 233 | type request struct { |
| 234 | kind reqKind |
| 235 | region int |
| 236 | key string |
| 237 | b *blob |
| 238 | ver int |
| 239 | srcRegion int |
| 240 | srcKey string |
| 241 | srcVer int |
| 242 | doneAt int |
| 243 | beyond bool // completes after H |
| 244 | ifSet bool // a conditional PUT: If-Match ifVer, or If-None-Match when ifVer is 0 |
| 245 | ifVer int |
| 246 | hold bool // the biased schedule holds it until its worst moment (rev 7.5: a generation marker) |
| 247 | by string |
| 248 | done bool // completed (or refused) on the server; the client may have given up long before |
| 249 | at int // when the client issued it |
| 250 | // result, for an immediate completion |
| 251 | resultVer int |
| 252 | } |
| 253 | |
| 254 | // ---------- local box state ---------- |
| 255 | |
| 256 | type filesDir struct { |
| 257 | Inc int |
| 258 | Key int // the app's instance.key identity |
| 259 | Gen string // .files-gen marker |
| 260 | Env int // admin token identity in <host>.env |
| 261 | Done bool // markers written last |
| 262 | Stamp int // the installation stamp that produced it (claim rev 6.5 §6.3) |
| 263 | // Obj is the files object that holds this content (region HA §5.6, |
| 264 | // rev 4): written by the generation that first held it, in ObjRegion's |
| 265 | // bucket; an unchanged file keeps naming it generations later |
| 266 | Obj string |
| 267 | ObjRegion int |
| 268 | } |
| 269 | |
| 270 | func (f *filesDir) clone() *filesDir { |
| 271 | if f == nil { |
| 272 | return nil |
| 273 | } |
| 274 | c := *f |
| 275 | return &c |
| 276 | } |
| 277 | |
| 278 | type localDB struct { |
| 279 | Inc int |
| 280 | Loc string // the holder location it was restored from (claim C3a) |
| 281 | Gen string // <dbPath>.gen |
| 282 | Key int // the key it was sealed with |
| 283 | State map[string]int |
| 284 | TX int // the lineage's transaction id: the oracle's order of acknowledged writes |
| 285 | Pos int // the replication position: litestream's TXID, the count of files shipped, which every LTX range is numbered in (R5-1) |
| 286 | Pending []int // writes since Pos (what the next LTX file ships) |
| 287 | // Epoch is the agent process that was admitted for this database: a |
| 288 | // session belongs to the agent's replicator, and a new agent process |
| 289 | // is a new session (claim rev 6.10), so a restarted agent neither |
| 290 | // replicates nor certifies for it (seed 8528 / 30,000: the restarted |
| 291 | // agent's first sync was skipped at the dead session's remote position) |
| 292 | Epoch int |
| 293 | // the local level-0 files not yet confirmed uploaded, oldest first: |
| 294 | // litestream writes each sync's file locally and the replica uploads |
| 295 | // them in TXID order, never past one that has not completed (rev 7.6) |
| 296 | Queue []*blob |
| 297 | InFlight *request // the head's upload, as the client sees it |
| 298 | InFlightAt int |
| 299 | // FirstFull: the next level-0 file carries every page (litestream's |
| 300 | // first sync after a cold initialization, fact R5-1c) |
| 301 | FirstFull bool |
| 302 | // Closing: the writer stopped cleanly and is draining its uploads |
| 303 | // before writing its certificate (claim rev 6.8 §6.4a); CloseReq is the |
| 304 | // marker PUT once issued |
| 305 | Closing bool |
| 306 | CloseReq *request |
| 307 | // Session is the writer session this database was admitted under; Issued |
| 308 | // is every request the writer issued that did not return at once (level |
| 309 | // 0, compaction, snapshot, retention), and Uncertain is sticky once any |
| 310 | // of them timed out and was retried (R8-5): no certificate then. |
| 311 | Session int |
| 312 | Issued []*request |
| 313 | Uncertain bool |
| 314 | // RemotePos is the remote position the pinned replica caches until an |
| 315 | // initialization or an error: the newest remote level-0 TXID it has |
| 316 | // seen or uploaded (R8-5) |
| 317 | RemotePos int |
| 318 | Log []int // every write applied here, for the oracle |
| 319 | Stamp int // the installation stamp that produced this artifact (claim rev 6.5 §6.3) |
| 320 | Seq int |
| 321 | } |
| 322 | |
| 323 | func (d *localDB) clone() *localDB { |
| 324 | if d == nil { |
| 325 | return nil |
| 326 | } |
| 327 | c := *d |
| 328 | c.State = cloneState(d.State) |
| 329 | c.Pending = append([]int(nil), d.Pending...) |
| 330 | c.Queue = append([]*blob(nil), d.Queue...) |
| 331 | c.Log = append([]int(nil), d.Log...) |
| 332 | return &c |
| 333 | } |
| 334 | |
| 335 | type proc struct { |
| 336 | Main bool |
| 337 | Strict bool // spawned into the host cgroup by strict placement |
| 338 | Inc int |
| 339 | Gen string |
| 340 | Session int // the writer session the process was started under: what its acknowledgements carry (rev 7.13, R12-1) |
| 341 | Box int |
| 342 | } |
| 343 | |
| 344 | type row struct { |
| 345 | Inc int |
| 346 | App string |
| 347 | Status string // ready, moving, landing, restoring, releasing |
| 348 | HoldOp string |
| 349 | Repl string // carried column |
| 350 | Next int // carried column |
| 351 | } |
| 352 | |
| 353 | type box struct { |
| 354 | ID int |
| 355 | Region int |
| 356 | Destroyed bool |
| 357 | Frozen bool // whole-VM pause: nothing on the box runs |
| 358 | AgentPaused bool // the agent alone is paused |
| 359 | AgentDown bool // the agent crashed and has not restarted |
| 360 | Partitioned bool // cannot reach the control bucket |
| 361 | Old bool // running a pre-floor executable |
| 362 | HasKey bool |
| 363 | Skew int |
| 364 | FailApp bool // the app fails its readiness check on this box |
| 365 | FailArchive bool // the final archive fails (too large) on this box |
| 366 | FailSettle bool // the app passes one readiness check, works, then fails |
| 367 | Nested bool // nested layout: children survive an agent crash |
| 368 | // region HA (two boxes per region, L18) |
| 369 | Terminated bool // the cloud terminated the instance (H1): it never runs again and never returns; a Destroyed box that is not Terminated is stopped and may start again with its disk |
| 370 | TerminatedAt int |
| 371 | // a relocation controller's durable record (hostexec, 1b-next Task 7): |
| 372 | // the operation it belongs to, whether its scoped cleanup is still owed |
| 373 | // (ground truth for INV-29), and the fault that makes the cleanup fail |
| 374 | execRecord string |
| 375 | cleanupPending bool |
| 376 | cleanupFails bool |
| 377 | relRecord *releaseRecord // (rev 9) ReleasePositions: the flushed positions of one release, recorded on disk against its stop; an agent restart keeps it |
| 378 | fencePending bool // (rev 8) this worker step found a relocation participant's fence it could not consume |
| 379 | FenceObservedAt int // the box-fences record's observed_at: when a worker first saw it terminated; 0 no record (rev 4) |
| 380 | Enrolled bool // the roster holds an active entry with its proven cloud identity (H11); a replacement box is enrolled automatically enrollDelay steps after it launches (H16, H17) |
| 381 | EnrollAt int |
| 382 | DeleteOnTermination bool // every volume the box had attached carried the flag while it ran (§5.9): decides only the automatic discharge of its park-local chores (H19), never a fence |
| 383 | installEpoch int // the agent process that made this box's local install for a relocation (B2-5): a later process never remakes it once an admission named P |
| 384 | // receipt is the box's install journal for a relocation (1b-next Task 8c, |
| 385 | // VerifyReceipt): durable, it survives an agent restart; a park of the |
| 386 | // installation removes it, and so does a lost volume (a witness) |
| 387 | receipt *receiptEntry |
| 388 | // the files publisher (§5.6, Task 4): the generation it publishes in, |
| 389 | // its sequence there, the state its last manifest carried (in memory), |
| 390 | // and the release's final manifest while its PUT is outstanding |
| 391 | pubGen string |
| 392 | pubSeq int |
| 393 | published string |
| 394 | releaseSeq int |
| 395 | // attemptTag is the probe attempt this agent process has counted and |
| 396 | // not yet ended (memory: a restart forgets it, and the next attempt is |
| 397 | // counted again, ruling 19) |
| 398 | attemptTag string |
| 399 | // L18 joint round findings 2 and 3 (regionha_completion_test.go): |
| 400 | // actFence is the activator's fence on the host (its owner; "" none), |
| 401 | // in the agent's memory, so a restart empties it; probeFence is the |
| 402 | // persisted owner a probe stop installs under (probe-fence.json), |
| 403 | // kept until the completion is marked; relFence is root's admission |
| 404 | // fence of a release (the op it closed admission for), written with |
| 405 | // Collect after the flush and the positions (ruling 28), never a row |
| 406 | // hold; owedDischarge |
| 407 | // is ground truth, the completed relocation whose participation this |
| 408 | // box has not yet discharged (C10). foreignFence is a witness's |
| 409 | // stand-in for another operation's fence that its owner never lifted |
| 410 | // (INV-32's ground truth). dischargeFails, markFails and crashAfter |
| 411 | // are witness knobs on the completion pass |
| 412 | actFence string |
| 413 | probeFence string |
| 414 | relFence string |
| 415 | // launchClosedOp and launchClosedSession: the session whose launch |
| 416 | // journal a release's StopWriters closed (durable; L18 joint round 2 |
| 417 | // finding 3): it is never relaunched, an admitted start included |
| 418 | launchClosedOp string |
| 419 | launchClosedSession int |
| 420 | // probeRecord is the probe stop's recorded positions (ruling 87), |
| 421 | // durable: a restart after it stops the session without a new flush |
| 422 | probeRecord *probeRecordEntry |
| 423 | owedDischarge string |
| 424 | foreignFence string |
| 425 | dischargeFails bool |
| 426 | markFails bool |
| 427 | crashAfter string |
| 428 | |
| 429 | Row *row |
| 430 | DB *localDB |
| 431 | Files *filesDir |
| 432 | Config int // incarnation the config.env was rendered for; 0 none |
| 433 | CfgVer int // the bundle version it was rendered from |
| 434 | Live string // app the live symlink points at |
| 435 | LiveInc int |
| 436 | Timers []int // active once-timers (registration ids) |
| 437 | History []int // delivered history (disposable) |
| 438 | Attempt int // runner bookkeeping |
| 439 | Procs []*proc |
| 440 | // Stamps is the local record per host incarnation (claim rev 6.5 §6.4, |
| 441 | // R4-2): {active_stamp | none, retired_stamps}. A stamp is the claim |
| 442 | // gen captured at the CAS that made an installation current here. A |
| 443 | // writer is admitted only if its stamp equals the active one. |
| 444 | Stamps map[int]*stamps |
| 445 | Parked int // count of locally parked artifacts |
| 446 | // open is an admitted session's start in progress (rev 7.11 §7.14): |
| 447 | // the claim CAS is done; the purge, the restore, the app start and |
| 448 | // readiness, the first upload, the marker and the anchor follow, each |
| 449 | // retried by the same agent process; the session is the agent's, and a |
| 450 | // new agent process is a new session (claim rev 6.10) |
| 451 | open *openState |
| 452 | // lastProbe is the last probe attempt's timing on this box (INV-19); |
| 453 | // envUnreadyFor is a witness knob holding the launch environment |
| 454 | // unready for that many steps after an attempt's app stage first runs |
| 455 | lastProbe probeTiming |
| 456 | envUnreadyFor int |
| 457 | // the retry policy for failed app starts within a session (rev 7.11 |
| 458 | // §7.14): consecutive failures, the earliest next attempt, and the |
| 459 | // host marked failed once the limit is reached (no new sessions until |
| 460 | // an operator clears it) |
| 461 | startFails int |
| 462 | nextStart int |
| 463 | hostFailed bool |
| 464 | failCounted bool // the operation's probe counted this host failure as one failed try |
| 465 | failedAt int // when the host was marked failed; the operator looks after a while |
| 466 | // PurgeFails is the fault: the purge of the local database an admitted |
| 467 | // writer must make before it starts returns an error (claim rev 6.9) |
| 468 | PurgeFails bool |
| 469 | // anchors are the PUTs this box's activator must see acknowledged before |
| 470 | // it goes on (an anchor, a recovery's snapshot, a closed.json), by key |
| 471 | // (rev 7.7, R6-1): a request the client has waited uploadTimeout steps |
| 472 | // for is retried with the same bytes. |
| 473 | anchors map[string][]*request |
| 474 | |
| 475 | ExecUntil int // local exec-lease file (watchdog input); 0 none |
| 476 | // in-memory, lost on crash |
| 477 | snap *claim |
| 478 | stale *claim // a stalled worker's old read |
| 479 | deferred []*localWrite |
| 480 | Epoch int |
| 481 | plans []*plan |
| 482 | stopped map[string]bool |
| 483 | StopEvidence map[string]bool // published stop evidence, by operation (survives a restart) |
| 484 | mem map[string]bool |
| 485 | evidAt map[string]int |
| 486 | pendingTimers []int |
| 487 | } |
| 488 | |
| 489 | // plan is a host-specific write by a separate OS process |
| 490 | // (carlos-config-sync, carlos-adopt), decided now and acted on later: the |
| 491 | // shape of every stale-writer race (J-N8, J2-R2-3). It survives an agent |
| 492 | // crash, because it is not the agent; a reboot ends it. It may pause |
| 493 | // before it takes the host guard. |
| 494 | type plan struct { |
| 495 | Kind string // "config", "adopt" |
| 496 | Inc int |
| 497 | App string |
| 498 | Ver int // the config bundle version it selected |
| 499 | At int // it takes the guard no earlier than this |
| 500 | // Stamp is the installation stamp the pass read when it selected the |
| 501 | // row (claim rev 6.5 §6.4, R2-3): the host guard admits the write only |
| 502 | // if it is still the active stamp. |
| 503 | Stamp int |
| 504 | } |
| 505 | |
| 506 | // stamps is a box's local record for one incarnation of the host (claim |
| 507 | // rev 6.3 §6.4): the active installation's stamp (0 is none) and the |
| 508 | // stamps of the installations retired here. |
| 509 | type stamps struct { |
| 510 | Active int |
| 511 | Retired []int |
| 512 | } |
| 513 | |
| 514 | func (b *box) stampOf(inc int) int { |
| 515 | if s := b.Stamps[inc]; s != nil { |
| 516 | return s.Active |
| 517 | } |
| 518 | return 0 |
| 519 | } |
| 520 | |
| 521 | // stampRetired: st is in the record's retired_stamps for inc. |
| 522 | func (b *box) stampRetired(inc, st int) bool { |
| 523 | s := b.Stamps[inc] |
| 524 | return s != nil && contains(s.Retired, st) |
| 525 | } |
| 526 | |
| 527 | // install is activation (claim rev 6.5 §6.4): the box's record for inc |
| 528 | // takes holder.stamp as the installing CAS wrote it (a create's serving |
| 529 | // CAS, a landing's flip, an adoption, a reinstall, a dirty rollback's |
| 530 | // probe CAS, a push's commit), or as initRecord read it fresh under the |
| 531 | // guard. Activation is one of the two moves of a stamp: the old active |
| 532 | // stamp, if any, goes into retired_stamps first, then the new one is set. |
| 533 | // Under the guard. |
| 534 | func (b *box) install(inc, gen int) { |
| 535 | if b.Stamps == nil { |
| 536 | b.Stamps = map[int]*stamps{} |
| 537 | } |
| 538 | if b.Stamps[inc] == nil { |
| 539 | b.Stamps[inc] = &stamps{} |
| 540 | } |
| 541 | s := b.Stamps[inc] |
| 542 | if s.Active != 0 && s.Active != gen && !contains(s.Retired, s.Active) { |
| 543 | s.Retired = append(s.Retired, s.Active) |
| 544 | } |
| 545 | s.Active = gen |
| 546 | } |
| 547 | |
| 548 | // retireArtifacts is claim rev 6.5's retire-artifacts(S): the local |
| 549 | // artifacts tagged S (the database, the files directory) are parked, and |
| 550 | // the record is untouched: neither active_stamp nor retired_stamps moves. |
| 551 | // Only activation and retire-installation move stamps. A landing uses it |
| 552 | // on its predecessor's leftovers; a dirty rollback parks its pre-move |
| 553 | // database with S still active, and S retires when the probe CAS's new |
| 554 | // stamp activates. It parks by tag, as the real inventory does (R6-4): an |
| 555 | // artifact of incarnation inc that carries another stamp stays, and the |
| 556 | // callers assert what they expect the tags to be (INV-6). |
| 557 | func (w *world) retireArtifacts(b *box, inc, stamp int) { |
| 558 | w.retireDatabase(b, inc, stamp) |
| 559 | if b.Files != nil && b.Files.Inc == inc && b.Files.Stamp == stamp { |
| 560 | b.Files = nil |
| 561 | b.Parked++ |
| 562 | } |
| 563 | } |
| 564 | |
| 565 | // retireDatabase is retire-artifacts(S) for the database alone: the files |
| 566 | // directory is carried into the new generation (a push, F7 on §5.1; a |
| 567 | // landing's restore phase after its files were installed; the activator's |
| 568 | // park of a warm database from an earlier stay before a cold restore). |
| 569 | func (w *world) retireDatabase(b *box, inc, stamp int) { |
| 570 | if b.DB != nil && b.DB.Inc == inc && b.DB.Stamp == stamp { |
| 571 | b.DB = nil |
| 572 | b.Parked++ |
| 573 | } |
| 574 | } |
| 575 | |
| 576 | // retireStamp is claim rev 6.5's retire-installation: the active stamp |
| 577 | // moves into retired_stamps and becomes none; the caller parks every |
| 578 | // artifact. Used at a delete, a move away, and the quarantine. |
| 579 | func (b *box) retireStamp(inc int) { |
| 580 | if b.Stamps == nil { |
| 581 | b.Stamps = map[int]*stamps{} |
| 582 | } |
| 583 | if b.Stamps[inc] == nil { |
| 584 | b.Stamps[inc] = &stamps{} |
| 585 | } |
| 586 | if a := b.Stamps[inc].Active; a != 0 { |
| 587 | b.Stamps[inc].Retired = append(b.Stamps[inc].Retired, a) |
| 588 | } |
| 589 | b.Stamps[inc].Active = 0 |
| 590 | } |
| 591 | |
| 592 | // admitsStamp is the local record's admission (claim rev 6.5 §6.4): the |
| 593 | // writer's stamp must equal the active stamp; none active refuses all, |
| 594 | // and so does no record at all (R5-4: a writer is never admitted before |
| 595 | // initialization). The mutation of fence-stamp admits any writer for the |
| 596 | // incarnation while an installation is active (rev 7.4's behaviour); the |
| 597 | // mutation of fence-by-installation is rev 5.2's marker: once retired, |
| 598 | // never active again. |
| 599 | func (b *box) admitsStamp(inc, stamp int) bool { |
| 600 | s := b.Stamps[inc] |
| 601 | if s == nil { |
| 602 | return false |
| 603 | } |
| 604 | if !on("fence-by-installation") && len(s.Retired) > 0 { |
| 605 | return false |
| 606 | } |
| 607 | if s.Active == 0 { |
| 608 | return false |
| 609 | } |
| 610 | if !on("fence-stamp") { |
| 611 | return true |
| 612 | } |
| 613 | return stamp == s.Active |
| 614 | } |
| 615 | |
| 616 | func (b *box) forget() { |
| 617 | b.Epoch++ // every goroutine of the old agent is gone |
| 618 | // a new agent process is a new session (claim rev 6.10): an admitted |
| 619 | // start in progress is gone with its restored database and its |
| 620 | // outstanding requests (R10-2), and the start retry count with it |
| 621 | b.open = nil |
| 622 | b.startFails, b.nextStart = 0, 0 |
| 623 | b.deferred = nil |
| 624 | b.snap, b.stopped, b.stale = nil, nil, nil |
| 625 | b.mem = map[string]bool{} |
| 626 | b.evidAt = map[string]int{} |
| 627 | b.pendingTimers = nil |
| 628 | b.attemptTag = "" |
| 629 | b.actFence = "" // the activator's fences die with the agent; probe-fence.json survives (ruling 75) |
| 630 | if b.DB != nil { |
| 631 | b.DB.InFlight = nil // the upload's client is gone; the restarted replica uploads the same file again |
| 632 | // a writer that was draining before its clean close is gone with |
| 633 | // its uploads unaccounted for: no closed.json (claim rev 6.6 §6.4a) |
| 634 | b.DB.Closing, b.DB.CloseReq = false, nil |
| 635 | } |
| 636 | b.anchors = nil // the activator issues the anchor again, the same bytes |
| 637 | } |
| 638 | |
| 639 | // ackedPut is a PUT the activator must see acknowledged before it goes on |
| 640 | // (R6-1): it issues the request once, retries the same bytes after |
| 641 | // uploadTimeout steps while none has returned, and reports whether one has. |
| 642 | func (w *world) ackedPut(b *box, key string, bl *blob, ifNone bool) bool { |
| 643 | acked, inflight := false, false |
| 644 | for _, r := range b.anchors[key] { |
| 645 | if r.done { |
| 646 | acked = true |
| 647 | } else if w.now-r.at < uploadTimeout { |
| 648 | inflight = true |
| 649 | } |
| 650 | } |
| 651 | if acked || inflight { |
| 652 | return acked |
| 653 | } |
| 654 | r := &request{kind: rPut, region: b.Region, key: key, b: bl, ifSet: ifNone} |
| 655 | if v := w.issue(b.ID, r); v > 0 { |
| 656 | return true |
| 657 | } |
| 658 | if r.done { |
| 659 | return true // refused (412): the object is already there, written once |
| 660 | } |
| 661 | if b.anchors == nil { |
| 662 | b.anchors = map[string][]*request{} |
| 663 | } |
| 664 | b.anchors[key] = append(b.anchors[key], r) |
| 665 | return false |
| 666 | } |
| 667 | |
| 668 | // ---------- control plane ---------- |
| 669 | |
| 670 | type holder struct { |
| 671 | Inc int |
| 672 | App string |
| 673 | Serial int // ground-truth creation event (model only) |
| 674 | Legacy bool |
| 675 | // Location is holder.location (claim C3a): instances/<host>/<inc>/ for a |
| 676 | // new incarnation, instances/<host>/ for an adopted legacy host. It never |
| 677 | // changes while this holder holds the host. |
| 678 | Location string |
| 679 | // Gen is the generation within the location that the claim names as |
| 680 | // current (moves rev 6 §5.1): "" is origin; a move, a push and a dirty |
| 681 | // rollback each install a generation named by their op id. |
| 682 | Gen string |
| 683 | // WriterBox is holder.writer_box (claim rev 6.9): the box every |
| 684 | // admission names as the current writer; it survives operation |
| 685 | // replacement, so a later cold admission's writes_lost names it (R9-2). |
| 686 | WriterBox int |
| 687 | // Admissions is holder.admissions (claim rev 6.12): the record of writer |
| 688 | // admissions whose chain is not yet finished or whose predecessors are |
| 689 | // not yet queued for retirement, plus the last few covered ones; it |
| 690 | // lives in the holder, so it survives every operation transition, |
| 691 | // release and new operation. An admission's predecessor is always the |
| 692 | // last entry here (session, box, generation), never the generation an |
| 693 | // operation chose for a restore (R11-4) |
| 694 | Admissions []admissionRecord |
| 695 | // Session is holder.session (claim rev 6.8 §6.4a, R8-1): the gen of the |
| 696 | // AdmitWriter CAS that admitted the current writer session. Every path |
| 697 | // that opens replication goes through that CAS, which moves the |
| 698 | // session forward, so a clean-close certificate (written per session) |
| 699 | // is one-use by construction. |
| 700 | Session int |
| 701 | // Stamp is holder.stamp (claim rev 6.5 §2, R5-4): the gen produced by |
| 702 | // the CAS that made the current installation current, written by that |
| 703 | // same CAS: a create's serving CAS, adoption, a flip, a reinstall, a |
| 704 | // dirty rollback's install, a push's commit. The claim is where a box |
| 705 | // recovers its local record from. |
| 706 | Stamp int |
| 707 | } |
| 708 | |
| 709 | type obligation struct { |
| 710 | ID string |
| 711 | Op string |
| 712 | Kind string // park-replica, park-local, park-superseded, park-staging |
| 713 | Region int |
| 714 | Box int |
| 715 | Prefix string |
| 716 | Ret string |
| 717 | Quiet int // not before |
| 718 | Scope *parkScope // the persisted park scope of a remote chore (claim rev 6.15 §2), bound before its first step runs |
| 719 | Owner string // a regional chore's owner: "" is region:<r> (any worker of the region, P6-D5); box:<b> is the legacy form a fence passes to the region (1b-next rev 6 finding 2) |
| 720 | } |
| 721 | |
| 722 | // parkScope is claim rev 6.23's park scope {location, incarnation, |
| 723 | // evidence_at, request_limit_ns} (§2), persisted in the chore when it is |
| 724 | // queued or bound before its first step, so every retry, an agent |
| 725 | // restart's included, uses the same location, archive incarnation and |
| 726 | // original evidence time: a retry's own clock is never evidence (R13-4, |
| 727 | // R15-1). Location is exactly one of instances/<host>, |
| 728 | // instances/<host>/<incarnation>, moves/<host>/<op id> (a move's staging |
| 729 | // or a rollback's return lane) or moves/<host> (the staging sweep), with |
| 730 | // no trailing "/". EvidenceAt is always the original evidence or fencing |
| 731 | // bound: the stop evidence a whole-location park cites, the seal bound of |
| 732 | // a staging lane (the time after which no staging writer, its lease |
| 733 | // holder included, can still write), the sweeping box's listing, the |
| 734 | // publication that supersedes a generation; never cleanup's start time. |
| 735 | // Every scope has the one deadline: acknowledge only after a listing |
| 736 | // later than EvidenceAt + H, H = sigAgeH + RequestLimit. |
| 737 | type parkScope struct { |
| 738 | Location string |
| 739 | Inc int |
| 740 | EvidenceAt int |
| 741 | RequestLimit int // request_limit_ns: the longest request, which H adds to the signature age |
| 742 | } |
| 743 | |
| 744 | // deadline is the scope's acknowledgement bound: a listing later than |
| 745 | // evidence_at + H (claim rev 6.23 §2, §6.2a). |
| 746 | func (s *parkScope) deadline() int { return s.EvidenceAt + sigAgeH + s.RequestLimit } |
| 747 | |
| 748 | // admissionRecord is one AdmitWriter (claim rev 6.8 §6.4a): the session it |
| 749 | // produced, the box and generation it admitted, the stamp, the mode (warm |
| 750 | // or cold), whether the writer has opened, and the predecessor it observed. |
| 751 | type admissionRecord struct { |
| 752 | Session, Box int |
| 753 | Gen string |
| 754 | Stamp int |
| 755 | Mode string // warm or cold (claim rev 6.9) |
| 756 | Predecessor pred |
| 757 | Lost *writesLost // a cold admission whose observed session had no certificate (claim rev 6.9, R9-2) |
| 758 | // Coverage is the admission's coverage of its predecessor's writes |
| 759 | // (claim rev 6.12): "" (uncovered: writes_lost unless certified), |
| 760 | // "sealed" (a from_db seal), "clean-return" (a clean rollback with |
| 761 | // src_covered). The entry always names it |
| 762 | Coverage string |
| 763 | Covered bool // this cold admission's predecessor has had its park-generation chore queued by a PublishGeneration (claim rev 6.12) |
| 764 | // Region is where this writer's generation keeps its objects; |
| 765 | // PredRegion where the predecessor's are, -1 when it holds none |
| 766 | // anywhere (claim rev 6.14 §6.4a item 1: region, predecessor_region) |
| 767 | Region int |
| 768 | PredRegion int |
| 769 | // AdditionalWritesLost (claim rev 6.22 item 2, additional_writes_lost): |
| 770 | // behind a declared-lost target, every other session the target was |
| 771 | // admitted into since the cut, certified or not (no return lane carries |
| 772 | // any of their writes, seed 33373 / 100,000), and the source's cut |
| 773 | // session when src_covered is false (the seal in the lost region was |
| 774 | // the one holder of its writes beyond the replica, seeds 16395 and |
| 775 | // 27191 / 30,000; rev 7.11's LostSrc). With Lost, unique by (box, |
| 776 | // session) (R14-2) |
| 777 | AdditionalWritesLost []*writesLost |
| 778 | } |
| 779 | |
| 780 | // pred is the predecessor an admission journals: the session, writer box, |
| 781 | // generation and stamp it observed. |
| 782 | type pred struct { |
| 783 | Session, Box int |
| 784 | Gen string |
| 785 | Stamp int |
| 786 | } |
| 787 | |
| 788 | // openState is an admitted writer between its AdmitWriter CAS and its |
| 789 | // process start (rev 7.10 §7.14): the generation and session it was |
| 790 | // admitted to, the database it restored, and the stage whose PUT it waits |
| 791 | // for: "first" (a fresh generation's full first upload), "marker" |
| 792 | // (generation.json), "anchor" (a warm restore above the level-0 maximum). |
| 793 | type openState struct { |
| 794 | Gen, Want string |
| 795 | Session int |
| 796 | Mode string |
| 797 | Prepared bool |
| 798 | Probe bool |
| 799 | Source string // the generation the restore reads |
| 800 | SourcePin int // how: -1 the marker's generation (restoreCalc); 0 a generation the run walk selected, rooted at [1, 1] (R14-1) |
| 801 | RemoteMax int // the certificate's max_txid a warm restore must reach |
| 802 | DB *localDB |
| 803 | stage string // restore, app, first, marker, anchor, open |
| 804 | req *request |
| 805 | blob *blob // the first upload's or the anchor's bytes, captured once: a retry carries the same bytes (R10-7; seed 7574 / 30,000) |
| 806 | pendAt int // the pending writes the captured blob covers; later acknowledgements stay pending |
| 807 | startedAt int // when the app stage first ran: a probe attempt's readiness window runs from here (rev 7.12 §7.7) |
| 808 | } |
| 809 | |
| 810 | // probeTiming is what INV-19 reads: when a probe attempt's app stage first |
| 811 | // ran and when its app answered readiness (rev 7.13, R12-2) |
| 812 | type probeTiming struct { |
| 813 | startedAt, readyAt int |
| 814 | } |
| 815 | |
| 816 | // writesLost is claim rev 6.9's writes_lost record: the writer whose |
| 817 | // acknowledged, unuploaded writes a cold admission leaves behind, named by |
| 818 | // holder.writer_box, never inferred from op.exec (R9-2). The box alerts. |
| 819 | type writesLost struct { |
| 820 | Box int |
| 821 | Gen string |
| 822 | Session int |
| 823 | RemoteMaxTXID int |
| 824 | } |
| 825 | |
| 826 | type opState struct { |
| 827 | Kind string // serving, creating, deleting, parking, purging, moving, landing, reverting, restoring, pushing |
| 828 | ID string |
| 829 | Phase string |
| 830 | Exec int // -1 none |
| 831 | Parts []int |
| 832 | // ParkSweep is intent.park_sweep (claim rev 6.15 §6.2a): a free host's |
| 833 | // at-rest sweep runs as a holderless parking op, {kind: parking, |
| 834 | // intent: {park_sweep: "v1"}}, with no exec and no holder, carrying |
| 835 | // only scoped remote chores; its last acknowledgement frees the claim |
| 836 | // again in the same CAS (FreeAfterPark) |
| 837 | ParkSweep string |
| 838 | |
| 839 | // FenceBox is the journal's fence.<box> reference (claim rev 6.28, |
| 840 | // moves rev 7.20 §7.10): the terminated source whose termination fence |
| 841 | // converted a pre-flip move to relocating. Alerted: the operator was |
| 842 | // told once that the relocation waits for a box in the region. |
| 843 | FenceBox int |
| 844 | Alerted bool |
| 845 | |
| 846 | // intent |
| 847 | Src, Tgt int |
| 848 | SrcRegion, TgtRegion int |
| 849 | NewInc int |
| 850 | NewApp string |
| 851 | NewRegion int |
| 852 | NewSerial int |
| 853 | NewBox int // the executor a create named once (region HA §5.2, H12): never substituted |
| 854 | // region HA relocation (spec 1 §5.8; claim rev 6.30 §4 L1). The |
| 855 | // journal entries below are what the claim's op.journal carries |
| 856 | RelocReason string // drain or failover |
| 857 | FenceAt int // fence.<box>.observed_at of the latest fence the operation cites; 0 none |
| 858 | FailedAt int // when the target entered probe-failed |
| 859 | Release *releaseEntry // the release sequence's journal entry (§5.8): the source's in releasing, a failed target's in probe-failed |
| 860 | Pin *pinEntry // the pinned recovery set |
| 861 | Prepared string // P, the prepared generation this installation builds; "" before installing |
| 862 | InstallStamp int // the stamp of the CAS that handed op.exec to the current target (op.journal.install_stamp) |
| 863 | Receipt *receiptEntry // the executor's local install receipt (local_install) |
| 864 | ProbingSince int |
| 865 | Replacements int // targets replaced in this operation; two, then stuck |
| 866 | Excluded []int // replaced targets, never named again for this host |
| 867 | InstalledOn []int // every box this operation handed op.exec for an installation: each owes a park-local at serving unless discharged |
| 868 | Discharged []int // fenced boxes whose park-local chores the fence CAS discharged (L3, H19) |
| 869 | Stuck string |
| 870 | // 1b-next rev 16's journal additions |
| 871 | ReleasingSince int // releasing_since: the release deadline's start (ruling 14) |
| 872 | Attempts int // probe_attempts.<op.exec>: counted before each attempt, at most probeTries (ruling 19) |
| 873 | PreparedOpened string // prepared_opened: journaled by the admission that opened P (rev 12 S1) |
| 874 | PinFailover bool // (rev 6) the initial failover's starting, 1b-next's StartRelocation with a fence: set by startFailover and by a drain's source lost in starting, cleared by the PinFailover CAS once the target is named and every participant has acknowledged |
| 875 | Resolved bool // an operator's resolve (model ruling 13): the source is eligible as a target again, and an empty listing is accepted |
| 876 | Observed []int // every fence.<box>.observed_at the operation consumed, kept through replacements (rev 4) |
| 877 | Acks []int // exec_ack.<box>: the participants that acknowledged, durable (rev 4) |
| 878 | Abandoned []string // abandoned_prepared: every unopened P the operation replaced or dropped, parked at serving (1b-next ruling 27) |
| 879 | // L18 joint round finding 2: the built completion protocol |
| 880 | // (regionha_completion_test.go). ProbePassedAt is the probe's |
| 881 | // journaled time (Probe.At, ruling 67's bound); ProbeStop the target's |
| 882 | // journaled stop of the passed probe's session (ruling 49); Completed |
| 883 | // the serving op's completed_relocation record (ruling 56), which the |
| 884 | // completion pass marks discharged last (ruling 80) |
| 885 | ProbePassedAt int |
| 886 | ProbeStop *probeStopEntry |
| 887 | Completed *completedEntry |
| 888 | |
| 889 | // journal |
| 890 | ReportAt int |
| 891 | ReportOK bool |
| 892 | CutAt int |
| 893 | CutDeadline int |
| 894 | StopAt int |
| 895 | StopDigest digest |
| 896 | StopFiles *filesDir |
| 897 | SealDB ref |
| 898 | SealFiles ref |
| 899 | SealQuiet int |
| 900 | LandPhase string |
| 901 | Installed digest |
| 902 | ProbeTries int |
| 903 | ProbedAt int |
| 904 | RevPhase string |
| 905 | SrcPhase string |
| 906 | Dirty bool |
| 907 | DirtyKnown bool |
| 908 | ReturnDB ref |
| 909 | ReturnFiles ref |
| 910 | ReturnQuiet int |
| 911 | ReturnParked bool // the return lane's park-staging chore is owed (rev 7.10) |
| 912 | // SrcCovered (rev 7.11): at the seal, the source's own replica of its |
| 913 | // generation reached the stopped database's position, so a clean |
| 914 | // rollback may restore the source from it; otherwise the seal holds |
| 915 | // writes the replica does not, and the return carries the seal |
| 916 | SrcCovered bool |
| 917 | // CutSession (rev 7.12) is holder.session at the cut's stop: the |
| 918 | // source's session whose writes src_covered speaks for; a clean return's |
| 919 | // coverage applies to it and to the target's probe session only |
| 920 | CutSession int |
| 921 | // SealFromDB (rev 7.11): the seal was built from the stopped database |
| 922 | // itself, every page of it, so it covers every write the predecessor |
| 923 | // acknowledged; false when the disk was gone and the seal is the |
| 924 | // remote as it stood, which stops at the remote's position. The |
| 925 | // prepared generation's admission declares writes_lost in that case |
| 926 | // (seed 34260 / 100,000). ReturnFromDB is the same for a dirty |
| 927 | // return's seal of the target |
| 928 | SealFromDB bool |
| 929 | ReturnFromDB bool |
| 930 | LostBox int |
| 931 | LostAt int |
| 932 | RollbackID string |
| 933 | PushSnap *blob // a push's installed snapshot (the final checkpoint plus the push's mark) |
| 934 | BaseKey string |
| 935 | BaseTX int |
| 936 | RecVer int // a delete's or purge's intent: the record version it will DeleteIfMatch (claim §5.2 step 1, §5.3 step 4) |
| 937 | FlipGen int // the holder.stamp the flip CAS wrote: the landing's installation stamp (claim rev 6.5 §6.4) |
| 938 | SrcStamp int // the source installation's stamp before the flip, for the return to source (claim rev 6.5) |
| 939 | // SrcGen is the source's generation at the cut (rev 7.10): a clean |
| 940 | // rollback's return CAS names it again for the restore. Rev 7.11's |
| 941 | // op.journal.writers moved to holder.admissions (claim rev 6.12) |
| 942 | SrcGen string |
| 943 | Committed bool |
| 944 | Opened bool |
| 945 | ParkLocalNow bool |
| 946 | PinVer int // move.inputs: the bundle version pinned at admission |
| 947 | Auto bool |
| 948 | ReqAt int |
| 949 | Repl string |
| 950 | Next int |
| 951 | FlipAt int |
| 952 | TgtStopAt int |
| 953 | Reason string |
| 954 | App string |
| 955 | // FencedAbsent: a purge fence placed where no claim existed (claim rev |
| 956 | // 5.2 §5.3). Its release writes a free claim; the mutation of |
| 957 | // claim-never-deleted deletes the object instead |
| 958 | FencedAbsent bool |
| 959 | // BaseVer is the version id of the generation's installed snapshot, |
| 960 | // recorded by the install manifest and named by generation.json: the |
| 961 | // immutable snapshot identity the restore starts from (rev 7.4 §5.1, |
| 962 | // R3-1) |
| 963 | BaseVer int |
| 964 | } |
| 965 | |
| 966 | // releaseEntry is §5.8's release journal entry: the box, generation and |
| 967 | // session that gave the host up, its stopped database's final TXID (the |
| 968 | // listing shows it before pinning may cite it), and, until Task 4's files |
| 969 | // manifest, the files directory and wake state the box published. Flushed |
| 970 | // is false when the session's replicator was gone (an agent restart) and |
| 971 | // the entry names what the remote held: released coverage never applies |
| 972 | // to it, and the next admission declares the rest. |
| 973 | // releaseRecord is 1b-next Task 7's ReleasePositions record: the |
| 974 | // release a box computed once its writers stopped and its database and |
| 975 | // files flushed, bound to the stop (the operation, the phase and the |
| 976 | // writer session), durable before the producers close (rev 9). |
| 977 | type releaseRecord struct { |
| 978 | Op, Phase string |
| 979 | E releaseEntry |
| 980 | // Ctl is the flushing controller's identity: the agent process |
| 981 | // (box.Epoch) that flushed and recorded (rev 11). Receipt is root's |
| 982 | // durable stop receipt for this stop, persisted after the producers |
| 983 | // drained (step 4), tracked apart from the recorded positions: only |
| 984 | // the same controller may finish from the positions alone, and after a |
| 985 | // restart the release needs the receipt too (1b-next Task 7 Release, |
| 986 | // RecoveryReleaseDrain; Astra round 8) |
| 987 | Ctl int |
| 988 | Receipt bool |
| 989 | } |
| 990 | |
| 991 | type releaseEntry struct { |
| 992 | Box, Session int |
| 993 | Gen string |
| 994 | FinalTX int |
| 995 | ManifestSeq int |
| 996 | Flushed bool |
| 997 | Files *filesDir |
| 998 | Timers []int |
| 999 | At int |
| 1000 | } |
| 1001 | |
| 1002 | // pinEntry is §5.8's pinned recovery set: the database position N the |
| 1003 | // build restores to (exact versions in the real pin; the model's build |
| 1004 | // never restores past N), the files manifest version (Task 4), and when |
| 1005 | // the pin was taken (after a release's final_txid is visible, or after a |
| 1006 | // fence's observed_at plus failoverPinDelay). |
| 1007 | type pinEntry struct { |
| 1008 | Gen string // the generation the pin reads (genselect over the admitted chain) |
| 1009 | TX int |
| 1010 | ManKey string |
| 1011 | ManVer, ManSeq int |
| 1012 | At int |
| 1013 | ClaimVer int // the claim version it was selected against (1b-next ruling 16: pin-<gen>.json) |
| 1014 | // Files and Timers are the files set the pin was taken with, until |
| 1015 | // Task 4's manifest: the release's, or a failover's stand-in |
| 1016 | Files *filesDir |
| 1017 | Timers []int |
| 1018 | ManGen string // the generation whose manifest the files pin names (Task 4) |
| 1019 | } |
| 1020 | |
| 1021 | // receiptEntry is the local install receipt (§5.8 local_install): the |
| 1022 | // box and the install_stamp of the CAS that handed it op.exec. A |
| 1023 | // replacement executor never inherits its predecessor's. |
| 1024 | // probeStopEntry is hostclaim.ProbeStop: the target's stop of the passed |
| 1025 | // probe's session, with root's receipt (ruling 49). |
| 1026 | type probeStopEntry struct { |
| 1027 | Box, Session int |
| 1028 | } |
| 1029 | |
| 1030 | // completedEntry is hostclaim.CompletedRelocation on the serving op: the |
| 1031 | // relocation, the box and stopped probe session it completed with, and |
| 1032 | // Discharged, the mark (MarkCompletedDischarged). |
| 1033 | type completedEntry struct { |
| 1034 | Op string |
| 1035 | Box, Session int |
| 1036 | Discharged bool |
| 1037 | } |
| 1038 | |
| 1039 | type receiptEntry struct { |
| 1040 | Op string |
| 1041 | Box, Stamp int |
| 1042 | } |
| 1043 | |
| 1044 | type digest struct { |
| 1045 | Writes string |
| 1046 | Files string |
| 1047 | Timers string |
| 1048 | Valid bool |
| 1049 | } |
| 1050 | |
| 1051 | type claim struct { |
| 1052 | Ver int |
| 1053 | Holder *holder |
| 1054 | Op opState |
| 1055 | Regions []int |
| 1056 | Boxes []int |
| 1057 | Complete bool |
| 1058 | Obl []obligation |
| 1059 | Lost []int |
| 1060 | // Retired is retired_incarnations: anti-reuse only, capped at |
| 1061 | // retiredCap entries (claim rev 6 §2, §6.2a). The sweep does not read |
| 1062 | // it; it discovers locations from the namespace (R3-4). |
| 1063 | Retired []int |
| 1064 | Quiet [nRegions]int |
| 1065 | PurgeRes bool |
| 1066 | // Cancelled is cancelled_creates (claim rev 4 §5.1, J2-R2-7): creates |
| 1067 | // recovery cancelled, so a late record PUT can be removed. It survives free. |
| 1068 | Cancelled []cancelledCreate |
| 1069 | // readStamp is model bookkeeping on a box's read of the claim: the |
| 1070 | // installation stamp active on that box at the read, which a worker |
| 1071 | // carries with the claim it validated under (claim rev 6.5 §6.4) |
| 1072 | readStamp int |
| 1073 | } |
| 1074 | |
| 1075 | type cancelledCreate struct { |
| 1076 | Inc int |
| 1077 | Until int |
| 1078 | } |
| 1079 | |
| 1080 | // liteHost is a second hostname of the same apps, modelled for the |
| 1081 | // control plane only: create, app admission and purge (J2-R2-2). |
| 1082 | type liteHost struct { |
| 1083 | Inc int |
| 1084 | App string |
| 1085 | Box int // the box its create named (region HA §5.2); control-plane only |
| 1086 | Kind string // "", "creating", "serving", "purging", "fenced" |
| 1087 | OpID string |
| 1088 | Rec bool // its record is published |
| 1089 | At int |
| 1090 | // FencedAbsent: the fence found no claim (epoch 0). Its release writes |
| 1091 | // free; the mutation of claim-never-deleted deletes the object, so the |
| 1092 | // epoch returns to 0 and a creator's If-None-Match: * passes again |
| 1093 | FencedAbsent bool |
| 1094 | } |
| 1095 | |
| 1096 | // admission is apps/<acct>/<app>/admission.json (claim rev 4 §5.1 step 0). |
| 1097 | type admission struct { |
| 1098 | Closed bool |
| 1099 | Reg map[string]regEntry // create id -> registration |
| 1100 | } |
| 1101 | |
| 1102 | type regEntry struct { |
| 1103 | Host string |
| 1104 | Until int // a registration is a lease: a create claims before it ends (CC16) |
| 1105 | } |
| 1106 | |
| 1107 | type pendingRec struct { |
| 1108 | rec *record |
| 1109 | at int |
| 1110 | } |
| 1111 | |
| 1112 | type record struct { |
| 1113 | Ver int |
| 1114 | Inc int |
| 1115 | App string |
| 1116 | Region int |
| 1117 | MoveID string |
| 1118 | // MoveState is the record's move journal state for the four transitions |
| 1119 | // the moves spec makes record-first (§7.5, §7.8, §7.9): "landing" after |
| 1120 | // the flip, "committed", "rolling_back". The claim follows each. |
| 1121 | MoveState string |
| 1122 | RollbackID string |
| 1123 | Reason string |
| 1124 | // LastMove names the move whose close cleared MoveID: the close is record |
| 1125 | // first (moves rev 7.23 §7.5, Paul's ruling M4), so a record can say a |
| 1126 | // move is over while the claim still holds its op, until the release. |
| 1127 | LastMove string |
| 1128 | } |
| 1129 | |
| 1130 | // ---------- the world ---------- |
| 1131 | |
| 1132 | type ack struct { |
| 1133 | W int |
| 1134 | Inc int |
| 1135 | Box int |
| 1136 | Session int // the writer session that acknowledged it (rev 7.13, R12-1): a writes_lost record exempts the writes of the session it names, no other |
| 1137 | Gen string // the generation that session wrote |
| 1138 | At int |
| 1139 | Kind string // "write" or "timer" |
| 1140 | Exempt bool // lost under a declared loss (M16) or past the last checkpoint of a lost disk |
| 1141 | } |
| 1142 | |
| 1143 | // intner is what the model draws from: the seed's *rand.Rand in the random |
| 1144 | // sweep, a quiet source in a witness scenario (witness_test.go), so the |
| 1145 | // witnesses never touch the seeds' streams. |
| 1146 | type intner interface{ Intn(n int) int } |
| 1147 | |
| 1148 | type world struct { |
| 1149 | perRegion int // boxes per region at the start (region HA L18): 1, today's model, or 2 |
| 1150 | issued int // files manifests issued, in order: INV-28's ground truth (blob.Base) |
| 1151 | // pinWatch is INV-30's memory: per region that could still serve, the |
| 1152 | // manifest its next install would pin, as the oracle saw it last step |
| 1153 | pinWatch map[int]pinWatch |
| 1154 | // noPinWatch turns INV-30 off: TestFilesWitnessesStuckWithoutINV30's |
| 1155 | // liveness runs only |
| 1156 | noPinWatch bool |
| 1157 | // oneBoxRegion: a witness's region kept at one box by its group in the |
| 1158 | // two-box shape (H5's minimum is per region) |
| 1159 | oneBoxRegion [nRegions]bool |
| 1160 | // L18 joint round findings 2 and 4 (regionha_completion_test.go): |
| 1161 | // haOff is CARLOS_REGION_HA off with claim mode on, where only the |
| 1162 | // completion pass runs (ruling 82); claimC1 and claimC11 are claim |
| 1163 | // asks C1 (a failed target's release obligation) and C11 (root |
| 1164 | // launches a later probe attempt after P's opening). Both are open |
| 1165 | // today, so the model runs the built fallbacks; a witness or test of |
| 1166 | // the post-C1 or post-C11 behaviour sets them |
| 1167 | haOff, claimC1, claimC11 bool |
| 1168 | t testingT |
| 1169 | seed int64 |
| 1170 | rng intner |
| 1171 | // hold, when set, is a witness's hand on S3: a request it answers true |
| 1172 | // for is accepted and completes only when the witness says so |
| 1173 | // (witness_test.go). The random sweep never sets it. |
| 1174 | hold func(r *request) bool |
| 1175 | // alerts raised to the operator (writes_lost, a marker disagreement, a |
| 1176 | // failed host, an uncertified close): counted for the oracle that every |
| 1177 | // writes_lost record was alerted (R10-6) |
| 1178 | alerts int |
| 1179 | lostAlert int |
| 1180 | markerAlerted map[string]bool |
| 1181 | // startHook runs right after the app starts, before replication opens: |
| 1182 | // a witness's background worker acknowledging work (R10-1) |
| 1183 | startHook func(b *box) bool // true: the hook crashed the box |
| 1184 | // openYield (rev 5, Astra round 2 on claim §11's open boundaries): a |
| 1185 | // witness's yield after generation.json names the new generation and |
| 1186 | // before replication opens; true: the start returns there and resumes |
| 1187 | // at "open" on the next call. Nil outside the witnesses |
| 1188 | openYield func(b *box) bool |
| 1189 | // lastIssued is the request issue saw last, for a caller that needs |
| 1190 | // the request object behind a helper's return value (resumeOpen) |
| 1191 | lastIssued *request |
| 1192 | // stampBox records, for every installation stamp the claim issued, the |
| 1193 | // box whose installation it names (claim rev 6.5: holder.stamp always |
| 1194 | // names the installation op.exec should run). The oracle refuses an |
| 1195 | // activation of another box's stamp (INV-6, R6-4). |
| 1196 | stampBox map[int]int |
| 1197 | now int |
| 1198 | ver int |
| 1199 | verbose bool |
| 1200 | |
| 1201 | claim *claim // nil = absent |
| 1202 | rec *record |
| 1203 | stores map[string]bool |
| 1204 | cfgVer map[string]int // each app's current config bundle version |
| 1205 | purgeRes map[string]bool |
| 1206 | purgeStep map[string]int // the reservation's durable phase (purge journal) |
| 1207 | admit map[string]*admission |
| 1208 | h2 liteHost |
| 1209 | recPend *pendingRec // a record PUT whose response was lost |
| 1210 | lastRegion int // where the host served when it was last deleted |
| 1211 | legacyIncs map[int]bool // incarnations that were adopted legacy hosts |
| 1212 | purgeOp map[string]string // the purge id, kept in the reservation (the purge journal) |
| 1213 | h2Epoch int // the second host claim's ETag, for its fence and release; 0 is absent |
| 1214 | floor bool |
| 1215 | buckets [nRegions]*bucket |
| 1216 | control *bucket |
| 1217 | boxes []*box |
| 1218 | pending []*request |
| 1219 | acks []ack |
| 1220 | writeInc map[int]int // which incarnation acknowledged each write |
| 1221 | txs map[int]tx // every write as a transaction (ltx_test.go) |
| 1222 | durable map[string]map[int]bool // per generation prefix: writes a completed replica object holds |
| 1223 | genParent map[string]string // generation prefix -> the one it superseded |
| 1224 | nextW int |
| 1225 | nextInc int |
| 1226 | serial int |
| 1227 | nextID int |
| 1228 | delivered map[int]bool |
| 1229 | doorReads []*doorPlan |
| 1230 | execLease map[int]execLease |
| 1231 | staging [nRegions]stagingLease |
| 1232 | console []*consolePlan |
| 1233 | fail map[string]bool // which faults this seed exercises |
| 1234 | stats map[string]int |
| 1235 | stalled []*stalledSign |
| 1236 | ccache *claim // the console's short-lived claim cache |
| 1237 | |
| 1238 | violations []string |
| 1239 | opsDone int |
| 1240 | calm bool |
| 1241 | trace []string |
| 1242 | } |
| 1243 | |
| 1244 | type testingT interface { |
| 1245 | Fatalf(format string, args ...any) |
| 1246 | Logf(format string, args ...any) |
| 1247 | } |
| 1248 | |
| 1249 | func (w *world) logf(format string, args ...any) { |
| 1250 | if w.verbose { |
| 1251 | w.trace = append(w.trace, fmt.Sprintf("%5d ", w.now)+fmt.Sprintf(format, args...)) |
| 1252 | } |
| 1253 | } |
| 1254 | |
| 1255 | func (w *world) violate(format string, args ...any) { |
| 1256 | msg := fmt.Sprintf("t=%d: ", w.now) + fmt.Sprintf(format, args...) |
| 1257 | if len(w.violations) >= 3 { |
| 1258 | return |
| 1259 | } |
| 1260 | w.violations = append(w.violations, msg) |
| 1261 | w.logf("VIOLATION %s", msg) |
| 1262 | } |
| 1263 | |
| 1264 | func (w *world) newID(prefix string) string { |
| 1265 | w.nextID++ |
| 1266 | return fmt.Sprintf("%s%d", prefix, w.nextID) |
| 1267 | } |
| 1268 | |
| 1269 | func (w *world) newVer() int { |
| 1270 | w.ver++ |
| 1271 | return w.ver |
| 1272 | } |
| 1273 | |
| 1274 | // nextGen is the gen the claim CAS in progress will carry: what a writer |
| 1275 | // captures as its installation stamp (claim rev 6.5 §6.4). |
| 1276 | func (w *world) nextGen() int { |
| 1277 | if w.claim == nil { |
| 1278 | return 1 |
| 1279 | } |
| 1280 | return w.claim.Ver + 1 |
| 1281 | } |
| 1282 | |
| 1283 | func (w *world) boxByID(id int) *box { |
| 1284 | for _, b := range w.boxes { |
| 1285 | if b.ID == id { |
| 1286 | return b |
| 1287 | } |
| 1288 | } |
| 1289 | return nil |
| 1290 | } |
| 1291 | |
| 1292 | // regionBox is the live (not destroyed) box in a region. |
| 1293 | func (w *world) regionBox(r int) *box { |
| 1294 | for _, b := range w.boxes { |
| 1295 | if b.Region == r && !b.Destroyed { |
| 1296 | return b |
| 1297 | } |
| 1298 | } |
| 1299 | return nil |
| 1300 | } |
| 1301 | |
| 1302 | func contains(xs []int, x int) bool { |
| 1303 | for _, y := range xs { |
| 1304 | if y == x { |
| 1305 | return true |
| 1306 | } |
| 1307 | } |
| 1308 | return false |
| 1309 | } |
| 1310 | |
| 1311 | func addUniq(xs []int, x int) []int { |
| 1312 | if contains(xs, x) { |
| 1313 | return xs |
| 1314 | } |
| 1315 | return append(xs, x) |
| 1316 | } |
| 1317 | |
| 1318 | func intsKey(xs []int) string { |
| 1319 | c := append([]int(nil), xs...) |
| 1320 | sort.Ints(c) |
| 1321 | return fmt.Sprint(c) |
| 1322 | } |
| 1323 | |
| 1324 | func (c *claim) clone() *claim { |
| 1325 | if c == nil { |
| 1326 | return nil |
| 1327 | } |
| 1328 | n := *c |
| 1329 | if c.Holder != nil { |
| 1330 | h := *c.Holder |
| 1331 | n.Holder = &h |
| 1332 | } |
| 1333 | n.Op.Parts = append([]int(nil), c.Op.Parts...) |
| 1334 | n.Op.StopFiles = c.Op.StopFiles.clone() |
| 1335 | n.Op.Excluded = append([]int(nil), c.Op.Excluded...) |
| 1336 | n.Op.InstalledOn = append([]int(nil), c.Op.InstalledOn...) |
| 1337 | n.Op.Discharged = append([]int(nil), c.Op.Discharged...) |
| 1338 | n.Op.Abandoned = append([]string(nil), c.Op.Abandoned...) |
| 1339 | n.Op.Acks = append([]int(nil), c.Op.Acks...) |
| 1340 | n.Op.Observed = append([]int(nil), c.Op.Observed...) |
| 1341 | if r := c.Op.Release; r != nil { |
| 1342 | cp := *r |
| 1343 | cp.Files = r.Files.clone() |
| 1344 | cp.Timers = append([]int(nil), r.Timers...) |
| 1345 | n.Op.Release = &cp |
| 1346 | } |
| 1347 | if p := c.Op.Pin; p != nil { |
| 1348 | cp := *p |
| 1349 | cp.Files = p.Files.clone() |
| 1350 | cp.Timers = append([]int(nil), p.Timers...) |
| 1351 | n.Op.Pin = &cp |
| 1352 | } |
| 1353 | if r := c.Op.Receipt; r != nil { |
| 1354 | cp := *r |
| 1355 | n.Op.Receipt = &cp |
| 1356 | } |
| 1357 | if c.Holder != nil { |
| 1358 | n.Holder.Admissions = append([]admissionRecord(nil), c.Holder.Admissions...) |
| 1359 | for i := range n.Holder.Admissions { |
| 1360 | if l := n.Holder.Admissions[i].Lost; l != nil { |
| 1361 | cp := *l |
| 1362 | n.Holder.Admissions[i].Lost = &cp |
| 1363 | } |
| 1364 | } |
| 1365 | } |
| 1366 | n.Regions = append([]int(nil), c.Regions...) |
| 1367 | n.Boxes = append([]int(nil), c.Boxes...) |
| 1368 | n.Obl = append([]obligation(nil), c.Obl...) |
| 1369 | n.Lost = append([]int(nil), c.Lost...) |
| 1370 | n.Retired = append([]int(nil), c.Retired...) |
| 1371 | n.Cancelled = append([]cancelledCreate(nil), c.Cancelled...) |
| 1372 | return &n |
| 1373 | } |
| 1374 | |
| 1375 | // ---------- bucket access with IAM ---------- |
| 1376 | |
| 1377 | // actor names: "box:N" or "console" or "operator". |
| 1378 | |
| 1379 | func (w *world) iamCheck(actorBox int, r *request) bool { |
| 1380 | if actorBox < 0 { // console: control bucket only, plus GetObjectVersion on data (door) |
| 1381 | return false |
| 1382 | } |
| 1383 | b := w.boxByID(actorBox) |
| 1384 | if r.region == b.Region { |
| 1385 | if r.kind == rCopy && r.srcRegion != b.Region { |
| 1386 | return false // no Get on a sibling |
| 1387 | } |
| 1388 | return true |
| 1389 | } |
| 1390 | // sibling bucket: Put/Delete on moves/* only, and CopyObject INTO moves/* |
| 1391 | // from the box's own bucket. |
| 1392 | if !strings.HasPrefix(r.key, "moves/") { |
| 1393 | return false |
| 1394 | } |
| 1395 | switch r.kind { |
| 1396 | case rPut, rDelKey: |
| 1397 | return true |
| 1398 | case rCopy: |
| 1399 | return r.srcRegion == b.Region |
| 1400 | } |
| 1401 | return false // DeleteObjectVersion is not granted on a sibling |
| 1402 | } |
| 1403 | |
| 1404 | // issue sends a request. It returns the new version id when it completed |
| 1405 | // immediately and the client saw the answer; 0 when the client timed out |
| 1406 | // (the request may still complete later). |
| 1407 | func (w *world) issue(actorBox int, r *request) int { |
| 1408 | r.at = w.now |
| 1409 | w.lastIssued = r |
| 1410 | if r.kind == rPut && r.b != nil && isDataKey(r.key) && (r.b.Min == 0 || r.b.Max == 0) { |
| 1411 | // INV-12 (R8-3): the pinned LTX encoder refuses a zero TXID, so no |
| 1412 | // such file can exist; a position-0 snapshot [1,0] or anchor [0,0] |
| 1413 | // is a builder bug, never an object |
| 1414 | w.violate("INV-12: box %d wrote an LTX file with a zero TXID, %s, which the pinned encoder refuses (R8-3)", actorBox, r.key) |
| 1415 | } |
| 1416 | if !w.iamCheck(actorBox, r) { |
| 1417 | w.violate("IAM: box %d may not %v %s in region %d", actorBox, r.kind, r.key, r.region) |
| 1418 | return 0 |
| 1419 | } |
| 1420 | if w.hold != nil && w.hold(r) { |
| 1421 | r.doneAt, r.by = 1<<30, fmt.Sprintf("box:%d", actorBox) |
| 1422 | w.pending = append(w.pending, r) |
| 1423 | w.logf("box %d issued %v %s r%d (held by the witness)", actorBox, r.kind, r.key, r.region) |
| 1424 | return 0 |
| 1425 | } |
| 1426 | if r.hold { |
| 1427 | // the biased schedule: accepted, completing at its worst moment or |
| 1428 | // long after everything else |
| 1429 | r.doneAt, r.by, r.beyond = w.now+40*horizonH, fmt.Sprintf("box:%d", actorBox), true |
| 1430 | w.pending = append(w.pending, r) |
| 1431 | w.logf("box %d issued %v %s r%d (held for its worst moment)", actorBox, r.kind, r.key, r.region) |
| 1432 | return 0 |
| 1433 | } |
| 1434 | if w.rng.Intn(10) < 7 { |
| 1435 | return w.complete(r) |
| 1436 | } |
| 1437 | r.doneAt = w.now + 1 + w.rng.Intn(6) |
| 1438 | tail := 8 |
| 1439 | if strings.HasPrefix(r.key, "moves/") { |
| 1440 | tail = 3 // staging rounds stall more often: the cross-region path is the slow one |
| 1441 | } |
| 1442 | if w.rng.Intn(tail) == 0 { |
| 1443 | r.doneAt = w.now + 1 + w.rng.Intn(horizonH) // the long tail: signed, cancelled, completed late |
| 1444 | if w.rng.Intn(4) == 0 { |
| 1445 | r.doneAt = w.now + horizonH // as late as the signature-age limit allows |
| 1446 | } |
| 1447 | if w.rng.Intn(beyondH) == 0 { |
| 1448 | // accepted before the signature limit, completed after it: S3 |
| 1449 | // bounds acceptance, not completion (claim C3a, J2-R2-1) |
| 1450 | r.doneAt = w.now + horizonH + 1 + w.rng.Intn(10*horizonH) |
| 1451 | r.beyond = true |
| 1452 | if w.fail["recreate"] && !w.calm && w.rng.Intn(2) == 0 { |
| 1453 | // the biased schedule: no bound at all, so it can outlive a |
| 1454 | // delete and a recreate; it lands at its worst moment. Chaos |
| 1455 | // only: in the calm phase a chain of such holds, one per park |
| 1456 | // of a dead generation, can outlast the whole convergence |
| 1457 | // window (seed 20077 / 30,000), which says nothing about the |
| 1458 | // protocol |
| 1459 | r.doneAt = w.now + 40*horizonH |
| 1460 | } |
| 1461 | } |
| 1462 | } |
| 1463 | r.by = fmt.Sprintf("box:%d", actorBox) |
| 1464 | w.pending = append(w.pending, r) |
| 1465 | w.logf("box %d issued %v %s r%d (late until %d)", actorBox, r.kind, r.key, r.region, r.doneAt) |
| 1466 | return 0 |
| 1467 | } |
| 1468 | |
| 1469 | func (w *world) complete(r *request) int { |
| 1470 | r.done = true |
| 1471 | bk := w.buckets[r.region] |
| 1472 | switch r.kind { |
| 1473 | case rPut: |
| 1474 | if r.ifSet { |
| 1475 | cur := 0 |
| 1476 | if v := bk.current(r.key); v != nil { |
| 1477 | cur = v.ID |
| 1478 | } |
| 1479 | if cur != r.ifVer { |
| 1480 | return 0 // 412 Precondition Failed |
| 1481 | } |
| 1482 | } |
| 1483 | v := &version{ID: w.newVer(), B: r.b, Straggler: r.beyond} |
| 1484 | bk.objs[r.key] = append(bk.objs[r.key], v) |
| 1485 | w.markDurable(r.key, r.b) |
| 1486 | return v.ID |
| 1487 | case rDelVer: |
| 1488 | vs := bk.objs[r.key] |
| 1489 | for i, v := range vs { |
| 1490 | if v.ID == r.ver { |
| 1491 | bk.objs[r.key] = append(vs[:i:i], vs[i+1:]...) |
| 1492 | break |
| 1493 | } |
| 1494 | } |
| 1495 | return -1 |
| 1496 | case rDelKey: |
| 1497 | v := &version{ID: w.newVer(), Marker: true} |
| 1498 | bk.objs[r.key] = append(bk.objs[r.key], v) |
| 1499 | return v.ID |
| 1500 | case rCopy: |
| 1501 | src := w.buckets[r.srcRegion].byID(r.srcKey, r.srcVer) |
| 1502 | if src == nil || src.Marker { |
| 1503 | return 0 |
| 1504 | } |
| 1505 | v := &version{ID: w.newVer(), B: src.B, Straggler: r.beyond} |
| 1506 | bk.objs[r.key] = append(bk.objs[r.key], v) |
| 1507 | w.markDurable(r.key, src.B) |
| 1508 | return v.ID |
| 1509 | } |
| 1510 | return 0 |
| 1511 | } |
| 1512 | |
| 1513 | // markDurable: a write is durable in a generation once a completed replica |
| 1514 | // object of that generation holds it. The cold-restore checks (§14.2.3) |
| 1515 | // require every write durable in the claim's generation or in any |
| 1516 | // generation it superseded. |
| 1517 | func (w *world) markDurable(key string, b *blob) { |
| 1518 | if b == nil || !isDataKey(key) { |
| 1519 | return |
| 1520 | } |
| 1521 | p := genPrefixOf(key) |
| 1522 | if w.durable[p] == nil { |
| 1523 | w.durable[p] = map[int]bool{} |
| 1524 | } |
| 1525 | for _, x := range b.TXs { |
| 1526 | w.durable[p][x] = true |
| 1527 | } |
| 1528 | } |
| 1529 | |
| 1530 | // isDurable: W is durable anywhere (the disk-loss fault's RPO line). |
| 1531 | func (w *world) isDurable(x int) bool { |
| 1532 | for _, m := range w.durable { |
| 1533 | if m[x] { |
| 1534 | return true |
| 1535 | } |
| 1536 | } |
| 1537 | return false |
| 1538 | } |
| 1539 | |
| 1540 | // newGen records that the claim's generation moved from old to gen within |
| 1541 | // loc, so the durability promise carries over. |
| 1542 | func (w *world) newGen(loc, old, gen string) { |
| 1543 | if old != gen { |
| 1544 | w.genParent[dataKey(loc, gen, "")] = dataKey(loc, old, "") |
| 1545 | } |
| 1546 | } |
| 1547 | |
| 1548 | // worstMoment: the biased schedule completes a pending write of an earlier |
| 1549 | // incarnation's replica data the moment another incarnation holds the host |
| 1550 | // with an executor in that region, inside its own window or past H, which |
| 1551 | // is the interleaving C3a exists for (a recreate while the previous |
| 1552 | // incarnation's requests are still in flight). |
| 1553 | func (w *world) worstMoment(r *request) bool { |
| 1554 | if r.hold && r.b != nil && r.b.Kind == "gen" { |
| 1555 | // a held marker publication lands once a newer marker is current |
| 1556 | cur := w.buckets[r.region].current(r.key) |
| 1557 | return cur != nil && cur.B.Gen != r.b.Gen |
| 1558 | } |
| 1559 | if !w.fail["recreate"] || r.kind != rPut || r.b == nil || r.b.Inc == 0 || !isDataKey(r.key) { |
| 1560 | return false |
| 1561 | } |
| 1562 | c := w.claim |
| 1563 | if c == nil || c.Holder == nil || c.Holder.Inc == r.b.Inc { |
| 1564 | return false |
| 1565 | } |
| 1566 | if c.Op.Kind == "creating" && c.Op.NewRegion == r.region { |
| 1567 | return w.rng.Intn(2) == 0 |
| 1568 | } |
| 1569 | e := w.execBox(c) |
| 1570 | return e != nil && e.Region == r.region && w.rng.Intn(2) == 0 |
| 1571 | } |
| 1572 | |
| 1573 | func (w *world) completeDue(force bool) { |
| 1574 | var keep []*request |
| 1575 | for _, r := range w.pending { |
| 1576 | if force || r.doneAt <= w.now || w.worstMoment(r) { |
| 1577 | w.complete(r) |
| 1578 | if r.beyond { |
| 1579 | w.stats["completed beyond H"]++ |
| 1580 | } |
| 1581 | w.logf("late completion %v %s r%d (%s)", r.kind, r.key, r.region, r.by) |
| 1582 | } else { |
| 1583 | keep = append(keep, r) |
| 1584 | } |
| 1585 | } |
| 1586 | w.pending = keep |
| 1587 | } |
| 1588 | |
amadan