amadan
sim: stale comments corrected: reloc-pin-evidenced-empty is caught by its witness, relocRelease's steps name the flush and receipt rules, startFailover names its target at the start, and mutate.sh's STALE verdict cites the merged expectations at two boxes (final review minor 7)
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
3 files changed,
+24
−13
internal/sim/hostlife/mutate.sh+4 −2internal/sim/hostlife/regionha_test.go+19 −10internal/sim/hostlife/rules_test.go+1 −1
diff --git a/internal/sim/hostlife/mutate.sh b/internal/sim/hostlife/mutate.sh| index 27579b126..72501c06c 100755 |
| --- a/internal/sim/hostlife/mutate.sh |
| +++ b/internal/sim/hostlife/mutate.sh |
| @@ -71,8 +71,10 @@ if [ -n "${HOSTLIFE_LIST:-}" ]; then |
| fi |
| mkdir -p "$SCRATCH/logs" "$SCRATCH/verdicts" || { echo "cannot create $SCRATCH" >&2; exit 2; } |
| EXPECT="$PKG/expected-outcomes.txt" |
| +EXPECT_NAME=expected-outcomes.txt # the file the verdicts cite |
| if [ "$SHAPE" = 2 ] && [ -f "$PKG/expected-outcomes.two-box.txt" ]; then |
| EXPECT="$SCRATCH/expected-outcomes.merged" |
| + EXPECT_NAME="expected-outcomes.txt merged with expected-outcomes.two-box.txt" |
| awk 'FNR==NR { if ($0 !~ /^#/ && NF) ov[$1]=$0; next } !($1 in ov)' "$PKG/expected-outcomes.two-box.txt" "$PKG/expected-outcomes.txt" >"$EXPECT" |
| awk '$0 !~ /^#/ && NF && $2 != "-"' "$PKG/expected-outcomes.two-box.txt" >>"$EXPECT" |
| fi |
| @@ -150,7 +152,7 @@ one() { |
| fi |
| if [ $caught -eq 1 ]; then |
| if [ "$expect" = "missed" ]; then |
| - echo "STALE $r [boxes=$SHAPE]: $sweep; witness $wit; but expected-outcomes.txt says missed" | tee "$verdict" |
| + echo "STALE $r [boxes=$SHAPE]: $sweep; witness $wit; but $EXPECT_NAME says missed" | tee "$verdict" |
| else |
| echo "CAUGHT $r [boxes=$SHAPE]: $sweep; witness $wit" | tee "$verdict" |
| fi |
| @@ -163,7 +165,7 @@ one() { |
| fi |
| } |
| export -f one |
| -export SEEDS PKG SCRATCH BIN WRULES SHAPE EXPECT |
| +export SEEDS PKG SCRATCH BIN WRULES SHAPE EXPECT EXPECT_NAME |
| printf '%s\n' $RULES | xargs -P "${HOSTLIFE_PAR:-8}" -I{} bash -c 'one "$@"' _ {} |
| xrc=$? |
| if [ $xrc -ne 0 ]; then |
diff --git a/internal/sim/hostlife/regionha_test.go b/internal/sim/hostlife/regionha_test.go| index b13fcb347..92840e779 100644 |
| --- a/internal/sim/hostlife/regionha_test.go |
| +++ b/internal/sim/hostlife/regionha_test.go |
| @@ -130,11 +130,18 @@ func relocExcept(op opState, extra ...int) []int { |
| // tree stopped and empty; an escaped descendant fails the step (L10); |
| // 2. flush: the final checkpoint and SyncAndWait, passing only once the |
| // listing shows the stopped database's position N (moves §5.1 step |
| -// 1). When the session's replicator died with its agent (claim rev |
| -// 6.10) nothing can flush: the entry names what the remote holds, |
| -// Flushed false, and the next admission declares the rest; |
| -// 3. publish every pending file and wake-state mutation: the entry |
| -// carries them until Task 4's manifest. |
| +// 1). It needs the session's own replicator and the box's own files |
| +// directory, or the positions this box recorded for this stop (rule |
| +// reloc-release-needs-flush, rev 9). When the replicator died with |
| +// its agent (claim rev 6.10) and nothing was recorded there is no |
| +// release, and the release deadline makes the operation stuck; the |
| +// mutation journals what the remote holds, Flushed false; |
| +// 3. publish every pending file and wake-state mutation as one final |
| +// manifest of the generation (ReleaseFlushFiles, Task 4); |
| +// 4. record the positions, then the producers' drain and root's |
| +// receipt; recorded positions finish a release only for the |
| +// controller that recorded them or with that receipt (rule |
| +// 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" { |
| @@ -1782,11 +1789,13 @@ 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); 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. |
| +// with op.PinFailover standing for 1b-next's starting (ruling 4). The |
| +// start names the target to and makes it the only participant (rev 7, |
| +// Astra round 4 finding 3); only the mutation of |
| +// reloc-failover-start-guard starts with none, and pinning names one. |
| +// The target 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, to *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), PinFailover: true} |
diff --git a/internal/sim/hostlife/rules_test.go b/internal/sim/hostlife/rules_test.go| index baa39e93d..bfe2660e6 100644 |
| --- a/internal/sim/hostlife/rules_test.go |
| +++ b/internal/sim/hostlife/rules_test.go |
| @@ -162,7 +162,7 @@ var allRules = []string{ |
| "reloc-drain-needs-writer", // 1b-next ruling 11 (Worker.Start): a host that never admitted a writer is never drained, only failed over; liveness (expected miss) |
| "reloc-ack-before-pinning", // 1b-next rev 4 N6 (PinAfterRelease requires requireAcks from releasing): a target replaced in releasing acknowledges before the operation leaves the phase; defence in depth (expected miss) |
| "reloc-pin-claim-gen", // 1b-next ruling 16 (JournalPin, RecoveryPinKey pin-<gen>.json): a pin is journaled only against the claim version it was selected against; the mutation journals a pin selected before a nested reset |
| - "reloc-pin-evidenced-empty", // 1b-next ruling 15 (JournalPin, StorePinner's Empty evidence): an empty pin needs a release flushed at 0 or a holder that never had a writer; otherwise stuck for an operator (expected miss: the model's listings are exact and the probe declares) |
| + "reloc-pin-evidenced-empty", // 1b-next ruling 15 (JournalPin, StorePinner's Empty evidence): an empty pin needs a release flushed at 0 or a holder that never had a writer; otherwise stuck for an operator; the mutation pins the empty listing and the install loses the durable writes (caught by its witness, INV-2) |
| "reloc-release-deadline", // 1b-next ruling 14 (Worker.releaseOverdue, ReleaseDeadline): a release not journaled 10 minutes after releasing or probe-failed began marks the operation stuck; the mutation waits forever (INV-3) |
| "reloc-probe-attempts", // 1b-next ruling 19 (BeginProbeAttempt, MaxProbeAttempts): each probe attempt is counted in the claim before it is made, the fourth is probe-failed; liveness (expected miss) |
| "reloc-ensure-local", // 1b-next rev 15 finding 2 (Effects.EnsureLocal): before P's first admission the local install is verified, and restored under the same install_stamp if a lost lease's scoped cleanup retired it; the mutation admits over a missing install |