amadan
hostlife model: rev 7.13, joint round 12 and claim rev 6.14
Regional coverage recorded (R12-3): admission records carry Region and PredRegion; publishGeneration is claim rev 6.14's walk over the uncovered records (live predecessor or none anywhere: covered, no chore; this region: one deduplicated chore, covered; another region: left uncovered) and every cold admission publishes, prepared generations included; coverRegionPredecessors runs inside the CAS that queues a region's whole-location park (the commit, the target's release, the console's lost-target release); a record admitted under such a park is born covered; the sweep covers what it parks; INV-17 as a park-superseded completes. Retention trims covered records from the front only. The declared identity (R12-1): acknowledgements carry the session and generation of the process that gave them; exemptDeclared/declaredBy match a writes_lost record to its session; witness wTwoSessionDeclaration (INV-18). The probe deadline (R12-2): checked before each start and before readiness is accepted; INV-19 at every probe acceptance; witness wProbeWindowAt and TestProbeWindow at k = 29, 30, 31. Rule absent-marker-origin isolates wOriginSwept's fault from baseline-live. Rules: 101. Witnesses: 65. Faults found on the way: the lost-target release's park did not cover (seed 1036 / 3,000); acknowledgements took their session from a database a purge had removed (seed 899 / 3,000); the generation-conditional witness now waits for the publication chore before its second push.
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
8 files changed,
+743
−191
internal/sim/hostlife/background_test.go+5 −3internal/sim/hostlife/console_test.go+5 −0internal/sim/hostlife/moves_test.go+21 −2internal/sim/hostlife/protocol_test.go+310 −133internal/sim/hostlife/rules_test.go+30 −25internal/sim/hostlife/sim_test.go+2 −2internal/sim/hostlife/witness_test.go+338 −12internal/sim/hostlife/world_test.go+32 −14
diff --git a/internal/sim/hostlife/background_test.go b/internal/sim/hostlife/background_test.go| index a6987b728..bb5781ef5 100644 |
| --- a/internal/sim/hostlife/background_test.go |
| +++ b/internal/sim/hostlife/background_test.go |
| @@ -20,13 +20,15 @@ func (w *world) traffic(b *box) { |
| w.txs[wr] = tx{W: wr} // into a purged or foreign database: nowhere |
| } |
| // acknowledged to the client or the outside world either way: a |
| - // write into a purged or foreign database is a lost write |
| - w.acks = append(w.acks, ack{W: wr, Inc: p.Inc, Box: b.ID, At: w.now, Kind: "write"}) |
| + // write into a purged or foreign database is a lost write. The |
| + // acknowledgement is the process's session's (rev 7.13, R12-1): the |
| + // database under it may be gone (seed 899 / 3,000) |
| + w.acks = append(w.acks, ack{W: wr, Inc: p.Inc, Box: b.ID, Session: p.Session, Gen: p.Gen, At: w.now, Kind: "write"}) |
| w.writeInc[wr] = p.Inc |
| if p.Main && w.rng.Intn(4) == 0 && b.Row != nil && b.Row.Inc == p.Inc { |
| w.nextW++ |
| b.Timers = append(b.Timers, w.nextW) |
| - w.acks = append(w.acks, ack{W: w.nextW, Inc: p.Inc, Box: b.ID, At: w.now, Kind: "timer"}) |
| + w.acks = append(w.acks, ack{W: w.nextW, Inc: p.Inc, Box: b.ID, Session: p.Session, Gen: p.Gen, At: w.now, Kind: "timer"}) |
| } |
| } |
| } |
diff --git a/internal/sim/hostlife/console_test.go b/internal/sim/hostlife/console_test.go| index 533022cbe..a0f9608f0 100644 |
| --- a/internal/sim/hostlife/console_test.go |
| +++ b/internal/sim/hostlife/console_test.go |
| @@ -1216,6 +1216,11 @@ func (w *world) operator() { |
| n.Obl = append(n.Obl, |
| w.newObl(n, "park-superseded", op.TgtRegion, -1, c.Holder.Location, "", w.now+horizonH), |
| w.newObl(n, "park-staging", op.TgtRegion, -1, fmt.Sprintf("moves/%s/%s/", host, op.ID), "", op.SealQuiet)) |
| + // the lost target's region is parked whole: the records whose |
| + // predecessors are there (a restarted probe's, whose dead |
| + // writer never published) are covered in this CAS (claim rev |
| + // 6.14 item 6; seed 1036 / 3,000) |
| + w.coverRegionPredecessors(n, op.TgtRegion, "lost-target release") |
| } |
| return true |
| }) { |
diff --git a/internal/sim/hostlife/moves_test.go b/internal/sim/hostlife/moves_test.go| index cba286fdc..24e87c338 100644 |
| --- a/internal/sim/hostlife/moves_test.go |
| +++ b/internal/sim/hostlife/moves_test.go |
| @@ -778,6 +778,7 @@ func (w *world) revertSource(b *box, c *claim) { |
| b.Config, b.CfgVer, b.Live, b.LiveInc = c.Holder.Inc, w.cfgVer[c.Holder.App], c.Holder.App, c.Holder.Inc |
| } |
| if hasMain(b) || w.spawn(b, c, c.Holder.Gen, true) { |
| + w.probeAccepted(b, c) |
| w.cas(c, func(n *claim) bool { n.Op.RevPhase = "probed"; return sameOp(n.Op.ID, op.ID) }) |
| return |
| } |
| @@ -873,6 +874,10 @@ func (w *world) followRecord(c *claim) bool { |
| if q > n.Quiet[op.SrcRegion] { |
| n.Quiet[op.SrcRegion] = q |
| } |
| + // the source region's whole location is parked: its uncovered |
| + // predecessors are covered here, in the same CAS, with no chore |
| + // (claim rev 6.14 §6.4a item 6, CoverRegionPredecessors) |
| + w.coverRegionPredecessors(n, op.SrcRegion, "commit") |
| return true |
| }) |
| case r.MoveState == "rolling_back" && op.Kind == "landing": |
| @@ -1036,6 +1041,7 @@ func (w *world) landTarget(b *box, c *claim) { |
| return |
| } |
| if hasMain(b) || w.spawn(b, c, g, true) { |
| + w.probeAccepted(b, c) |
| if !on("commit-before-open") { |
| w.openRow(b, op.ID) |
| } |
| @@ -1270,6 +1276,7 @@ func (w *world) releaseTarget(b *box, c *claim) { |
| q := w.now + horizonH |
| if on("target-park") { |
| n.Obl = append(n.Obl, w.newObl(n, "park-superseded", op.TgtRegion, -1, c.Holder.Location, "", q)) |
| + w.coverRegionPredecessors(n, op.TgtRegion, "rollback") // the target region's whole location is parked (claim rev 6.14 item 6) |
| } |
| n.Obl = append(n.Obl, w.newObl(n, "park-staging", op.TgtRegion, -1, fmt.Sprintf("moves/%s/%s/", host, op.ID), "", op.SealQuiet)) |
| if !dirty { |
| @@ -1459,6 +1466,7 @@ func (w *world) recoverSource(b *box, c *claim) { |
| want = installGen(&op) // the return generation prepared from the target's sealed copy |
| } |
| if hasMain(b) || w.spawn(b, c, want, true) { |
| + w.probeAccepted(b, c) |
| w.cas(c, func(n *claim) bool { n.Op.SrcPhase = "probed"; return sameOp(n.Op.ID, op.ID) }) |
| return |
| } |
| @@ -1528,7 +1536,7 @@ func (w *world) pushStep(b *box, c *claim) { |
| snap.Gen = g |
| w.nextW++ |
| mark := w.nextW |
| - w.acks = append(w.acks, ack{W: mark, Inc: c.Holder.Inc, Box: b.ID, At: w.now, Kind: "write"}) |
| + w.acks = append(w.acks, ack{W: mark, Inc: c.Holder.Inc, Box: b.ID, Session: c.Holder.Session, Gen: c.Holder.Gen, At: w.now, Kind: "write"}) |
| w.writeInc[mark] = c.Holder.Inc |
| snap.Max++ |
| snap.Pages[fmt.Sprintf("k%d", mark)] = mark |
| @@ -1586,6 +1594,7 @@ func (w *world) pushStep(b *box, c *claim) { |
| return |
| } |
| if hasMain(b) || w.spawn(b, c, g, true) { |
| + w.probeAccepted(b, c) |
| w.cas(c, func(n *claim) bool { |
| n.Op.Phase = "probed" // holder.generation and holder.stamp moved at the probe's cold admission (claim rev 6.9) |
| q := op.StopAt + horizonH |
| @@ -1675,6 +1684,10 @@ func (w *world) sweep(b *box, c *claim) { |
| for _, p := range prefixes { |
| n.Obl = append(n.Obl, obligation{ID: w.newID("ob"), Op: "sweep", Kind: "park-sweep", Region: b.Region, Box: -1, Prefix: p, Ret: "sweep"}) |
| } |
| + // the sweep retires this region's dead generations wholesale: the |
| + // records whose predecessors it parks are covered here (rev 7.13; a |
| + // reading for the claim: item 6's composition applies to the sweep) |
| + w.coverSweptPredecessors(n, b.Region) |
| return true |
| }) |
| } |
| @@ -1757,9 +1770,15 @@ func (w *world) deadGeneration(c *claim, r int, k string) bool { |
| // publishes one, and that admission's unfinished chain protects the |
| // origin exactly as the residue oracle reads it |
| mg := "" |
| - if v := w.buckets[r].current(genMarkerKey(h.Location)); v != nil { |
| + v := w.buckets[r].current(genMarkerKey(h.Location)) |
| + if v != nil { |
| mg = v.B.Gen |
| } |
| + if v == nil && !on("absent-marker-origin") { |
| + // the mutation (rev 7.11's sweep): an absent marker is no |
| + // disagreement, so nothing protects the unfinished chain's origin |
| + mg = h.Gen |
| + } |
| if authoritative && mg != h.Gen { |
| // the marker disagrees with holder.generation. Normal while the |
| // latest admission is unfinished: the marker names its predecessor, |
diff --git a/internal/sim/hostlife/protocol_test.go b/internal/sim/hostlife/protocol_test.go| index df2e4e835..d94625e30 100644 |
| --- a/internal/sim/hostlife/protocol_test.go |
| +++ b/internal/sim/hostlife/protocol_test.go |
| @@ -475,7 +475,6 @@ func (w *world) spawn(b *box, c *claim, want string, probe bool) bool { |
| return false |
| } |
| } |
| - dead := []string{h.Gen} // what the new marker retires (claim rev 6.10 QueueGenerationRetire) |
| if bg != h.Gen && on("start-check") { |
| if !w.hasFiles(b, loc, h.Gen) { |
| // an empty holder.generation: only an unfinished admission's, |
| @@ -499,7 +498,6 @@ func (w *world) spawn(b *box, c *claim, want string, probe bool) bool { |
| break |
| } |
| } |
| - dead = append(append([]string{h.Gen}, chain[min(1, len(chain)):]...), bg) |
| w.stats["abandoned empty generation skipped"]++ |
| } else if !w.republishMarker(b, loc, h.Gen) { |
| // no earlier version names it: the admitted writer's marker |
| @@ -518,16 +516,9 @@ func (w *world) spawn(b *box, c *claim, want string, probe bool) bool { |
| // the marker names holder.generation now: the dead writer's |
| // predecessor, and the chain's, are retired as its own marker |
| // stage would have (seed 8528 / 30,000: a warm successor |
| - // continued the generation and nothing ever retired rec19) |
| - chain, _ := w.unfinishedChain(c, bg) |
| - lagDead := []string{bg} |
| - for _, g := range chain { |
| - if g != h.Gen && !hasStr(lagDead, g) { |
| - lagDead = append(lagDead, g) |
| - } |
| - } |
| - lagDead = w.uncovered(b, c, loc, h.Gen, lagDead) |
| - if !w.publishGeneration(b, c, c.Op.ID, phaseOf(&c.Op), h.Session, h.Gen, b.Region, w.newID("ob"), lagDead) { |
| + // continued the generation and nothing ever retired rec19). |
| + // The walk over holder.admissions finds them (claim rev 6.14) |
| + if !w.publishGeneration(b, c, c.Op.ID, phaseOf(&c.Op), h.Session, h.Gen, b.Region, w.newID("ob")) { |
| return false // the claim moved: next time |
| } |
| } |
| @@ -549,7 +540,7 @@ func (w *world) spawn(b *box, c *claim, want string, probe bool) bool { |
| return false |
| } |
| nh := w.claim.Holder |
| - o := &openState{Gen: nh.Gen, Want: want, Session: nh.Session, Mode: adm.Mode, Prepared: prepared, Probe: probe, Source: source, Dead: dead, RemoteMax: adm.RemoteMaxTXID, stage: "restore"} |
| + o := &openState{Gen: nh.Gen, Want: want, Session: nh.Session, Mode: adm.Mode, Prepared: prepared, Probe: probe, Source: source, RemoteMax: adm.RemoteMaxTXID, stage: "restore"} |
| b.open = o |
| return w.resumeOpen(b, c, o) |
| } |
| @@ -678,7 +669,7 @@ func (w *world) resumeOpen(b *box, c *claim, o *openState) bool { |
| if o.startedAt == 0 { |
| o.startedAt = w.now |
| } |
| - if o.Probe && w.now-o.startedAt >= probeStartWindow { |
| + if o.Probe && on("probe-window") && w.now-o.startedAt >= probeStartWindow { |
| // a probe attempt whose restore cannot proceed within its |
| // window fails like one whose app will not start (§7.7) |
| b.open = nil |
| @@ -717,9 +708,13 @@ func (w *world) resumeOpen(b *box, c *claim, o *openState) bool { |
| if !hasMain(b) { |
| if o.startedAt == 0 { |
| o.startedAt = w.now |
| + if o.Probe { |
| + b.lastProbe = probeTiming{startedAt: w.now} // INV-19 reads it at the probe's acceptance |
| + } |
| } |
| - if !(b.Config == h.Inc && b.Live == h.App && b.LiveInc == h.Inc) { |
| - if o.Probe && w.now-o.startedAt >= probeStartWindow { |
| + late := o.Probe && on("probe-window") && w.now-o.startedAt >= probeStartWindow |
| + if !(b.Config == h.Inc && b.Live == h.App && b.LiveInc == h.Inc) || w.now < o.startedAt+b.envUnreadyFor { |
| + if late { |
| // a probe attempt's readiness window has passed with the |
| // environment never ready: the attempt fails (§7.7) |
| b.open = nil |
| @@ -729,11 +724,23 @@ func (w *world) resumeOpen(b *box, c *claim, o *openState) bool { |
| } |
| return false // the environment: wait, no failure counted |
| } |
| + if late { |
| + // the deadline is checked before the start (rev 7.13 §7.7, |
| + // R12-2): an attempt whose window passed while the agent was |
| + // paused, or between a failed start and its retry, does not |
| + // start the app at all; a start that succeeded here would |
| + // have made an expired attempt the admitted writer |
| + b.open = nil |
| + b.startFails, b.nextStart = 0, 0 |
| + w.stats["probe attempt failed: deadline before the start"]++ |
| + w.probeAttemptFailed(b, cur) |
| + return false |
| + } |
| if !w.appStart(b, cur, o.Want, o.Probe, o.Mode) { |
| b.startFails++ |
| b.nextStart = w.now + startBackoff0<<(b.startFails-1) |
| w.stats["start failed"]++ |
| - if o.Probe && (b.startFails >= startAttemptsMax || w.now-o.startedAt >= probeStartWindow) { |
| + if o.Probe && (b.startFails >= startAttemptsMax || on("probe-window") && w.now-o.startedAt >= probeStartWindow) { |
| // a probe attempt's readiness window is the budget's 30 s |
| // (§7.3, §7.7): the retry policy's restarts share it, and |
| // when the fifth fails or the window passes the attempt |
| @@ -754,6 +761,26 @@ func (w *world) resumeOpen(b *box, c *claim, o *openState) bool { |
| return false |
| } |
| b.startFails = 0 |
| + if o.Probe { |
| + // and before readiness is accepted (R12-2): the app answered |
| + // after the deadline; it is stopped, the attempt fails, and |
| + // nothing it did is a session's (replication is not open) |
| + b.lastProbe.readyAt = w.now |
| + if on("probe-window") && w.now-o.startedAt >= probeStartWindow { |
| + var keep []*proc |
| + for _, p := range b.Procs { |
| + if !p.Main && !p.Strict { |
| + keep = append(keep, p) |
| + } |
| + } |
| + b.Procs = keep |
| + b.open = nil |
| + b.startFails, b.nextStart = 0, 0 |
| + w.stats["probe attempt failed: readiness after the deadline"]++ |
| + w.probeAttemptFailed(b, cur) |
| + return false |
| + } |
| + } |
| if on("admit-before-start") && w.startHook != nil { |
| if w.startHook(b) { // a witness's background work right after the start, inside the session |
| return false // the witness's crash |
| @@ -866,19 +893,17 @@ func (w *world) resumeOpen(b *box, c *claim, o *openState) bool { |
| } |
| } |
| o.req = nil |
| - // the marker names the new generation: the predecessor of a fresh |
| - // generation is dead from here and its retirement is queued |
| - // (claim rev 6.10 QueueGenerationRetire, R10-2); an operation's |
| - // prepared generation leaves its predecessor to the operation |
| - if o.Mode == "cold" && !o.Prepared { |
| - // the predecessor, the empty generations of a chain of |
| - // unfinished admissions, and any generation of this |
| - // operation's writers journal that still holds objects: an |
| - // earlier writer of the operation that died after its marker |
| - // landed but before it queued the chore left its own |
| - // predecessor behind (seed 899 / 30,000) |
| - dead := w.uncovered(b, cur, loc, o.Gen, append([]string(nil), o.Dead...)) |
| - if !w.publishGeneration(b, cur, cur.Op.ID, phaseOf(&cur.Op), o.Session, o.Gen, b.Region, w.newID("ob"), dead) { |
| + // the marker names the new generation: every cold admission, |
| + // a prepared generation's included, publishes it (claim rev |
| + // 6.14 §6.4a item 5; rev 7.12 left prepared generations to the |
| + // operation, R12-3). The walk over holder.admissions covers what |
| + // this region may retire: the predecessor, the empty |
| + // generations of a chain of unfinished admissions, an earlier |
| + // dead writer's predecessor (seed 899 / 30,000); a predecessor |
| + // whose objects are another region's stays uncovered for that |
| + // region's whole-location park |
| + if o.Mode == "cold" { |
| + if !w.publishGeneration(b, cur, cur.Op.ID, phaseOf(&cur.Op), o.Session, o.Gen, b.Region, w.newID("ob")) { |
| return false // the claim moved: next time |
| } |
| } |
| @@ -909,18 +934,28 @@ func (w *world) resumeOpen(b *box, c *claim, o *openState) bool { |
| // region, under the session's op id "session:<holder.session>". The |
| // mutation of baseline-live queues it at the admitting CAS instead, as |
| // rev 7.10 did, before the new generation has a root. |
| -// publishGeneration is claim rev 6.12's PublishGeneration(observedOpID, |
| -// observedPhase, observedSession, publishedGeneration, region): the one |
| -// CAS that retires generations, made after generation.json names the |
| -// published one, bound to the observed operation and phase like the |
| -// admission, legal while serving and inside any operation a writer runs |
| -// in (R11-5). It marks every admission entry up to the published |
| -// generation covered and queues one park-generation per dead generation, |
| -// deduplicated, with op = op.id inside an operation and "session:<n>" |
| -// while serving; only predecessors recorded in holder.admissions are ever |
| -// retired, and "" and "@root" are one origin (R11-2). Covered entries |
| -// beyond the last eight are trimmed. |
| -func (w *world) publishGeneration(b *box, c *claim, observedOpID, observedPhase string, session int, published string, region int, newID string, dead []string) bool { |
| +// publishGeneration is claim rev 6.14's PublishGeneration(observedOpID, |
| +// observedPhase, observedSession, publishedGeneration, region, newID) |
| +// (§6.4a item 5): the one CAS that retires generations, made after |
| +// generation.json names the published one, bound to the observed |
| +// operation and phase like the admission, legal while serving and inside |
| +// any operation a writer runs in (R11-5). It walks every uncovered cold |
| +// record of holder.admissions: a predecessor that is the published |
| +// generation is covered with no chore (it is live again: a clean return); |
| +// one with no objects anywhere (predecessor_region "") is covered with no |
| +// chore; one whose objects are this region's gets a deduplicated |
| +// park-generation chore, op = op.id inside an operation and "session:<n>" |
| +// while serving, and is covered; one whose objects are another region's |
| +// stays uncovered, with no chore, for that region's whole-location park |
| +// (CoverRegionPredecessors) or its own publication: a chore queued into |
| +// the source's region from the target's publication would park the |
| +// generation the rollback restores from (seeds 33646, 40148, 1296 / rev |
| +// 7.12; R12-3). The mutation of foreign-region-uncovered queues it there. |
| +// Only predecessors recorded in holder.admissions are ever retired, and |
| +// "" and "@root" are one origin (R11-2). Retention is conservative (claim |
| +// rev 6.14 item 8): covered records are trimmed from the front only, to |
| +// eight, and an uncovered record is never dropped, nor anything behind it. |
| +func (w *world) publishGeneration(b *box, c *claim, observedOpID, observedPhase string, session int, published string, region int, newID string) bool { |
| return w.cas(c, func(n *claim) bool { |
| if n.Holder == nil || n.Holder.Session != session || n.Holder.Gen != published { |
| return false |
| @@ -934,47 +969,38 @@ func (w *world) publishGeneration(b *box, c *claim, observedOpID, observedPhase |
| } |
| for i := range n.Holder.Admissions { |
| e := &n.Holder.Admissions[i] |
| - if e.Mode != "cold" || e.Session > session || e.Covered { |
| + if e.Mode != "cold" || e.Covered { |
| continue |
| } |
| - // covered: its predecessor is in this dead set (a chore in this |
| - // region), or is the published generation, or holds no object in |
| - // any region. A predecessor whose files live in another region |
| - // (a move's source generation, seen by the target's publication) |
| - // stays uncovered for that region's next PublishGeneration: a |
| - // chore queued there from here would park a generation the |
| - // rollback may still need (seeds 33646, 40148, 1296 / rev 7.12) |
| - if e.Predecessor.Gen == published || hasStr(dead, e.Predecessor.Gen) && (w.hasFilesIn(region, n.Holder.Location, e.Predecessor.Gen) || !w.hasFilesAnywhere(n.Holder.Location, e.Predecessor.Gen)) { |
| - e.Covered = true |
| - } |
| - } |
| - var keep []admissionRecord |
| - covered := 0 |
| - for i := len(n.Holder.Admissions) - 1; i >= 0; i-- { |
| - e := n.Holder.Admissions[i] |
| - if e.Covered || e.Mode != "cold" { |
| - covered++ |
| - if covered > 8 { |
| - continue // trimmed (claim rev 6.12: at most the last eight covered entries) |
| - } |
| + switch { |
| + case e.Predecessor.Gen == published: |
| + e.Covered = true // the predecessor is the live generation again |
| + w.stats["publish: predecessor live"]++ |
| + continue |
| + case e.PredRegion < 0: |
| + e.Covered = true // it holds nothing anywhere and no writer can add to it |
| + w.stats["publish: predecessor empty everywhere"]++ |
| + continue |
| + case e.PredRegion != region && on("foreign-region-uncovered"): |
| + w.stats["publish: predecessor left to its region"]++ |
| + continue // uncovered: that region's whole-location park covers it |
| } |
| - keep = append([]admissionRecord{e}, keep...) |
| - } |
| - n.Holder.Admissions = keep |
| - for _, retire := range dead { |
| - if retire == published || !w.hasFilesIn(region, n.Holder.Location, retire) && w.hasFilesAnywhere(n.Holder.Location, retire) { |
| - continue // its objects are another region's: that region's publication retires it |
| + chore := region |
| + if e.PredRegion != region { |
| + chore = e.PredRegion // the mutation: queued into the other region |
| + w.stats["publish: chore queued into another region (mutation)"]++ |
| } |
| // an empty dead generation still gets its chore: a dead writer's |
| // late upload or certificate may land in it within the chore's |
| // horizon (seeds 15273 and 20810 / 30,000) |
| - ret := retire |
| + ret := e.Predecessor.Gen |
| if ret == "" { |
| ret = "@root" // the sentinel for the origin generation (claim rev 6.10) |
| } |
| + e.Covered = true |
| queued := false |
| for _, o := range n.Obl { |
| - if o.Kind == "park-generation" && o.Region == region && o.Ret == ret && o.Prefix == n.Holder.Location { |
| + if o.Kind == "park-generation" && o.Region == chore && o.Ret == ret && o.Prefix == n.Holder.Location { |
| queued = true // already queued |
| } |
| } |
| @@ -985,14 +1011,81 @@ func (w *world) publishGeneration(b *box, c *claim, observedOpID, observedPhase |
| if hasObl(n.Obl, oid) { |
| oid = fmt.Sprintf("%s-%s", newID, ret) // one caller id, one chore per dead generation |
| } |
| - n.Obl = append(n.Obl, obligation{ID: oid, Op: id, Kind: "park-generation", Region: region, Box: -1, Prefix: n.Holder.Location, Ret: ret, Quiet: w.now + horizonH}) |
| + n.Obl = append(n.Obl, obligation{ID: oid, Op: id, Kind: "park-generation", Region: chore, Box: -1, Prefix: n.Holder.Location, Ret: ret, Quiet: w.now + horizonH}) |
| + } |
| + covered := 0 |
| + for _, e := range n.Holder.Admissions { |
| + if e.Covered || e.Mode != "cold" { |
| + covered++ |
| + } |
| + } |
| + for covered > 8 && len(n.Holder.Admissions) > 1 && (n.Holder.Admissions[0].Covered || n.Holder.Admissions[0].Mode != "cold") { |
| + n.Holder.Admissions = n.Holder.Admissions[1:] |
| + covered-- |
| } |
| return true |
| }) |
| } |
| -// hasFilesIn is hasFiles for a region. |
| -func (w *world) hasFilesIn(r int, loc, gen string) bool { |
| +// coverRegionPredecessors is claim rev 6.14's CoverRegionPredecessors |
| +// (§6.4a item 6), composed into the CAS that queues a region's |
| +// whole-location park (the commit's park of the source region, a |
| +// rollback's park of the target region): every uncovered cold record |
| +// whose predecessor's objects are that region's is covered, with no |
| +// chore, since the park retires the whole location there (R12-3, note 5). |
| +// The mutation of cover-at-park leaves them uncovered, and a later |
| +// publication in the region (or none) is their only cover. |
| +func (w *world) coverRegionPredecessors(n *claim, region int, why string) { |
| + if n.Holder == nil || !on("cover-at-park") { |
| + return |
| + } |
| + for i := range n.Holder.Admissions { |
| + e := &n.Holder.Admissions[i] |
| + if e.Mode == "cold" && !e.Covered && e.PredRegion == region && e.Predecessor.Gen != n.Holder.Gen { |
| + e.Covered = true |
| + w.stats["admissions covered at the "+why+" park"]++ |
| + } |
| + } |
| +} |
| + |
| +// coverSweptPredecessors is the sweep's reading of item 6 (rev 7.13, a |
| +// claim question): the at-rest sweep parks a region's dead generations |
| +// wholesale, so the records whose predecessors it parks are covered in |
| +// its CASes, the one that queues the park-sweep (a predecessor with a |
| +// sweepable object) and the one that acknowledges it (a predecessor whose |
| +// objects it retired on the way). An empty predecessor, with nothing to |
| +// sweep, waits for its publication's chore. |
| +func (w *world) coverSweptPredecessors(n *claim, region int) { |
| + if n.Holder == nil || !on("cover-at-park") { |
| + return |
| + } |
| + bk := w.buckets[region] |
| + loc := n.Holder.Location |
| + for i := range n.Holder.Admissions { |
| + e := &n.Holder.Admissions[i] |
| + if e.Mode != "cold" || e.Covered || e.PredRegion != region || e.Predecessor.Gen == n.Holder.Gen { |
| + continue |
| + } |
| + if w.hadFilesIn(region, loc, e.Predecessor.Gen) && !w.hasFilesIn(region, loc, e.Predecessor.Gen) { |
| + e.Covered = true // retired already: by this sweep or an earlier park |
| + w.stats["admissions covered at the sweep park"]++ |
| + continue |
| + } |
| + for _, k := range bk.keys(dataKey(loc, e.Predecessor.Gen, "")) { |
| + if genOf(loc, k) == e.Predecessor.Gen && w.sweepable(n, region, k) { |
| + e.Covered = true |
| + w.stats["admissions covered at the sweep park"]++ |
| + break |
| + } |
| + } |
| + } |
| +} |
| + |
| +// hadFilesIn: the generation held an object in region r at some time: a |
| +// key under its prefix, whatever versions remain (a parked key keeps its |
| +// entry with none). With hasFilesIn it tells a parked generation from one |
| +// that never had anything (INV-17). |
| +func (w *world) hadFilesIn(r int, loc, gen string) bool { |
| for _, k := range w.buckets[r].keys(dataKey(loc, gen, "")) { |
| if genOf(loc, k) == gen { |
| return true |
| @@ -1001,13 +1094,13 @@ func (w *world) hasFilesIn(r int, loc, gen string) bool { |
| return false |
| } |
| -// hasFilesAnywhere: the generation holds an object in some region. |
| -func (w *world) hasFilesAnywhere(loc, gen string) bool { |
| - for r := range w.buckets { |
| - for _, k := range w.buckets[r].keys(dataKey(loc, gen, "")) { |
| - if genOf(loc, k) == gen { |
| - return true |
| - } |
| +// hasFilesIn: the generation holds a current object (an LTX file or a |
| +// certificate, not a delete marker) in region r. |
| +func (w *world) hasFilesIn(r int, loc, gen string) bool { |
| + bk := w.buckets[r] |
| + for _, k := range bk.keys(dataKey(loc, gen, "")) { |
| + if genOf(loc, k) == gen && bk.current(k) != nil { |
| + return true |
| } |
| } |
| return false |
| @@ -1022,21 +1115,6 @@ func hasObl(obl []obligation, id string) bool { |
| return false |
| } |
| -// uncovered adds to dead the predecessor of every cold admission in |
| -// holder.admissions whose chores were never queued (its writer died after |
| -// its marker landed, before the PublishGeneration CAS) and that still |
| -// holds objects (seeds 899 and 98677 / 100,000). Every entry is marked |
| -// covered by the CAS that queues them. |
| -func (w *world) uncovered(b *box, c *claim, loc, published string, dead []string) []string { |
| - for i := range c.Holder.Admissions { |
| - e := &c.Holder.Admissions[i] |
| - if e.Mode == "cold" && !e.Covered && e.Gen != published && e.Predecessor.Gen != published && !hasStr(dead, e.Predecessor.Gen) && w.hasFiles(b, loc, e.Predecessor.Gen) { |
| - dead = append(dead, e.Predecessor.Gen) |
| - } |
| - } |
| - return dead |
| -} |
| - |
| // hasFiles: the generation holds at least one object (an LTX file or a |
| // certificate) in b's region; for the origin generation "", the objects |
| // directly under the location, not those of its g-<id>/ generations. |
| @@ -1123,9 +1201,11 @@ func (w *world) unfinishedChain(c *claim, bg string) ([]string, bool) { |
| } |
| // probeAttemptFailed counts a failed probe attempt against the operation's |
| -// budget (§7.3, §7.7): a landing rolls back at probeTries, a revert or a |
| -// rollback's source is stuck at three times that; the next attempt, if |
| -// any, is a new cold admission into a fresh generation. |
| +// budget (§7.3, §7.7): a landing rolls back at probeTries (three), a |
| +// revert or a rollback's source is stuck at three times that (nine, rev |
| +// 7.13 R12-5); the next attempt, if any, is a new cold admission into a |
| +// fresh generation. A probe never marks the host failed (claim rev 6.14): |
| +// the retry limit of §7.14 belongs to a serving wake. |
| func (w *world) probeAttemptFailed(b *box, c *claim) { |
| id := c.Op.ID |
| w.cas(c, func(n *claim) bool { |
| @@ -1179,9 +1259,9 @@ func (w *world) startProc(b *box, c *claim, want string, probe bool, mode string |
| if b.DB != nil { |
| gen = b.DB.Gen |
| } |
| - b.Procs = append(b.Procs, &proc{Main: true, Strict: strict, Inc: h.Inc, Gen: gen, Box: b.ID}) |
| + b.Procs = append(b.Procs, &proc{Main: true, Strict: strict, Inc: h.Inc, Gen: gen, Session: h.Session, Box: b.ID}) |
| if w.rng.Intn(2) == 0 { |
| - b.Procs = append(b.Procs, &proc{Main: false, Strict: strict, Inc: h.Inc, Gen: gen, Box: b.ID}) |
| + b.Procs = append(b.Procs, &proc{Main: false, Strict: strict, Inc: h.Inc, Gen: gen, Session: h.Session, Box: b.ID}) |
| } |
| w.logf("box %d spawned inc %d gen %q (%s, probe=%v strict=%v) claim=%s/%s exec=%d", b.ID, h.Inc, gen, mode, probe, strict, c.Op.Kind, c.Op.ID, c.Op.Exec) |
| return true |
| @@ -1372,6 +1452,11 @@ type admitInput struct { |
| // src_covered: the unchanged target and the source's complete replica |
| // establish preservation, R11-4) |
| Coverage string |
| + // Region is where the new writer keeps its generation's objects (its |
| + // box's region); PredecessorRegion where the predecessor's are, -1 for |
| + // a predecessor holding nothing anywhere (claim rev 6.14 §6.4a item 1) |
| + Region int |
| + PredecessorRegion int |
| } |
| // admitWriter decides the admission for a start on b under the claim it |
| @@ -1384,7 +1469,7 @@ type admitInput struct { |
| // (want, when it is not holder.generation) or a fresh one. |
| func (w *world) admitWriter(b *box, c *claim, want string, probe bool) (admitInput, bool) { |
| h := c.Holder |
| - a := admitInput{ObservedOpID: c.Op.ID, ObservedPhase: phaseOf(&c.Op), ObservedSession: h.Session, ObservedGeneration: h.Gen, Box: b.ID} |
| + a := admitInput{ObservedOpID: c.Op.ID, ObservedPhase: phaseOf(&c.Op), ObservedSession: h.Session, ObservedGeneration: h.Gen, Box: b.ID, Region: b.Region, PredecessorRegion: w.predecessorRegion(h)} |
| if on("exec-writer") && c.Op.Exec != b.ID { |
| w.stats["admission refused: not op.exec"]++ |
| w.logf("box %d: admission refused, op.exec is %d (%s/%s)", b.ID, c.Op.Exec, c.Op.Kind, c.Op.ID) |
| @@ -1451,6 +1536,33 @@ func (w *world) admitWriter(b *box, c *claim, want string, probe bool) (admitInp |
| return a, true |
| } |
| +// predecessorRegion is the next admission's predecessor_region (claim rev |
| +// 6.14 item 1): the region of the last admitted writer's box, where its |
| +// generation's objects are; before any record, the adopted or created |
| +// host's writer box, else wherever holder.generation holds an object. It |
| +// is -1, nothing to retire, when it holds none anywhere. A generation |
| +// whose objects were already parked, or that never held one, keeps its |
| +// region: a dead writer's late upload may still land in it, and the chore |
| +// a later publication queues there is what parks it (seeds 15273 and |
| +// 20810 / 30,000). |
| +func (w *world) predecessorRegion(h *holder) int { |
| + box, gen := h.WriterBox, h.Gen |
| + if l := lastAdmission(h); l != nil { |
| + box, gen = l.Box, l.Gen |
| + } |
| + for _, b := range w.boxes { |
| + if b.ID == box && box >= 0 { |
| + return b.Region |
| + } |
| + } |
| + for x := range w.buckets { |
| + if w.hasFilesIn(x, h.Location, gen) { |
| + return x |
| + } |
| + } |
| + return -1 |
| +} |
| + |
| // lastAdmission is the newest entry of holder.admissions, or nil: the next |
| // admission's predecessor (claim rev 6.12). |
| func lastAdmission(h *holder) *admissionRecord { |
| @@ -1536,7 +1648,22 @@ func (w *world) admitCommit(b *box, c *claim, a admitInput) bool { |
| if a.Mode != "cold" { |
| gen = n.Holder.Gen |
| } |
| - e := admissionRecord{Session: n.Holder.Session, Box: b.ID, Gen: gen, Stamp: n.Holder.Stamp, Mode: a.Mode, Coverage: a.Coverage, Predecessor: p} |
| + e := admissionRecord{Session: n.Holder.Session, Box: b.ID, Gen: gen, Stamp: n.Holder.Stamp, Mode: a.Mode, Coverage: a.Coverage, Predecessor: p, Region: a.Region, PredRegion: a.PredecessorRegion} |
| + if a.Mode == "cold" && on("cover-at-park") { |
| + // born covered (rev 7.13, a reading for the claim's item 6): the |
| + // claim already holds a whole-location park for the |
| + // predecessor's region, so the predecessor is being retired there |
| + // and this record needs no chore. A rollback's return is admitted |
| + // after the release queued the target region's park, and |
| + // CoverRegionPredecessors in that CAS could not see this record |
| + for _, o := range n.Obl { |
| + if o.Kind == "park-superseded" && o.Region == e.PredRegion && o.Prefix == n.Holder.Location { |
| + e.Covered = true |
| + w.stats["admissions born covered: whole-location park pending"]++ |
| + break |
| + } |
| + } |
| + } |
| if a.Mode == "cold" { |
| w.newGen(n.Holder.Location, h.Gen, a.NewGeneration) |
| n.Holder.Gen = a.NewGeneration |
| @@ -1616,42 +1743,14 @@ func (w *world) admitCommit(b *box, c *claim, a admitInput) bool { |
| if lost != nil { |
| // the writes the predecessor acknowledged and never uploaded are |
| // lost, declared and alerted (claim rev 6.9), never silently |
| - n := 0 |
| - for i := range w.acks { |
| - x := &w.acks[i] |
| - if x.Box == lost.Box && x.Inc == h.Inc && x.Kind == "write" && !x.Exempt && !w.durableInLineage(h.Location, a.NewGeneration, x.W) { |
| - // a rollback whose target was declared lost has no return lane: |
| - // what the seal holds in the target's region is the operator's |
| - // (§7.10), and the source declares what its own replica lacks |
| - // (seed 8035 / 30,000) |
| - declaredLost := contains(w.claim.Lost, lost.Box) || w.claim.Op.LostAt != 0 |
| - if w.isDurable(x.W) && !declaredLost { |
| - // INV-15 (rev 7.11): a write the host's remote holds is never |
| - // declared lost while its writer's box is still with us; the |
| - // lineage must adopt the generation that holds it (a dirty |
| - // rollback's return lane), not declare it. A box declared |
| - // lost may leave such writes behind: the record's |
| - // remote_max_txid names where an operator finds them |
| - w.violate("INV-15: box %d declared write %d lost, which is durable in the remote outside the new lineage (box %d's session %d)", b.ID, x.W, lost.Box, lost.Session) |
| - } |
| - x.Exempt = true |
| - n++ |
| - } |
| - } |
| + n := w.exemptDeclared(b, lost, h, a.NewGeneration, true) |
| w.stats["writes_lost declared"]++ |
| w.stats["writes declared lost"] += n |
| w.lostAlert++ |
| w.alert("box %d: writes_lost {box %d, generation %q, session %d, remote_max_txid %d}: %d acknowledged writes", b.ID, lost.Box, lost.Gen, lost.Session, lost.RemoteMaxTXID, n) |
| } |
| if lostSrc != nil { |
| - n := 0 |
| - for i := range w.acks { |
| - x := &w.acks[i] |
| - if x.Box == lostSrc.Box && x.Inc == h.Inc && x.Kind == "write" && !x.Exempt && !w.durableInLineage(h.Location, a.NewGeneration, x.W) { |
| - x.Exempt = true |
| - n++ |
| - } |
| - } |
| + n := w.exemptDeclared(b, lostSrc, h, a.NewGeneration, false) |
| w.stats["writes_lost declared"]++ |
| w.stats["writes declared lost"] += n |
| w.stats["writes_lost: source session behind a lost target"]++ |
| @@ -1661,6 +1760,67 @@ func (w *world) admitCommit(b *box, c *claim, a admitInput) bool { |
| return true |
| } |
| +// exemptDeclared applies a writes_lost record to the acknowledgements: the |
| +// writes the declared session acknowledged and never uploaded into the |
| +// new lineage are exempt from the loss oracles, since the record and its |
| +// alert declared them (claim rev 6.9, R10-6). It returns how many. With |
| +// inv15 it checks INV-15 for the predecessor's record. |
| +func (w *world) exemptDeclared(b *box, l *writesLost, h *holder, newGen string, inv15 bool) int { |
| + n := 0 |
| + for i := range w.acks { |
| + x := &w.acks[i] |
| + if !w.declaredBy(x, l, h.Inc) || w.durableInLineage(h.Location, newGen, x.W) { |
| + continue |
| + } |
| + if inv15 { |
| + // a rollback whose target was declared lost has no return lane: |
| + // what the seal holds in the target's region is the operator's |
| + // (§7.10), and the source declares what its own replica lacks |
| + // (seed 8035 / 30,000) |
| + declaredLost := contains(w.claim.Lost, l.Box) || w.claim.Op.LostAt != 0 |
| + if w.isDurable(x.W) && !declaredLost { |
| + // INV-15 (rev 7.11): a write the host's remote holds is never |
| + // declared lost while its writer's box is still with us; the |
| + // lineage must adopt the generation that holds it (a dirty |
| + // rollback's return lane), not declare it. A box declared |
| + // lost may leave such writes behind: the record's |
| + // remote_max_txid names where an operator finds them |
| + w.violate("INV-15: box %d declared write %d lost, which is durable in the remote outside the new lineage (box %d's session %d)", b.ID, x.W, l.Box, l.Session) |
| + } |
| + } |
| + x.Exempt = true |
| + n++ |
| + } |
| + return n |
| +} |
| + |
| +// declaredBy: acknowledgement x is one the writes_lost record covers: a |
| +// write of the host's incarnation on the record's box, acknowledged by |
| +// the writer session the record names, into the generation it names (rev |
| +// 7.13 §14.2.3, R12-1). A declaration for one session exempts nothing |
| +// another session acknowledged: those are undeclared losses still. The |
| +// mutation of session-scoped-loss is rev 7.12's box-wide match. |
| +func (w *world) declaredBy(x *ack, l *writesLost, inc int) bool { |
| + if x.Box != l.Box || x.Inc != inc || x.Kind != "write" || x.Exempt { |
| + return false |
| + } |
| + if !on("session-scoped-loss") { |
| + return true |
| + } |
| + return x.Session == l.Session && x.Gen == l.Gen |
| +} |
| + |
| +// probeAccepted is INV-19 (rev 7.13 §7.7, R12-2), checked where a probe |
| +// is accepted: the attempt whose app this is answered readiness within |
| +// its window of its first start; an attempt that answered at or after |
| +// the deadline is never the probed writer. |
| +func (w *world) probeAccepted(b *box, c *claim) { |
| + p := b.lastProbe |
| + if p.startedAt > 0 && p.readyAt >= p.startedAt && p.readyAt-p.startedAt >= probeStartWindow { |
| + w.violate("INV-19: box %d's probe was accepted %d steps after its first start (%s/%s), beyond the %d-step window", b.ID, p.readyAt-p.startedAt, c.Op.Kind, c.Op.ID, probeStartWindow) |
| + } |
| +} |
| + |
| // ---------- parking (claim §6.2) ---------- |
| // parkStep advances one park of `prefix` in b's own bucket into dest. It |
| @@ -1884,6 +2044,23 @@ func (w *world) doObligation(b *box, c *claim, o obligation) { |
| if (o.Kind == "park-replica" || o.Kind == "park-superseded") && on("quiet-before-ack") && o.Region >= 0 && evid+horizonH > n.Quiet[o.Region] { |
| n.Quiet[o.Region] = evid + horizonH // quiet_after survives free |
| } |
| + if o.Kind == "park-superseded" && n.Holder != nil && o.Prefix == n.Holder.Location { |
| + // INV-17 (rev 7.13, R12-3): the whole location in this region |
| + // is retired now; every record whose predecessor kept its |
| + // objects here was covered by the CAS that queued the park |
| + // (item 6) or born covered under it. One still uncovered |
| + // would wait for a publication in this region that may never |
| + // come, with a chore for a prefix already parked |
| + for _, e := range n.Holder.Admissions { |
| + if e.Mode == "cold" && !e.Covered && e.PredRegion == o.Region && e.Predecessor.Gen != n.Holder.Gen { |
| + w.violate("INV-17: the whole-location park %s of region %d retired admission %d's predecessor %q, and the record is uncovered", o.ID, o.Region, e.Session, e.Predecessor.Gen) |
| + break |
| + } |
| + } |
| + } |
| + if o.Kind == "park-sweep" && n.Holder != nil { |
| + w.coverSweptPredecessors(n, o.Region) // what the sweep retired on its way is covered as it finishes (rev 7.13 reading) |
| + } |
| n.Obl = append(n.Obl[:i:i], n.Obl[i+1:]...) |
| if o.Ret == "legacy" && n.oblFor("adopt") == 0 { |
| n.Complete = true // every region has acknowledged |
diff --git a/internal/sim/hostlife/rules_test.go b/internal/sim/hostlife/rules_test.go| index 0d0faf225..8c9ff288a 100644 |
| --- a/internal/sim/hostlife/rules_test.go |
| +++ b/internal/sim/hostlife/rules_test.go |
| @@ -107,29 +107,34 @@ var allRules = []string{ |
| "sweep-namespace", // claim rev 6 §6.2a (R3-4): the sweep discovers locations from the namespace; the mutation reads the capped retired_incarnations |
| "live-set-region", // claim rev 6.5 §6.2a (R4-3): the live set is {authoritative region, location, generation}; the mutation exempts matching keys in every region |
| // moves spec |
| - "seal-by-version", // J-N2: landing copies sealed versions |
| - "staging-quiet", // J-N2: staging retired after its writers' horizon |
| - "commit-before-open", // INV-5 |
| - "hold-op-open", // §5.2 conditional open |
| - "start-check", // INV-4: markers agree |
| - "start-check-claim-gen", // rev 6 §5.1 (R2-8): and name the generation the claim expects |
| - "generation-conditional", // rev 7.1 §5.1 (model 29): generation.json is written If-Match the marker it supersedes |
| - "markers-last", // R2-6 |
| - "revert-journal", // J-N11 |
| - "rollback-journal", // R2-3 |
| - "dirty-return", // INV-2 |
| - "seal-return", // rev 7.11 §7.8: a rollback whose source replica stops short of the stopped database returns the seal |
| - "clean-return-identity", // claim rev 6.12, R11-4: the predecessor is the last admitted writer, and a clean return with src_covered declares nothing |
| - "lost-return-park", // rev 7 §7.10 (model 27): declare-lost parks a return lane the lost target had begun (rev 7.2: a biased schedule stops the target mid-return) |
| - "target-park", // R2-5/INV-10 |
| - "abort-target-owner", // J-N13 |
| - "timer-freeze", // J-N14 runner bookkeeping |
| - "timer-canonical", // J-N14 prune path |
| - "cut-deadline", // J-N15 |
| - "readiness-key", // T2 |
| - "source-readiness", // S1: the source can run the instance before the cut |
| - "readiness-quiet", // T12: the target region's quiet_after has passed |
| - "files-carried", // §8 (the kpmg outage) |
| - "config-before-probe", // L3 (the kpmg outage) |
| - "recovery-current-inputs", // rev 6 §7.7 (J2-R2-5): a recovery probe is not bound to the move's pinned inputs |
| + "seal-by-version", // J-N2: landing copies sealed versions |
| + "staging-quiet", // J-N2: staging retired after its writers' horizon |
| + "commit-before-open", // INV-5 |
| + "hold-op-open", // §5.2 conditional open |
| + "start-check", // INV-4: markers agree |
| + "start-check-claim-gen", // rev 6 §5.1 (R2-8): and name the generation the claim expects |
| + "generation-conditional", // rev 7.1 §5.1 (model 29): generation.json is written If-Match the marker it supersedes |
| + "markers-last", // R2-6 |
| + "revert-journal", // J-N11 |
| + "rollback-journal", // R2-3 |
| + "dirty-return", // INV-2 |
| + "seal-return", // rev 7.11 §7.8: a rollback whose source replica stops short of the stopped database returns the seal |
| + "clean-return-identity", // claim rev 6.12, R11-4: the predecessor is the last admitted writer, and a clean return with src_covered declares nothing |
| + "foreign-region-uncovered", // claim rev 6.14 item 5: a predecessor in another region stays uncovered, never queued into its region from here (R12-3) |
| + "cover-at-park", // claim rev 6.14 item 6: CoverRegionPredecessors inside the CAS that queues a region's whole-location park (R12-3) |
| + "session-scoped-loss", // rev 7.13 §14.2.3: a writes_lost record exempts the writes of the session it names, no other (R12-1) |
| + "probe-window", // rev 7.13 §7.7: a probe attempt's deadline is checked before the start and before readiness is accepted (R12-2) |
| + "absent-marker-origin", // rev 7.12 §6.4: the sweep reads an absent generation.json as the origin (R11-1), isolated from baseline-live |
| + "lost-return-park", // rev 7 §7.10 (model 27): declare-lost parks a return lane the lost target had begun (rev 7.2: a biased schedule stops the target mid-return) |
| + "target-park", // R2-5/INV-10 |
| + "abort-target-owner", // J-N13 |
| + "timer-freeze", // J-N14 runner bookkeeping |
| + "timer-canonical", // J-N14 prune path |
| + "cut-deadline", // J-N15 |
| + "readiness-key", // T2 |
| + "source-readiness", // S1: the source can run the instance before the cut |
| + "readiness-quiet", // T12: the target region's quiet_after has passed |
| + "files-carried", // §8 (the kpmg outage) |
| + "config-before-probe", // L3 (the kpmg outage) |
| + "recovery-current-inputs", // rev 6 §7.7 (J2-R2-5): a recovery probe is not bound to the move's pinned inputs |
| } |
diff --git a/internal/sim/hostlife/sim_test.go b/internal/sim/hostlife/sim_test.go| index 644977127..144675cac 100644 |
| --- a/internal/sim/hostlife/sim_test.go |
| +++ b/internal/sim/hostlife/sim_test.go |
| @@ -88,7 +88,7 @@ func (w *world) legacyStart() { |
| b.DB = &localDB{Inc: inc, Loc: locationFor(inc, true), Key: key, State: map[string]int{}, Epoch: b.Epoch} |
| for i := 0; i < 3; i++ { |
| w.nextW++ |
| - w.acks = append(w.acks, ack{W: w.nextW, Inc: inc, Box: b.ID, At: 0, Kind: "write"}) |
| + w.acks = append(w.acks, ack{W: w.nextW, Inc: inc, Box: b.ID, Session: 1, Gen: "", At: 0, Kind: "write"}) // the pre-release writer: adoption's session 1 |
| w.writeInc[w.nextW] = inc |
| w.commit(b.DB, w.nextW) |
| } |
| @@ -697,7 +697,7 @@ func (w *world) keyHistory(inc int, why string, have map[int]bool) string { |
| if k != key { |
| continue |
| } |
| - out = append(out, fmt.Sprintf("W%d:TX%d=%d have=%v exempt=%v", a.W, t.TX, t.Val, have[a.W], a.Exempt)) |
| + out = append(out, fmt.Sprintf("W%d:TX%d=%d have=%v exempt=%v session=%d gen=%q", a.W, t.TX, t.Val, have[a.W], a.Exempt, a.Session, a.Gen)) |
| } |
| return "history of " + key + ": " + strings.Join(out, " ") |
| } |
diff --git a/internal/sim/hostlife/witness_test.go b/internal/sim/hostlife/witness_test.go| index 25e01bb76..10346da3b 100644 |
| --- a/internal/sim/hostlife/witness_test.go |
| +++ b/internal/sim/hostlife/witness_test.go |
| @@ -153,8 +153,20 @@ var witnesses = []witness{ |
| "a cold admission into a fresh generation; the box crashes before the first upload, so the generation is empty and the marker names the predecessor; the predecessor is the unfinished admission's baseline and stays live until the marker names the new generation; with the retire chore queued at the CAS, the predecessor is parked and the recovery restores nothing (claim rev 6.10, R10-2)", wBaselineParked}, |
| {"clean-return-identity", "clean-return-identity", "INV-16", |
| "a move's target is probed and writes nothing; the rollback is clean and the seal recorded src_covered; the source's re-admission journals the target's writer as its predecessor and coverage clean-return, declaring nothing; the mutation journals the target's session and box with the source's generation, a writer that never was, and declares a loss (claim rev 6.12, R11-4)", wCleanReturnIdentity}, |
| - {"baseline-live", "baseline-live", "INV-2", |
| - "an adopted host's origin replica holds durable writes and no generation.json; a cold admission into a fresh generation crashes before its first upload; the ordinary serving-time sweep runs before the recovery; with the absent marker read as the origin the chain protects it, and under the mutation the sweep parks the origin and the recovery restores nothing (R11-1)", wOriginSwept}, |
| + {"absent-marker-origin", "absent-marker-origin", "INV-2", |
| + "an adopted host's origin replica holds durable writes and no generation.json; a cold admission into a fresh generation crashes before its first upload; the ordinary serving-time sweep runs before the recovery; with the absent marker read as the origin the chain protects it, and under the mutation (rev 7.11's sweep, which read absence as agreement) the sweep parks the origin and the recovery restores nothing (R11-1; isolated from baseline-live in rev 7.13, R12 evidence)", wOriginSwept}, |
| + {"session-scoped-loss", "session-scoped-loss", "INV-18", |
| + "two writer sessions of one box each acknowledged a write that never uploaded; a writes_lost record for the second session exempts only its own write; matched box-wide (rev 7.12), the record absolves the first session's undeclared write too (R12-1)", wTwoSessionDeclaration}, |
| + {"foreign-region-uncovered", "foreign-region-uncovered", "INV-2", |
| + "a landing's probe publishes the target's generation; the source's generation, in another region, stays uncovered with no chore; a chore queued into the source's region from here parks the rollback's baseline within the horizon, and the clean rollback's return restores an empty database (claim rev 6.14 item 5, R12-3)", wRollbackBaselinePreserved}, |
| + {"cover-at-park", "cover-at-park", "INV-17", |
| + "a committed move: the CAS that queues the source region's whole-location park covers the target's record, whose predecessor is the source's generation there; without CoverRegionPredecessors the record stays uncovered after the park retired its predecessor (claim rev 6.14 item 6, R12-3)", wCommitCoverage}, |
| + {"cover-at-park", "cover-at-park", "INV-17", |
| + "the commit is interrupted between the record's flip and the claim's CAS: every actor pauses past the horizon; whoever follows the record later performs the one CAS, parks and coverage together (R12-3, interruption)", wCommitInterrupted}, |
| + {"cover-at-park", "cover-at-park", "INV-17", |
| + "the commit's CAS is followed again by another reader: the replay is refused, the park is queued once and the coverage stands (R12-3, replay)", wCommitReplayed}, |
| + {"probe-window", "probe-window", "INV-19", |
| + "a landing probe's launch environment is ready exactly at the 30-step deadline; the deadline is checked before the start, so the attempt fails and a fresh admission follows; unchecked, the expired attempt starts, answers readiness and becomes the probed writer (R12-2)", wProbeWindowAt}, |
| {"seal-return", "seal-return", "INV-15", |
| "the source acknowledges a write whose upload is still in flight when the cut stops it: the seal carries the write, the source's replica does not; the landing is rolled back before its probe; the return must carry the seal, and treated as clean the source's cold admission declares the write lost while the landing's built generation holds it (rev 7.11 §7.8)", wSealReturn}, |
| {"close-evidence", "close-evidence", "certificate while", |
| @@ -337,7 +349,7 @@ func (w *world) serve(b *box, inc int, app string) { |
| db := &localDB{Inc: inc, Loc: loc, Key: key, State: map[string]int{}, Epoch: b.Epoch} |
| for i := 0; i < 2; i++ { |
| w.nextW++ |
| - w.acks = append(w.acks, ack{W: w.nextW, Inc: inc, Box: b.ID, At: w.now, Kind: "write"}) |
| + w.acks = append(w.acks, ack{W: w.nextW, Inc: inc, Box: b.ID, Session: -1, At: w.now, Kind: "write"}) // the session is the holder's below |
| w.writeInc[w.nextW] = inc |
| w.commit(db, w.nextW) |
| } |
| @@ -354,6 +366,12 @@ func (w *world) serve(b *box, inc int, app string) { |
| n.Op = opState{Kind: "serving", Exec: b.ID, Parts: []int{b.ID}} |
| n.Regions, n.Boxes, n.Complete, n.Obl = []int{b.Region}, []int{b.ID}, true, nil |
| w.claim = n |
| + for i := range w.acks { |
| + if w.acks[i].Session == -1 { |
| + w.acks[i].Session = n.Holder.Session // the one writer session so far acknowledged them |
| + } |
| + } |
| + db.Session = n.Holder.Session |
| w.rec = &record{Ver: w.newVer(), Inc: inc, App: app, Region: b.Region} |
| b.Row = &row{Inc: inc, App: app, Status: "ready"} |
| b.DB = db |
| @@ -384,10 +402,11 @@ func (w *world) legacy(b *box, other int) { |
| b.DB = &localDB{Inc: inc, Loc: locationFor(inc, true), Key: key, State: map[string]int{}, Epoch: b.Epoch} |
| for i := 0; i < 2; i++ { |
| w.nextW++ |
| - w.acks = append(w.acks, ack{W: w.nextW, Inc: inc, Box: b.ID, At: w.now, Kind: "write"}) |
| + w.acks = append(w.acks, ack{W: w.nextW, Inc: inc, Box: b.ID, Session: 1, At: w.now, Kind: "write"}) // the pre-release writer: adoption's session 1 |
| w.writeInc[w.nextW] = inc |
| w.commit(b.DB, w.nextW) |
| } |
| + b.DB.Session = 1 |
| b.Files = &filesDir{Inc: inc, Key: key, Env: 1, Done: true} |
| b.Config, b.CfgVer, b.Live, b.LiveInc = inc, 1, app0, inc |
| full := w.deltaOf(b.DB, 0) |
| @@ -537,7 +556,8 @@ func (w *world) appWrite(b *box) int { |
| } else { |
| w.txs[wr] = tx{W: wr} |
| } |
| - w.acks = append(w.acks, ack{W: wr, Inc: p.Inc, Box: b.ID, At: w.now, Kind: "write"}) |
| + sess, gen := w.sessionOf(b) |
| + w.acks = append(w.acks, ack{W: wr, Inc: p.Inc, Box: b.ID, Session: sess, Gen: gen, At: w.now, Kind: "write"}) |
| w.writeInc[wr] = p.Inc |
| w.logf("witness: box %d wrote %d", b.ID, wr) |
| return wr |
| @@ -611,6 +631,11 @@ func wGenerationConditional(t *testing.T, w *world) { |
| w.serve(e, 1, app0) |
| loc := w.claim.Holder.Location |
| push := func(holdMarker bool) { |
| + // the previous push's publication queued the predecessor's |
| + // park-generation chore (claim rev 6.14 item 5: a prepared |
| + // generation publishes too); an obligation in the region blocks a |
| + // new operation until it runs (rule obligations-block-ops) |
| + w.reach(t, 400, "obligations clear", func() bool { return len(w.claim.Obl) == 0 }, w.act(e)) |
| w.userPush() |
| id := w.claim.Op.ID |
| if !w.reach(t, 400, "push "+id+" probing", func() bool { return w.claim.Op.ID == id && w.claim.Op.Phase == "probing" }, w.act(e)) { |
| @@ -718,7 +743,7 @@ func wMarkersLast(t *testing.T, w *world) { |
| w.serve(src, 1, app0) |
| w.nextW++ |
| src.Timers = []int{w.nextW} |
| - w.acks = append(w.acks, ack{W: w.nextW, Inc: 1, Box: src.ID, At: w.now, Kind: "timer"}) |
| + w.acks = append(w.acks, ack{W: w.nextW, Inc: 1, Box: src.ID, Session: src.DB.Session, Gen: src.DB.Gen, At: w.now, Kind: "timer"}) |
| w.moveTo(tgt.Region) |
| id := w.claim.Op.ID |
| w.reach(t, 600, "files extracted", func() bool { return tgt.Files != nil && tgt.Files.Gen == id }, w.act(src, tgt), w.recoveryPass) |
| @@ -860,7 +885,7 @@ func wStrictSpawn(t *testing.T, w *world) { |
| t.Fatalf("witness: source did not wake: %s", w.state()) |
| } |
| main := src.Procs[0] |
| - src.Procs = append(src.Procs, &proc{Main: false, Strict: main.Strict, Inc: 1, Box: src.ID}) |
| + src.Procs = append(src.Procs, &proc{Main: false, Strict: main.Strict, Inc: 1, Gen: main.Gen, Session: main.Session, Box: src.ID}) |
| w.moveTo(tgt.Region) |
| w.finish(t) |
| } |
| @@ -1429,7 +1454,8 @@ func (w *world) appWriteKey(b *box, key string, val int) int { |
| db.Pending = append(db.Pending, wr) |
| db.Log = append(db.Log, wr) |
| w.txs[wr] = t |
| - w.acks = append(w.acks, ack{W: wr, Inc: p.Inc, Box: b.ID, At: w.now, Kind: "write"}) |
| + sess, gen := w.sessionOf(b) |
| + w.acks = append(w.acks, ack{W: wr, Inc: p.Inc, Box: b.ID, Session: sess, Gen: gen, At: w.now, Kind: "write"}) |
| w.writeInc[wr] = p.Inc |
| w.logf("witness: box %d wrote %d: %s = %d", b.ID, wr, key, val) |
| return wr |
| @@ -1437,6 +1463,15 @@ func (w *world) appWriteKey(b *box, key string, val int) int { |
| // recovered drives the box until it runs again: a cold recovery first, |
| // when its replication state was lost, then the wake. |
| +// sessionOf is the writer session and generation b's database was admitted |
| +// under: what its acknowledgements carry (rev 7.13, R12-1). |
| +func (w *world) sessionOf(b *box) (int, string) { |
| + if b.DB == nil { |
| + return 0, "" |
| + } |
| + return b.DB.Session, b.DB.Gen |
| +} |
| + |
| func (w *world) recovered(t *testing.T, b *box, what string) { |
| if !w.reach(t, 120, what, func() bool { return hasMain(b) }, w.act(b), w.recoveryPass, func() { w.wake(b) }) { |
| t.Fatalf("witness: %s: the host did not run again: %s%s", what, w.state(), w.boxesState()) |
| @@ -1750,7 +1785,7 @@ func wEvidenceWholeTree(t *testing.T, w *world) { |
| if !hasMain(b0) { |
| w.recovered(t, b0, "running after adoption") |
| } |
| - b0.Procs = append(b0.Procs, &proc{Main: false, Strict: false, Inc: 1, Box: b0.ID}) // an escaped descendant |
| + b0.Procs = append(b0.Procs, &proc{Main: false, Strict: false, Inc: 1, Gen: b0.Procs[0].Gen, Session: b0.Procs[0].Session, Box: b0.ID}) // an escaped descendant |
| w.moveTo(b1.Region) |
| w.finish(t) |
| } |
| @@ -1763,7 +1798,7 @@ func wTimerFreeze(t *testing.T, w *world) { |
| w.serve(src, 1, app0) |
| w.nextW++ |
| src.Timers = []int{w.nextW} |
| - w.acks = append(w.acks, ack{W: w.nextW, Inc: 1, Box: src.ID, At: w.now, Kind: "timer"}) |
| + w.acks = append(w.acks, ack{W: w.nextW, Inc: 1, Box: src.ID, Session: src.DB.Session, Gen: src.DB.Gen, At: w.now, Kind: "timer"}) |
| w.landProbed(t, src, tgt) // the source is stopped and its row held |
| for i := 0; i < 3; i++ { |
| w.runner(src) // deliveries refused while the row is held |
| @@ -2097,7 +2132,8 @@ func (w *world) ackInto(b *box, inc int) int { |
| w.nextW++ |
| wr := w.nextW |
| w.commit(db, wr) |
| - w.acks = append(w.acks, ack{W: wr, Inc: inc, Box: b.ID, At: w.now, Kind: "write"}) |
| + sess, gen := w.sessionOf(b) |
| + w.acks = append(w.acks, ack{W: wr, Inc: inc, Box: b.ID, Session: sess, Gen: gen, At: w.now, Kind: "write"}) |
| w.writeInc[wr] = inc |
| w.logf("witness: a background worker on box %d acknowledged %d", b.ID, wr) |
| return wr |
| @@ -2212,7 +2248,8 @@ func wAnchorRetry(t *testing.T, w *world) { |
| snap.Max = 2 |
| w.nextW++ |
| wr := w.nextW |
| - w.acks = append(w.acks, ack{W: wr, Inc: 1, Box: b.ID, At: w.now, Kind: "write"}) |
| + sess, gen := w.sessionOf(b) |
| + w.acks = append(w.acks, ack{W: wr, Inc: 1, Box: b.ID, Session: sess, Gen: gen, At: w.now, Kind: "write"}) |
| w.writeInc[wr] = 1 |
| w.txs[wr] = tx{W: wr, TX: 3, Key: fmt.Sprintf("k%d", wr), Val: wr} |
| snap.Pages[fmt.Sprintf("k%d", wr)] = wr |
| @@ -2378,3 +2415,292 @@ func wOriginSwept(t *testing.T, w *world) { |
| w.checkDurable(w.claim, "after the recovery") |
| w.finish(t) |
| } |
| + |
| +// ---------- rev 7.13 ---------- |
| + |
| +// wTwoSessionDeclaration (R12-1) is a constructed-state oracle test: the |
| +// loss oracle's exemption, applied to acknowledgements of two sessions. |
| +// A box's first session acknowledged a write that never uploaded; so did |
| +// its second. A writes_lost record naming the second session exempts the |
| +// second write only (INV-18): the first stays an undeclared loss for the |
| +// oracles to report. Rev 7.12's match by box and incarnation absolved it. |
| +func wTwoSessionDeclaration(t *testing.T, w *world) { |
| + b := w.boxes[0] |
| + w.serve(b, 1, app0) |
| + h := w.claim.Holder |
| + s1 := h.Session |
| + w1 := w.ackInto(b, 1) // session 1's write, never uploaded |
| + s2 := s1 + 1 |
| + b.DB.Session = s2 // the constructed second session on the same box, same generation |
| + w2 := w.ackInto(b, 1) |
| + rec := &writesLost{Box: b.ID, Gen: h.Gen, Session: s2} |
| + n := w.exemptDeclared(b, rec, h, h.Gen, false) |
| + var x1, x2 *ack |
| + for i := range w.acks { |
| + switch w.acks[i].W { |
| + case w1: |
| + x1 = &w.acks[i] |
| + case w2: |
| + x2 = &w.acks[i] |
| + } |
| + } |
| + if x2 == nil || !x2.Exempt { |
| + t.Fatalf("witness: the declared session's write %d was not exempted", w2) |
| + } |
| + if x1 != nil && x1.Exempt { |
| + w.violate("INV-18 (witness): the writes_lost record for session %d exempted write %d, which session %d acknowledged and no record declares (%d exempted)", s2, w1, s1, n) |
| + } |
| +} |
| + |
| +// wRollbackBaselinePreserved (claim rev 6.14 item 5, R12-3): the target's |
| +// publication leaves the source's generation uncovered, with no chore, in |
| +// the source's region. Under the mutation a park-generation chore for it |
| +// is queued into the source's region from the target's publication; the |
| +// witness brings the chore's quiet time forward to now (the schedule |
| +// seeds 1036 and 1296 / rev 7.12 found with a landing open past the |
| +// horizon), lets the source's obligation runner work within the settle |
| +// window, then rolls the landing back cleanly: the return restores from |
| +// the source's generation. |
| +func wRollbackBaselinePreserved(t *testing.T, w *world) { |
| + src, tgt := w.boxes[0], w.boxes[1] |
| + w.serve(src, 1, app0) |
| + w.wake(src) |
| + w.appWrite(src) |
| + w.replicate(src) |
| + w.landProbed(t, src, tgt) |
| + loc, gen0 := w.claim.Holder.Location, w.claim.Op.SrcGen |
| + chores := 0 |
| + w.cas(w.claim, func(n *claim) bool { |
| + for i := range n.Obl { |
| + if n.Obl[i].Kind == "park-generation" && n.Obl[i].Region == src.Region { |
| + n.Obl[i].Quiet = w.now // the horizon has passed |
| + chores++ |
| + } |
| + } |
| + return true |
| + }) |
| + w.logf("witness: %d park-generation chores in the source's region after the target's publication", chores) |
| + // within the settle window, before the target's commit: the source |
| + // region's runner works the chore, if any |
| + w.drive(12, func() bool { return !w.hasFilesIn(src.Region, loc, gen0) }, w.act(src, tgt)) |
| + if len(w.violations) > 0 { |
| + return |
| + } |
| + if !w.hasFilesIn(src.Region, loc, gen0) { |
| + w.logf("witness: the source's generation %q is gone from region %d before the rollback", gen0, src.Region) |
| + } |
| + w.rollback(w.claim, "settle check failed") // the target wrote nothing: a clean rollback |
| + w.reach(t, 800, "source re-admitted after the rollback", func() bool { |
| + c := w.claim |
| + return len(w.violations) > 0 || c.Op.Kind == "serving" || c.Op.Kind == "restoring" && (c.Op.SrcPhase == "probed" || c.Op.SrcPhase == "opened" || c.Op.SrcPhase == "stuck") |
| + }, w.act(src, tgt), w.recoveryPass, w.runConsole) |
| + if len(w.violations) > 0 { |
| + return |
| + } |
| + if w.claim.Op.Kind == "restoring" && w.claim.Op.SrcPhase == "stuck" { |
| + w.violate("stuck: source could not recover %s: its generation %q was parked while the landing was still open", w.claim.Op.ID, gen0) |
| + return |
| + } |
| + w.recovered(t, src, "source serving again") |
| + w.checkLocal(w.claim, src, src.DB) |
| + w.checkDurable(w.claim, "after the rollback") |
| + w.finish(t) |
| +} |
| + |
| +// commitLanding drives a probed landing through its commit: the record |
| +// flips first, then whoever reads both follows it with the claim's CAS. |
| +// It returns the target's admission record, whose predecessor is the |
| +// source's generation in the source's region. |
| +func (w *world) commitLanding(t *testing.T, src, tgt *box) *admissionRecord { |
| + w.landProbed(t, src, tgt) |
| + var target *admissionRecord |
| + for i := range w.claim.Holder.Admissions { |
| + e := &w.claim.Holder.Admissions[i] |
| + if e.Box == tgt.ID && e.Mode == "cold" { |
| + target = e |
| + } |
| + } |
| + if target == nil || target.PredRegion != src.Region || target.Predecessor.Gen != w.claim.Op.SrcGen { |
| + t.Fatalf("witness: the target's record does not name the source's generation in the source's region: %s", w.state()) |
| + } |
| + if target.Covered { |
| + t.Fatalf("witness: the target's record was covered by its own publication, with its predecessor in another region: %s", w.state()) |
| + } |
| + w.reach(t, 400, "landing committed", func() bool { return w.claim.Op.Kind == "landing" && w.claim.Op.Committed }, w.act(src, tgt), w.recoveryPass, w.runConsole) |
| + return target |
| +} |
| + |
| +// targetRecord finds the target's cold admission record in the claim now. |
| +func (w *world) targetRecord(tgt *box) *admissionRecord { |
| + var out *admissionRecord |
| + for i := range w.claim.Holder.Admissions { |
| + e := &w.claim.Holder.Admissions[i] |
| + if e.Box == tgt.ID && e.Mode == "cold" { |
| + out = e |
| + } |
| + } |
| + return out |
| +} |
| + |
| +// wCommitCoverage (claim rev 6.14 item 6, R12-3): the commit's CAS queues |
| +// the source region's whole-location park and covers the target's record |
| +// in the same CAS. |
| +func wCommitCoverage(t *testing.T, w *world) { |
| + src, tgt := w.boxes[0], w.boxes[1] |
| + w.serve(src, 1, app0) |
| + w.wake(src) |
| + w.appWrite(src) |
| + w.commitLanding(t, src, tgt) |
| + if len(w.violations) > 0 { |
| + return |
| + } |
| + e := w.targetRecord(tgt) |
| + if e == nil { |
| + t.Fatalf("witness: the target's record is gone after the commit: %s", w.state()) |
| + } |
| + parks := 0 |
| + for _, o := range w.claim.Obl { |
| + if o.Kind == "park-superseded" && o.Region == src.Region { |
| + parks++ |
| + } |
| + } |
| + if parks != 1 { |
| + t.Fatalf("witness: %d park-superseded obligations for the source region after the commit: %s", parks, w.state()) |
| + } |
| + if !e.Covered { |
| + w.logf("witness: the target's record is uncovered after the commit's CAS queued the source region's park") |
| + } |
| + w.finish(t) // INV-17 at the end: an uncovered record whose predecessor's objects the park retired |
| +} |
| + |
| +// wCommitInterrupted (R12-3, interruption): the record flips to committed |
| +// and nothing follows it for longer than the horizon; the claim's CAS, |
| +// parks and coverage in one, is performed by whoever reads both later. |
| +func wCommitInterrupted(t *testing.T, w *world) { |
| + src, tgt := w.boxes[0], w.boxes[1] |
| + w.serve(src, 1, app0) |
| + w.wake(src) |
| + w.appWrite(src) |
| + w.landProbed(t, src, tgt) |
| + // the record commits (the target's settle check passed) with no claim CAS following |
| + w.reach(t, 400, "record committed", func() bool { return w.rec != nil && w.rec.MoveState == "committed" }, func() { w.worker(tgt) }) |
| + if w.claim.Op.Committed { |
| + t.Fatalf("witness: the claim followed the record in the same step; the interruption needs a gap: %s", w.state()) |
| + } |
| + for i := 0; i < horizonH+10; i++ { |
| + w.tick() // every actor paused: nobody follows the record |
| + } |
| + if w.claim.Op.Committed { |
| + t.Fatalf("witness: the claim committed while every actor was paused: %s", w.state()) |
| + } |
| + w.reach(t, 400, "landing committed after the interruption", func() bool { return w.claim.Op.Kind == "landing" && w.claim.Op.Committed }, w.act(src, tgt), w.recoveryPass, w.runConsole) |
| + if len(w.violations) > 0 { |
| + return |
| + } |
| + if e := w.targetRecord(tgt); e != nil && !e.Covered { |
| + w.logf("witness: the target's record is uncovered after the replayed commit") |
| + } |
| + w.finish(t) |
| +} |
| + |
| +// wCommitReplayed (R12-3, replay): after the commit's CAS another reader |
| +// follows the record again; the replay is refused, the source region's |
| +// park is queued once and the coverage stands. |
| +func wCommitReplayed(t *testing.T, w *world) { |
| + src, tgt := w.boxes[0], w.boxes[1] |
| + w.serve(src, 1, app0) |
| + w.wake(src) |
| + w.appWrite(src) |
| + w.commitLanding(t, src, tgt) |
| + if len(w.violations) > 0 { |
| + return |
| + } |
| + before := w.claim.Ver |
| + if w.followRecord(w.claim) || w.claim.Ver != before { |
| + w.violate("INV-17 (witness): the commit's CAS was replayed after it committed (claim %d, now %d)", before, w.claim.Ver) |
| + return |
| + } |
| + parks := 0 |
| + for _, o := range w.claim.Obl { |
| + if o.Kind == "park-superseded" && o.Region == src.Region { |
| + parks++ |
| + } |
| + } |
| + if parks != 1 { |
| + w.violate("INV-17 (witness): %d park-superseded obligations for the source region after the replay", parks) |
| + return |
| + } |
| + w.finish(t) |
| +} |
| + |
| +// wProbeWindowAt (R12-2): the landing probe's environment is ready exactly |
| +// at the deadline. Under the rule the attempt fails before the start and |
| +// the next admission's probe is accepted; without the check before the |
| +// start, the expired attempt starts and is accepted (INV-19). |
| +func wProbeWindowAt(t *testing.T, w *world) { |
| + w.probeWindow(t, probeStartWindow) |
| + if len(w.violations) > 0 { |
| + return |
| + } |
| + w.finish(t) |
| +} |
| + |
| +// probeWindow runs a landing whose target's launch environment is ready k |
| +// steps after the probe attempt's app stage first runs, and reports how |
| +// the first attempt ended. The knob is released once the first attempt |
| +// has been counted, so the next attempt proceeds at once. |
| +func (w *world) probeWindow(t *testing.T, k int) (accepted bool) { |
| + src, tgt := w.boxes[0], w.boxes[1] |
| + w.serve(src, 1, app0) |
| + w.wake(src) |
| + tgt.envUnreadyFor = k |
| + w.moveTo(tgt.Region) |
| + id := w.claim.Op.ID |
| + w.reach(t, 800, "landing probed", func() bool { |
| + c := w.claim |
| + if c.Op.ID == id && c.Op.ProbeTries > 0 { |
| + tgt.envUnreadyFor = 0 |
| + } |
| + return len(w.violations) > 0 || c.Op.ID != id || c.Op.Kind == "landing" && c.Op.LandPhase == "probed" && hasMain(tgt) |
| + }, w.act(src, tgt), w.recoveryPass) |
| + if w.claim.Op.ID != id { |
| + t.Fatalf("witness: the move %s ended before its probe: %s", id, w.state()) |
| + } |
| + return w.claim.Op.ProbeTries == 0 |
| +} |
| + |
| +// TestProbeWindow (R12-2) walks the boundary: readiness k steps after the |
| +// attempt's first app stage, for k just before, at and after the window. |
| +func TestProbeWindow(t *testing.T) { |
| + for _, k := range []int{probeStartWindow - 1, probeStartWindow, probeStartWindow + 1} { |
| + w := newWitness() |
| + accepted := w.probeWindow(t, k) |
| + if len(w.violations) > 0 { |
| + t.Fatalf("k=%d: %s", k, w.violations[0]) |
| + } |
| + p := w.boxes[1].lastProbe |
| + tries := w.claim.Op.ProbeTries |
| + beforeStart, atEnv := w.stats["probe attempt failed: deadline before the start"], w.stats["probe attempt failed: environment"] |
| + switch { |
| + case k < probeStartWindow && !accepted: |
| + t.Errorf("k=%d: the attempt within the window was not accepted (tries %d)", k, tries) |
| + case k < probeStartWindow && p.readyAt-p.startedAt != k: |
| + t.Errorf("k=%d: the accepted attempt answered %d steps after its first start", k, p.readyAt-p.startedAt) |
| + case k >= probeStartWindow && accepted: |
| + t.Errorf("k=%d: an attempt at or beyond the deadline was accepted", k) |
| + case k == probeStartWindow && beforeStart != 1: |
| + // ready exactly at the deadline: the check before the start |
| + t.Errorf("k=%d: the deadline check before the start did not fail the attempt (stats %v)", k, w.stats) |
| + case k > probeStartWindow && atEnv != 1: |
| + // still unready at the deadline: the attempt fails there |
| + t.Errorf("k=%d: the deadline did not fail the attempt while the environment was unready (stats %v)", k, w.stats) |
| + case k >= probeStartWindow && tries != 1: |
| + t.Errorf("k=%d: %d probe tries counted, want 1", k, tries) |
| + } |
| + w.finish(t) |
| + if len(w.violations) > 0 { |
| + t.Fatalf("k=%d: %s", k, w.violations[0]) |
| + } |
| + t.Logf("k=%d: accepted=%v tries=%d probe start %d ready %d (failed before the start %d, at the deadline unready %d)", k, accepted, tries, p.startedAt, p.readyAt, beforeStart, atEnv) |
| + } |
| +} |
diff --git a/internal/sim/hostlife/world_test.go b/internal/sim/hostlife/world_test.go| index fdea52508..0b10aa0a8 100644 |
| --- a/internal/sim/hostlife/world_test.go |
| +++ b/internal/sim/hostlife/world_test.go |
| @@ -321,11 +321,12 @@ func (d *localDB) clone() *localDB { |
| } |
| type proc struct { |
| - Main bool |
| - Strict bool // spawned into the host cgroup by strict placement |
| - Inc int |
| - Gen string |
| - Box int |
| + Main bool |
| + Strict bool // spawned into the host cgroup by strict placement |
| + Inc int |
| + Gen string |
| + Session int // the writer session the process was started under: what its acknowledgements carry (rev 7.13, R12-1) |
| + Box int |
| } |
| type row struct { |
| @@ -376,6 +377,11 @@ type box struct { |
| // retried by the same agent process; the session is the agent's, and a |
| // new agent process is a new session (claim rev 6.10) |
| open *openState |
| + // lastProbe is the last probe attempt's timing on this box (INV-19); |
| + // envUnreadyFor is a witness knob holding the launch environment |
| + // unready for that many steps after an attempt's app stage first runs |
| + lastProbe probeTiming |
| + envUnreadyFor int |
| // the retry policy for failed app starts within a session (rev 7.11 |
| // §7.14): consecutive failures, the earliest next attempt, and the |
| // host marked failed once the limit is reached (no new sessions until |
| @@ -652,6 +658,11 @@ type admissionRecord struct { |
| // src_covered). The entry always names it |
| Coverage string |
| Covered bool // this cold admission's predecessor has had its park-generation chore queued by a PublishGeneration (claim rev 6.12) |
| + // Region is where this writer's generation keeps its objects; |
| + // PredRegion where the predecessor's are, -1 when it holds none |
| + // anywhere (claim rev 6.14 §6.4a item 1: region, predecessor_region) |
| + Region int |
| + PredRegion int |
| // LostSrc (rev 7.11): a rollback's source re-admitted from its own |
| // generation after the target was declared lost while the seal was the |
| // one holder of the source's writes beyond its replica (src_covered |
| @@ -679,9 +690,8 @@ type openState struct { |
| Mode string |
| Prepared bool |
| Probe bool |
| - Source string // the generation the restore reads |
| - Dead []string // what the new marker retires: the predecessor and, behind a lagging marker, every empty generation of the unfinished admissions between (claim rev 6.10) |
| - RemoteMax int // the certificate's max_txid a warm restore must reach |
| + Source string // the generation the restore reads |
| + RemoteMax int // the certificate's max_txid a warm restore must reach |
| DB *localDB |
| stage string // restore, app, first, marker, anchor, open |
| req *request |
| @@ -690,6 +700,12 @@ type openState struct { |
| startedAt int // when the app stage first ran: a probe attempt's readiness window runs from here (rev 7.12 §7.7) |
| } |
| +// probeTiming is what INV-19 reads: when a probe attempt's app stage first |
| +// ran and when its app answered readiness (rev 7.13, R12-2) |
| +type probeTiming struct { |
| + startedAt, readyAt int |
| +} |
| + |
| // writesLost is claim rev 6.9's writes_lost record: the writer whose |
| // acknowledged, unuploaded writes a cold admission leaves behind, named by |
| // holder.writer_box, never inferred from op.exec (R9-2). The box alerts. |
| @@ -876,12 +892,14 @@ type record struct { |
| // ---------- the world ---------- |
| type ack struct { |
| - W int |
| - Inc int |
| - Box int |
| - At int |
| - Kind string // "write" or "timer" |
| - Exempt bool // lost under a declared loss (M16) or past the last checkpoint of a lost disk |
| + W int |
| + Inc int |
| + Box int |
| + 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 |
| + Gen string // the generation that session wrote |
| + At int |
| + Kind string // "write" or "timer" |
| + Exempt bool // lost under a declared loss (M16) or past the last checkpoint of a lost disk |
| } |
| // intner is what the model draws from: the seed's *rand.Rand in the random |