amadan

carlos / platform Public

sim: Astra's round 8 on the two-box model: root's stop receipt is tracked apart from the recorded positions, with the flushing controller's identity; only that controller finishes from the positions, and after a restart the receipt is needed too

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Paul Campbell pushed by claude 2ea08a48e04b64fae79810828bba85501b62dd71 parent 33f684b
5 files changed, +137 −20
  • internal/sim/hostlife/console_test.go +8 −5
  • internal/sim/hostlife/regionha_round1_test.go +92 −11
  • internal/sim/hostlife/regionha_test.go +27 −4
  • internal/sim/hostlife/rules_test.go +1 −0
  • internal/sim/hostlife/world_test.go +9 −0
diff --git a/internal/sim/hostlife/console_test.go b/internal/sim/hostlife/console_test.go
index 9c219e278..d8aae4592 100644
--- a/internal/sim/hostlife/console_test.go
+++ b/internal/sim/hostlife/console_test.go
@@ -1346,9 +1346,11 @@ func (w *world) operator() {
// releaseUnrecoverable is the operator's check before it stops a live
// target that has not released (rev 10, Astra round 7): only when no
-// release can ever come. That needs no flush recorded for this stop, and
-// either the session's replicator or the box's files directory gone for
-// good (relocRelease refuses without either). Any other release, a slow
+// release can ever come. That needs no usable flush record for this
+// stop (rev 11: a record counts only with root's durable receipt, or while
+// the controller that recorded it is still running), and either the
+// session's replicator or the box's files directory gone for good
+// (relocRelease refuses without either). Any other release, a slow
// acknowledgement or a recorded flush not yet journaled, is resumed: the
// resolve clears stuck and sends the target back to probe-failed. The
// mutation of operator-stop-unrecoverable-only stops every such target,
@@ -1358,8 +1360,9 @@ func (w *world) releaseUnrecoverable(b *box, c *claim) bool {
return true
}
h := c.Holder
- if r := b.relRecord; r != nil && r.Op == c.Op.ID && r.Phase == c.Op.Phase && r.E.Session == h.Session && r.E.Gen == h.Gen {
- return false // a recorded flush: the release replays it
+ if r := b.relRecord; r != nil && r.Op == c.Op.ID && r.Phase == c.Op.Phase && r.E.Session == h.Session && r.E.Gen == h.Gen &&
+ (r.Receipt || r.Ctl == b.Epoch || !on("reloc-release-needs-receipt")) {
+ return false // a recorded flush with root's receipt, or its own controller still alive to finish it (rev 11)
}
replicator := b.DB != nil && b.DB.Inc == h.Inc && b.DB.Gen == h.Gen && b.DB.Epoch == b.Epoch && b.DB.Session == h.Session
files := b.Files != nil && b.Files.Inc == h.Inc
diff --git a/internal/sim/hostlife/regionha_round1_test.go b/internal/sim/hostlife/regionha_round1_test.go
index 4e8d93b9d..59c8f7bb0 100644
--- a/internal/sim/hostlife/regionha_round1_test.go
+++ b/internal/sim/hostlife/regionha_round1_test.go
@@ -811,12 +811,14 @@ func TestReleaseRefusedAfterACrashBeforeTheFlush(t *testing.T) {
}
// TestReleaseReplaysTheRecordedFlush (reloc-release-needs-flush; rev 9,
-// Astra round 6): the source's release sequence completes and records
-// its flushed positions (ReleasePositions), and its agent crashes before
-// the release is journaled. The restarted agent has no replicator for
-// the session, but the record is durable: the release is replayed with
-// the recorded positions, Flushed, and the drain completes. The mutation
-// records nothing and journals the remote position with Flushed false.
+// Astra round 6; rev 11, round 8): the source's release sequence
+// completes, records its flushed positions (ReleasePositions), and root
+// persists the stop receipt; its agent then crashes before the release
+// is journaled. The restarted agent has no replicator for the session,
+// but the record and the receipt are durable: the release is replayed
+// with the recorded positions, Flushed, and the drain completes. The
+// mutation of reloc-release-needs-flush records nothing and journals the
+// remote position with Flushed false.
func TestReleaseReplaysTheRecordedFlush(t *testing.T) {
w := twoBoxWitness()
from, to := w.boxes[0], w.boxes[3]
@@ -830,7 +832,7 @@ func TestReleaseReplaysTheRecordedFlush(t *testing.T) {
}
var r *releaseEntry
for i := 0; i < 60 && r == nil; i++ {
- r = w.relocRelease(from, w.claim.clone()) // steps 1 to 3 and the record, not yet journaled
+ r = w.relocRelease(from, w.claim.clone()) // steps 1 to 3, the record and the receipt, not yet journaled
w.tick()
}
if r == nil || !r.Flushed {
@@ -913,9 +915,9 @@ func TestOperatorResumesASlowRelease(t *testing.T) {
// TestOperatorResumesARecordedFlush (operator-stop-unrecoverable-only;
// rev 10, Astra round 7 finding 2): the failed target completes its
-// release sequence and records it, then its agent restarts (the
-// session's replicator is gone) before the release is journaled, and the
-// deadline passes. The recorded flush is a release waiting to be
+// release sequence, records it and gets root's receipt (rev 11), then its
+// agent restarts (the session's replicator is gone) before the release is
+// journaled, and the deadline passes. The recorded flush is a release waiting to be
// journaled: the resolve resumes it, the target replays the record, and
// the nested relocation serves. The mutation stops the box.
func TestOperatorResumesARecordedFlush(t *testing.T) {
@@ -923,7 +925,7 @@ func TestOperatorResumesARecordedFlush(t *testing.T) {
from, to := w.probeFailedTarget(t)
var r *releaseEntry
for i := 0; i < 60 && r == nil; i++ {
- r = w.relocRelease(to, w.claim.clone()) // steps 1 to 3 and the record, not journaled
+ r = w.relocRelease(to, w.claim.clone()) // steps 1 to 3, the record and the receipt, not journaled
w.tick()
}
if r == nil {
@@ -976,6 +978,85 @@ func TestStoppedTargetKeepsItsLocalCleanup(t *testing.T) {
w.mustHold(t)
}
+// recordWithoutReceipt runs b's release sequence until its flushed
+// positions are recorded, and stops before the producers drain and root
+// persists the receipt.
+func (w *world) recordWithoutReceipt(t *testing.T, b *box) {
+ for i := 0; i < 60 && b.relRecord == nil; i++ {
+ w.relocRelease(b, w.claim.clone())
+ w.tick()
+ }
+ if r := b.relRecord; r == nil || r.Receipt {
+ t.Fatalf("no record without a receipt on box %d: %+v %s", b.ID, r, w.state())
+ }
+}
+
+// TestReleaseRefusedAfterACrashBeforeTheReceipt (reloc-release-needs-receipt;
+// rev 11, Astra round 8): the source records its flushed positions, and
+// its agent crashes before root persists the stop receipt. The positions
+// are not proof of the stop: the restarted agent's release is refused
+// (RecoveryReleaseDrain), no release or pin appears, the deadline makes
+// the operation stuck, and the resolve returns the host to its source.
+// TestReleaseReplaysTheRecordedFlush is the other side: the crash after
+// the receipt, replayed. The mutation replays the positions alone.
+func TestReleaseRefusedAfterACrashBeforeTheReceipt(t *testing.T) {
+ w := twoBoxWitness()
+ from, to := w.boxes[0], w.boxes[3]
+ w.serve(from, 1, app0)
+ w.running(t, from)
+ w.published(t, from)
+ w.drainTo(t, to)
+ w.appWrite(from)
+ if !w.stepUntil(t, 1500, "releasing", w.atPhase("releasing")) {
+ w.mustHold(t)
+ }
+ w.recordWithoutReceipt(t, from)
+ w.crash(from)
+ for i := 0; i < releaseDeadline+20; i++ {
+ w.tick(w.act(from, to))
+ c := w.claim
+ if c.Op.Release != nil || c.Op.Pin != nil {
+ t.Fatalf("a release or a pin from recorded positions with no receipt (step %d): %s", i, w.state())
+ }
+ if c.Op.Stuck != "" {
+ break
+ }
+ }
+ if c := w.claim; c.Op.Stuck == "" || c.Op.Phase != "releasing" {
+ t.Fatalf("not stuck in releasing at the release deadline: %s", w.state())
+ }
+ w.finish(t)
+ w.mustHold(t)
+ if c := w.claim; c.Op.Kind != "serving" || c.Op.Exec != from.ID {
+ t.Fatalf("the operator's resolve did not return the host to its source: %s", w.state())
+ }
+}
+
+// TestOperatorStopsATargetWithNoReceipt (reloc-release-needs-receipt,
+// operator-stop-unrecoverable-only; rev 11, Astra round 8): the failed
+// target records its flushed positions and its agent restarts before root
+// persists the receipt. Its release can never come, so the operator stops
+// it, and the next resolve replays the operation; the host serves
+// elsewhere. The mutation treats the positions as recoverable and resumes
+// a release that replays them.
+func TestOperatorStopsATargetWithNoReceipt(t *testing.T) {
+ w := twoBoxWitness()
+ _, to := w.probeFailedTarget(t)
+ w.recordWithoutReceipt(t, to)
+ w.crash(to)
+ if !w.reach(t, 3000, "serving after the operator's stop and replay", func() bool {
+ c := w.claim
+ return c.Op.Kind == "serving" && c.Op.Exec >= 0 && c.Op.Exec != to.ID
+ }, w.actAll(), w.recoveryPass, w.wakeExec, w.resolveOnly) {
+ w.mustHold(t)
+ }
+ if !to.Destroyed || w.stats["operator stopped a target that cannot release"] == 0 || w.stats["release journaled: failed target"] != 0 {
+ t.Fatalf("the target was not stopped, or released from positions with no receipt: %v %s", w.stats, w.state())
+ }
+ w.finish(t)
+ w.mustHold(t)
+}
+
// TestPinNeverShortOfTheRelease (reloc-pin-reaches-release): the listing
// lags behind the journaled release (its newest file is not yet visible);
// no pin is journaled short of the release's final_txid.
diff --git a/internal/sim/hostlife/regionha_test.go b/internal/sim/hostlife/regionha_test.go
index 1407d22f6..1d4677fea 100644
--- a/internal/sim/hostlife/regionha_test.go
+++ b/internal/sim/hostlife/regionha_test.go
@@ -146,11 +146,29 @@ func (w *world) relocRelease(b *box, c *claim) *releaseEntry {
}
if r := b.relRecord; r != nil && on("reloc-release-needs-flush") && r.Op == c.Op.ID && r.Phase == c.Op.Phase && r.E.Session == h.Session && r.E.Gen == h.Gen {
// a flush this box recorded for this stop (ReleasePositions.Recorded):
- // the release is replayed with the recorded positions, never
- // flushed or guessed again (rev 9)
+ // never flushed or guessed again (rev 9). Rev 11 (Astra round 8):
+ // the positions are not proof of the stop. The controller that
+ // recorded them resumes at the producers' drain, and root persists
+ // the receipt (step 4); after a restart only root's durable receipt
+ // for the recorded identity finishes the release, and with none
+ // RecoveryReleaseDrain refuses: no release, and the deadline
+ // makes the operation stuck. The mutation of
+ // reloc-release-needs-receipt replays the positions alone, as rev
+ // 10 did
+ switch {
+ case r.Receipt || !on("reloc-release-needs-receipt"):
+ if r.Ctl != b.Epoch {
+ w.stats["release: replayed from the recorded positions"]++
+ }
+ case r.Ctl == b.Epoch:
+ r.Receipt = true // the producers drain; root persists the receipt
+ w.stats["release: receipt persisted"]++
+ default:
+ w.stats["release: recorded positions without a receipt, refused"]++
+ return nil
+ }
e := r.E
e.Files, e.Timers = r.E.Files.clone(), append([]int(nil), r.E.Timers...)
- w.stats["release: replayed from the recorded positions"]++
return &e
}
prefix := dataKey(h.Location, h.Gen, "")
@@ -227,8 +245,13 @@ func (w *world) relocRelease(b *box, c *claim) *releaseEntry {
Files: files, Timers: append([]int(nil), b.Timers...), At: w.now}
if on("reloc-release-needs-flush") {
// ReleasePositions.Record: durable before the producers close
- b.relRecord = &releaseRecord{Op: c.Op.ID, Phase: c.Op.Phase, E: *e}
+ b.relRecord = &releaseRecord{Op: c.Op.ID, Phase: c.Op.Phase, E: *e, Ctl: b.Epoch}
b.relRecord.E.Files, b.relRecord.E.Timers = files.clone(), append([]int(nil), b.Timers...)
+ if on("reloc-release-needs-receipt") {
+ // the producers' drain and root's receipt are the next step:
+ // a crash here leaves positions and no receipt (rev 11)
+ return nil
+ }
}
return e
}
diff --git a/internal/sim/hostlife/rules_test.go b/internal/sim/hostlife/rules_test.go
index a35e9995f..eef576edf 100644
--- a/internal/sim/hostlife/rules_test.go
+++ b/internal/sim/hostlife/rules_test.go
@@ -197,6 +197,7 @@ var allRules = []string{
"files-live-set-moves-parks", // finding F4 (rev 4), claim §6.2a: moves' parks (a push's whole-location park, a landing's install park, a rollback's return park) keep the files live set; the mutation archives it with the rest and the next failover can never pin the live files (INV-3)
"reloc-clear-after-cleanup", // 1b-next ruling 20 and rev 6 R4-5 (Finish clears the record only after a successful scoped cleanup): a failed cleanup keeps the controller record, which blocks executable updates (claim §11's witness); the mutation clears it and an update runs over the unfinished cleanup (INV-29)
"fence-converts-committed-landing", // finding F5 (rev 4; claim §11 "automatic target loss racing the record commit CAS"): a landing whose record committed and whose target is then terminated becomes a failover in the target's region; the mutation leaves it to the operator, and it never completes (INV-3)
+ "reloc-release-needs-receipt", // rev 11 (Astra round 8; 1b-next rev 19 Task 7 Release, RecoveryReleaseDrain): recorded positions finish a release only for the controller that recorded them, or with root's durable receipt after a restart; the mutation replays the positions alone (TestReleaseRefusedAfterACrashBeforeTheReceipt, TestOperatorStopsATargetWithNoReceipt)
"operator-stop-unrecoverable-only", // rev 10 (Astra round 7; plan ruling 13, no 1b-next code): the operator stops a live target that has not released only when its release is unrecoverable (no recorded flush, and the session's replicator or its files gone); otherwise the resolve resumes the release; the mutation stops every such target (TestOperatorResumesASlowRelease, TestOperatorResumesARecordedFlush)
"reloc-release-needs-flush", // rev 9 (Astra round 6; 1b-next rev 19 Task 7 Release, relocationFlushDB, ReleaseFlushFiles, ReleasePositions): a release needs the session's own replicator and the box's own files directory, or the positions it recorded for this stop; otherwise none, and the deadline makes the operation stuck; the mutation journals the remote position with Flushed false (TestReleaseRefusedAfterACrashBeforeTheFlush, TestReleaseReplaysTheRecordedFlush)
"reloc-fence-pending-blocks", // rev 8 (Astra round 5; 1b-next rev 19 Worker.Step returns w.replace(...) before its phase switch): while a relocation participant's fence is pending (a dead target, no spare, before its deadline) no regional phase transition runs; the participant's own release still does; the mutation goes on into the phase switch (TestPendingTargetFenceHoldsThePhase)
diff --git a/internal/sim/hostlife/world_test.go b/internal/sim/hostlife/world_test.go
index af8e3645f..7d5827e72 100644
--- a/internal/sim/hostlife/world_test.go
+++ b/internal/sim/hostlife/world_test.go
@@ -936,6 +936,15 @@ type opState struct {
type releaseRecord struct {
Op, Phase string
E releaseEntry
+ // Ctl is the flushing controller's identity: the agent process
+ // (box.Epoch) that flushed and recorded (rev 11). Receipt is root's
+ // durable stop receipt for this stop, persisted after the producers
+ // drained (step 4), tracked apart from the recorded positions: only
+ // the same controller may finish from the positions alone, and after a
+ // restart the release needs the receipt too (1b-next Task 7 Release,
+ // RecoveryReleaseDrain; Astra round 8)
+ Ctl int
+ Receipt bool
}
type releaseEntry struct {