| 1 | package hostlife |
| 2 | |
| 3 | import ( |
| 4 | "fmt" |
| 5 | "sort" |
| 6 | ) |
| 7 | |
| 8 | // consolePlan is a multi-step console operation. A console crash drops |
| 9 | // every plan; the claim-recovery pass must then finish or undo the work |
| 10 | // from the claim alone (claim C2). |
| 11 | type consolePlan struct { |
| 12 | Kind string // create, delete, purge |
| 13 | Step int |
| 14 | App string |
| 15 | OpID string |
| 16 | Host string // "h" or "h2" for a create |
| 17 | Inc int |
| 18 | Region int |
| 19 | Read bool // a create's registration re-read has passed |
| 20 | Stall int // the console is paused on this plan until then |
| 21 | // an orphan cleanup's observations (claim rev 6 §5.1 step 5): the |
| 22 | // record's ETag and incarnation, the claim read, and the verdict |
| 23 | RecVer int |
| 24 | RecInc int |
| 25 | Snap *claim |
| 26 | Orphan bool |
| 27 | // the claim's ETag as the create read it when it registered: its |
| 28 | // claim CAS is conditional on it (CC22) |
| 29 | SeenVer int |
| 30 | SeenAbsent bool |
| 31 | } |
| 32 | |
| 33 | // doorPlan is one pull-door listing (claim rev 4 §6.5): O1 is the claim |
| 34 | // read it authorized against; it selects versions under O1's location after |
| 35 | // a pause, reads the claim again (O2), and only then signs handles, which a |
| 36 | // file request opens after another pause. |
| 37 | type doorPlan struct { |
| 38 | Region int |
| 39 | Loc string |
| 40 | Gen string |
| 41 | Inc int // O1's holder incarnation |
| 42 | OpID string // O1's op |
| 43 | Key string |
| 44 | Ver int |
| 45 | Signed bool |
| 46 | Adv bool // the biased schedule stalls this one until its worst moment |
| 47 | Until int // a stalled step may resume until then (one in four stall long) |
| 48 | } |
| 49 | |
| 50 | func (w *world) execBox(c *claim) *box { |
| 51 | if c == nil { |
| 52 | return nil |
| 53 | } |
| 54 | return w.boxByID(c.Op.Exec) |
| 55 | } |
| 56 | |
| 57 | // fixRecord is the recovery owner for the record halves of a move (claim |
| 58 | // C2): the request's `move` field after the claim's intent; the claim half |
| 59 | // of a record-first transition (followRecord); the claim's release after a |
| 60 | // move's record-first close, from last_move (rev 7.23 §7.5, ruling M4: the |
| 61 | // closing box may stop between the halves and never comes back); and, after |
| 62 | // any other release (a push, a relocation, or rev 7.22's claim-first close |
| 63 | // under its mutation), the CAS that clears `move` and names the executor's |
| 64 | // region. |
| 65 | func (w *world) fixRecord() { |
| 66 | c := w.claim |
| 67 | if c == nil || c.Holder == nil || w.rec == nil || w.rec.Inc != c.Holder.Inc { |
| 68 | return |
| 69 | } |
| 70 | if moveClose(c.Op) && w.rec.LastMove == c.Op.ID && w.rec.MoveID == "" { |
| 71 | if c.oblFor(c.Op.ID) == 0 { |
| 72 | w.stats["recovery: release from last_move"]++ |
| 73 | w.release(c, closeExec(c.Op)) |
| 74 | } |
| 75 | return |
| 76 | } |
| 77 | switch c.Op.Kind { |
| 78 | case "serving": |
| 79 | if b := w.execBox(c); b != nil && (w.rec.MoveID != "" || w.rec.Region != b.Region) { |
| 80 | w.rec.Region, w.rec.MoveID, w.rec.MoveState, w.rec.RollbackID = b.Region, "", "", "" |
| 81 | w.rec.Ver = w.newVer() |
| 82 | } |
| 83 | case "moving": |
| 84 | if w.rec.MoveID == "" { |
| 85 | w.rec.MoveID, w.rec.MoveState = c.Op.ID, "" |
| 86 | w.rec.Ver = w.newVer() |
| 87 | } |
| 88 | } |
| 89 | w.followRecord(c) |
| 90 | } |
| 91 | |
| 92 | func (w *world) liveBoxes() []*box { |
| 93 | var out []*box |
| 94 | for _, b := range w.boxes { |
| 95 | if !b.Destroyed { |
| 96 | out = append(out, b) |
| 97 | } |
| 98 | } |
| 99 | return out |
| 100 | } |
| 101 | |
| 102 | // ---------- user operations ---------- |
| 103 | |
| 104 | // userCreate starts a create as a console plan: registration, the claim |
| 105 | // CAS, the record and serving are separate steps on separate objects, and |
| 106 | // the console may pause or crash between any two (J2-R2-2, J2-R2-7). |
| 107 | func (w *world) userCreate() { |
| 108 | app := app0 |
| 109 | if w.rng.Intn(2) == 0 { |
| 110 | app = app1 |
| 111 | } |
| 112 | if w.rng.Intn(3) == 0 { |
| 113 | if w.h2.Kind != "" { |
| 114 | return |
| 115 | } |
| 116 | w.nextInc++ |
| 117 | w.console = append(w.console, &consolePlan{Kind: "create", Host: "h2", App: app, OpID: w.newID("cr"), Inc: w.nextInc}) |
| 118 | return |
| 119 | } |
| 120 | c := w.claim |
| 121 | if c != nil && (c.Holder != nil || (c.Op.Kind != "" && c.Op.Kind != "serving")) { |
| 122 | return |
| 123 | } |
| 124 | if w.rec != nil || w.recPend != nil { |
| 125 | return |
| 126 | } |
| 127 | r := w.rng.Intn(nRegions) |
| 128 | var inc int |
| 129 | if on("fresh-incarnation") || c == nil || len(c.Retired) == 0 { |
| 130 | w.nextInc++ |
| 131 | inc = w.nextInc |
| 132 | } else { |
| 133 | inc = c.Retired[len(c.Retired)-1] // a caller-supplied CreatedAt repeats an identity |
| 134 | } |
| 135 | w.console = append(w.console, &consolePlan{Kind: "create", Host: "h", App: app, OpID: w.newID("cr"), Inc: inc, Region: r}) |
| 136 | } |
| 137 | |
| 138 | func (w *world) createSteps(p *consolePlan) bool { |
| 139 | ad := w.admit[p.App] |
| 140 | abandon := func() bool { |
| 141 | delete(ad.Reg, p.OpID) |
| 142 | return true |
| 143 | } |
| 144 | // 412 on the claim CAS: something wrote the claim since the read the |
| 145 | // registration took, a purge fence among the possibilities. The create |
| 146 | // starts again from step 0, with a new registration and a new read; it |
| 147 | // never re-reads and retries the CAS alone (claim rev 5.2 §5.1, CC22) |
| 148 | restart := func() bool { |
| 149 | delete(ad.Reg, p.OpID) |
| 150 | w.logf("create %s: claim CAS 412, restarting from step 0", p.OpID) |
| 151 | w.stats["create restarted on 412"]++ |
| 152 | w.nextInc++ |
| 153 | p.OpID, p.Inc = w.newID("cr"), w.nextInc |
| 154 | p.Step, p.Read, p.Stall, p.SeenVer, p.SeenAbsent = 0, false, 0, 0, false |
| 155 | return false |
| 156 | } |
| 157 | if e, ok := ad.Reg[p.OpID]; ok && p.Step > 0 { |
| 158 | // the creating console renews its registration lease (CC16) |
| 159 | e.Until = w.now + 60 |
| 160 | ad.Reg[p.OpID] = e |
| 161 | } |
| 162 | switch p.Step { |
| 163 | case 0: |
| 164 | // app admission (claim rev 4 §5.1 step 0): register while open. |
| 165 | // The mutation is rev 3's check of the purge reservation, a read of |
| 166 | // another object than the claim the create then writes. |
| 167 | if on("admission-registration") { |
| 168 | if ad.Closed { |
| 169 | return true |
| 170 | } |
| 171 | ad.Reg[p.OpID] = regEntry{Host: p.Host, Until: w.now + 60} |
| 172 | w.logf("create %s registered for app %s (%s)", p.OpID, p.App, p.Host) |
| 173 | } else if w.purgeRes[p.App] { |
| 174 | return true |
| 175 | } |
| 176 | w.stores[p.App] = true // the app exists, or exists again after a purge |
| 177 | // the host claim's ETag, read with the registration, or its absence |
| 178 | // (claim rev 5.2 §5.1 step 0): the claim CAS is conditional on it |
| 179 | // (CC22), so any purge fence placed after this, even one since |
| 180 | // released, refuses the create |
| 181 | if p.Host == "h2" { |
| 182 | p.SeenVer = w.h2Epoch |
| 183 | } else if w.claim == nil { |
| 184 | p.SeenAbsent = true |
| 185 | } else { |
| 186 | p.SeenVer = w.claim.Ver |
| 187 | } |
| 188 | p.Step = 1 |
| 189 | return false |
| 190 | case 1: |
| 191 | if !p.Read { |
| 192 | // the re-read, the last step before the claim CAS (claim rev |
| 193 | // 5.1 §5.3): stop if the registration is gone or admission is |
| 194 | // closed. Cheap, and not sufficient: the console can pause |
| 195 | // between this read and the CAS |
| 196 | if _, ok := ad.Reg[p.OpID]; on("admission-registration") && on("registration-check") && (!ok || ad.Closed) { |
| 197 | return abandon() |
| 198 | } |
| 199 | p.Read = true |
| 200 | if w.fail["pausecreate"] && w.rng.Intn(2) == 0 { |
| 201 | // the biased schedule: the console pauses here, past the |
| 202 | // registration's expiry, while a purge may run |
| 203 | p.Stall = w.now + 100 + w.rng.Intn(200) |
| 204 | w.logf("create %s: console paused before its claim CAS", p.OpID) |
| 205 | } |
| 206 | return false |
| 207 | } |
| 208 | if p.Host == "h2" { |
| 209 | if w.h2.Kind != "" { |
| 210 | return abandon() |
| 211 | } |
| 212 | if on("fence-etag") && w.h2Epoch != p.SeenVer { |
| 213 | return restart() // If-Match the epoch read at registration (If-None-Match: * when it was 0) |
| 214 | } |
| 215 | w.h2 = liteHost{Inc: p.Inc, App: p.App, Kind: "creating", OpID: p.OpID, At: w.now, Box: w.h2Box(p.App)} |
| 216 | w.h2Epoch++ // every write changes the claim's ETag |
| 217 | w.logf("create %s: second host claimed for app %s", p.OpID, p.App) |
| 218 | p.Step = 2 |
| 219 | return false |
| 220 | } |
| 221 | c := w.claim |
| 222 | if c != nil && c.Holder == nil && c.Op.Kind == "parking" && c.Op.ParkSweep != "" { |
| 223 | return false // the holderless sweep blocks free's successor create until FreeAfterPark (claim rev 6.15 §6.2a) |
| 224 | } |
| 225 | if c != nil && (c.Holder != nil || (c.Op.Kind != "" && c.Op.Kind != "serving")) || w.recPend != nil { |
| 226 | return abandon() |
| 227 | } |
| 228 | if on("fence-etag") && (p.SeenAbsent != (c == nil) || c != nil && c.Ver != p.SeenVer) { |
| 229 | // If-Match the ETag read at registration (If-None-Match: * if |
| 230 | // the claim was absent then): a fence placed and released |
| 231 | // meanwhile changed it, and the 412 restarts the create |
| 232 | return restart() |
| 233 | } |
| 234 | if c != nil && len(c.Obl) > 0 && on("holderless-park") { |
| 235 | return false // a pending chore finishes first (CC11); since rev 7.14 a free host's sweep is the parking op above |
| 236 | } |
| 237 | if w.rec != nil { |
| 238 | // the record key is occupied: an orphan is removed by the |
| 239 | // cleanup of claim rev 6 §5.1 step 5, run by this console as |
| 240 | // its own plan, and the create retries (CC17); anything else |
| 241 | // refuses the create |
| 242 | if c != nil && w.orphanOf(c, w.rec.Inc) && on("cancelled-creates") { |
| 243 | if !w.hasPlan("orphan", "create") { |
| 244 | w.logf("create %s: cleaning up an orphan record inc %d", p.OpID, w.rec.Inc) |
| 245 | w.console = append(w.console, &consolePlan{Kind: "orphan", Host: "create"}) |
| 246 | } |
| 247 | return false |
| 248 | } |
| 249 | return abandon() |
| 250 | } |
| 251 | // the executor, chosen once and recorded in the intent (region HA |
| 252 | // §5.2, H12, L8; claim P5-D6 selected_executor) |
| 253 | b := w.chooseBox(p.Region, p.App) |
| 254 | if b == nil || (c != nil && contains(c.Lost, b.ID)) { |
| 255 | return abandon() |
| 256 | } |
| 257 | if on("fresh-incarnation") && c != nil && contains(c.Retired, p.Inc) { |
| 258 | return abandon() |
| 259 | } |
| 260 | w.serial++ |
| 261 | if !w.cas(c, func(n *claim) bool { |
| 262 | if len(n.Obl) > 0 { |
| 263 | // INV-20 (rev 7.14, R13-4): a create never claims a host while a |
| 264 | // park of its namespace is outstanding; the holderless sweep's |
| 265 | // op blocks it until FreeAfterPark |
| 266 | w.violate("INV-20: create %s claimed the host while %d obligation(s) were outstanding (%s %s)", p.OpID, len(n.Obl), n.Obl[0].Kind, n.Obl[0].Prefix) |
| 267 | } |
| 268 | n.Holder = &holder{Inc: p.Inc, App: p.App, Serial: w.serial, Location: locationFor(p.Inc, false), WriterBox: -1} // no writer yet |
| 269 | n.Op = opState{Kind: "creating", ID: p.OpID, Exec: -1, NewInc: p.Inc, NewApp: p.App, NewRegion: p.Region, NewBox: b.ID, ReqAt: w.now} |
| 270 | n.Regions, n.Boxes, n.Complete, n.Obl = []int{p.Region}, []int{b.ID}, true, nil |
| 271 | return true |
| 272 | }) { |
| 273 | return abandon() |
| 274 | } |
| 275 | w.logf("create %s inc %d app %s in region %d", p.OpID, p.Inc, p.App, p.Region) |
| 276 | p.Step = 2 |
| 277 | return false |
| 278 | case 2: |
| 279 | if p.Host == "h2" { |
| 280 | if w.h2.OpID != p.OpID || w.h2.Kind != "creating" { |
| 281 | return abandon() |
| 282 | } |
| 283 | w.h2.Rec = true |
| 284 | w.h2Epoch++ // every write changes the claim's ETag |
| 285 | p.Step = 3 |
| 286 | return false |
| 287 | } |
| 288 | c := w.claim |
| 289 | if c == nil || c.Op.ID != p.OpID || c.Op.Kind != "creating" { |
| 290 | return abandon() |
| 291 | } |
| 292 | if w.rec == nil && w.recPend == nil { |
| 293 | rec := &record{Ver: w.newVer(), Inc: c.Holder.Inc, App: c.Holder.App, Region: c.Op.NewRegion} |
| 294 | switch n := w.rng.Intn(10); { |
| 295 | case n < 7: |
| 296 | w.rec = rec |
| 297 | case n < 9: |
| 298 | // the response is lost and the PUT lands later, rarely after |
| 299 | // cancelled_creates' window |
| 300 | at := w.now + 1 + w.rng.Intn(2*horizonH) |
| 301 | if w.rng.Intn(beyondH) == 0 { |
| 302 | at = w.now + 4*horizonH + w.rng.Intn(10*horizonH) |
| 303 | } |
| 304 | w.recPend = &pendingRec{rec: rec, at: at} |
| 305 | } |
| 306 | // otherwise it failed outright; the next step retries |
| 307 | } |
| 308 | p.Step = 3 |
| 309 | return false |
| 310 | default: |
| 311 | if p.Host == "h2" { |
| 312 | if w.h2.OpID != p.OpID || w.h2.Kind != "creating" { |
| 313 | return abandon() |
| 314 | } |
| 315 | w.h2.Kind = "serving" // a CAS from creating, like the main host's |
| 316 | w.h2Epoch++ // every write changes the claim's ETag |
| 317 | w.logf("create %s: second host serving", p.OpID) |
| 318 | delete(ad.Reg, p.OpID) |
| 319 | return true |
| 320 | } |
| 321 | c := w.claim |
| 322 | if c == nil || c.Op.ID != p.OpID || c.Op.Kind != "creating" { |
| 323 | return abandon() |
| 324 | } |
| 325 | if w.rec == nil || w.rec.Inc != c.Holder.Inc { |
| 326 | if w.rec == nil && w.recPend == nil { |
| 327 | p.Step = 2 // publish again |
| 328 | } |
| 329 | return false |
| 330 | } |
| 331 | b := w.createExecutor(c) |
| 332 | if b == nil { |
| 333 | return false |
| 334 | } |
| 335 | if w.cas(c, func(n *claim) bool { |
| 336 | if !sameOp(n.Op.ID, p.OpID) { |
| 337 | return false |
| 338 | } |
| 339 | n.Op = opState{Kind: "serving", Exec: b.ID, Parts: []int{b.ID}} |
| 340 | n.Holder.Stamp = w.issueStamp(n, n.Op.Exec) // create step 4: holder.stamp is this CAS's gen (claim rev 6.5 §2) |
| 341 | return true |
| 342 | }) { |
| 343 | delete(ad.Reg, p.OpID) |
| 344 | return true |
| 345 | } |
| 346 | return false |
| 347 | } |
| 348 | } |
| 349 | |
| 350 | func (w *world) userDelete() { |
| 351 | c := w.claim |
| 352 | if c == nil || c.Holder == nil { |
| 353 | return |
| 354 | } |
| 355 | if on("claim-op-exclusive") && c.Op.Kind != "serving" { |
| 356 | return |
| 357 | } |
| 358 | id := w.newID("del") |
| 359 | if e := w.execBox(c); e != nil { |
| 360 | w.lastRegion = e.Region |
| 361 | } |
| 362 | if w.fail["recreate"] && c.Op.Kind == "serving" { |
| 363 | w.doorAuthorize() // a door listing that will race the delete and a recreate |
| 364 | if e := w.execBox(c); e != nil && e.DB != nil && hasMain(e) && w.rng.Intn(2) == 0 { |
| 365 | // the replicator's last PUT before the delete's stop evidence: |
| 366 | // accepted, then completing after the host is recreated |
| 367 | bl := snapshotOf(e.DB, e.DB.Inc) |
| 368 | bl.Kind, bl.Level = "ltx", 0 // a level-0 file covering everything so far |
| 369 | w.pending = append(w.pending, &request{kind: rPut, region: e.Region, key: ltxKey(e.DB.Loc, e.DB.Gen, 0, 1, bl.Max), b: bl, |
| 370 | doneAt: w.now + 40*horizonH, beyond: true, by: fmt.Sprintf("box:%d", e.ID)}) |
| 371 | } |
| 372 | } |
| 373 | recVer := 0 |
| 374 | if w.rec != nil { |
| 375 | recVer = w.rec.Ver |
| 376 | } |
| 377 | if w.cas(c, func(n *claim) bool { |
| 378 | if w.completionBarrier(n, w.verifiedCompletionFence(n)) { |
| 379 | return false // StartGuard's completion barrier (ruling 77), a verified fence exempt (ruling 86) |
| 380 | } |
| 381 | n.Op = opState{Kind: "deleting", ID: id, Exec: -1, ReqAt: w.now, RecVer: recVer} // intent: the record's ETag (claim §5.2 step 1) |
| 382 | return true |
| 383 | }) { |
| 384 | w.console = append(w.console, &consolePlan{Kind: "delete", OpID: id}) |
| 385 | w.logf("delete %s inc %d", id, c.Holder.Inc) |
| 386 | } |
| 387 | } |
| 388 | |
| 389 | func (w *world) userMove() { |
| 390 | c := w.claim |
| 391 | if c == nil || c.Holder == nil || c.Op.Kind != "serving" { |
| 392 | return |
| 393 | } |
| 394 | if src := w.execBox(c); src == nil || src.Destroyed { |
| 395 | return |
| 396 | } |
| 397 | w.moveTo(w.rng.Intn(nRegions)) // drawn only when a move is possible, as before rev 7.3 |
| 398 | } |
| 399 | |
| 400 | // h2Box is the executor the second host's create names (region HA §5.2): |
| 401 | // choose() in region 0, where the model keeps the control-plane-only |
| 402 | // host. With one box per region it is box 0, as the model always implied. |
| 403 | func (w *world) h2Box(app string) int { |
| 404 | if b := w.chooseBoxFor("h2", 0, app); b != nil { |
| 405 | return b.ID |
| 406 | } |
| 407 | return 0 |
| 408 | } |
| 409 | |
| 410 | // createExecutor is the box a create's step 4 hands op.exec to: the one |
| 411 | // its intent named, never another (region HA §5.2, claim P5-D2: recovery |
| 412 | // never substitutes a newly available box); nil while that box is gone. |
| 413 | // The mutation of create-choice-once chooses again, as rev 7.22's |
| 414 | // region-wide pick did. |
| 415 | func (w *world) createExecutor(c *claim) *box { |
| 416 | if w.perRegion <= 1 { |
| 417 | return w.regionBox(c.Op.NewRegion) // the one-box shape: today's region-wide pick, unchanged (spec §4; rev 4, Astra R1-1) |
| 418 | } |
| 419 | if !on("create-choice-once") { |
| 420 | return w.chooseBox(c.Op.NewRegion, c.Holder.App) |
| 421 | } |
| 422 | b := w.boxByID(c.Op.NewBox) |
| 423 | if b == nil || b.Destroyed { |
| 424 | return nil |
| 425 | } |
| 426 | return b |
| 427 | } |
| 428 | |
| 429 | // moveTo requests a move of the serving host to region r. A witness calls |
| 430 | // it directly (witness_test.go). |
| 431 | func (w *world) moveTo(r int) { |
| 432 | c := w.claim |
| 433 | if c == nil || c.Holder == nil || c.Op.Kind != "serving" { |
| 434 | return |
| 435 | } |
| 436 | src := w.execBox(c) |
| 437 | if src == nil || src.Destroyed { |
| 438 | return |
| 439 | } |
| 440 | if r == src.Region { |
| 441 | return |
| 442 | } |
| 443 | tgt := w.chooseBox(r, c.Holder.App) // the target box, chosen in the start CAS (region HA L15) |
| 444 | if tgt == nil || contains(c.Lost, tgt.ID) || tgt.Old { |
| 445 | return |
| 446 | } |
| 447 | if on("obligations-block-ops") { |
| 448 | for _, o := range c.Obl { |
| 449 | if o.Region == r || o.Box == tgt.ID || o.Box == src.ID || o.Region == src.Region { |
| 450 | return // an operation never starts over a pending chore in its regions |
| 451 | } |
| 452 | } |
| 453 | } |
| 454 | id := w.newID("mv") |
| 455 | if w.cas(c, func(n *claim) bool { |
| 456 | if n.Op.Kind != "serving" || w.completionBarrier(n, -1) { |
| 457 | return false |
| 458 | } |
| 459 | n.Op = opState{Kind: "moving", ID: id, Phase: "leases", Exec: src.ID, Parts: []int{src.ID, tgt.ID}, |
| 460 | Src: src.ID, Tgt: tgt.ID, SrcRegion: src.Region, TgtRegion: r, ReqAt: w.now, Auto: true, App: c.Holder.App, |
| 461 | SrcGen: c.Holder.Gen} // the source's generation, which a clean rollback's return names again (rev 7.10) |
| 462 | return true |
| 463 | }) { |
| 464 | w.logf("move %s inc %d from box %d to box %d", id, c.Holder.Inc, src.ID, tgt.ID) |
| 465 | } |
| 466 | } |
| 467 | |
| 468 | func (w *world) userPush() { |
| 469 | c := w.claim |
| 470 | if c == nil || c.Holder == nil || c.Op.Kind != "serving" { |
| 471 | return |
| 472 | } |
| 473 | b := w.execBox(c) |
| 474 | if b == nil || b.FailApp || b.Terminated { // a terminated executor is fenced and failed over, never pushed (region HA §5.9) |
| 475 | return |
| 476 | } |
| 477 | if on("obligations-block-ops") { |
| 478 | for _, o := range c.Obl { |
| 479 | if o.Region == b.Region || o.Box == b.ID { |
| 480 | return |
| 481 | } |
| 482 | } |
| 483 | } |
| 484 | id := w.newID("push") |
| 485 | if w.cas(c, func(n *claim) bool { |
| 486 | if n.Op.Kind != "serving" || w.completionBarrier(n, -1) { |
| 487 | return false |
| 488 | } |
| 489 | n.Op = opState{Kind: "pushing", ID: id, Phase: "stopping", Exec: b.ID, Parts: []int{b.ID}, Src: b.ID, Tgt: b.ID, SrcRegion: b.Region, TgtRegion: b.Region, ReqAt: w.now} |
| 490 | return true |
| 491 | }) { |
| 492 | w.logf("push %s on box %d", id, b.ID) |
| 493 | } |
| 494 | } |
| 495 | |
| 496 | func (w *world) userPurge() { |
| 497 | c := w.claim |
| 498 | app := app0 |
| 499 | if c != nil && c.Holder != nil { |
| 500 | app = c.Holder.App |
| 501 | } |
| 502 | for _, p := range w.console { |
| 503 | if p.Kind == "purge" { |
| 504 | return |
| 505 | } |
| 506 | } |
| 507 | w.console = append(w.console, &consolePlan{Kind: "purge", App: app}) |
| 508 | w.logf("purge app %s", app) |
| 509 | } |
| 510 | |
| 511 | func (w *world) parkingObligations(n *claim, inc int) { |
| 512 | regions := append([]int(nil), n.Regions...) |
| 513 | var boxes []int |
| 514 | boxes = append(boxes, n.Boxes...) |
| 515 | if !n.Complete && on("touched-incomplete") { |
| 516 | regions = nil |
| 517 | for r := 0; r < nRegions; r++ { |
| 518 | regions = append(regions, r) |
| 519 | } |
| 520 | for _, b := range w.liveBoxes() { |
| 521 | boxes = addUniq(boxes, b.ID) |
| 522 | } |
| 523 | } |
| 524 | // the deleted incarnation's own location (the legacy instances/<host> |
| 525 | // for a legacy host, which excludes child incarnations; claim rev |
| 526 | // 6.24 §2) and the staging namespace, each its own chore; an older |
| 527 | // incarnation's residue is the at-rest sweep's (R3-4). The mutation of |
| 528 | // scope-membership parks the whole host prefix, as rev 7.16 did |
| 529 | loc := "instances/" + host + "/" |
| 530 | if n.Holder != nil && on("scope-membership") { |
| 531 | loc = n.Holder.Location |
| 532 | } |
| 533 | for _, r := range regions { |
| 534 | for _, p := range []string{loc, "moves/" + host + "/"} { |
| 535 | n.Obl = append(n.Obl, w.newObl(n, "park-replica", r, -1, p, fmt.Sprint(inc), 0)) |
| 536 | } |
| 537 | } |
| 538 | for _, id := range boxes { |
| 539 | if b := w.boxByID(id); b != nil && !b.Destroyed { |
| 540 | n.Obl = append(n.Obl, w.newObl(n, "park-local", -1, id, "", fmt.Sprint(inc), 0)) |
| 541 | } |
| 542 | } |
| 543 | n.Retired = retire(n.Retired, inc) |
| 544 | } |
| 545 | |
| 546 | // consoleStep runs the next step of one console plan, chosen at random: |
| 547 | // the console's requests run concurrently. |
| 548 | func (w *world) consoleStep() { |
| 549 | if len(w.console) == 0 { |
| 550 | return |
| 551 | } |
| 552 | i := w.rng.Intn(len(w.console)) |
| 553 | if w.console[i].Stall > w.now { |
| 554 | return // this request's console goroutine is paused |
| 555 | } |
| 556 | if w.runPlan(w.console[i]) { |
| 557 | w.console = append(w.console[:i:i], w.console[i+1:]...) |
| 558 | } |
| 559 | } |
| 560 | |
| 561 | func (w *world) runPlan(p *consolePlan) bool { |
| 562 | c := w.claim |
| 563 | switch p.Kind { |
| 564 | case "create": |
| 565 | return w.createSteps(p) |
| 566 | case "delete": |
| 567 | if c == nil || c.Op.ID != p.OpID { |
| 568 | return true |
| 569 | } |
| 570 | return w.deleteSteps(c) |
| 571 | case "purge": |
| 572 | return w.purgeSteps(p) |
| 573 | case "orphan": |
| 574 | return w.orphanSteps(p) |
| 575 | } |
| 576 | return true |
| 577 | } |
| 578 | |
| 579 | // hasPlan: a console plan of this kind, by this owner, is in flight. |
| 580 | func (w *world) hasPlan(kind, owner string) bool { |
| 581 | for _, p := range w.console { |
| 582 | if p.Kind == kind && p.Host == owner { |
| 583 | return true |
| 584 | } |
| 585 | } |
| 586 | return false |
| 587 | } |
| 588 | |
| 589 | // orphanSteps is the orphan cleanup of claim rev 6 §5.1 step 5 (R3-2) as |
| 590 | // a console plan, so the console can pause between its observations and |
| 591 | // its delete: read the record (ETag E, incarnation I); read the claim |
| 592 | // fresh, afterwards; it is an orphan only if that claim names neither I |
| 593 | // as holder nor a creating operation for I; DeleteIfMatch(E). The |
| 594 | // mutation reads the claim first and the record second, and decides on |
| 595 | // the stale claim: a successor that claimed and published in between is |
| 596 | // then deleted. |
| 597 | func (w *world) orphanSteps(p *consolePlan) bool { |
| 598 | switch p.Step { |
| 599 | case 0: |
| 600 | if on("orphan-order") { |
| 601 | if w.rec == nil { |
| 602 | return true |
| 603 | } |
| 604 | p.RecVer, p.RecInc = w.rec.Ver, w.rec.Inc |
| 605 | } else { |
| 606 | p.Snap = w.claim.clone() |
| 607 | } |
| 608 | p.Step = 1 |
| 609 | return false |
| 610 | case 1: |
| 611 | if on("orphan-order") { |
| 612 | p.Orphan = w.orphanOf(w.claim, p.RecInc) // fresh, after the record |
| 613 | } else { |
| 614 | if w.rec == nil { |
| 615 | return true |
| 616 | } |
| 617 | p.RecVer, p.RecInc = w.rec.Ver, w.rec.Inc |
| 618 | p.Orphan = w.orphanOf(p.Snap, p.RecInc) |
| 619 | } |
| 620 | p.Step = 2 |
| 621 | return false |
| 622 | default: |
| 623 | if !p.Orphan || w.rec == nil || w.rec.Ver != p.RecVer { |
| 624 | return true // 412, or nothing to do |
| 625 | } |
| 626 | if c := w.claim; c != nil && (c.Holder != nil && c.Holder.Inc == w.rec.Inc || c.Op.Kind == "creating" && c.Op.NewInc == w.rec.Inc) { |
| 627 | w.violate("claim/record: orphan cleanup deleted the record of incarnation %d, which the claim names", w.rec.Inc) |
| 628 | } |
| 629 | w.logf("orphan cleanup (%s): removed record inc %d", p.Host, w.rec.Inc) |
| 630 | w.rec = nil |
| 631 | return true |
| 632 | } |
| 633 | } |
| 634 | |
| 635 | // deleteSteps: record DeleteIfMatch on the version the intent names, then |
| 636 | // parking with obligations, then free once every obligation is |
| 637 | // acknowledged (claim §5.2). Under a purge (claim rev 6.5 §5.3 step 4, |
| 638 | // R4-4) the same steps run under the purge's own claim: the record version |
| 639 | // is recorded in op.intent first, the delete is conditional on it, and |
| 640 | // purging → parking is legal only with the record authoritatively gone |
| 641 | // and the purge journal at torn-down or later. A purged host never returns |
| 642 | // to serving. |
| 643 | func (w *world) deleteSteps(c *claim) bool { |
| 644 | switch c.Op.Kind { |
| 645 | case "deleting", "purging": |
| 646 | if c.Op.Kind == "purging" && on("purge-journal") && w.purgeStep[c.Holder.App] < 4 { |
| 647 | return false // the journal is not at torn-down yet |
| 648 | } |
| 649 | if w.rec != nil && w.rec.Inc == c.Holder.Inc { |
| 650 | if c.Op.RecVer == 0 { |
| 651 | // the intent: the exact record version to delete |
| 652 | ver := w.rec.Ver |
| 653 | w.cas(c, func(n *claim) bool { |
| 654 | if !sameOp(n.Op.ID, c.Op.ID) || n.Op.Kind != c.Op.Kind { |
| 655 | return false |
| 656 | } |
| 657 | n.Op.RecVer = ver |
| 658 | return true |
| 659 | }) |
| 660 | return false |
| 661 | } |
| 662 | if w.rec.Ver == c.Op.RecVer { |
| 663 | w.rec = nil // DeleteIfMatch |
| 664 | } |
| 665 | return false |
| 666 | } |
| 667 | if w.rec != nil { |
| 668 | return false // C6: a mismatched record means wait |
| 669 | } |
| 670 | inc := c.Holder.Inc |
| 671 | w.cas(c, func(n *claim) bool { |
| 672 | if !sameOp(n.Op.ID, c.Op.ID) || n.Op.Kind != c.Op.Kind { |
| 673 | return false |
| 674 | } |
| 675 | n.Op.Kind = "parking" |
| 676 | w.parkingObligations(n, inc) |
| 677 | return true |
| 678 | }) |
| 679 | return false |
| 680 | case "parking": |
| 681 | if len(c.Obl) > 0 { |
| 682 | return false |
| 683 | } |
| 684 | w.free(c) |
| 685 | return true |
| 686 | } |
| 687 | return true |
| 688 | } |
| 689 | |
| 690 | func (w *world) free(c *claim) { |
| 691 | app := "" |
| 692 | if c.Holder != nil { |
| 693 | app = c.Holder.App |
| 694 | } |
| 695 | if w.cas(c, func(n *claim) bool { |
| 696 | if !sameOp(n.Op.ID, c.Op.ID) || len(n.Obl) > 0 { |
| 697 | return false |
| 698 | } |
| 699 | n.Holder, n.Op, n.Regions, n.Boxes, n.Complete = nil, opState{}, nil, nil, true |
| 700 | return true |
| 701 | }) { |
| 702 | w.logf("host freed") |
| 703 | w.opsDone++ |
| 704 | if r := w.residueAtEnd(); len(r) > 0 { |
| 705 | w.violate("INV-10: the host was freed with residue %v", r) |
| 706 | } |
| 707 | w.stats["freed"]++ |
| 708 | if w.fail["recreate"] && w.rng.Intn(2) == 0 && !w.calm { |
| 709 | // the biased schedule: recreate the host at once, where it last |
| 710 | // served, while the old incarnation's requests are in flight |
| 711 | w.nextInc++ |
| 712 | w.console = append(w.console, &consolePlan{Kind: "create", Host: "h", App: app, OpID: w.newID("cr"), Inc: w.nextInc, Region: w.lastRegion}) |
| 713 | } |
| 714 | if w.purgeRes[app] && !on("purge-journal") { |
| 715 | w.purgeRes[app] = false // freeing the host drops the reservation |
| 716 | } |
| 717 | } |
| 718 | } |
| 719 | |
| 720 | func (w *world) purgeSteps(p *consolePlan) bool { |
| 721 | c := w.claim |
| 722 | reserve := func() { |
| 723 | w.purgeRes[p.App] = true |
| 724 | } |
| 725 | claimIt := func() bool { |
| 726 | if c == nil && w.rec != nil && w.rec.App == p.App && on("purge-adopts") { |
| 727 | // an unclaimed legacy record of this app: adopt it first (§9), |
| 728 | // so the purge decides over claims, not over their absence |
| 729 | w.adopt() |
| 730 | return false |
| 731 | } |
| 732 | if c == nil || c.Holder == nil || c.Holder.App != p.App { |
| 733 | return true // nothing of this app holds the host |
| 734 | } |
| 735 | if c.Op.Kind == "purging" || c.Op.Kind == "parking" || c.Op.Kind == "deleting" { |
| 736 | return true |
| 737 | } |
| 738 | if c.Op.Kind != "serving" { |
| 739 | return false // retry later; the reservation stays |
| 740 | } |
| 741 | id := w.newID("pg") |
| 742 | return w.cas(c, func(n *claim) bool { |
| 743 | if n.Op.Kind != "serving" || w.completionBarrier(n, w.verifiedCompletionFence(n)) { |
| 744 | return false // ruling 86: a completion box whose termination fence verifies is exempt |
| 745 | } |
| 746 | n.Op = opState{Kind: "purging", ID: id, Exec: -1, ReqAt: w.now} |
| 747 | return true |
| 748 | }) |
| 749 | } |
| 750 | if on("purge-journal") { |
| 751 | if st, ok := w.purgeStep[p.App]; ok && st > p.Step { |
| 752 | p.Step = st // resume from the reservation's journal |
| 753 | } |
| 754 | defer func() { |
| 755 | if w.purgeRes[p.App] { |
| 756 | w.purgeStep[p.App] = p.Step |
| 757 | } |
| 758 | }() |
| 759 | } |
| 760 | ad := w.admit[p.App] |
| 761 | if p.OpID == "" { |
| 762 | // the purge id lives in the reservation, so a resumed purge |
| 763 | // releases its own fences |
| 764 | if id, ok := w.purgeOp[p.App]; ok { |
| 765 | p.OpID = id |
| 766 | } else { |
| 767 | p.OpID = w.newID("pg") |
| 768 | w.purgeOp[p.App] = p.OpID |
| 769 | } |
| 770 | } |
| 771 | switch p.Step { |
| 772 | case 0: |
| 773 | if on("purge-reserve-first") { |
| 774 | reserve() |
| 775 | } else { |
| 776 | w.stores[p.App] = false // tear down first |
| 777 | } |
| 778 | p.Step = 1 |
| 779 | return false |
| 780 | case 1: |
| 781 | // close admission (claim rev 4 §5.3 step 1b), so no new create can |
| 782 | // register |
| 783 | if on("admission-registration") { |
| 784 | ad.Closed = true |
| 785 | w.logf("purge %s: admission closed", p.App) |
| 786 | } |
| 787 | p.Step = 2 |
| 788 | return false |
| 789 | case 2: |
| 790 | // drain: every registered create reaches serving or is cancelled |
| 791 | // before the host set is fixed; an expired registration is dead |
| 792 | if on("admission-registration") { |
| 793 | // in create-id order: Go's map order would make the drain, and |
| 794 | // with it every seed after a purge, differ from run to run |
| 795 | // (found in rev 7.3; the sole source of nondeterminism) |
| 796 | ids := make([]string, 0, len(ad.Reg)) |
| 797 | for id := range ad.Reg { |
| 798 | ids = append(ids, id) |
| 799 | } |
| 800 | sort.Strings(ids) |
| 801 | for _, id := range ids { |
| 802 | e := ad.Reg[id] |
| 803 | // an expired registration whose host's claim does not name |
| 804 | // its create is dead: the create checks the expiry right |
| 805 | // before its claim CAS, so it can no longer claim (CC16) |
| 806 | claimed := e.Host == "h2" && w.h2.OpID == id && w.h2.Kind == "creating" || |
| 807 | e.Host == "h" && w.claim != nil && w.claim.Op.ID == id && w.claim.Op.Kind == "creating" |
| 808 | if on("registration-recovery") && w.now > e.Until && !claimed { |
| 809 | // fence the host's claim first, so a paused creator's |
| 810 | // CAS from free or absent fails (CC21); then remove |
| 811 | if on("purge-claim-fence") && !w.fenceHost(e.Host, p) { |
| 812 | return false |
| 813 | } |
| 814 | delete(ad.Reg, id) |
| 815 | continue |
| 816 | } |
| 817 | return false |
| 818 | } |
| 819 | } |
| 820 | p.Step = 3 |
| 821 | return false |
| 822 | case 3: |
| 823 | // the host set: records, plus registered in-flight creates (drained |
| 824 | // above). A second host the purge cannot see is not in it. |
| 825 | if !claimIt() { |
| 826 | return false |
| 827 | } |
| 828 | if w.h2.App == p.App && w.h2.Rec { |
| 829 | switch w.h2.Kind { |
| 830 | case "serving": |
| 831 | w.h2.Kind = "purging" |
| 832 | w.h2Epoch++ // every write changes the claim's ETag |
| 833 | case "purging": |
| 834 | default: |
| 835 | return false |
| 836 | } |
| 837 | } |
| 838 | p.Step = 4 |
| 839 | return false |
| 840 | case 4: |
| 841 | if on("purge-reserve-first") { |
| 842 | w.logf("purge %s: store torn down", p.App) |
| 843 | w.stores[p.App] = false |
| 844 | } else { |
| 845 | reserve() |
| 846 | } |
| 847 | p.Step = 5 |
| 848 | return false |
| 849 | default: |
| 850 | if w.h2.App == p.App && w.h2.Kind == "purging" { |
| 851 | w.h2 = liteHost{} // record deleted, claim freed |
| 852 | w.h2Epoch++ // every write changes the claim's ETag |
| 853 | } |
| 854 | if c == nil || c.Holder == nil || c.Holder.App != p.App { |
| 855 | // done: release this purge's fences by writing a free claim, |
| 856 | // never by deleting the object (CC21; claim rev 5.2 §5.3, C5a). |
| 857 | // The mutation deletes a fence that found no claim, so the |
| 858 | // claim is absent again and a paused creator's If-None-Match: * |
| 859 | // passes |
| 860 | if c != nil && c.Holder == nil && c.Op.Kind == "purging" && c.Op.ID == p.OpID { |
| 861 | if c.Op.FencedAbsent && !on("claim-never-deleted") { |
| 862 | w.claim = nil |
| 863 | w.logf("purge %s: fence on host %s deleted (the claim is absent again)", p.App, host) |
| 864 | } else { |
| 865 | w.cas(c, func(n *claim) bool { |
| 866 | if n.Holder != nil || n.Op.ID != p.OpID { |
| 867 | return false |
| 868 | } |
| 869 | n.Op = opState{} |
| 870 | return true |
| 871 | }) |
| 872 | } |
| 873 | } |
| 874 | if w.h2.Kind == "fenced" && w.h2.OpID == p.OpID { |
| 875 | if w.h2.FencedAbsent && !on("claim-never-deleted") { |
| 876 | w.h2, w.h2Epoch = liteHost{}, 0 // deleted: absent again |
| 877 | } else { |
| 878 | w.h2 = liteHost{} |
| 879 | w.h2Epoch++ // every write changes the claim's ETag |
| 880 | } |
| 881 | } |
| 882 | delete(w.purgeOp, p.App) |
| 883 | w.purgeRes[p.App] = false |
| 884 | delete(w.purgeStep, p.App) |
| 885 | ad.Closed = false // the purge's completion reopens admission |
| 886 | return true |
| 887 | } |
| 888 | w.deleteSteps(c) |
| 889 | return false |
| 890 | } |
| 891 | } |
| 892 | |
| 893 | // fenceHost CASes a host's claim from free or absent to a purge fence with |
| 894 | // no holder (claim rev 5.1 §5.3, CC21). A claim held by anyone already |
| 895 | // refuses a creator's CAS from free, so it needs no fence. A fence that |
| 896 | // found no claim is the one create-only write of a host's claim (claim |
| 897 | // rev 5.2 C5a); the fence remembers it, because its release must write |
| 898 | // free rather than restore the absence. |
| 899 | func (w *world) fenceHost(h string, p *consolePlan) bool { |
| 900 | if h == "h2" { |
| 901 | switch { |
| 902 | case w.h2.Kind == "": |
| 903 | w.h2 = liteHost{Kind: "fenced", OpID: p.OpID, App: p.App, FencedAbsent: w.h2Epoch == 0} |
| 904 | w.h2Epoch++ // every write changes the claim's ETag |
| 905 | w.logf("purge %s: fenced the second host", p.App) |
| 906 | case w.h2.Kind == "fenced" && w.h2.OpID != p.OpID: |
| 907 | return false // another purge's fence: wait for it |
| 908 | } |
| 909 | return true |
| 910 | } |
| 911 | c := w.claim |
| 912 | if c != nil && (c.Holder != nil || c.Op.Kind != "") { |
| 913 | return !(c.Holder == nil && c.Op.Kind == "purging" && c.Op.ID != p.OpID) |
| 914 | } |
| 915 | ok := w.cas(c, func(n *claim) bool { |
| 916 | if n.Holder != nil || n.Op.Kind != "" { |
| 917 | return false |
| 918 | } |
| 919 | n.Op = opState{Kind: "purging", ID: p.OpID, App: p.App, Exec: -1, FencedAbsent: c == nil} |
| 920 | return true |
| 921 | }) |
| 922 | if ok { |
| 923 | w.logf("purge %s: fenced host %s", p.App, host) |
| 924 | } |
| 925 | return ok |
| 926 | } |
| 927 | |
| 928 | // resumePurges: the recovery pass restarts a purge whose plan was lost, |
| 929 | // from its reservation's journal. |
| 930 | func (w *world) resumePurges() { |
| 931 | if !on("purge-journal") { |
| 932 | return |
| 933 | } |
| 934 | for _, app := range []string{app0, app1} { |
| 935 | if !w.purgeRes[app] { |
| 936 | continue |
| 937 | } |
| 938 | running := false |
| 939 | for _, p := range w.console { |
| 940 | if p.Kind == "purge" && p.App == app { |
| 941 | running = true |
| 942 | } |
| 943 | } |
| 944 | if !running { |
| 945 | w.console = append(w.console, &consolePlan{Kind: "purge", App: app, Step: w.purgeStep[app]}) |
| 946 | } |
| 947 | } |
| 948 | } |
| 949 | |
| 950 | // ---------- the door (claim §6.5) ---------- |
| 951 | |
| 952 | func (w *world) doorAuthorize() { |
| 953 | c := w.claim // O1 |
| 954 | if c == nil || c.Holder == nil || c.Op.Kind != "serving" { |
| 955 | return |
| 956 | } |
| 957 | b := w.execBox(c) |
| 958 | if b == nil { |
| 959 | return |
| 960 | } |
| 961 | // the listing will select the generation's newest LTX object |
| 962 | bk := w.buckets[b.Region] |
| 963 | key := "" |
| 964 | for _, k := range bk.keys(dataKey(c.Holder.Location, c.Holder.Gen, "")) { |
| 965 | if !isDataKey(k) || genPrefixOf(k) != dataKey(c.Holder.Location, c.Holder.Gen, "") { |
| 966 | continue |
| 967 | } |
| 968 | if v := bk.current(k); v != nil && (key == "" || v.ID > bk.current(key).ID) { |
| 969 | key = k |
| 970 | } |
| 971 | } |
| 972 | if key == "" { |
| 973 | return |
| 974 | } |
| 975 | d := &doorPlan{Region: b.Region, Loc: c.Holder.Location, Gen: c.Holder.Gen, Inc: c.Holder.Inc, OpID: c.Op.ID, |
| 976 | Key: key, Until: w.now + 1 + w.pauseLen()} |
| 977 | if w.fail["recreate"] && w.rng.Intn(2) == 0 { |
| 978 | d.Adv = true |
| 979 | if w.rng.Intn(2) == 0 { |
| 980 | d.Until = w.now + 40*horizonH // stalls before selecting |
| 981 | } |
| 982 | } |
| 983 | w.doorReads = append(w.doorReads, d) |
| 984 | } |
| 985 | |
| 986 | // doorOpen advances one stalled listing or file request. A stalled step |
| 987 | // resumes at its worst moment if one comes before its stall ends: when the |
| 988 | // claim's holder has changed since O1. Otherwise it waits out its stall. |
| 989 | func (w *world) doorOpen() { |
| 990 | if len(w.doorReads) == 0 { |
| 991 | return |
| 992 | } |
| 993 | i := w.rng.Intn(len(w.doorReads)) |
| 994 | worst := -1 |
| 995 | for j, d := range w.doorReads { |
| 996 | // its worst moment: the object its key names now belongs to |
| 997 | // another incarnation |
| 998 | if cur := w.buckets[d.Region].current(d.Key); cur != nil && !cur.Marker && cur.B.Inc != 0 && cur.B.Inc != d.Inc { |
| 999 | worst = j |
| 1000 | break |
| 1001 | } |
| 1002 | } |
| 1003 | switch { |
| 1004 | case worst >= 0: |
| 1005 | i = worst |
| 1006 | case w.doorReads[i].Until > w.now: |
| 1007 | return |
| 1008 | } |
| 1009 | d := w.doorReads[i] |
| 1010 | bk := w.buckets[d.Region] |
| 1011 | if !d.Signed { |
| 1012 | // select versions only under O1's location (step 3) |
| 1013 | if on("door-by-version") { |
| 1014 | v := bk.current(d.Key) |
| 1015 | if v == nil { |
| 1016 | w.doorReads = append(w.doorReads[:i:i], w.doorReads[i+1:]...) |
| 1017 | return |
| 1018 | } |
| 1019 | d.Ver = v.ID |
| 1020 | } |
| 1021 | // O2: refuse if the holder or the op changed since O1 (step 5) |
| 1022 | if c := w.claim; on("door-reread") && (c == nil || c.Holder == nil || c.Holder.Inc != d.Inc || c.Op.ID != d.OpID) { |
| 1023 | w.doorReads = append(w.doorReads[:i:i], w.doorReads[i+1:]...) |
| 1024 | return |
| 1025 | } |
| 1026 | d.Signed, d.Until = true, w.now+1+w.pauseLen() |
| 1027 | if d.Adv { |
| 1028 | d.Until = w.now + 40*horizonH // stalls between signing and the open |
| 1029 | } |
| 1030 | return |
| 1031 | } |
| 1032 | w.doorReads = append(w.doorReads[:i:i], w.doorReads[i+1:]...) |
| 1033 | var v *version |
| 1034 | if d.Ver != 0 { |
| 1035 | v = bk.byID(d.Key, d.Ver) |
| 1036 | } else { |
| 1037 | v = bk.current(d.Key) |
| 1038 | } |
| 1039 | if v != nil && v.B.Inc != 0 && v.B.Inc != d.Inc { |
| 1040 | w.violate("door: a read authorized for inc %d returned data of inc %d", d.Inc, v.B.Inc) |
| 1041 | } |
| 1042 | } |
| 1043 | |
| 1044 | // ---------- the console's claim-recovery pass (claim §8) ---------- |
| 1045 | |
| 1046 | func (w *world) recoveryPass() { |
| 1047 | if !on("recovery-pass") { |
| 1048 | return |
| 1049 | } |
| 1050 | w.resumePurges() |
| 1051 | // the second host's create (control plane only) |
| 1052 | if h := w.h2; h.Kind == "creating" && w.now-h.At >= 15 { |
| 1053 | if h.Rec { |
| 1054 | w.h2.Kind = "serving" |
| 1055 | w.h2Epoch++ // every write changes the claim's ETag |
| 1056 | } else { |
| 1057 | w.h2 = liteHost{} |
| 1058 | w.h2Epoch++ // every write changes the claim's ETag |
| 1059 | } |
| 1060 | w.logf("recovery: second host's create %s -> %q", h.OpID, w.h2.Kind) |
| 1061 | delete(w.admit[h.App].Reg, h.OpID) |
| 1062 | } |
| 1063 | c := w.claim |
| 1064 | if c == nil { |
| 1065 | return |
| 1066 | } |
| 1067 | // a terminated source of a pre-flip move (moves rev 7.20 §7.10, claim |
| 1068 | // rev 6.28 §4): the termination fence converts the operation to |
| 1069 | // relocating at pinning. The flip is the record's decision, so a record |
| 1070 | // at landing refuses the conversion and §7.10's own recovery applies. |
| 1071 | if on("fence-converts-moving") && c.Holder != nil && c.Op.Kind == "moving" && !c.Op.Committed && |
| 1072 | !(w.rec != nil && w.rec.MoveID == c.Op.ID && w.rec.MoveState == "landing") { |
| 1073 | if src := w.boxByID(c.Op.Src); src != nil && src.Destroyed { |
| 1074 | w.convertToRelocating(c, src) |
| 1075 | return |
| 1076 | } |
| 1077 | } |
| 1078 | // a relocation with no box in its region (a one-box region whose only |
| 1079 | // box was fenced): safe, nothing runs, the data is pinned; not |
| 1080 | // recovered until region HA enrolls a replacement. The operator is |
| 1081 | // told once (moves rev 7.20 §7.10, §13) |
| 1082 | if c.Op.Kind == "relocating" && c.Op.Phase == "pinning" && c.Op.Exec == -1 && !c.Op.Alerted && w.regionBox(c.Op.SrcRegion) == nil { |
| 1083 | if w.cas(c, func(n *claim) bool { n.Op.Alerted = true; return sameOp(n.Op.ID, c.Op.ID) && n.Op.Kind == "relocating" }) { |
| 1084 | w.alerts++ |
| 1085 | w.stats["relocation: waiting for a box in the region"]++ |
| 1086 | w.logf("relocation %s waits at pinning: no box in region %d", c.Op.ID, c.Op.SrcRegion) |
| 1087 | } |
| 1088 | return |
| 1089 | } |
| 1090 | // a late record PUT from a cancelled create: an orphan, never admitted |
| 1091 | // (C1); removed by the ordered cleanup of claim rev 6 §5.1 step 5, as |
| 1092 | // a plan of this console (J2-R2-7, R3-2) |
| 1093 | if w.rec != nil && on("cancelled-creates") && w.orphanOf(c, w.rec.Inc) { |
| 1094 | if !w.hasPlan("orphan", "recovery") { |
| 1095 | w.logf("recovery: cleaning up an orphan record inc %d", w.rec.Inc) |
| 1096 | w.console = append(w.console, &consolePlan{Kind: "orphan", Host: "recovery"}) |
| 1097 | } |
| 1098 | return |
| 1099 | } |
| 1100 | switch c.Op.Kind { |
| 1101 | case "creating": |
| 1102 | if w.now-c.Op.ReqAt < 15 { |
| 1103 | return |
| 1104 | } |
| 1105 | if w.rec != nil && w.rec.Inc == c.Holder.Inc { |
| 1106 | b := w.createExecutor(c) |
| 1107 | if b == nil { |
| 1108 | if nb := w.boxByID(c.Op.NewBox); w.perRegion > 1 && on("create-choice-once") && (nb == nil || nb.Destroyed) { |
| 1109 | // the chosen box cannot complete the create (the two-box |
| 1110 | // shape only; the one-box shape waits for its region's |
| 1111 | // box, as the baseline does): recovery cancels it (claim |
| 1112 | // §5.1 step 5, P5-D6), retiring the |
| 1113 | // incarnation; the record is an orphan the cleanup removes |
| 1114 | inc, app, id := c.Holder.Inc, c.Holder.App, c.Op.ID |
| 1115 | if w.cas(c, func(n *claim) bool { |
| 1116 | if !sameOp(n.Op.ID, id) { |
| 1117 | return false |
| 1118 | } |
| 1119 | n.Holder, n.Op = nil, opState{} |
| 1120 | n.Regions, n.Boxes = nil, nil |
| 1121 | n.Retired = retire(n.Retired, inc) |
| 1122 | n.Cancelled = append(n.Cancelled, cancelledCreate{Inc: inc, Until: w.now + 4*horizonH}) |
| 1123 | return true |
| 1124 | }) { |
| 1125 | delete(w.admit[app].Reg, id) |
| 1126 | w.stats["create cancelled: its box is gone"]++ |
| 1127 | w.logf("recovery: cancelled create %s inc %d, its chosen box %d is gone", id, inc, c.Op.NewBox) |
| 1128 | } |
| 1129 | } |
| 1130 | return |
| 1131 | } |
| 1132 | if w.cas(c, func(n *claim) bool { |
| 1133 | if !sameOp(n.Op.ID, c.Op.ID) { |
| 1134 | return false |
| 1135 | } |
| 1136 | n.Op = opState{Kind: "serving", Exec: b.ID, Parts: []int{b.ID}} |
| 1137 | n.Holder.Stamp = w.issueStamp(n, n.Op.Exec) // the recovery pass finishing create step 4 writes holder.stamp too (claim rev 6.5 §2) |
| 1138 | return true |
| 1139 | }) { |
| 1140 | delete(w.admit[c.Holder.App].Reg, c.Op.ID) |
| 1141 | } |
| 1142 | } else if w.rec == nil { |
| 1143 | // authoritatively absent: cancel, retiring the incarnation and |
| 1144 | // remembering it, so a late record PUT can be removed |
| 1145 | inc, app, id := c.Holder.Inc, c.Holder.App, c.Op.ID |
| 1146 | if w.cas(c, func(n *claim) bool { |
| 1147 | if !sameOp(n.Op.ID, id) { |
| 1148 | return false |
| 1149 | } |
| 1150 | n.Holder, n.Op = nil, opState{} |
| 1151 | n.Regions, n.Boxes = nil, nil |
| 1152 | n.Retired = retire(n.Retired, inc) |
| 1153 | n.Cancelled = append(n.Cancelled, cancelledCreate{Inc: inc, Until: w.now + 4*horizonH}) |
| 1154 | return true |
| 1155 | }) { |
| 1156 | delete(w.admit[app].Reg, id) |
| 1157 | w.logf("recovery: cancelled create %s inc %d", id, inc) |
| 1158 | } |
| 1159 | } |
| 1160 | case "deleting", "parking": |
| 1161 | if c.Holder == nil && c.Op.ParkSweep != "" { |
| 1162 | // a holderless sweep (claim rev 6.15 §6.2a) is the obligation |
| 1163 | // runners' to finish; the recovery pass only replays |
| 1164 | // FreeAfterPark for one whose chores are all acknowledged |
| 1165 | if c.oblFor(c.Op.ID) == 0 && w.now-c.Op.ReqAt >= 15 { |
| 1166 | id := c.Op.ID |
| 1167 | w.cas(c, func(n *claim) bool { |
| 1168 | if n.Holder != nil || n.Op.ID != id || n.oblFor(id) != 0 { |
| 1169 | return false |
| 1170 | } |
| 1171 | n.Op = opState{} |
| 1172 | return true |
| 1173 | }) |
| 1174 | } |
| 1175 | return |
| 1176 | } |
| 1177 | if w.now-c.Op.ReqAt < 15 { |
| 1178 | return |
| 1179 | } |
| 1180 | w.deleteSteps(c) |
| 1181 | case "purging": |
| 1182 | if c.Holder == nil { |
| 1183 | return // a purge fence: its purge releases it (CC21) |
| 1184 | } |
| 1185 | if w.now-c.Op.ReqAt < 15 { |
| 1186 | return |
| 1187 | } |
| 1188 | if on("purge-journal") { |
| 1189 | w.resumePurges() // the purge's own phases, in order |
| 1190 | return |
| 1191 | } |
| 1192 | w.deleteSteps(c) |
| 1193 | case "landing": |
| 1194 | w.fixRecord() |
| 1195 | if !c.Op.Committed && w.now > c.Op.CutDeadline+10 && w.now > c.Op.FlipAt+10 { |
| 1196 | w.rollback(c, "landing deadline") |
| 1197 | } |
| 1198 | case "moving", "reverting", "restoring", "serving": |
| 1199 | w.fixRecord() |
| 1200 | } |
| 1201 | } |
| 1202 | |
| 1203 | // orphan: claim rev 5 §5.1 (CC17). A record whose incarnation is retired, |
| 1204 | // or is not the claim's holder, is an orphan at any time; rev 4's |
| 1205 | // cancelled_creates window is the mutation. |
| 1206 | func (w *world) orphanOf(c *claim, inc int) bool { |
| 1207 | if c == nil { |
| 1208 | return false // no claim at all: a legacy record, adopted (§9), never an orphan |
| 1209 | } |
| 1210 | if c.Holder != nil && c.Holder.Inc == inc { |
| 1211 | return false |
| 1212 | } |
| 1213 | if c.Op.Kind == "creating" && c.Op.NewInc == inc { |
| 1214 | return false |
| 1215 | } |
| 1216 | if !on("orphan-no-deadline") { |
| 1217 | for _, x := range c.Cancelled { |
| 1218 | if x.Inc == inc && w.now <= x.Until { |
| 1219 | return true |
| 1220 | } |
| 1221 | } |
| 1222 | return false |
| 1223 | } |
| 1224 | return true |
| 1225 | } |
| 1226 | |
| 1227 | // ---------- the operator (calm phase only) ---------- |
| 1228 | |
| 1229 | func (w *world) operator() { |
| 1230 | c := w.claim |
| 1231 | if c == nil { |
| 1232 | return |
| 1233 | } |
| 1234 | // readmit a quarantined box once it has retired its old state (--readmit) |
| 1235 | for _, id := range c.Lost { |
| 1236 | if b := w.boxByID(id); b != nil && !b.Destroyed && b.Row == nil && b.DB == nil && b.Files == nil && len(b.Procs) == 0 { |
| 1237 | w.cas(c, func(n *claim) bool { |
| 1238 | var keep []int |
| 1239 | for _, x := range n.Lost { |
| 1240 | if x != id { |
| 1241 | keep = append(keep, x) |
| 1242 | } |
| 1243 | } |
| 1244 | n.Lost = keep |
| 1245 | return true |
| 1246 | }) |
| 1247 | w.logf("operator readmitted box %d", id) |
| 1248 | return |
| 1249 | } |
| 1250 | } |
| 1251 | // a stuck relocation (§5.8): carlos ops host resolve (model ruling 13; |
| 1252 | // the spec names the command and leaves its effect open). Nothing |
| 1253 | // moves away from a live box without its stop evidence: |
| 1254 | // - a live source still op.exec (starting, releasing, no release): |
| 1255 | // the relocation is abandoned and the host serves on the source; |
| 1256 | // - a live target op.exec without a release (its receipt lost after |
| 1257 | // P opened, its release overdue): it is sent to probe-failed, where |
| 1258 | // it runs its release sequence; |
| 1259 | // - op.exec none, released, or lost: replayed from pinning with the |
| 1260 | // replacement count reset, the exclusions cleared and the source |
| 1261 | // eligible again (Resolved), an empty listing accepted |
| 1262 | if c.Holder != nil && c.Op.Kind == "relocating" && c.Op.Stuck != "" { |
| 1263 | op := c.Op |
| 1264 | released := op.Release != nil && op.Release.Box == op.Exec |
| 1265 | dead := w.boxByID(op.Exec) |
| 1266 | if dead != nil && !dead.Destroyed { |
| 1267 | dead = nil |
| 1268 | } |
| 1269 | if ex := w.boxByID(op.Exec); ex != nil && !ex.Destroyed && op.Phase == "probe-failed" && !released && !contains(c.Lost, ex.ID) && (w.c1Fallback() || on("reloc-release-needs-flush") && w.releaseUnrecoverable(ex, c)) { |
| 1270 | // with claim ask C1 open no failed target can release at all |
| 1271 | // (finding 4), so its release is unrecoverable by construction |
| 1272 | // a live target that cannot release (its replicator and its |
| 1273 | // files are gone and nothing recorded a flush, rev 9): no |
| 1274 | // release will ever come, so the operator stops the box, and |
| 1275 | // its declared loss (claim D2) lets the next resolve replay |
| 1276 | // the operation from pinning |
| 1277 | w.stop(ex) |
| 1278 | w.stats["operator stopped a target that cannot release"]++ |
| 1279 | w.logf("operator stopped box %d: it cannot release relocation %s", ex.ID, op.ID) |
| 1280 | return |
| 1281 | } |
| 1282 | var what string |
| 1283 | if w.cas(c, func(n *claim) bool { |
| 1284 | if !sameOp(n.Op.ID, op.ID) || n.Op.Kind != "relocating" || n.Op.Stuck == "" { |
| 1285 | return false |
| 1286 | } |
| 1287 | if dead != nil && !contains(n.Lost, dead.ID) { |
| 1288 | // a stopped or terminated executor: the operator's declare-lost |
| 1289 | // (claim D2) puts it on lost, as a fence would, before the replay |
| 1290 | w.fenceBox(n, dead) |
| 1291 | released = false |
| 1292 | } |
| 1293 | switch { |
| 1294 | case op.Exec >= 0 && op.Exec == op.Src && !released && !contains(n.Lost, op.Exec) && (op.Phase == "starting" || op.Phase == "releasing"): |
| 1295 | src := op.Src |
| 1296 | n.Op = opState{Kind: "serving", Exec: src, Parts: []int{src}} |
| 1297 | what = "abandoned; the host serves on its source" |
| 1298 | case op.Exec >= 0 && !released && !contains(n.Lost, op.Exec): |
| 1299 | n.Op.Stuck, n.Op.Phase, n.Op.FailedAt, n.Op.Release = "", "probe-failed", w.now, nil |
| 1300 | what = "sent its live target to probe-failed" |
| 1301 | default: |
| 1302 | w.abandonPrepared(n) |
| 1303 | n.Op.Stuck, n.Op.Replacements, n.Op.Excluded, n.Op.Resolved = "", 0, nil, true |
| 1304 | n.Op.PinFailover = false // the replay enters pinning directly (rev 6) |
| 1305 | if released && op.Exec >= 0 && op.Exec != op.Src { |
| 1306 | // the target that just failed its probe is not the |
| 1307 | // operator's fresh choice (rev 4); a released source is |
| 1308 | // eligible again, as ruling 13 says (final review minor 4) |
| 1309 | n.Op.Excluded = []int{op.Exec} |
| 1310 | } |
| 1311 | n.Op.Phase, n.Op.Exec, n.Op.Tgt = "pinning", -1, -1 |
| 1312 | n.Op.Pin, n.Op.Prepared, n.Op.Receipt = nil, "", nil |
| 1313 | n.Op.BaseKey, n.Op.BaseVer, n.Op.BaseTX = "", 0, 0 |
| 1314 | n.Op.ProbeTries, n.Op.Attempts = 0, 0 |
| 1315 | var parts []int |
| 1316 | for _, p := range n.Op.Parts { |
| 1317 | if !contains(n.Lost, p) && p != op.Exec { |
| 1318 | parts = append(parts, p) |
| 1319 | } |
| 1320 | } |
| 1321 | n.Op.Parts = parts |
| 1322 | what = "replayed from pinning" |
| 1323 | } |
| 1324 | return true |
| 1325 | }) { |
| 1326 | w.stats["operator resolved a stuck relocation"]++ |
| 1327 | w.logf("operator resolved stuck relocation %s: %s", op.ID, what) |
| 1328 | } |
| 1329 | return |
| 1330 | } |
| 1331 | // a host marked failed by the retry policy (rev 7.11 §7.14): the operator |
| 1332 | // looks at it and clears the mark; the next attempt is a new session |
| 1333 | for _, b := range w.liveBoxes() { |
| 1334 | if b.hostFailed && w.now >= b.failedAt+horizonH/2 { |
| 1335 | b.hostFailed, b.failCounted, b.startFails, b.nextStart = false, false, 0, 0 |
| 1336 | w.stats["failed hosts cleared"]++ |
| 1337 | w.logf("operator cleared the failed host on box %d", b.ID) |
| 1338 | return |
| 1339 | } |
| 1340 | } |
| 1341 | // a destroyed box that owes only local chores: declare it lost (claim |
| 1342 | // §7.2 removes its obligations); compute fencing is the box being gone |
| 1343 | for _, o := range c.Obl { |
| 1344 | if o.Kind != "park-local" { |
| 1345 | continue |
| 1346 | } |
| 1347 | if b := w.boxByID(o.Box); b != nil && b.Destroyed { |
| 1348 | w.cas(c, func(n *claim) bool { |
| 1349 | var keep []obligation |
| 1350 | for _, x := range n.Obl { |
| 1351 | if !(x.Kind == "park-local" && x.Box == o.Box) { |
| 1352 | keep = append(keep, x) |
| 1353 | } |
| 1354 | } |
| 1355 | n.Obl = keep |
| 1356 | n.Lost = addUniq(n.Lost, o.Box) |
| 1357 | return true |
| 1358 | }) |
| 1359 | w.logf("operator declared box %d lost (local chores only)", o.Box) |
| 1360 | return |
| 1361 | } |
| 1362 | } |
| 1363 | w.declareTargetLost(c) |
| 1364 | } |
| 1365 | |
| 1366 | // releaseUnrecoverable is the operator's check before it stops a live |
| 1367 | // target that has not released (rev 10, Astra round 7): only when no |
| 1368 | // release can ever come. That needs no usable flush record for this |
| 1369 | // stop (rev 11: a record counts only with root's durable receipt, or while |
| 1370 | // the controller that recorded it is still running), and either the |
| 1371 | // session's replicator or the box's files directory gone for good |
| 1372 | // (relocRelease refuses without either). Any other release, a slow |
| 1373 | // acknowledgement or a recorded flush not yet journaled, is resumed: the |
| 1374 | // resolve clears stuck and sends the target back to probe-failed. The |
| 1375 | // mutation of operator-stop-unrecoverable-only stops every such target, |
| 1376 | // as rev 9 did. |
| 1377 | func (w *world) releaseUnrecoverable(b *box, c *claim) bool { |
| 1378 | if !on("operator-stop-unrecoverable-only") { |
| 1379 | return true |
| 1380 | } |
| 1381 | h := c.Holder |
| 1382 | if r := b.relRecord; r != nil && r.Op == c.Op.ID && r.Phase == c.Op.Phase && r.E.Session == h.Session && r.E.Gen == h.Gen && |
| 1383 | (r.Receipt || r.Ctl == b.Epoch || !on("reloc-release-needs-receipt")) { |
| 1384 | return false // a recorded flush with root's receipt, or its own controller still alive to finish it (rev 11) |
| 1385 | } |
| 1386 | replicator := b.DB != nil && b.DB.Inc == h.Inc && b.DB.Gen == h.Gen && b.DB.Epoch == b.Epoch && b.DB.Session == h.Session |
| 1387 | files := b.Files != nil && b.Files.Inc == h.Inc |
| 1388 | return !replicator || !files |
| 1389 | } |
| 1390 | |
| 1391 | // declareTargetLost is the declared loss of a landing's or a rollback's |
| 1392 | // target that is gone (claim D2, moves §7.10): the operator's path, and, |
| 1393 | // for a terminated target, the regional worker's automatic fence (claim |
| 1394 | // D2 "Automatic termination", rev 4). It proceeds record first, so a loss |
| 1395 | // racing the record's commit CAS follows whichever the record holds. |
| 1396 | func (w *world) declareTargetLost(c *claim) { |
| 1397 | if c.Holder == nil { |
| 1398 | return |
| 1399 | } |
| 1400 | op := c.Op |
| 1401 | if (op.Kind != "landing" && op.Kind != "restoring") || op.Committed { |
| 1402 | return |
| 1403 | } |
| 1404 | t := w.boxByID(op.Tgt) |
| 1405 | if t == nil { |
| 1406 | return |
| 1407 | } |
| 1408 | owesEvidence := op.Exec == op.Tgt |
| 1409 | owesReturn := op.Kind == "restoring" && op.Exec == -1 && op.DirtyKnown && op.Dirty && op.Phase != "returned" |
| 1410 | if !owesEvidence && !owesReturn { |
| 1411 | return |
| 1412 | } |
| 1413 | ok := false |
| 1414 | if on("declare-lost-compute") { |
| 1415 | ok = t.Destroyed // cloud API: stopped or terminated |
| 1416 | } else { |
| 1417 | l := w.execLease[t.ID] |
| 1418 | ok = t.Destroyed || (l.Op == op.ID && w.now > l.Expires+lostMargin) |
| 1419 | } |
| 1420 | if !ok { |
| 1421 | return |
| 1422 | } |
| 1423 | if op.Kind == "landing" { |
| 1424 | // it proceeds as a rollback, record first (§7.8, §7.10); the |
| 1425 | // claim follows, and the loss is applied to the restoring claim on |
| 1426 | // the operator's next call |
| 1427 | if w.rec != nil && w.rec.MoveID == op.ID && w.rec.MoveState == "landing" { |
| 1428 | w.rollback(c, "declared lost") |
| 1429 | } else { |
| 1430 | w.followRecord(c) |
| 1431 | } |
| 1432 | return |
| 1433 | } |
| 1434 | if w.cas(c, func(n *claim) bool { |
| 1435 | if !sameOp(n.Op.ID, op.ID) || n.Op.Committed || n.Op.Kind != "restoring" { |
| 1436 | return false |
| 1437 | } |
| 1438 | n.Lost = addUniq(n.Lost, t.ID) |
| 1439 | n.Op.Exec, n.Op.DirtyKnown, n.Op.Dirty, n.Op.Phase, n.Op.LostBox, n.Op.LostAt = -1, true, false, "released", t.ID, w.now |
| 1440 | var keep []obligation |
| 1441 | for _, o := range n.Obl { |
| 1442 | if o.Kind == "park-local" && o.Box == t.ID { |
| 1443 | continue |
| 1444 | } |
| 1445 | keep = append(keep, o) |
| 1446 | } |
| 1447 | n.Obl = keep |
| 1448 | if owesReturn && n.Op.RollbackID != "" && on("lost-return-park") { |
| 1449 | // a return the lost target had begun: park its lane in the |
| 1450 | // source's region, after the lane's staging horizon (model 27) |
| 1451 | n.Obl = append(n.Obl, w.scoped(w.newObl(n, "park-staging", op.SrcRegion, -1, fmt.Sprintf("moves/%s/%s/", host, op.RollbackID), "", w.now+stagingTTL+horizonH), w.now+stagingTTL, c.Holder.Inc)) |
| 1452 | } |
| 1453 | if owesEvidence { // a box that released already queued these |
| 1454 | // the lost target's parks cite the declaration's fencing bound |
| 1455 | // (claim rev 6.23 §2: a lost-box source uses the persisted |
| 1456 | // fenced_at), the staging lane its seal bound |
| 1457 | n.Obl = append(n.Obl, |
| 1458 | w.scoped(w.newObl(n, "park-superseded", op.TgtRegion, -1, c.Holder.Location, "", w.now+horizonH), w.now, c.Holder.Inc), |
| 1459 | w.scoped(w.newObl(n, "park-staging", op.TgtRegion, -1, fmt.Sprintf("moves/%s/%s/", host, op.ID), "", op.SealQuiet), stagingBound(op.SealQuiet), c.Holder.Inc)) |
| 1460 | // the lost target's region is parked whole: the records whose |
| 1461 | // predecessors are there (a restarted probe's, whose dead |
| 1462 | // writer never published) are covered in this CAS (claim rev |
| 1463 | // 6.14 item 6; seed 1036 / 3,000) |
| 1464 | w.coverRegionPredecessors(n, op.TgtRegion, "lost-target release") |
| 1465 | } |
| 1466 | return true |
| 1467 | }) { |
| 1468 | // the lost target's acknowledged writes are declared by the source's |
| 1469 | // admission (writes_lost for the target's uncertified session, or a |
| 1470 | // sealed baseline), never exempted here (R10-6). Its registered |
| 1471 | // timers went with it and no return lane will carry them: the |
| 1472 | // declaration names them, and alerts (seed 4120 / 30,000) |
| 1473 | w.logf("operator declared box %d lost for %s", t.ID, op.ID) |
| 1474 | n := 0 |
| 1475 | for i := range w.acks { |
| 1476 | x := &w.acks[i] |
| 1477 | if x.Box == t.ID && x.Inc == c.Holder.Inc && x.Kind == "timer" && !x.Exempt && !w.delivered[x.W] { |
| 1478 | x.Exempt = true |
| 1479 | n++ |
| 1480 | } |
| 1481 | } |
| 1482 | if n > 0 { |
| 1483 | w.stats["timers declared lost"] += n |
| 1484 | w.alert("box %d declared lost for %s: %d acknowledged timers registered on it are lost with it", t.ID, op.ID, n) |
| 1485 | } |
| 1486 | } |
| 1487 | } |
| 1488 | |
amadan