amadan

carlos / platform Public

sim: Astra's rounds 2 and 3 on the two-box model: an initial failover's target acknowledges before its pin is selected (PinFailover), while converted moves, nested failovers and replays pin first, a crash between the published marker and the open replication, the adverse volume under a failover of the current executor, and the pinned manifest's generation parked at completion

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Paul Campbell pushed by claude 8439910135f6df021431a01964064be811eff72a parent 8b673c9
7 files changed, +276 −37
  • internal/sim/hostlife/console_test.go +1 −0
  • internal/sim/hostlife/protocol_test.go +3 −0
  • internal/sim/hostlife/regionha_cases_test.go +26 −15
  • internal/sim/hostlife/regionha_round1_test.go +146 −4
  • internal/sim/hostlife/regionha_test.go +93 −18
  • internal/sim/hostlife/rules_test.go +1 −0
  • internal/sim/hostlife/world_test.go +6 −0
diff --git a/internal/sim/hostlife/console_test.go b/internal/sim/hostlife/console_test.go
index 1e7f99d23..806116598 100644
--- a/internal/sim/hostlife/console_test.go
+++ b/internal/sim/hostlife/console_test.go
@@ -1274,6 +1274,7 @@ func (w *world) operator() {
default:
w.abandonPrepared(n)
n.Op.Stuck, n.Op.Replacements, n.Op.Excluded, n.Op.Resolved = "", 0, nil, true
+ n.Op.PinFailover = false // the replay enters pinning directly (rev 6)
if released && op.Exec >= 0 {
n.Op.Excluded = []int{op.Exec} // the target that just failed its probe is not the operator's fresh choice (rev 4)
}
diff --git a/internal/sim/hostlife/protocol_test.go b/internal/sim/hostlife/protocol_test.go
index 219c9e2c5..3f442bcdb 100644
--- a/internal/sim/hostlife/protocol_test.go
+++ b/internal/sim/hostlife/protocol_test.go
@@ -925,6 +925,9 @@ func (w *world) resumeOpen(b *box, c *claim, o *openState) bool {
}
}
o.stage = "open"
+ if w.openYield != nil && w.openYield(b) {
+ return false // the marker is published; replication is not open yet
+ }
case "open":
if !hasMain(b) && b.DB != nil {
// the app was stopped idle while the start was still
diff --git a/internal/sim/hostlife/regionha_cases_test.go b/internal/sim/hostlife/regionha_cases_test.go
index 36efb1e61..39e9b52df 100644
--- a/internal/sim/hostlife/regionha_cases_test.go
+++ b/internal/sim/hostlife/regionha_cases_test.go
@@ -223,31 +223,42 @@ func TestL18UnenrolledReference(t *testing.T) {
})
}
+// TestL18AdverseVolume (claim §11's adverse-volume case; H19; rev 5, Astra
+// round 2 finding 2): the current executor is terminated with a
+// volume that was not DeleteOnTermination. Execution recovery proceeds
+// to serving on the region's other box (two-box) or on the group's
+// replacement (one-box) with no operator, and the dead box's park-local
+// stays open throughout; only the operator's cleanup (the declared
+// destroyed-local loss) removes it.
func TestL18AdverseVolume(t *testing.T) {
bothShapes(t, func(t *testing.T, w *world, boxes int) {
from := w.serveAndPublish(t)
from.DeleteOnTermination = false
- if boxes == 2 {
- // a former executor that still owes its park-local
- w.drainTo(t, w.peer())
- w.servingOn(t, w.peer())
- if !w.owesLocal(w.claim, from) {
- t.Fatalf("the former executor owes no park-local: %s", w.state())
- }
+ w.terminate(from) // the current executor
+ if !w.reach(t, 3000, "serving after the failover, with no operator", func() bool {
+ c := w.claim
+ return c.Op.Kind == "serving" && c.Op.Exec >= 0 && c.Op.Exec != from.ID
+ }, w.actAll(), w.recoveryPass, w.wakeExec) {
+ return
}
- w.terminate(from)
- if boxes == 2 {
- w.reach(t, 60, "the former executor fenced", func() bool { return contains(w.claim.Lost, from.ID) }, w.act(w.peer()))
- if !w.owesLocal(w.claim, from) {
- t.Fatalf("the fence discharged the park-local without qualifying evidence: %s", w.state())
- }
- } else {
- w.failedOver(t, from) // execution recovery proceeds (H19)
+ to := w.execBox(w.claim)
+ if boxes == 2 && to != w.peer() {
+ t.Fatalf("served on %v, want the region's other box %d", to, w.peer().ID)
+ }
+ if !w.owesLocal(w.claim, from) {
+ t.Fatalf("the dead box's park-local is not open after the failover: %s", w.state())
}
if w.stats["fence: park-local chores left open (volume evidence)"] == 0 || w.stats["fence: park-local chores discharged"] != 0 {
t.Fatalf("the fence's discharge ignored the volume evidence: %v", w.stats)
}
+ w.drive(200, never, w.actAll(), w.recoveryPass, w.wakeExec)
+ if !w.owesLocal(w.claim, from) {
+ t.Fatalf("the dead box's park-local closed without the operator: %s", w.state())
+ }
w.finish(t) // the operator's destroyed-local declaration clears it
+ if w.owesLocal(w.claim, from) {
+ t.Fatalf("the park-local is still open after the operator's cleanup: %s", w.state())
+ }
})
}
diff --git a/internal/sim/hostlife/regionha_round1_test.go b/internal/sim/hostlife/regionha_round1_test.go
index ad0f45d10..3f56952b1 100644
--- a/internal/sim/hostlife/regionha_round1_test.go
+++ b/internal/sim/hostlife/regionha_round1_test.go
@@ -408,6 +408,127 @@ func TestFailoverPinWaitsOutTheDelay(t *testing.T) {
w.mustHold(t)
}
+// TestFailoverPinWaitsForTheAcknowledgement (reloc-failover-ack-before-pin;
+// rev 5, Astra round 2 finding 1; 1b-next rev 19 PinFailover): the
+// executor's newer files manifest is still in flight when it is
+// terminated. The target is named, but its controller does not run, so
+// it has not acknowledged; the pin waits past the delay, the manifest
+// lands, and only then does the target acknowledge. The pin names the
+// newer manifest. The mutation pins before the acknowledgement, and the
+// pin misses it.
+func TestFailoverPinWaitsForTheAcknowledgement(t *testing.T) {
+ w := twoBoxWitness()
+ from := w.boxes[0]
+ w.serve(from, 1, app0)
+ w.running(t, from)
+ w.published(t, from)
+ spare := w.extraBox(0, 30) // a second live box of the region: the worker while the target's controller is down
+ c := w.claim
+ loc, gen := c.Holder.Location, c.Holder.Gen
+ from.Files.Env++ // a newer files state: the admin token rotated
+ newer := manifestKey(loc, gen, from.pubSeq+1)
+ w.holdKey(newer)
+ w.publishFiles(from)
+ w.hold = nil
+ if from.pubSeq == 0 || manifestKey(loc, gen, from.pubSeq) != newer {
+ t.Fatalf("the newer manifest was not issued: %s", w.state())
+ }
+ w.terminate(from)
+ if !w.stepUntil(t, 400, "the failover's target named", func() bool {
+ c := w.claim
+ return c.Op.Kind == "relocating" && (c.Op.Tgt >= 0 || c.Op.Pin != nil)
+ }) {
+ w.mustHold(t)
+ }
+ if w.claim.Op.Pin != nil {
+ t.Fatalf("pinned before a target was named and acknowledged: %s", w.state())
+ }
+ tgt := w.boxByID(w.claim.Op.Tgt)
+ worker := spare
+ if tgt == spare {
+ worker = w.boxes[3]
+ }
+ w.drive(failoverPinDelay+20, never, w.act(worker)) // the target's controller does not run
+ if contains(w.claim.Op.Acks, tgt.ID) {
+ t.Fatalf("the target acknowledged without running")
+ }
+ if p := w.claim.Op.Pin; p != nil {
+ t.Fatalf("pinned %s before the target acknowledged: %s", p.ManKey, w.state())
+ }
+ if n := w.completeHeld(newer); n != 1 {
+ t.Fatalf("held manifest PUTs completed: %d, want 1", n)
+ }
+ if !w.reach(t, 400, "the pin", func() bool { return w.claim.Op.Pin != nil }, w.act(worker, tgt)) {
+ w.mustHold(t)
+ }
+ if p := w.claim.Op.Pin; p.ManKey != newer {
+ t.Fatalf("the pin names %s, want the manifest that landed while the target had not acknowledged, %s", p.ManKey, newer)
+ }
+ w.servingOn(t, tgt)
+ w.finish(t)
+ w.mustHold(t)
+}
+
+// TestConvertedMovePinsBeforeAcknowledgement (rev 6, Astra round 3
+// finding 1): a move whose source is terminated before the flip becomes
+// a relocation at pinning (moves §7.10). It enters pinning directly, as
+// it does in 1b-next, where Worker.pinning selects and journals the pin
+// first and checks the acknowledgements only for ToInstalling: the pin is
+// journaled before the box that installs has acknowledged, and that box's
+// acknowledgement still comes before the installing CAS. Under rev 5's
+// wider guard the target acknowledged first, and this test fails.
+func TestConvertedMovePinsBeforeAcknowledgement(t *testing.T) {
+ w := twoBoxWitness()
+ src := w.boxes[0]
+ w.serve(src, 1, app0)
+ w.running(t, src)
+ w.published(t, src)
+ w.moveTo(1)
+ if w.claim.Op.Kind != "moving" {
+ t.Fatalf("no move: %s", w.state())
+ }
+ tgt := w.boxByID(w.claim.Op.Tgt)
+ w.reach(t, 100, "staging begins", func() bool {
+ c := w.claim
+ return c.Op.Kind == "moving" && c.Op.Phase == "preparing" && contains(c.Regions, tgt.Region)
+ }, w.act(src, tgt))
+ w.terminate(src)
+ var acksAtPin []int
+ if !w.stepUntil(t, 400, "the converted move's pin", func() bool {
+ c := w.claim
+ if c.Op.Kind == "relocating" && c.Op.Pin != nil {
+ acksAtPin = append([]int(nil), c.Op.Acks...)
+ return true
+ }
+ return false
+ }) {
+ w.mustHold(t)
+ }
+ if c := w.claim; c.Op.FenceBox != src.ID || c.Op.PinFailover {
+ t.Fatalf("not a converted move: %s", w.state())
+ }
+ var installer int = -1
+ if !w.stepUntil(t, 1500, "installing", func() bool {
+ c := w.claim
+ if c.Op.Kind == "relocating" && c.Op.Phase == "installing" {
+ installer = c.Op.Exec
+ if !acked(c) {
+ t.Fatalf("installing without the acknowledgements: %s", w.state())
+ }
+ return true
+ }
+ return false
+ }) {
+ w.mustHold(t)
+ }
+ if contains(acksAtPin, installer) {
+ t.Fatalf("box %d acknowledged before the pin: a converted move waited for PinFailover's barrier", installer)
+ }
+ w.servingOn(t, w.boxByID(installer))
+ 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.
@@ -451,10 +572,12 @@ func TestPinNeverShortOfTheRelease(t *testing.T) {
// admission, marker publication and replication opening"): the target's
// agent crashes exactly at each boundary of P's first admitted session:
// admitted with the app starting (its launch environment held unready),
-// admitted with generation.json's PUT in flight (held), and replication
-// open; in a one-box and a two-box region.
+// admitted with generation.json's PUT in flight (held), generation.json
+// published and replication not yet open (rev 5, Astra round 2: the
+// witness yield openYield stops the start between the two), and
+// replication open; in a one-box and a two-box region.
func TestCrashAtEachOpenBoundary(t *testing.T) {
- for _, stage := range []string{"app", "marker", "open"} {
+ for _, stage := range []string{"app", "marker", "published", "open"} {
t.Run(stage, func(t *testing.T) {
bothShapes(t, func(t *testing.T, w *world, boxes int) {
from := w.serveAndPublish(t)
@@ -468,6 +591,16 @@ func TestCrashAtEachOpenBoundary(t *testing.T) {
if stage == "marker" {
w.holdKey(genMarkerKey(loc))
}
+ yielded := false
+ if stage == "published" {
+ w.openYield = func(b *box) bool {
+ if yielded || b.open == nil || !b.open.Prepared {
+ return false
+ }
+ yielded = true
+ return true
+ }
+ }
var to *box
hit := w.stepUntil(t, 2000, "P's open at "+stage, func() bool {
c := w.claim
@@ -481,6 +614,15 @@ func TestCrashAtEachOpenBoundary(t *testing.T) {
if stage == "open" {
return preparedOpened(c) && to.open == nil && hasMain(to)
}
+ if stage == "published" {
+ if !yielded || to.open == nil || to.open.stage != "open" {
+ return false
+ }
+ if g, _ := w.bucketGen(to, loc); g != to.open.Gen {
+ t.Fatalf("yielded before generation.json named %q", to.open.Gen)
+ }
+ return true
+ }
return to.open != nil && to.open.Prepared && to.open.stage == stage
})
if !hit {
@@ -488,7 +630,7 @@ func TestCrashAtEachOpenBoundary(t *testing.T) {
}
w.crash(to)
to.envUnreadyFor = 0
- w.hold = nil
+ w.hold, w.openYield = nil, nil
w.servingOn(t, nil)
w.finish(t)
})
diff --git a/internal/sim/hostlife/regionha_test.go b/internal/sim/hostlife/regionha_test.go
index 11c1ee7af..28784de7d 100644
--- a/internal/sim/hostlife/regionha_test.go
+++ b/internal/sim/hostlife/regionha_test.go
@@ -530,6 +530,33 @@ func (w *world) relocationLeftovers(n *claim, op opState) {
w.stats["relocation: abandoned prepared generation parked"]++
}
}
+ // the pinned manifest of a superseded generation (rev 5): the files
+ // live set kept it while the operation ran, so a park-generation of
+ // that generation that ran meanwhile left it; once the operation
+ // completes it is a dead generation's key, parked here. This is the
+ // model's abstraction, not a CompleteRelocation guarantee (rev 6,
+ // Astra round 3 finding 2): in 1b-next rev 19 completion queues only
+ // the local chores and the abandoned prepared generations; an obsolete
+ // files manifest is the at-rest sweep's (claim §6.2a), and the
+ // pinner's retained control object is the storage follow-up's (1b-next
+ // ruling 21). The model parks it at once so INV-10 can check the
+ // residue at completion
+ if h := n.Holder; h != nil && op.Pin != nil && op.Pin.ManKey != "" && op.Pin.ManGen != h.Gen {
+ ret := op.Pin.ManGen
+ if ret == "" {
+ ret = "@root"
+ }
+ queued := false
+ for _, o := range n.Obl {
+ if o.Kind == "park-generation" && o.Region == op.SrcRegion && o.Ret == ret && o.Prefix == h.Location {
+ queued = true
+ }
+ }
+ if !queued {
+ n.Obl = append(n.Obl, w.scoped(obligation{ID: w.newID("ob"), Op: op.ID, Kind: "park-generation", Region: op.SrcRegion, Box: -1, Prefix: h.Location, Ret: ret, Quiet: w.now + horizonH}, w.now, h.Inc))
+ w.stats["relocation: the pinned manifest's generation parked"]++
+ }
+ }
owed := append([]int{op.Src}, op.InstalledOn...)
for _, id := range owed {
if id < 0 || id == op.Exec || contains(op.Discharged, id) {
@@ -546,8 +573,10 @@ func (w *world) relocationLeftovers(n *claim, op opState) {
// drain leaves starting for releasing once both participants' execution
// leases are current (role() writes them on every read of the claim), and
// the CAS records releasing_since for the release deadline; a failover
-// never enters starting in this model (it starts at pinning, Task 3). The
-// mutation of reloc-exec-ack-barrier moves on with no acknowledgement.
+// never enters starting in this model (it starts at pinning, Task 3, and
+// PinFailover's barrier is checked there before the pin is selected:
+// rule reloc-failover-ack-before-pin, rev 5 and 6). The mutation of
+// reloc-exec-ack-barrier moves on with no acknowledgement.
func (w *world) relocStarting(b *box, c *claim) {
op := c.Op
if on("reloc-exec-ack-barrier") && !acked(c) {
@@ -633,8 +662,41 @@ func (w *world) relocReleasing(b *box, c *claim) {
// target for a new installation (ToInstalling): a new stamp, journaled as
// install_stamp, and a fresh prepared generation id (claim R6-4). The
// target must owe no park-local for the host.
+//
+// An initial failover (op.PinFailover: 1b-next's starting after
+// StartRelocation with a fence) first passes PinFailover's barrier (rev
+// 5, Astra round 2 finding 1; narrowed in rev 6, round 3 finding 1): the
+// target is named, every participant has acknowledged, and the PinFailover
+// CAS clears the flag, all before any pin is selected; so a manifest that
+// lands while the target's controller is unavailable is in the pin (rule
+// reloc-failover-ack-before-pin). The flag is the model's starting
+// (ruling 4). A converted move, a nested failover after a replacement and
+// an operator's replay enter pinning directly, as in 1b-next, where
+// Worker.pinning selects and journals the pin first and checks the
+// acknowledgements only for ToInstalling. The mutation selects the pin
+// before the barrier, as rev 4 did.
func (w *world) relocPinning(b *box, c *claim) {
- op, h := c.Op, c.Holder
+ op := c.Op
+ if op.PinFailover && on("reloc-failover-ack-before-pin") {
+ if op.Tgt < 0 {
+ w.relocNameTarget(c)
+ return
+ }
+ if !acked(c) {
+ w.stats["failover pin: waits for the acknowledgements"]++
+ return
+ }
+ if w.cas(c, func(n *claim) bool {
+ ok := sameOp(n.Op.ID, op.ID) && n.Op.Kind == "relocating" && n.Op.Phase == "pinning" && n.Op.PinFailover && n.Op.Tgt == op.Tgt && n.Op.Stuck == ""
+ if ok {
+ n.Op.PinFailover = false
+ }
+ return ok
+ }) {
+ w.logf("relocation %s: PinFailover, box %d acknowledged", op.ID, op.Tgt)
+ }
+ return
+ }
if op.Pin == nil {
if on("reloc-failover-pin-delay") && (op.Release == nil || on("reloc-pin-delay-every-fence")) && w.now < latestObservation(op)+failoverPinDelay {
return
@@ -659,17 +721,7 @@ func (w *world) relocPinning(b *box, c *claim) {
return
}
if op.Tgt < 0 {
- to := w.chooseBoxExcept(op.SrcRegion, h.App, relocExcept(op)...)
- if to == nil {
- return // no eligible box: the recovery pass alerts once (moves §7.10)
- }
- w.cas(c, func(n *claim) bool {
- ok := sameOp(n.Op.ID, op.ID) && n.Op.Kind == "relocating" && n.Op.Phase == "pinning" && n.Op.Tgt < 0
- if ok {
- ok = w.nameReplacement(n, to.ID, "pinning")
- }
- return ok
- })
+ w.relocNameTarget(c)
return
}
if on("reloc-exec-ack-barrier") && !acked(c) {
@@ -691,6 +743,23 @@ func (w *world) relocPinning(b *box, c *claim) {
}
}
+// relocNameTarget is NameTarget at pinning: choose() in the source region
+// over the eligible boxes, the excluded ones left out.
+func (w *world) relocNameTarget(c *claim) {
+ op := c.Op
+ to := w.chooseBoxExcept(op.SrcRegion, c.Holder.App, relocExcept(op)...)
+ if to == nil {
+ return // no eligible box: the recovery pass alerts once (moves §7.10)
+ }
+ w.cas(c, func(n *claim) bool {
+ ok := sameOp(n.Op.ID, op.ID) && n.Op.Kind == "relocating" && n.Op.Phase == "pinning" && n.Op.Tgt < 0
+ if ok {
+ ok = w.nameReplacement(n, to.ID, "pinning")
+ }
+ return ok
+ })
+}
+
// abandonPrepared is abandonPrepared(c) in hostclaim (1b-next ruling
// 27, rev 18 finding 3): before an unopened P is replaced or dropped, it
// is journaled in abandoned_prepared, so the serving CAS parks it. Every
@@ -1594,11 +1663,14 @@ func (w *world) deadBoxFiles(x *box) *filesDir {
// startFailover is the fence's start of a relocation for a serving
// executor (§5.8 reason failover, StartRelocation with a fence; spec 3's
// placer supplies the decision): op.exec none, the stamp kept, at pinning
-// with the target named there (ruling 4); the pin waits out
+// with the target named there (ruling 4); op.PinFailover stands for
+// 1b-next's starting, so the target is named and acknowledges before the
+// pin is selected (PinFailover's barrier, rule
+// reloc-failover-ack-before-pin, rev 5 and 6), and the pin waits out
// failoverPinDelay from the fence.
func (w *world) startFailover(n *claim, x *box) {
n.Op = opState{Kind: "relocating", ID: w.newID("rl"), Phase: "pinning", Exec: -1, Src: x.ID, Tgt: -1, SrcRegion: x.Region,
- RelocReason: "failover", ReqAt: w.now, App: n.Holder.App, SrcGen: n.Holder.Gen, SrcStamp: n.Holder.Stamp, StopFiles: w.deadBoxFiles(x)}
+ RelocReason: "failover", ReqAt: w.now, App: n.Holder.App, SrcGen: n.Holder.Gen, SrcStamp: n.Holder.Stamp, StopFiles: w.deadBoxFiles(x), PinFailover: true}
w.stats["relocation started: failover"]++
}
@@ -1608,8 +1680,10 @@ func (w *world) startFailover(n *claim, x *box) {
// the barrier, its files directory the publisher's stand-in; after its
// release only its liveness changes. (1b-next keeps a source lost in
// starting at starting until the remaining participant acknowledges,
-// then PinFailover; the model goes to pinning at once, where the pin
-// waits out the delay and installing waits for the barrier.) The
+// then PinFailover; the model goes to pinning at once with
+// op.PinFailover set for a source lost in starting, so the target
+// acknowledges before the pin is selected, rule
+// reloc-failover-ack-before-pin, and the pin waits out the delay.) The
// mutation of reloc-source-loss takes a source lost in releasing as
// released at what the remote holds, so its unuploaded writes go
// undeclared.
@@ -1622,6 +1696,7 @@ func (w *world) fenceSource(n *claim, x *box) {
n.Op.Exec, n.Op.Phase = -1, "pinning"
return
}
+ n.Op.PinFailover = n.Op.Phase == "starting" // 1b-next keeps it in starting until PinFailover (rev 6)
n.Op.RelocReason, n.Op.Exec, n.Op.Phase = "failover", -1, "pinning"
n.Op.Release, n.Op.StopFiles = nil, w.deadBoxFiles(x)
w.stats["relocation: source lost before its release, converted to failover"]++
diff --git a/internal/sim/hostlife/rules_test.go b/internal/sim/hostlife/rules_test.go
index 598d7ba0a..034684e3b 100644
--- a/internal/sim/hostlife/rules_test.go
+++ b/internal/sim/hostlife/rules_test.go
@@ -197,4 +197,5 @@ 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-failover-ack-before-pin", // rev 5 and 6 (Astra rounds 2 and 3; 1b-next rev 19 PinFailover): an initial failover (op.PinFailover, the model's starting) selects its pin only after the target is named and every participant acknowledged; converted moves, nested failovers and replays pin first, as Worker.pinning does; the mutation pins first, and a manifest that lands while the target's controller is unavailable is left out (a loss bound: TestFailoverPinWaitsForTheAcknowledgement)
}
diff --git a/internal/sim/hostlife/world_test.go b/internal/sim/hostlife/world_test.go
index a1b97b293..f901aeded 100644
--- a/internal/sim/hostlife/world_test.go
+++ b/internal/sim/hostlife/world_test.go
@@ -837,6 +837,7 @@ type opState struct {
ReleasingSince int // releasing_since: the release deadline's start (ruling 14)
Attempts int // probe_attempts.<op.exec>: counted before each attempt, at most probeTries (ruling 19)
PreparedOpened string // prepared_opened: journaled by the admission that opened P (rev 12 S1)
+ PinFailover bool // (rev 6) the initial failover's starting, 1b-next's StartRelocation with a fence: set by startFailover and by a drain's source lost in starting, cleared by the PinFailover CAS once the target is named and every participant has acknowledged
Resolved bool // an operator's resolve (model ruling 13): the source is eligible as a target again, and an empty listing is accepted
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)
@@ -1086,6 +1087,11 @@ type world struct {
// startHook runs right after the app starts, before replication opens:
// a witness's background worker acknowledging work (R10-1)
startHook func(b *box) bool // true: the hook crashed the box
+ // openYield (rev 5, Astra round 2 on claim §11's open boundaries): a
+ // witness's yield after generation.json names the new generation and
+ // before replication opens; true: the start returns there and resumes
+ // at "open" on the next call. Nil outside the witnesses
+ openYield func(b *box) bool
// lastIssued is the request issue saw last, for a caller that needs
// the request object behind a helper's return value (resumeOpen)
lastIssued *request