amadan
sim/hostlife: K8 judges only a release CAS that succeeded (Task 7 fix round 2)
The K8 oracle read the record before release's CAS, so a stale release the op-id guard correctly refused was reported as a violation. It now runs in the CAS's success branch only. TestK8JudgesOnlyASucceededRelease: the source closes a clean rollback's record and stalls before its release; the recovery pass releases from last_move; a purge runs to the end and removes the record; the stalled release resumes with only revalidate-before-effect dropped. The guard refuses it, the claim is untouched, and K8 does not fire. The record-first-close mutation is still caught (113 / 300; 1,060 / 3,000).
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
2 files changed,
+45
−4
internal/sim/hostlife/moves_test.go+6 −4internal/sim/hostlife/witness_test.go+39 −0
diff --git a/internal/sim/hostlife/moves_test.go b/internal/sim/hostlife/moves_test.go| index d66c63aad..b0af446ce 100644 |
| --- a/internal/sim/hostlife/moves_test.go |
| +++ b/internal/sim/hostlife/moves_test.go |
| @@ -1404,10 +1404,6 @@ func (w *world) closeRecord(c *claim, execBox int) bool { |
| func (w *world) release(c *claim, execBox int) { |
| op := c.Op |
| - 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 |
| - w.violate("K8: %s releases the claim before its record closed (record first, rev 7.23)", op.ID) |
| - } |
| if w.cas(c, func(n *claim) bool { |
| if !sameOp(n.Op.ID, op.ID) { |
| return false |
| @@ -1419,6 +1415,12 @@ func (w *world) release(c *claim, execBox int) { |
| return true |
| }) { |
| w.logf("released %s to serving on box %d", op.ID, execBox) |
| + 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 |
| + // op-id guard refused released nothing (fix round 2) |
| + w.violate("K8: %s released the claim before its record closed (record first, rev 7.23)", op.ID) |
| + } |
| w.opsDone++ |
| // a move's record closed before this (closeMove, rev 7.23); a |
| // push's or a relocation's record half follows on a later step |
diff --git a/internal/sim/hostlife/witness_test.go b/internal/sim/hostlife/witness_test.go| index b4f229f37..73515c8fd 100644 |
| --- a/internal/sim/hostlife/witness_test.go |
| +++ b/internal/sim/hostlife/witness_test.go |
| @@ -3571,3 +3571,42 @@ func TestProbeWindow(t *testing.T) { |
| 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) |
| } |
| } |
| + |
| +// TestK8JudgesOnlyASucceededRelease (Task 7 fix round 2): the K8 oracle |
| +// judges a release CAS that succeeded, never one the op-id guard refused. |
| +// The source closes a clean rollback's record and its goroutine stalls |
| +// before the release; the recovery pass releases from last_move; a purge |
| +// runs to the end and removes the record; the stalled release resumes with |
| +// only revalidate-before-effect dropped. Its CAS is conditional on the |
| +// rollback's op, which the claim no longer holds: refused, the claim is |
| +// untouched, and nothing is violated. |
| +func TestK8JudgesOnlyASucceededRelease(t *testing.T) { |
| + saved := mutated |
| + mutated = "revalidate-before-effect" |
| + defer func() { mutated = saved }() |
| + w := newWitness() |
| + src, tgt := w.boxes[0], w.boxes[1] |
| + w.serve(src, 1, app0) |
| + w.landProbed(t, src, tgt) |
| + w.rollback(w.claim, "cut deadline") |
| + w.reach(t, 1500, "source about to close", func() bool { |
| + c := w.claim |
| + return c.Op.Kind == "restoring" && c.Op.SrcPhase == "opened" && c.oblFor(c.Op.ID) == 0 |
| + }, w.act(src, tgt), w.recoveryPass) |
| + old := w.claim.clone() // the stalled goroutine's read |
| + if !w.closeRecord(old, src.ID) { |
| + t.Fatalf("the record did not close: %s", w.state()) |
| + } |
| + w.reach(t, 50, "released from last_move", func() bool { return w.claim.Op.Kind == "serving" }, w.recoveryPass) |
| + pg := &consolePlan{Kind: "purge", App: app0} |
| + w.reach(t, 2000, "the purge removed the record", func() bool { return w.rec == nil }, func() { w.runPlan(pg) }, w.actAll(), w.recoveryPass) |
| + before := w.claim.clone() |
| + w.resumeStaleRelease(src, old) |
| + if len(w.violations) > 0 { |
| + dump(t, w) |
| + t.Fatalf("a refused stale release was judged: %v", w.violations) |
| + } |
| + if w.claim.Ver != before.Ver || w.claim.Op.Kind == "serving" && w.claim.Op.Exec == src.ID && w.claim.Holder != nil { |
| + t.Fatalf("the stale release was not refused: before %s after %s", before.Op.Kind, w.state()) |
| + } |
| +} |