amadan
sim: a relocation ends as 1b-next builds it (probe stop, completion pass, barrier, N6), a delayed source catches up its row hold, and the C1/C11 fallbacks are today's behaviour
L18 joint round findings 2 to 4 (and finding 3 at the coordinator's request, ruling 85 / 1b-next a092ddc2). Finding 2: at probed the target stops its probe session under an owned activator fence with root's receipt and journals the stop (ruling 49, ruling 75, bounded by ruling 67); the serving CAS requires it and records completed_relocation; the completion pass on that box discharges (C10), releases the hold, lifts its own fence and marks last (rulings 66, 80), found from the claim and run with region HA off too (ruling 82); the first serving wake hands over from the probe's receipt (N6); every start from serving waits for the mark unless the box is lost or a failover's cited fenced source (ruling 77). Rev 7.20's settle window and the opened phase are gone. INV-31 and INV-32 are the new oracles. Finding 3: the release no longer holds the source's row (root's admission fence stands in, ruling 28); reconcile holds it while relocating (reloc-row-cases) and, after the completion, by the catch-up hold; INV-33 at reconcile. Finding 4: claimC1 and claimC11 are the switches for claim asks C1 and C11, false today: a failed target cannot release in probe-failed and is stuck at its deadline (the operator stops it), and a later cold attempt after P's opening is probe-failed before it is counted. Tests and witnesses of the post-C1/C11 paths set the switch. The model found a gap in the built code (seed 2224 / 3,000): a completion box terminated before its discharge while a purge holds admission closed blocks both the purge (barrier) and the failover (admission); the operator's declare-lost stands in. Eleven new region HA rules. One-box COUNTERS and traces unchanged.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
14 files changed,
+664
−64
internal/sim/hostlife/background_test.go+7 −1internal/sim/hostlife/console_test.go+12 −4internal/sim/hostlife/ltx_test.go+2 −1internal/sim/hostlife/moves_test.go+17 −3internal/sim/hostlife/protocol_test.go+11 −1internal/sim/hostlife/regionha_cases_test.go+2 −0internal/sim/hostlife/regionha_completion_test.go+447 −0internal/sim/hostlife/regionha_round1_test.go+2 −1internal/sim/hostlife/regionha_test.go+54 −36internal/sim/hostlife/regionha_witness_test.go+36 −12internal/sim/hostlife/rules_test.go+12 −0internal/sim/hostlife/sim_test.go+4 −0internal/sim/hostlife/witness_test.go+2 −2internal/sim/hostlife/world_test.go+56 −3
diff --git a/internal/sim/hostlife/background_test.go b/internal/sim/hostlife/background_test.go| index 91b0da4ae..6db74e13f 100644 |
| --- a/internal/sim/hostlife/background_test.go |
| +++ b/internal/sim/hostlife/background_test.go |
| @@ -91,6 +91,9 @@ func (w *world) wake(b *box) { |
| if !ok || !w.admits(b, c, "") { |
| return |
| } |
| + if !w.completedHandover(b, c) { |
| + return // N6: the first serving wake after a completion hands over from the probe's receipt |
| + } |
| if b.DB == nil && on("quiet-before-ack") && w.now < c.Quiet[b.Region] { |
| return // a first install into this region waits out quiet_after (claim §6.2a) |
| } |
| @@ -220,7 +223,7 @@ func (w *world) reconcileClaimed(b *box, c *claim) { |
| switch c.Op.Kind { |
| case "serving", "creating", "pushing": |
| if c.Op.Exec == b.ID { |
| - if b.Row != nil && b.Row.Status != "ready" && c.Op.Kind == "serving" && on("stale-hold-release") { |
| + if b.Row != nil && b.Row.Status != "ready" && c.Op.Kind == "serving" && on("stale-hold-release") && !w.completionHolds(c, b) { |
| // a hold whose operation has ended (the claim is serving here) |
| b.Row.Status, b.Row.HoldOp = "ready", "" |
| } |
| @@ -228,6 +231,9 @@ func (w *world) reconcileClaimed(b *box, c *claim) { |
| b.Row = &row{Inc: h.Inc, App: h.App, Status: "ready"} |
| w.initRecord(b, c) // the local record from holder.stamp, on this fresh read (claim rev 6.5 §6.4) |
| } |
| + } else if w.catchUpHold(b, c) { |
| + // a delayed source's row, held for the completed op until its |
| + // park-local retires it (finding 3, ruling 85) |
| } else if b.Row != nil && !(on("participant-rows") && w.ownsLocalObligation(c, b)) { |
| w.retireRow(b) |
| } |
diff --git a/internal/sim/hostlife/console_test.go b/internal/sim/hostlife/console_test.go| index 861a4e3ed..1e70a7126 100644 |
| --- a/internal/sim/hostlife/console_test.go |
| +++ b/internal/sim/hostlife/console_test.go |
| @@ -375,6 +375,9 @@ func (w *world) userDelete() { |
| recVer = w.rec.Ver |
| } |
| if w.cas(c, func(n *claim) bool { |
| + if w.completionBarrier(n, -1) { |
| + return false // StartGuard's completion barrier (ruling 77) |
| + } |
| n.Op = opState{Kind: "deleting", ID: id, Exec: -1, ReqAt: w.now, RecVer: recVer} // intent: the record's ETag (claim §5.2 step 1) |
| return true |
| }) { |
| @@ -450,7 +453,7 @@ func (w *world) moveTo(r int) { |
| } |
| id := w.newID("mv") |
| if w.cas(c, func(n *claim) bool { |
| - if n.Op.Kind != "serving" { |
| + if n.Op.Kind != "serving" || w.completionBarrier(n, -1) { |
| return false |
| } |
| n.Op = opState{Kind: "moving", ID: id, Phase: "leases", Exec: src.ID, Parts: []int{src.ID, tgt.ID}, |
| @@ -480,7 +483,7 @@ func (w *world) userPush() { |
| } |
| id := w.newID("push") |
| if w.cas(c, func(n *claim) bool { |
| - if n.Op.Kind != "serving" { |
| + if n.Op.Kind != "serving" || w.completionBarrier(n, -1) { |
| return false |
| } |
| 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} |
| @@ -737,7 +740,7 @@ func (w *world) purgeSteps(p *consolePlan) bool { |
| } |
| id := w.newID("pg") |
| return w.cas(c, func(n *claim) bool { |
| - if n.Op.Kind != "serving" { |
| + if n.Op.Kind != "serving" || w.completionBarrier(n, -1) { |
| return false |
| } |
| n.Op = opState{Kind: "purging", ID: id, Exec: -1, ReqAt: w.now} |
| @@ -1245,6 +1248,9 @@ func (w *world) operator() { |
| return |
| } |
| } |
| + if w.declareDeadCompletionBox(c) { |
| + return |
| + } |
| // a stuck relocation (§5.8): carlos ops host resolve (model ruling 13; |
| // the spec names the command and leaves its effect open). Nothing |
| // moves away from a live box without its stop evidence: |
| @@ -1263,7 +1269,9 @@ func (w *world) operator() { |
| if dead != nil && !dead.Destroyed { |
| dead = nil |
| } |
| - if ex := w.boxByID(op.Exec); ex != nil && !ex.Destroyed && op.Phase == "probe-failed" && !released && !contains(c.Lost, ex.ID) && on("reloc-release-needs-flush") && w.releaseUnrecoverable(ex, c) { |
| + 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)) { |
| + // with claim ask C1 open no failed target can release at all |
| + // (finding 4), so its release is unrecoverable by construction |
| // a live target that cannot release (its replicator and its |
| // files are gone and nothing recorded a flush, rev 9): no |
| // release will ever come, so the operator stops the box, and |
diff --git a/internal/sim/hostlife/ltx_test.go b/internal/sim/hostlife/ltx_test.go| index 0bd85c0f1..cd2e01a8f 100644 |
| --- a/internal/sim/hostlife/ltx_test.go |
| +++ b/internal/sim/hostlife/ltx_test.go |
| @@ -410,7 +410,8 @@ func (w *world) closeStep(b *box) { |
| // rollback's source was admitted cold at every wake and the rollback |
| // never released) |
| c := w.claim |
| - inside := c != nil && (c.Op.Kind == "serving" || c.Op.Kind == "moving" || c.Op.Kind == "landing" || c.Op.Kind == "restoring" || c.Op.Kind == "reverting") |
| + inside := c != nil && (c.Op.Kind == "serving" || c.Op.Kind == "moving" || c.Op.Kind == "landing" || c.Op.Kind == "restoring" || c.Op.Kind == "reverting" || |
| + c.Op.Kind == "relocating" && c.Op.Phase == "probed") // a relocation's probe stop drains its session (L18 finding 2) |
| if c == nil || c.Holder == nil || !inside || c.Op.Exec != b.ID || c.Holder.Inc != db.Inc || db.Gen != c.Holder.Gen { |
| // a push, a move's cut, a delete or a purge is taking this writer |
| // over: its generation is being replaced or parked, and a |
diff --git a/internal/sim/hostlife/moves_test.go b/internal/sim/hostlife/moves_test.go| index 9bf505a3e..56ae4313f 100644 |
| --- a/internal/sim/hostlife/moves_test.go |
| +++ b/internal/sim/hostlife/moves_test.go |
| @@ -203,6 +203,7 @@ func (w *world) role(b *box, c *claim) { |
| } |
| if w.localPark(b, inc) { // the quarantine retires the installation |
| b.Row = nil |
| + b.owedDischarge = "" // a lost box's participation binds nothing (ruling 77) |
| } |
| } |
| } |
| @@ -248,6 +249,8 @@ func (w *world) role(b *box, c *claim) { |
| } |
| case "relocating": |
| w.relocate(b, c) |
| + case "serving": |
| + w.completionPass(b, c) // a relocation completed on this box and not yet marked (ruling 80) |
| } |
| } |
| @@ -300,8 +303,8 @@ func (w *world) convertToRelocating(c *claim, src *box) { |
| // regionha_test.go. A stuck operation waits for the operator. |
| func (w *world) relocate(b *box, c *claim) { |
| op := c.Op |
| - if b.Region != op.SrcRegion || b.Destroyed || contains(c.Lost, b.ID) || !b.Enrolled || op.Stuck != "" { |
| - return |
| + if b.Region != op.SrcRegion || b.Destroyed || contains(c.Lost, b.ID) || !b.Enrolled || op.Stuck != "" || w.haOff { |
| + return // with region HA off no relocation pass runs, only the completion pass (ruling 82) |
| } |
| if b.fencePending && on("reloc-fence-pending-blocks") { |
| // Worker.Step returned w.replace(...) before its phase switch (rev |
| @@ -330,7 +333,7 @@ func (w *world) relocate(b *box, c *claim) { |
| w.relocProbing(b, c) |
| case "probe-failed": |
| w.relocProbeFailed(b, c) |
| - case "probed", "opened": |
| + case "probed": |
| w.relocSettle(b, c) |
| } |
| } |
| @@ -1393,6 +1396,9 @@ func (w *world) release(c *claim, execBox int) { |
| if !sameOp(n.Op.ID, op.ID) { |
| return false |
| } |
| + if op.Kind == "relocating" && (n.Op.Kind != "relocating" || n.Op.Phase != op.Phase || n.Op.Exec != execBox) { |
| + return false // CompleteRelocation's requireRelocation (L18 finding 2) |
| + } |
| // holder.admissions survives the release by living in the holder |
| // (claim rev 6.12): an admission whose start is unfinished at the |
| // release stays explained (seed 1052 / 30,000) |
| @@ -1400,9 +1406,17 @@ func (w *world) release(c *claim, execBox int) { |
| w.relocationLeftovers(n, op) // the abandoned installations' park-local chores (claim §4) |
| } |
| n.Op = opState{Kind: "serving", Exec: execBox, Parts: []int{execBox}} |
| + if op.Kind == "relocating" { |
| + // completed_relocation (ruling 56): the box and the probe's |
| + // session, unmarked until the completion pass discharges it |
| + n.Op.Completed = &completedEntry{Op: op.ID, Box: execBox, Session: n.Holder.Session} |
| + } |
| return true |
| }) { |
| w.logf("released %s to serving on box %d", op.ID, execBox) |
| + if b := w.boxByID(execBox); b != nil && op.Kind == "relocating" { |
| + b.owedDischarge = op.ID // ground truth for INV-31 |
| + } |
| if moveClose(op) && (w.rec == nil || w.rec.LastMove != op.ID || w.rec.MoveID == op.ID) { |
| // K8 as rev 7.23 amends it: never a serving claim over a live |
| // move. Judged only for a release CAS that succeeded: one the |
diff --git a/internal/sim/hostlife/protocol_test.go b/internal/sim/hostlife/protocol_test.go| index 4c9ece1e0..c8a803f37 100644 |
| --- a/internal/sim/hostlife/protocol_test.go |
| +++ b/internal/sim/hostlife/protocol_test.go |
| @@ -382,6 +382,16 @@ func (w *world) spawn(b *box, c *claim, want string, probe bool) bool { |
| } |
| } |
| } else { |
| + if b.actFence != "" { |
| + // the activator's fence on the host (a probe stop's, ruling 75) |
| + // refuses every start until its owner lifts it |
| + w.stats["start refused: the activator's fence"]++ |
| + return false |
| + } |
| + if b.foreignFence != "" { |
| + w.violate("INV-32: box %d started the host while %s's activator fence, which its owner never lifted, closed it", b.ID, b.foreignFence) |
| + return false |
| + } |
| bg, binc := w.bucketGen(b, loc) |
| if on("start-check") && bg != "" && binc != h.Inc { |
| w.logf("box %d start check refused: generation.json %q inc %d, claim inc %d", b.ID, bg, binc, h.Inc) |
| @@ -1446,7 +1456,7 @@ func (w *world) admits(b *box, c *claim, probe string) bool { |
| return probe == op.ID && role(op.Tgt) && op.Phase == "probing" |
| } |
| if role(op.Src) && (op.Phase == "starting" || op.Phase == "releasing" && op.Release == nil) { |
| - return b.Row.Status == "ready" // the source serves until its admission fence closes (§5.3, §5.8) |
| + return b.Row.Status == "ready" && b.relFence != op.ID // the source serves until its admission fence closes (§5.3, §5.8) |
| } |
| return role(op.Tgt) && op.Phase == "opened" && b.Row.Status == "ready" |
| } |
diff --git a/internal/sim/hostlife/regionha_cases_test.go b/internal/sim/hostlife/regionha_cases_test.go| index fb50f3d5e..e41ba1b01 100644 |
| --- a/internal/sim/hostlife/regionha_cases_test.go |
| +++ b/internal/sim/hostlife/regionha_cases_test.go |
| @@ -393,6 +393,7 @@ func TestEmptyDatabaseDrain(t *testing.T) { |
| // failed target's own release: nothing is declared. |
| func TestReleasedThenFailedProbe(t *testing.T) { |
| w := twoBoxWitness() |
| + w.claimC1 = true // the failed target's release (claim ask C1, finding 4) |
| from, to := w.boxes[0], w.boxes[3] |
| to.FailApp = true |
| w.serve(from, 1, app0) |
| @@ -632,6 +633,7 @@ func TestFailoverBeforeTheFirstManifest(t *testing.T) { |
| // operation waits for ever (INV-3) and this test fails. |
| func TestProbeFailedInATwoBoxRegion(t *testing.T) { |
| w := twoBoxWitness() |
| + w.claimC1 = true // the failed target's release (claim ask C1, finding 4) |
| from, to := w.boxes[0], w.boxes[3] |
| to.FailApp = true |
| w.serve(from, 1, app0) |
diff --git a/internal/sim/hostlife/regionha_completion_test.go b/internal/sim/hostlife/regionha_completion_test.go| new file mode 100644 |
| index 000000000..d8d629ccd |
| --- /dev/null |
| +++ b/internal/sim/hostlife/regionha_completion_test.go |
| @@ -0,0 +1,447 @@ |
| +package hostlife |
| + |
| +import ( |
| + "fmt" |
| + "strings" |
| +) |
| + |
| +// ---------- the built completion protocol (L18 joint round, findings 2 to 4) ---------- |
| +// |
| +// Finding 2: a relocation does not end with the probe still running. The |
| +// built sequence (1b-next 596fa8b1; hostrelocate Participant and Worker, |
| +// host relocationStopProbe and relocationReleaseHold, hostclaim |
| +// CompleteRelocation, completionBarrier) is: |
| +// |
| +// 1. probe stop (ruling 49): with the probe journaled (the model's |
| +// probed), the target persists the owner of the fence it will install |
| +// (probe-fence.json), installs that owned activator fence on an |
| +// unfenced host or meets its own (ruling 75; any other owner's fence |
| +// refuses with nothing stopped), stops the session's whole tree with |
| +// root's receipt and journals the stop (RecordProbeStop). Ruling 67 |
| +// bounds it: no stop ReleaseDeadline after the probe passed is stuck; |
| +// 2. the worker's serving CAS (CompleteRelocation) requires that stop and |
| +// records completed_relocation on the serving op; |
| +// 3. the completion pass on the box it completed on (relocationReleaseHold, |
| +// rulings 66, 76, 80): C10's discharge of the participation, then the |
| +// row's hold released, then the owned fence lifted, then the mark |
| +// (MarkCompletedDischarged) last; found from the claim record, never |
| +// from the row, so a failure at any step is retried; run whenever claim |
| +// mode is on, region HA on or off (ruling 82); |
| +// 4. the first serving wake after it is a separate admission that hands |
| +// over from the probe's receipt (N6), never main's stop; |
| +// 5. until the mark, every start from serving refuses (ruling 77), except |
| +// with the completion box on lost or cited as a failover's fenced |
| +// source. |
| +// |
| +// Finding 3 (ruling 85, 1b-next a092ddc2): the source's row hold is |
| +// reconcile's, not the release's (ruling 28 fences admission at the |
| +// release's end), so a source whose reconcile runs only after the |
| +// completion catches up: serving on another box, a completed relocation |
| +// that did not complete here, and a park-local this box owes for exactly |
| +// that op hold the row until the park-local retires it. |
| +// |
| +// Finding 4: today's fallbacks for claim asks C1 and C11. A failed target |
| +// cannot release in probe-failed (QueueRelocationRelease needs the |
| +// source's releasing; no failed-target obligation), so it reaches stuck at |
| +// the release deadline; and after P's opening a later cold probe attempt |
| +// is refused before it is counted (root pins every relocating launch to |
| +// install_stamp), which is probe-failed. world.claimC1 and claimC11 are |
| +// the switches that flip them when the asks land. |
| + |
| +// probeOwner is the owner a probe stop persists and installs its fence |
| +// under: the operation and the probe's session. |
| +func probeOwner(op string, session int) string { return fmt.Sprintf("probe:%s/%d", op, session) } |
| + |
| +// probeKey is the stop evidence key of op's probe stop: root's completed |
| +// writer-session receipt in the box's guard journal (durable). |
| +func probeKey(op string) string { return "probe:" + op } |
| + |
| +// relocStopProbe is relocationStopProbe and RecordProbeStop (ruling 49, |
| +// ruling 75): op.exec stops its passed probe's session while the op is |
| +// still relocating. The fence's owner is persisted first; the owned fence |
| +// is installed only on an unfenced host or met again (rule |
| +// reloc-probe-fence-owner; the mutation installs over any fence); then |
| +// the whole tree is stopped and the session's database closed cleanly, and |
| +// with root's receipt the stop is journaled. |
| +func (w *world) relocStopProbe(b *box, c *claim) { |
| + op, h := c.Op, c.Holder |
| + if h == nil || h.WriterBox != b.ID || op.Exec != b.ID { |
| + return |
| + } |
| + owner := probeOwner(op.ID, h.Session) |
| + if strings.HasPrefix(b.probeFence, probeKey(op.ID)+"/") && b.probeFence != owner { |
| + w.stats["probe stop: the persisted fence owner names another session"]++ |
| + return |
| + } |
| + b.probeFence = owner // probe-fence.json, persisted before anything is asked of the activator |
| + if b.actFence != "" && b.actFence != owner { |
| + if on("reloc-probe-fence-owner") { |
| + // ErrFenceHeld: nothing stopped, nothing asked of root |
| + w.stats["probe stop: another owner's fence, nothing stopped"]++ |
| + w.logf("relocation %s: box %d's probe stop meets %s's fence; nothing is stopped", op.ID, b.ID, b.actFence) |
| + return |
| + } |
| + w.stats["probe stop: another owner's fence replaced (mutation)"]++ |
| + } |
| + b.actFence = owner |
| + if !w.evidence(b, probeKey(op.ID)) { |
| + w.stats["probe stop: a process survives"]++ |
| + return |
| + } |
| + // main's writer-session stop drains the producers: the session's own |
| + // replicator closes cleanly (claim §6.4a), so the next serving wake |
| + // continues the generation; a replicator that died with its agent |
| + // certifies nothing, and that wake is cold and declares |
| + if db := b.DB; db != nil && db.Inc == h.Inc && db.Gen == h.Gen && db.Epoch == b.Epoch && db.Session == h.Session && !b.mem["close:"+owner] { |
| + b.mem["close:"+owner] = true |
| + db.Closing = true |
| + } |
| + w.closeStep(b) |
| + if b.DB != nil && b.DB.Closing { |
| + w.stats["probe stop: waits for the clean close"]++ |
| + return |
| + } |
| + if w.cas(c, func(n *claim) bool { |
| + ok := sameOp(n.Op.ID, op.ID) && n.Op.Kind == "relocating" && n.Op.Phase == "probed" && n.Op.Exec == b.ID && n.Holder.Session == h.Session && n.Op.ProbeStop == nil |
| + if ok { |
| + n.Op.ProbeStop = &probeStopEntry{Box: b.ID, Session: h.Session} |
| + } |
| + return ok |
| + }) { |
| + w.stats["probe stop journaled"]++ |
| + w.logf("relocation %s: box %d stopped its probe session %d with root's receipt", op.ID, b.ID, h.Session) |
| + } |
| +} |
| + |
| +// relocComplete is the worker's CompleteRelocation: the serving CAS |
| +// requires the journaled stop of exactly the probe's session (rule |
| +// reloc-probe-stop; the mutation completes over the running probe, which |
| +// strands its session across the kind change: INV-31). |
| +func (w *world) relocComplete(c *claim) { |
| + op := c.Op |
| + if on("reloc-probe-stop") && (op.ProbeStop == nil || op.ProbeStop.Box != op.Exec || op.ProbeStop.Session != c.Holder.Session) { |
| + return |
| + } |
| + w.release(c, op.Exec) |
| +} |
| + |
| +// completionPass is relocationReleaseHold for every serving claim whose |
| +// completion record names this box and is not marked (ruling 80). Each |
| +// step is idempotent; a failure or a crash leaves the record unmarked and |
| +// the next pass resumes. Rules: reloc-completion-claim-mode (ruling 82), |
| +// reloc-completion-from-claim (ruling 80's finding), reloc-completion- |
| +// discharge-first (ruling 66), reloc-completion-mark-last (ruling 80) and |
| +// reloc-probe-fence-owner (the owned lift). |
| +func (w *world) completionPass(b *box, c *claim) { |
| + d := c.Op.Completed |
| + if c.Op.Kind != "serving" || d == nil || d.Discharged || d.Box != b.ID || c.Holder == nil || c.Op.Exec != b.ID || c.Holder.WriterBox != b.ID { |
| + return |
| + } |
| + if w.haOff && !on("reloc-completion-claim-mode") { |
| + return // the mutation: the pass runs only with region HA on |
| + } |
| + if !on("reloc-completion-from-claim") && (b.Row == nil || b.Row.HoldOp != d.Op) { |
| + return // the mutation: the completion is found from the row's hold, which a finished release no longer shows |
| + } |
| + if b.Row == nil { |
| + w.stats["completion: no row, refused"]++ |
| + return |
| + } |
| + if b.Row.HoldOp != "" && b.Row.HoldOp != d.Op { |
| + w.stats["completion: the row is held by another op, refused"]++ |
| + return |
| + } |
| + owner := probeOwner(d.Op, d.Session) |
| + if b.probeFence != owner { |
| + w.stats["completion: no probe-fence owner, refused"]++ |
| + return |
| + } |
| + held := b.Row.HoldOp == d.Op |
| + if !on("reloc-completion-mark-last") && !w.markCompleted(b, c) { |
| + return // the mutation: the mark first |
| + } |
| + releaseHold := func() { |
| + if b.Row != nil && b.Row.HoldOp == d.Op { |
| + b.Row.Status, b.Row.HoldOp = "ready", "" |
| + w.logf("box %d: completion of %s released the row's hold", b.ID, d.Op) |
| + } |
| + } |
| + lift := func() { |
| + if b.actFence == owner || !on("reloc-probe-fence-owner") { |
| + b.actFence = "" // LiftFenceAs: only the owner's fence (the mutation lifts any) |
| + } |
| + } |
| + if !on("reloc-completion-discharge-first") { |
| + // the mutation: the hold released and the fence lifted before the |
| + // discharge, so a serving admission can move the holder first |
| + releaseHold() |
| + lift() |
| + if !w.dischargeCompleted(b, c, false) { |
| + return |
| + } |
| + } else { |
| + if held && c.Holder.Session != d.Session { |
| + w.stats["completion: the holder is not the stopped probe session, refused"]++ |
| + return |
| + } |
| + if !w.dischargeCompleted(b, c, held) { |
| + return |
| + } |
| + if w.crashed(b, "discharge") { |
| + return |
| + } |
| + releaseHold() |
| + if w.crashed(b, "release") { |
| + return |
| + } |
| + lift() |
| + if w.crashed(b, "lift") { |
| + return |
| + } |
| + } |
| + if on("reloc-completion-mark-last") { |
| + w.markCompleted(b, c) |
| + } |
| +} |
| + |
| +// crashed is a witness's agent crash after the named step of the |
| +// completion pass (a restart: the activator's fences are gone). |
| +func (w *world) crashed(b *box, step string) bool { |
| + if b.crashAfter != step { |
| + return false |
| + } |
| + b.crashAfter = "" |
| + b.forget() |
| + w.logf("witness: box %d's agent crashed after the completion's %s", b.ID, step) |
| + return true |
| +} |
| + |
| +// dischargeCompleted is C10's discharge (completedRelocationDischarge, |
| +// DischargeCompleted): keyed by the persisted binding, it needs, while the |
| +// row is still held for the op, root's receipt for the stopped probe |
| +// session; it closes main's participation slot and clears the .hostexec |
| +// record (the model's execRecord). A replay after the hold's release finds |
| +// no slot, which is positive evidence. dischargeFails is a witness's |
| +// failing discharge. |
| +func (w *world) dischargeCompleted(b *box, c *claim, held bool) bool { |
| + d := c.Op.Completed |
| + if b.dischargeFails { |
| + w.stats["completion: discharge failed"]++ |
| + return false |
| + } |
| + if held && !b.StopEvidence[probeKey(d.Op)] { |
| + w.stats["completion: no receipt for the probe's stop, discharge refused"]++ |
| + return false |
| + } |
| + if b.execRecord == d.Op { |
| + b.execRecord, b.cleanupPending = "", false |
| + } |
| + if b.owedDischarge == d.Op { |
| + b.owedDischarge = "" |
| + w.stats["completion: participation discharged"]++ |
| + } |
| + return true |
| +} |
| + |
| +// markCompleted is MarkCompletedDischarged: the serving op's record is |
| +// marked, which lets any successor start. markFails is a witness's failed |
| +// mark (the CAS lost, or the store refused it). |
| +func (w *world) markCompleted(b *box, c *claim) bool { |
| + d := c.Op.Completed |
| + if b.markFails { |
| + b.markFails = false |
| + w.stats["completion: mark failed"]++ |
| + return false |
| + } |
| + if w.cas(c, func(n *claim) bool { |
| + x := n.Op.Completed |
| + ok := n.Op.Kind == "serving" && x != nil && x.Op == d.Op && !x.Discharged |
| + if ok { |
| + cp := *x |
| + cp.Discharged = true |
| + n.Op.Completed = &cp |
| + } |
| + return ok |
| + }) { |
| + w.stats["completion marked discharged"]++ |
| + w.logf("box %d: completion of %s marked discharged", b.ID, d.Op) |
| + return true |
| + } |
| + return false |
| +} |
| + |
| +// completionBarrier is completionBarrier (ruling 77; rule |
| +// reloc-completion-barrier): true refuses a start from serving while the |
| +// serving op's completed relocation is not marked, unless its box is on |
| +// lost or is the source the start cites as fenced (fenced, -1 none). |
| +func (w *world) completionBarrier(c *claim, fenced int) bool { |
| + d := c.Op.Completed |
| + if c.Op.Kind != "serving" || d == nil || d.Discharged || !on("reloc-completion-barrier") { |
| + return false |
| + } |
| + if contains(c.Lost, d.Box) || fenced >= 0 && fenced == d.Box { |
| + return false |
| + } |
| + w.stats["start refused: a completed relocation is not discharged"]++ |
| + return true |
| +} |
| + |
| +// completedHandover is N6 (wireCompletedHandover): the first serving wake |
| +// on the box a relocation completed on, while the holder is still the |
| +// stopped probe session, hands over from the probe's receipt and stops |
| +// nothing. It reports whether the wake may go on. The mutation of |
| +// reloc-completed-handover routes it to main's stop, which installs a |
| +// serving-shaped fence over the probe's and re-stops S, whose stop root |
| +// already completed under the probe's fence: the handover refuses for |
| +// good, and the fence is never the probe's to lift. |
| +func (w *world) completedHandover(b *box, c *claim) bool { |
| + d := c.Op.Completed |
| + if c.Op.Kind != "serving" || d == nil || d.Box != b.ID || c.Holder == nil || c.Holder.Session != d.Session || c.Holder.WriterBox != b.ID { |
| + return true // not the completed prior: main's path |
| + } |
| + if !on("reloc-completed-handover") { |
| + if b.actFence == "" || strings.HasPrefix(b.actFence, "probe:") { |
| + b.actFence = fmt.Sprintf("main:%d", d.Session) |
| + } |
| + w.stats["serving wake: main's stop of the completed prior refused (mutation)"]++ |
| + return false |
| + } |
| + if !b.StopEvidence[probeKey(d.Op)] { |
| + w.stats["serving wake: no receipt for the completed probe, refused"]++ |
| + return false // absence is never evidence |
| + } |
| + w.stats["serving wake: handed over from the probe's receipt"]++ |
| + return true |
| +} |
| + |
| +// completionHolds: the row's hold is the unmarked completion's own, which |
| +// only the completion pass releases, after the discharge (ruling 66); the |
| +// mutation of reloc-completion-discharge-first lets reconcile release it |
| +// as a stale hold. |
| +func (w *world) completionHolds(c *claim, b *box) bool { |
| + d := c.Op.Completed |
| + return d != nil && !d.Discharged && d.Box == b.ID && b.Row != nil && b.Row.HoldOp == d.Op && on("reloc-completion-discharge-first") |
| +} |
| + |
| +// catchUpHold is reconcile's completedHold (finding 3, ruling 85): with |
| +// region HA on, a box that is not the serving executor, not on lost, and |
| +// owes a park-local for exactly the serving op's completed relocation |
| +// (which completed elsewhere) holds its row for that op until the |
| +// park-local retires it. It reports whether the case applied. The |
| +// mutation drops the hold, and the row a delayed source's release left |
| +// ready stays ready (INV-33: the edge routes requests to a box that does |
| +// not serve). |
| +func (w *world) catchUpHold(b *box, c *claim) bool { |
| + d := c.Op.Completed |
| + if w.haOff || c.Op.Kind != "serving" || d == nil || d.Box == b.ID || c.Op.Exec == b.ID || contains(c.Lost, b.ID) || b.Row == nil { |
| + return false |
| + } |
| + owes := false |
| + for _, o := range c.Obl { |
| + if o.Kind == "park-local" && o.Box == b.ID && o.Op == d.Op { |
| + owes = true |
| + } |
| + } |
| + if !owes { |
| + return false |
| + } |
| + if b.Row.Status == "ready" && on("reloc-completed-catchup-hold") { |
| + b.Row.Status, b.Row.HoldOp = "relocating", d.Op |
| + w.stats["catch-up hold: a delayed source held its row"]++ |
| + w.logf("box %d: reconcile caught up: its row is held for completed relocation %s until its park-local", b.ID, d.Op) |
| + } |
| + if b.Row.Status == "ready" { |
| + w.violate("INV-33: box %d's reconcile left its row ready after relocation %s completed on box %d, while it owes that op's park-local (the edge routes requests to a box that does not serve)", b.ID, d.Op, d.Box) |
| + } |
| + return true |
| +} |
| + |
| +// checkCompletion is INV-31 (rulings 49, 66, 77): while a box has not |
| +// discharged its participation in a completed relocation, nothing of the |
| +// host runs on it (the stopped probe session stays the holder until C10 |
| +// discharges it, and a session the kind change stranded is never |
| +// discharged), and no operation names it as a participant (main's Prepare |
| +// answers ErrLost). A box on lost, or destroyed, holds nothing a |
| +// successor needs. |
| +func (w *world) checkCompletion() { |
| + c := w.claim |
| + if c != nil && c.Holder != nil && c.Op.Kind == "serving" { |
| + if d := c.Op.Completed; d != nil && !d.Discharged && c.Holder.Session != d.Session { |
| + if b := w.boxByID(d.Box); b != nil && b.owedDischarge == d.Op && !b.Destroyed && !contains(c.Lost, b.ID) { |
| + w.violate("INV-31: a writer was admitted (session %d, box %d) before box %d discharged its participation in completed relocation %s, whose holder must still be the stopped probe session %d (ruling 66)", c.Holder.Session, c.Holder.WriterBox, b.ID, d.Op, d.Session) |
| + return |
| + } |
| + } |
| + } |
| + for _, b := range w.boxes { |
| + if b.owedDischarge == "" || b.Destroyed || c != nil && contains(c.Lost, b.ID) { |
| + continue |
| + } |
| + if len(b.Procs) > 0 { |
| + w.violate("INV-31: the host runs on box %d before its participation in completed relocation %s was discharged (rulings 49, 66)", b.ID, b.owedDischarge) |
| + return |
| + } |
| + if c != nil && c.Op.Kind != "serving" && c.Op.Kind != "" && opNames(c.Op, b.ID) { |
| + w.violate("INV-31: %s %s names box %d before its participation in completed relocation %s was discharged (ruling 77: main's Prepare answers ErrLost)", c.Op.Kind, c.Op.ID, b.ID, b.owedDischarge) |
| + return |
| + } |
| + } |
| +} |
| + |
| +// opNames: op names box id as its executor or a participant, or as its |
| +// source or target in the kinds that set them. |
| +func opNames(op opState, id int) bool { |
| + if op.Exec == id || contains(op.Parts, id) { |
| + return true |
| + } |
| + switch op.Kind { |
| + case "moving", "landing", "restoring", "reverting", "pushing", "relocating": |
| + return op.Src == id || op.Tgt == id |
| + } |
| + return false |
| +} |
| + |
| +// c1Fallback: claim ask C1 is open, so a failed target has no release |
| +// obligation and its release in probe-failed is refused (rule |
| +// reloc-c1-failed-release-refused; the mutation releases as if C1 had |
| +// landed). |
| +func (w *world) c1Fallback() bool { return !w.claimC1 && on("reloc-c1-failed-release-refused") } |
| + |
| +// c11Fallback: claim ask C11 is open, so root launches no cold probe |
| +// attempt after P's opening (rule reloc-c11-later-attempt-refused; the |
| +// mutation counts and makes it as if C11 had landed). |
| +func (w *world) c11Fallback() bool { return !w.claimC11 && on("reloc-c11-later-attempt-refused") } |
| + |
| +// declareDeadCompletionBox is the operator's declare-lost (claim D2) of a |
| +// completion box terminated before its discharge, while a purge holds the |
| +// app's admission closed: the gap the model found in the built code (seed |
| +// 2224 / 3,000, two boxes). completionBarrier refuses the purge's |
| +// StartGuard, because the box is not on lost; the failover that would |
| +// cite its fence is refused by Admission.Register, because the purge |
| +// closed admission; so neither starts and nothing finishes the |
| +// completion. 1b-next has no automatic way out, so the model's operator |
| +// declares the box lost (the barrier's lost exemption), counted, and the |
| +// purge proceeds. It acts only in that shape. |
| +func (w *world) declareDeadCompletionBox(c *claim) bool { |
| + d := c.Op.Completed |
| + if c.Holder == nil || c.Op.Kind != "serving" || d == nil || d.Discharged || contains(c.Lost, d.Box) { |
| + return false |
| + } |
| + x := w.boxByID(d.Box) |
| + ad := w.admit[c.Holder.App] |
| + if x == nil || !x.Terminated || ad == nil || !ad.Closed { |
| + return false |
| + } |
| + if w.cas(c, func(n *claim) bool { |
| + if n.Op.Completed == nil || n.Op.Completed.Op != d.Op || n.Op.Completed.Discharged || contains(n.Lost, d.Box) { |
| + return false |
| + } |
| + n.Lost = addUniq(n.Lost, d.Box) |
| + return true |
| + }) { |
| + w.stats["operator declared a terminated completion box lost (purge and failover both refused)"]++ |
| + w.logf("operator declared box %d lost: its completion of %s blocks the purge, and the purge's closed admission blocks the failover", d.Box, d.Op) |
| + return true |
| + } |
| + return false |
| +} |
diff --git a/internal/sim/hostlife/regionha_round1_test.go b/internal/sim/hostlife/regionha_round1_test.go| index a7620b164..06bc07303 100644 |
| --- a/internal/sim/hostlife/regionha_round1_test.go |
| +++ b/internal/sim/hostlife/regionha_round1_test.go |
| @@ -107,7 +107,7 @@ func (w *world) liveIn(r int) int { return len(w.regionBoxes(r)) } |
| // group launched) is terminated. Two-box region: the drain's source or |
| // target is. |
| func TestL18TerminationAtEveryExactPhase(t *testing.T) { |
| - phases := []string{"starting", "releasing", "pinning", "installing", "installed", "probing", "probe-failed", "probed", "opened"} |
| + phases := []string{"starting", "releasing", "pinning", "installing", "installed", "probing", "probe-failed", "probed"} |
| for _, boxes := range []int{1, 2} { |
| for _, who := range []string{"source", "target"} { |
| for _, phase := range phases { |
| @@ -904,6 +904,7 @@ func TestReleaseReplaysTheRecordedFlush(t *testing.T) { |
| // stops once the operation is in probe-failed with box 3 op.exec and no |
| // release journaled. |
| func (w *world) probeFailedTarget(t *testing.T) (from, to *box) { |
| + w.claimC1 = true // these tests are of the failed target's release, which claim ask C1 makes possible (finding 4) |
| from, to = w.boxes[0], w.boxes[3] |
| to.FailApp = true |
| w.serve(from, 1, app0) |
diff --git a/internal/sim/hostlife/regionha_test.go b/internal/sim/hostlife/regionha_test.go| index 270735ccb..f53016f5a 100644 |
| --- a/internal/sim/hostlife/regionha_test.go |
| +++ b/internal/sim/hostlife/regionha_test.go |
| @@ -34,7 +34,7 @@ const ( |
| // drain could only wait for its release deadline; a failover relocates it. |
| func (w *world) userRelocate() { |
| c := w.claim |
| - if c == nil || c.Holder == nil || c.Op.Kind != "serving" { |
| + if c == nil || c.Holder == nil || c.Op.Kind != "serving" || w.haOff { |
| return |
| } |
| from := w.execBox(c) |
| @@ -90,6 +90,13 @@ func (w *world) relocationStartAllowed(c *claim, from, to *box) bool { |
| // relocationStartGuard is RelocationStartGuard(c, region, source, target, |
| // sourceFenced): a failover's fenced source's park-local does not block. |
| func (w *world) relocationStartGuard(c *claim, from, to *box, sourceFenced bool) bool { |
| + fenced := -1 |
| + if sourceFenced { |
| + fenced = from.ID |
| + } |
| + if w.completionBarrier(c, fenced) { |
| + return false // ruling 77, before the chores (RelocationStartGuard) |
| + } |
| if !on("reloc-start-guard") { |
| return true |
| } |
| @@ -144,9 +151,11 @@ func relocExcept(op opState, extra ...int) []int { |
| // reloc-release-needs-receipt, rev 11). |
| func (w *world) relocRelease(b *box, c *claim) *releaseEntry { |
| h := c.Holder |
| - if b.Row != nil && b.Row.Status == "ready" { |
| - w.holdRow(b, "relocating", c.Op.ID, c) |
| - } |
| + // root's admission fence for this release (ruling 28 puts it at the |
| + // release's end; the model closes admission at the stop, which is |
| + // earlier, and the row hold is reconcile's alone: reloc-row-cases while |
| + // relocating, the catch-up hold after a completion, finding 3) |
| + b.relFence = c.Op.ID |
| if !w.evidence(b, c.Op.ID) { |
| w.stats["release: a process survives the stop"]++ |
| return nil |
| @@ -888,6 +897,7 @@ func (w *world) handExec(n *claim, box int, phase, prepared string) { |
| n.Op.Receipt = nil |
| } |
| n.Op.Attempts = 0 |
| + n.Op.ProbeStop, n.Op.ProbePassedAt = nil, 0 |
| n.Op.InstalledOn = addUniq(n.Op.InstalledOn, box) |
| n.Boxes = addUniq(n.Boxes, box) |
| } |
| @@ -1192,7 +1202,7 @@ func (w *world) relocProbing(b *box, c *claim) { |
| probed := func(n *claim) bool { |
| ok := sameOp(n.Op.ID, op.ID) && n.Op.Phase == "probing" && n.Op.Exec == b.ID |
| if ok { |
| - n.Op.Phase = "probed" |
| + n.Op.Phase, n.Op.ProbePassedAt = "probed", w.now // RecordProbe's At (ruling 67's bound) |
| } |
| return ok |
| } |
| @@ -1212,6 +1222,15 @@ func (w *world) relocProbing(b *box, c *claim) { |
| // attempt this agent counted (tag) or made (tag+"+"); one made and |
| // ended, or none counted, is counted now |
| if on("reloc-probe-attempts") && b.attemptTag != tag { |
| + if preparedOpened(c) && w.c11Fallback() { |
| + // Preflight's ErrLaterAttemptUnlaunchable (ruling 58, until |
| + // claim ask C11): root pins every relocating launch to |
| + // install_stamp, so a cold attempt after P's opening is not |
| + // made; probe-failed now, before any attempt is counted |
| + w.stats["probe-failed: a later attempt root cannot launch (C11 open)"]++ |
| + w.cas(c, failed) |
| + return |
| + } |
| if op.Attempts >= probeTries { |
| w.stats["probe-failed: attempts"]++ |
| w.cas(c, failed) |
| @@ -1300,44 +1319,32 @@ func (w *world) relocProbeFailed(b *box, c *claim) { |
| }) |
| } |
| -// relocSettle is the settle window and the open (rev 7.20's steps, kept): |
| -// a probe that died in its window is restarted, cold, from its own |
| -// generation; then the row opens and the operation is released to |
| -// serving (CompleteRelocation), where the leftovers' park-local chores |
| -// are queued (release()). |
| +// relocSettle is the end of a relocation as 1b-next builds it (L18 joint |
| +// round finding 2; regionha_completion_test.go): at probed (1b-next's |
| +// probing with the probe journaled) op.exec stops the probe's session with |
| +// root's receipt (relocStopProbe, ruling 49), bounded by ruling 67 (no |
| +// stop ReleaseDeadline after the probe passed is stuck for an operator); |
| +// then any worker of the region makes the serving CAS (relocComplete, |
| +// CompleteRelocation), which records the completion. The row stays held: |
| +// the completion pass releases it after the discharge, and the first |
| +// serving wake is a separate admission (N6). Rev 7.20's settle window and |
| +// open are gone: a probe that dies after it passed is stopped all the same. |
| func (w *world) relocSettle(b *box, c *claim) { |
| op := c.Op |
| - if op.Exec != b.ID { |
| + if op.Phase != "probed" { |
| return |
| } |
| - switch op.Phase { |
| - case "probed": |
| - if b.open != nil { |
| + if op.ProbeStop == nil && on("reloc-probe-stop") { |
| + if w.now > op.ProbePassedAt+releaseDeadline { |
| + w.markStuck(c, fmt.Sprintf("box %d passed its probe but has no root stop receipt for session %d", op.Exec, c.Holder.Session)) |
| return |
| } |
| - if !hasMain(b) { |
| - w.stats["probe restarted"]++ |
| - w.cas(c, func(n *claim) bool { |
| - ok := sameOp(n.Op.ID, op.ID) && n.Op.Phase == "probed" |
| - if ok { |
| - n.Op.Phase = "probing" |
| - } |
| - return ok |
| - }) |
| - return |
| - } |
| - if w.openRow(b, op.ID) { |
| - w.cas(c, func(n *claim) bool { |
| - ok := sameOp(n.Op.ID, op.ID) && n.Op.Phase == "probed" |
| - if ok { |
| - n.Op.Phase = "opened" |
| - } |
| - return ok |
| - }) |
| + if b.ID == op.Exec { |
| + w.relocStopProbe(b, c) |
| } |
| - case "opened": |
| - w.release(c, b.ID) // outstanding disjoint parks do not block serving (claim rev 6.28 §4) |
| + return |
| } |
| + w.relocComplete(c) |
| } |
| // scopedCleanup is the relocation controller's scoped cleanup when its |
| @@ -1501,7 +1508,7 @@ func (w *world) regionHAOwnsLoss(b *box) bool { |
| // to (HA7) and is never fenced. The source's fence is consumed before the |
| // target's, as Worker.Step orders them. |
| func (w *world) fenceStep(b *box, c *claim) (changed, pending bool) { |
| - if c == nil || !b.Enrolled || contains(c.Lost, b.ID) { |
| + if c == nil || !b.Enrolled || contains(c.Lost, b.ID) || w.haOff { |
| return false, false |
| } |
| var cands []*box |
| @@ -2385,6 +2392,9 @@ func (w *world) finishParticipation(b *box, c *claim) { |
| if b.execRecord == "" || c == nil { |
| return |
| } |
| + if d := c.Op.Completed; c.Op.Kind == "serving" && d != nil && !d.Discharged && d.Box == b.ID && b.execRecord == d.Op { |
| + return // the completion box's participation is C10's to discharge (completionPass), first |
| + } |
| if c.Op.Kind == "relocating" && c.Op.ID == b.execRecord && contains(c.Op.Parts, b.ID) && !contains(c.Lost, b.ID) { |
| return // still a participant |
| } |
| @@ -2568,6 +2578,14 @@ func (w *world) preparedManifestHere(b *box, c *claim, gen string) bool { |
| func (w *world) relocJournalRelease(b *box, c *claim, pending bool) { |
| op := c.Op |
| phase := op.Phase |
| + if phase == "probe-failed" && w.c1Fallback() { |
| + // QueueRelocationRelease needs the source in releasing: with claim |
| + // ask C1 open there is no failed-target obligation, so nothing is |
| + // queued, stopped or journaled, and the release deadline makes the |
| + // operation stuck (finding 4) |
| + w.stats["release refused: no failed-target obligation (C1 open)"]++ |
| + return |
| + } |
| r := w.relocRelease(b, c) |
| if r == nil { |
| return |
diff --git a/internal/sim/hostlife/regionha_witness_test.go b/internal/sim/hostlife/regionha_witness_test.go| index 118dab54f..d84a6028b 100644 |
| --- a/internal/sim/hostlife/regionha_witness_test.go |
| +++ b/internal/sim/hostlife/regionha_witness_test.go |
| @@ -38,7 +38,7 @@ func TestDrainEndToEnd(t *testing.T) { |
| seen[w.claim.Op.Phase] = true |
| return w.claim.Op.Kind == "serving" && w.claim.Op.Exec == to.ID |
| }, w.actAll(), w.recoveryPass, func() { w.wake(to) }) |
| - for _, p := range []string{"starting", "releasing", "pinning", "installing", "installed", "probing", "probed", "opened"} { |
| + for _, p := range []string{"starting", "releasing", "pinning", "installing", "installed", "probing", "probed"} { |
| if !seen[p] { |
| t.Errorf("phase %s never observed", p) |
| } |
| @@ -344,15 +344,29 @@ func wRelocInstallReceipt(t *testing.T, w *world) { |
| w.finish(t) |
| } |
| +// probeOpened drives until the target's first attempt has opened P and |
| +// is still starting (L18 finding 2: once its app answers, the probe has |
| +// passed and is stopped, never restarted). |
| +func (w *world) probeOpened(t *testing.T, from, to *box) bool { |
| + w.openYield = func(b *box) bool { return b == to } // the attempt pauses after its admission, before replication opens |
| + defer func() { w.openYield = nil }() |
| + return w.reach(t, 1500, "P opened by an attempt still starting", func() bool { |
| + c := w.claim |
| + return c.Op.Kind == "relocating" && c.Op.Phase == "probing" && preparedOpened(c) && to.open != nil |
| + }, w.act(from, to), w.recoveryPass) |
| +} |
| + |
| +// wRelocNoReinstall, wRelocVerifyReceipt and wRelocPreparedOpenedJournal |
| +// make a later attempt after P's opening, which root cannot launch while |
| +// claim ask C11 is open (finding 4): they show the rules C11 makes live. |
| func wRelocNoReinstall(t *testing.T, w *world) { |
| w.twoBox() |
| + w.claimC11 = true |
| from, to := w.boxes[0], w.boxes[3] |
| w.serve(from, 1, app0) |
| w.running(t, from) |
| w.drainTo(t, to) |
| - if !w.reach(t, 1500, "the probe runs on the target", func() bool { |
| - return preparedOpened(w.claim) && hasMain(to) |
| - }, w.act(from, to), w.recoveryPass) { |
| + if !w.probeOpened(t, from, to) { |
| return |
| } |
| w.timerOn(to) |
| @@ -412,13 +426,14 @@ func wRelocRowCases(t *testing.T, w *world) { |
| return |
| } |
| // a paused duplicate of the source's earlier open lands now: its row |
| - // is ready again while its admission fence is closed. Reconcile |
| - // decides the row; a request reaches the box through its stale edges |
| - // file |
| + // is ready again while its admission fence is closed. A request |
| + // reaches the box through its stale edges file, then reconcile decides |
| + // the row (in that order each step, so the request also meets the row |
| + // in the step after the completion, before the catch-up hold) |
| from.Row.Status, from.Row.HoldOp = "ready", "" |
| - w.drive(40, never, func() { |
| - w.reconcile(from) |
| + w.drive(80, never, func() { |
| w.wake(from) |
| + w.reconcile(from) |
| }, w.act(to), w.recoveryPass, func() { w.wake(to) }) |
| w.servingOn(t, to) |
| w.finish(t) |
| @@ -585,12 +600,13 @@ func wRelocEnsureLocal(t *testing.T, w *world) { |
| func wRelocVerifyReceipt(t *testing.T, w *world) { |
| w.twoBox() |
| + w.claimC11 = true |
| from, to := w.boxes[0], w.boxes[3] |
| w.serve(from, 1, app0) |
| w.running(t, from) |
| w.drainTo(t, to) |
| third := w.extraBox(0, 30) |
| - if !w.reach(t, 1500, "the probe runs on the target", func() bool { return preparedOpened(w.claim) && hasMain(to) }, w.act(from, to), w.recoveryPass, func() { w.wake(to) }) { |
| + if !w.probeOpened(t, from, to) { |
| return |
| } |
| // the volume holding the host's directory is replaced and the agent |
| @@ -604,16 +620,23 @@ func wRelocVerifyReceipt(t *testing.T, w *world) { |
| func wRelocPreparedOpenedJournal(t *testing.T, w *world) { |
| w.twoBox() |
| + w.claimC11 = true |
| from, to := w.boxes[0], w.boxes[3] |
| w.serve(from, 1, app0) |
| w.running(t, from) |
| w.drainTo(t, to) |
| - if !w.reach(t, 1500, "the probe runs on the target", func() bool { return preparedOpened(w.claim) && hasMain(to) }, w.act(from, to), w.recoveryPass, func() { w.wake(to) }) { |
| + if !w.probeOpened(t, from, to) { |
| return |
| } |
| w.timerOn(to) |
| w.crash(to) // the next attempt admits a fresh generation from P's |
| - if !w.reach(t, 400, "the second attempt runs", func() bool { return hasMain(to) && w.claim.Holder.Gen != w.claim.Op.Prepared }, w.act(from, to), w.recoveryPass) { |
| + w.openYield = func(b *box) bool { return b == to } |
| + reached := w.reach(t, 400, "the second attempt admitted and still starting", func() bool { |
| + c := w.claim |
| + return c.Op.Phase == "probing" && c.Holder.Gen != c.Op.Prepared && to.open != nil |
| + }, w.act(from, to), w.recoveryPass) |
| + w.openYield = nil |
| + if !reached { |
| return |
| } |
| // holder.admissions is trimmed as AdmitWriter trims it past eight: |
| @@ -793,6 +816,7 @@ func wL21Window(t *testing.T, w *world) { |
| // the operator returns the host to the source; without it, it waits. |
| func wNoSpareBound(t *testing.T, w *world) { |
| w.twoBox() |
| + w.claimC1 = true // the failed target's release (claim ask C1, finding 4) |
| from, to := w.boxes[0], w.boxes[3] |
| to.FailApp = true |
| w.serve(from, 1, app0) |
diff --git a/internal/sim/hostlife/rules_test.go b/internal/sim/hostlife/rules_test.go| index f1d8dd534..d2bd81f6d 100644 |
| --- a/internal/sim/hostlife/rules_test.go |
| +++ b/internal/sim/hostlife/rules_test.go |
| @@ -210,4 +210,16 @@ var allRules = []string{ |
| // Astra's joint round 1 on the two-box model |
| "files-live-region", // joint round 1 finding 1, claim §6.2a (the live set is {authoritative region, location, generation}; region HA §5.6, L13): the files live set is region-qualified: holder.generation's manifests, the pin's, P's, the chain's newest and the objects they or a box's files directory name are live only in the files home (filesHome: the authoritative region, and while a relocation runs its source region holds the whole files live set), and the newest manifest is read only in the key's own region; the mutation reads every region, so a manifest PUT landing in the former region after a move's cleanup protects itself and the object it names, and the sweep never retires them (INV-10; witness) |
| "files-home-move-phases", // joint round 1 review I1, claim §6.2a and moves §5.1's authoritative-region table: the files home also holds the source region while moving (op.exec none from stopped on), while landing until the move commits (op.Committed: admission does not rule out a clean rollback, joint round 2), and while restoring (released included); the mutation keeps op.exec's region and a relocation's source only, so a park-generation queued during the move archives the live manifest in stopped, or after the target's admission before a clean rollback, and the source-region failover pins no keyed manifest (INV-30, INV-3 with INV-30 off; wMoveStoppedKeepsLiveFiles, wRollbackKeepsSourceFiles) |
| + // L18 joint round findings 2 to 4 (regionha_completion_test.go; 1b-next 596fa8b1 and a092ddc2) |
| + "reloc-probe-stop", // finding 2, ruling 49 (Participant's EndProbe, RecordProbeStop, CompleteRelocation's probeStopped): the passed probe's session is stopped with root's receipt and the stop journaled before the serving CAS, bounded by ruling 67; the mutation completes over the running probe, which strands its session across the kind change (INV-31; wProbeStopBeforeServing) |
| + "reloc-probe-fence-owner", // finding 2, ruling 75 (relocationStopProbe's FenceAndStopAs, relocationReleaseHold's LiftFenceAs): the probe stop installs its owned activator fence only on an unfenced host or meets its own, and refuses any other owner's with nothing stopped; the lift lifts only its own; the mutation installs over, and lifts, any fence (INV-32; wProbeStopMeetsAnotherFence, wLiftAfterRestartMeetsAnotherFence) |
| + "reloc-completion-discharge-first", // finding 2, ruling 66 (relocationReleaseHold, DischargeCompleted): C10's discharge succeeds, while the row is still held for the op and the holder is still the stopped probe session, before the hold is released or the fence lifted, and reconcile never releases that hold as stale; the mutation releases and lifts first, and a serving wake moves the holder off the undischarged session (INV-31; wDischargeFailsHoldsTheRow) |
| + "reloc-completion-mark-last", // finding 2, ruling 80 (relocationReleaseHold, MarkCompletedDischarged): the mark is written last, after the discharge, the hold's release and the lift; the mutation marks first, so a discharge that then fails is never retried and the barrier lets a successor name the undischarged box (INV-31; wMarkLastAfterAFailedDischarge) |
| + "reloc-completion-from-claim", // finding 2, ruling 80 (RelocationRuntime.once, finishCompletion): the pass finds every unmarked completion on this box from the claim record, never from the row, so a mark that failed after the hold's release is retried; the mutation finds it from the row's hold, and the completion is never marked, so nothing ever starts from the host again (INV-3; wFailedMarkRetriedFromTheClaim) |
| + "reloc-completion-barrier", // finding 2, ruling 77 (completionBarrier in StartGuard and RelocationStartGuard): no move, delete, purge, push or relocation starts from serving while the completion is unmarked, unless the completion box is on lost or is a failover's cited fenced source; the mutation starts a drain and a move over the undischarged box (INV-31; wSuccessorWaitsForTheDischarge) |
| + "reloc-completion-claim-mode", // finding 2, ruling 82 (newCompletionRuntime): the completion pass runs whenever claim mode is on, region HA on or off; the mutation runs it with region HA on only, and a completion pending when region HA is turned off never finishes (INV-3; wCompletionWithRegionHAOff) |
| + "reloc-completed-handover", // finding 2, N6 (wireCompletedHandover, relocationCompletedHandover): the first serving wake after a completion hands over from the probe's receipt and stops nothing; the mutation routes it to main's stop, whose serving-shaped fence replaces the probe's, and the handover refuses for good (INV-3; wServingWakeHandsOver) |
| + "reloc-completed-catchup-hold", // finding 3, ruling 85 (hostbox completedHold, 1b-next a092ddc2): a source whose reconcile runs only after the target completed holds its row for the completed op until its park-local retires it; the mutation leaves the row its release left ready (INV-33; wDelayedSourceHoldsItsRow) |
| + "reloc-c1-failed-release-refused", // finding 4, claim ask C1 open (QueueRelocationRelease requires the source in releasing): a live failed target cannot release in probe-failed and reaches stuck at the release deadline, and the operator's resolve stops it; the mutation releases as if C1 had landed (a fidelity guard: TestFailedTargetCannotReleaseWithoutC1) |
| + "reloc-c11-later-attempt-refused", // finding 4, claim ask C11 open (Preflight's ErrLaterAttemptUnlaunchable, ruling 58): after P's opening a later cold probe attempt is refused before it is counted, which is probe-failed; the mutation counts and makes it as if C11 had landed (a fidelity guard: TestLaterAttemptRefusedWithoutC11) |
| } |
diff --git a/internal/sim/hostlife/sim_test.go b/internal/sim/hostlife/sim_test.go| index 24431d89a..b6f38161c 100644 |
| --- a/internal/sim/hostlife/sim_test.go |
| +++ b/internal/sim/hostlife/sim_test.go |
| @@ -352,6 +352,9 @@ func (w *world) atRest() bool { |
| if e == nil || e.Row == nil || e.Row.Status != "ready" { |
| return false |
| } |
| + if d := c.Op.Completed; d != nil && !d.Discharged || e.actFence != "" { |
| + return false // a completion not yet marked, or a fence not yet lifted (L18 finding 2) |
| + } |
| if e.Config != c.Holder.Inc || e.Live != c.Holder.App || e.LiveInc != c.Holder.Inc { |
| return false // config sync and adoption still owe this incarnation |
| } |
| @@ -406,6 +409,7 @@ func (w *world) checkStep() { |
| w.violate("INV-27: relocation %s names box %d as op.exec, which is unenrolled or lost", c.Op.ID, c.Op.Exec) |
| } |
| } |
| + w.checkCompletion() // INV-31 (L18 finding 2): only a relocation sets owedDischarge |
| if w.perRegion > 1 && !w.noPinWatch { |
| w.checkFilesPreserved() // INV-30 (joint round 2): only the two-box shape has files keys |
| } |
diff --git a/internal/sim/hostlife/witness_test.go b/internal/sim/hostlife/witness_test.go| index 3330dd894..597e6a357 100644 |
| --- a/internal/sim/hostlife/witness_test.go |
| +++ b/internal/sim/hostlife/witness_test.go |
| @@ -210,8 +210,8 @@ var witnesses = []witness{ |
| "a failover: the executor is terminated with an acknowledged write whose upload is still in flight; the first admission of P takes released coverage and the write is neither restored nor declared", wRelocReleasedCoverage}, |
| {"reloc-source-loss", "reloc-source-loss", "INV-2", |
| "a drain whose source is terminated in releasing before its release is journaled, with an unuploaded write; taken as released at what the remote holds, the write goes undeclared", wRelocSourceLoss}, |
| - {"reloc-row-cases", "reloc-row-cases,exec-admission,exec-writer", "INV-6", |
| - "a stale edges file: after the source's release a paused duplicate open makes its row ready again; reconcile holds it, and with the row case, the exec check and AdmitWriter's op.exec check gone a request admits the released source as a writer, and the stamp its admission issued is activated under the target (INV-6)", wRelocRowCases}, |
| + {"reloc-row-cases", "reloc-row-cases,exec-admission,exec-writer", "INV-31", |
| + "a stale edges file: after the source's release a paused duplicate open makes its row ready again; reconcile holds it, and with the row case, the exec check and AdmitWriter's op.exec check gone a request admits the released source as a writer; since L18 finding 2 no relocating phase admits a non-probe writer, so the admission lands just after the completion, before the target discharged its participation (INV-31; rev 4 to 11 saw INV-6 at the removed opened phase)", wRelocRowCases}, |
| {"fence-discharge-qualified", "fence-discharge-qualified", "INV-26", |
| "a terminated box with a volume that was not DeleteOnTermination has its park-local chores discharged automatically", wFenceDischargeQualified}, |
| {"fence-declares-timers", "fence-declares-timers", "acknowledged timer", |
diff --git a/internal/sim/hostlife/world_test.go b/internal/sim/hostlife/world_test.go| index c4832e223..a0ac5c504 100644 |
| --- a/internal/sim/hostlife/world_test.go |
| +++ b/internal/sim/hostlife/world_test.go |
| @@ -396,6 +396,26 @@ type box struct { |
| // not yet ended (memory: a restart forgets it, and the next attempt is |
| // counted again, ruling 19) |
| attemptTag string |
| + // L18 joint round findings 2 and 3 (regionha_completion_test.go): |
| + // actFence is the activator's fence on the host (its owner; "" none), |
| + // in the agent's memory, so a restart empties it; probeFence is the |
| + // persisted owner a probe stop installs under (probe-fence.json), |
| + // kept until the completion is marked; relFence is root's admission |
| + // fence of a release (the op it closed admission for), which ruling |
| + // 28 puts at the release's end instead of a row hold; owedDischarge |
| + // is ground truth, the completed relocation whose participation this |
| + // box has not yet discharged (C10). foreignFence is a witness's |
| + // stand-in for another operation's fence that its owner never lifted |
| + // (INV-32's ground truth). dischargeFails, markFails and crashAfter |
| + // are witness knobs on the completion pass |
| + actFence string |
| + probeFence string |
| + relFence string |
| + owedDischarge string |
| + foreignFence string |
| + dischargeFails bool |
| + markFails bool |
| + crashAfter string |
| Row *row |
| DB *localDB |
| @@ -597,6 +617,7 @@ func (b *box) forget() { |
| b.evidAt = map[string]int{} |
| b.pendingTimers = nil |
| b.attemptTag = "" |
| + b.actFence = "" // the activator's fences die with the agent; probe-fence.json survives (ruling 75) |
| if b.DB != nil { |
| b.DB.InFlight = nil // the upload's client is gone; the restarted replica uploads the same file again |
| // a writer that was draining before its clean close is gone with |
| @@ -846,6 +867,15 @@ type opState struct { |
| Observed []int // every fence.<box>.observed_at the operation consumed, kept through replacements (rev 4) |
| Acks []int // exec_ack.<box>: the participants that acknowledged, durable (rev 4) |
| Abandoned []string // abandoned_prepared: every unopened P the operation replaced or dropped, parked at serving (1b-next ruling 27) |
| + // L18 joint round finding 2: the built completion protocol |
| + // (regionha_completion_test.go). ProbePassedAt is the probe's |
| + // journaled time (Probe.At, ruling 67's bound); ProbeStop the target's |
| + // journaled stop of the passed probe's session (ruling 49); Completed |
| + // the serving op's completed_relocation record (ruling 56), which the |
| + // completion pass marks discharged last (ruling 80) |
| + ProbePassedAt int |
| + ProbeStop *probeStopEntry |
| + Completed *completedEntry |
| // journal |
| ReportAt int |
| @@ -982,6 +1012,21 @@ type pinEntry struct { |
| // receiptEntry is the local install receipt (§5.8 local_install): the |
| // box and the install_stamp of the CAS that handed it op.exec. A |
| // replacement executor never inherits its predecessor's. |
| +// probeStopEntry is hostclaim.ProbeStop: the target's stop of the passed |
| +// probe's session, with root's receipt (ruling 49). |
| +type probeStopEntry struct { |
| + Box, Session int |
| +} |
| + |
| +// completedEntry is hostclaim.CompletedRelocation on the serving op: the |
| +// relocation, the box and stopped probe session it completed with, and |
| +// Discharged, the mark (MarkCompletedDischarged). |
| +type completedEntry struct { |
| + Op string |
| + Box, Session int |
| + Discharged bool |
| +} |
| + |
| type receiptEntry struct { |
| Op string |
| Box, Stamp int |
| @@ -1103,9 +1148,17 @@ type world struct { |
| // oneBoxRegion: a witness's region kept at one box by its group in the |
| // two-box shape (H5's minimum is per region) |
| oneBoxRegion [nRegions]bool |
| - t testingT |
| - seed int64 |
| - rng intner |
| + // L18 joint round findings 2 and 4 (regionha_completion_test.go): |
| + // haOff is CARLOS_REGION_HA off with claim mode on, where only the |
| + // completion pass runs (ruling 82); claimC1 and claimC11 are claim |
| + // asks C1 (a failed target's release obligation) and C11 (root |
| + // launches a later probe attempt after P's opening). Both are open |
| + // today, so the model runs the built fallbacks; a witness or test of |
| + // the post-C1 or post-C11 behaviour sets them |
| + haOff, claimC1, claimC11 bool |
| + t testingT |
| + seed int64 |
| + rng intner |
| // hold, when set, is a witness's hand on S3: a request it answers true |
| // for is accepted and completes only when the witness says so |
| // (witness_test.go). The random sweep never sets it. |