amadan
sim: mutate.sh reports the shape (HOSTLIFE_BOXES), runs the region HA rules as a group and lists without running; expected-outcomes.txt lists the region HA rules caught only in combination or bounded by liveness, loss, determinism or the operator, with the test that shows each
Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
2 files changed,
+53
−14
internal/sim/hostlife/expected-outcomes.txt+28 −0internal/sim/hostlife/mutate.sh+25 −14
diff --git a/internal/sim/hostlife/expected-outcomes.txt b/internal/sim/hostlife/expected-outcomes.txt| index 72504e3d2..f46fe7b7b 100644 |
| --- a/internal/sim/hostlife/expected-outcomes.txt |
| +++ b/internal/sim/hostlife/expected-outcomes.txt |
| @@ -21,3 +21,31 @@ admit-bind-op missed caught with claim-cas-opid: the model's general CAS conditi |
| hostguard rare 30000 the guard's race is reached by the sweep at 30,000 (2 / 30,000 on rev 7.11; 5 / 3,000 on rev 7.10, before the admitting CAS moved ahead of the start) |
| stale-hold-release rare 30000 reached at 30,000 (15 / 30,000 on rev 7.11; 2 / 3,000 on rev 7.10) |
| strict-spawn rare 30000 its witness holds alone (the combination with evidence-whole-tree is the witness's); the sweep reaches it at 30,000 (1 / 30,000 on rev 7.11; 3 / 3,000 on rev 7.10) |
| +create-choice-once missed no box-side effect precedes the serving CAS in this model, so a substituted executor leaves nothing behind; the rule's effect is the cancellation of a create whose box is gone (TestCreateNamesItsExecutorOnce fails under the mutation) |
| +reloc-start-guard missed the chooser's §2 eligibility already excludes a target owing a park-local, a live source never owes one for the host it serves, and a whole-location chore cannot be pending in the region the host serves in (a move into it waits, CC11); TestRelocationStartGuardRefuses shows the refusal |
| +reloc-exec-ack-barrier missed liveness in the sweep: without the barrier a target that never acknowledged is handed op.exec and the operation waits there instead; TestReplacementWithoutAcknowledgementHoldsEachTransition fails under the mutation (rev 4) |
| +reloc-pin-reaches-release missed the release's step 2 already waits for the listing to show N, so in the sweep the pin's own check is never the first to see a short listing; TestPinNeverShortOfTheRelease hides the newest file after the release and fails under the mutation (rev 4) |
| +reloc-failover-pin-delay missed a loss bound, not a safety bound (§5.8): the pin names exact versions and a later PUT adds a version nothing reads; TestFailoverPinWaitsOutTheDelay fails under the mutation (rev 4) |
| +reloc-exec-only-installs missed every installing CAS is conditional on op.exec, so in the sweep a non-executor's writes are the same create-only objects and its install is retired by its park-local; TestOnlyTheExecutorWritesP lets only the source act at installing and fails under the mutation (rev 4) |
| +reloc-install-receipt missed caught with reloc-ensure-local (witness): EnsureLocal restores a replacement's missing install whatever the receipt says, as 1b-next rev 14 found ("each covers the other") |
| +reloc-row-cases missed caught with exec-admission and exec-writer (witness): a reopened stale row routes a request to a box the exec check and AdmitWriter refuse |
| +reloc-replacement-cap missed an operator bound: without the cap the operation replaces its target a third time instead of waiting for carlos ops host resolve; TestStuckAfterTwoReplacements fails under the mutation |
| +reloc-drain-needs-writer missed liveness only (1b-next ruling 11): a never-woken host's drain would wait for a release root refuses, until the release deadline; TestDrainRefusedForANeverWokenHost fails under the mutation |
| +reloc-ack-before-pinning missed defence in depth (1b-next rev 4 N6): installing still waits for the barrier, so a replaced target that never acknowledged holds the operation at pinning instead of releasing; TestReplacedTargetAcknowledgesBeforePinning fails under the mutation |
| +reloc-probe-attempts missed liveness only (ruling 19): uncounted attempts still end at the probe deadline; TestProbeAttemptsCountedBeforeTheyAreMade fails under the mutation |
| +fence-terminated-only missed redundant alone: a stopped box fenced by mistake is on lost, so lost-quarantine retires its state and exec-admission refuses it when it starts again; TestStoppedBoxNeverFenced fails under the mutation |
| +reloc-replacement-table missed after P's first admission the admission rules (recovery-generation, remote-baseline) already refuse reopening P, so resuming at installed with the same P admits a fresh generation from P's remote, as the nested failover does; TestL18NestedFailover fails under the mutation (no nested failover) |
| +files-pin-exact missed a determinism rule (§5.8): a later manifest PUT adds a version nothing reads; TestInstallAppliesThePinnedManifest lands the newer manifest between the pin and the install and fails under the mutation (rev 4) |
| +reloc-abandoned-prepared missed the at-rest sweep, which 1b-next ruling 27 keeps as the backstop, retires an unrecorded P before any invariant sees it; the operation's own park is the rule's effect, and TestAbandonedPreparedGenerationParked (both paths) fails under the mutation |
| +reloc-stuck-refuses-admission missed the stuck operation's live source is still op.exec, so admitting its wake makes no second writer; the refusal keeps a stuck operation from running anything until the operator resolves it (ruling 9); TestStuckSourceRefusesAdmission fails under the mutation |
| +ha-sole-box-eligibility missed the sweep's HA regions keep two boxes until a termination, and a depleted region's last box is normally eligible; TestHASoleBoxIsCheckedLikeAnyOther checks each refusal and fails under the mutation |
| +reloc-pin-delay-every-fence missed a loss bound like reloc-failover-pin-delay; TestPinWaitsForEveryFenceObservation replaces the target after the source's release and fails under the mutation |
| +reloc-deadline-from-observed-at missed liveness: a deadline from the termination marks stuck earlier than 1b-next would, which the operator then resolves; TestDeadTargetDeadlineFromObservation delays the observation past the deadline and fails under the mutation |
| +tie-hash-host missed a preference: either winner is a correct choice; TestTieHashFollowsTheHost computes both hosts' winners independently and fails under the mutation |
| +reloc-failover-ack-before-pin missed a loss bound like reloc-failover-pin-delay: an initial failover's pin selected before its target acknowledged misses only files that land later, and the sweep's controllers acknowledge within a step of being named; TestFailoverPinWaitsForTheAcknowledgement holds the target's controller while the newer manifest lands and fails under the mutation |
| +reloc-name-before-pin missed a loss bound like reloc-failover-pin-delay: a converted move's or a replay's pin selected before a target is named misses only files that land while no box is eligible; TestConvertedMoveWaitsForATargetBeforeItsPin holds every box ineligible while the newer manifest lands and fails under the mutation |
| +reloc-failover-start-guard missed a fidelity guard: the mutation starts the failover earlier (no target yet, admission closed, a park-replica outstanding), and no model invariant distinguishes the earlier start, whose target is then named at pinning; TestFailoverStartWaitsForAdmission and TestFailoverStartWaitsForParkReplica fail under the mutation |
| +reloc-fence-pending-blocks missed a fidelity guard: under the mutation the phase moves on while a dead target's fence waits for a spare, and the fence is consumed later by the replacement table at whatever phase the operation reached, which no model invariant distinguishes; TestPendingTargetFenceHoldsThePhase fails under the mutation |
| +reloc-release-needs-flush missed a fidelity guard: the mutation's unflushed release is legal in the model (the next admission declares what the remote does not hold, as writes_lost), so no invariant fails, but 1b-next refuses it and waits for the deadline; TestReleaseRefusedAfterACrashBeforeTheFlush and TestReleaseReplaysTheRecordedFlush fail under the mutation |
| +operator-stop-unrecoverable-only missed a fidelity guard on the operator's resolve: the mutation stops a target that could still release, and the declared loss and replay that follow are legal in the model, so no invariant fails; TestOperatorResumesASlowRelease and TestOperatorResumesARecordedFlush fail under the mutation |
| +reloc-release-needs-receipt missed a fidelity guard: under the mutation recorded positions replay without root's receipt, and the release they journal is the flushed one, so no model invariant fails, but 1b-next refuses it after a restart; TestReleaseRefusedAfterACrashBeforeTheReceipt and TestOperatorStopsATargetWithNoReceipt fail under the mutation |
diff --git a/internal/sim/hostlife/mutate.sh b/internal/sim/hostlife/mutate.sh| index c583d97f5..883996ece 100755 |
| --- a/internal/sim/hostlife/mutate.sh |
| +++ b/internal/sim/hostlife/mutate.sh |
| @@ -9,6 +9,9 @@ |
| # internal/sim/hostlife/mutate.sh 3000 # every rule |
| # internal/sim/hostlife/mutate.sh 30000 rule-a rule-b # named rules |
| # internal/sim/hostlife/mutate.sh 30000 rule-a,rule-b # a combination, dropped together |
| +# HOSTLIFE_BOXES=2 internal/sim/hostlife/mutate.sh 3000 # the two-box shape (region HA L18); unset is one box per region |
| +# HOSTLIFE_BOXES=2 internal/sim/hostlife/mutate.sh 3000 @regionha # the region HA rules alone (rules_test.go's region HA block) |
| +# HOSTLIFE_LIST=1 internal/sim/hostlife/mutate.sh 0 @regionha # print the rules a run would check, and run nothing |
| # |
| # Each rule gets two runs under its mutation (rev 7.3): the random sweep |
| # (TestHostLifecycle over the seeds) and the rule's deterministic witness |
| @@ -50,6 +53,18 @@ ROOT=$(git -C "$(dirname "$0")" rev-parse --show-toplevel) |
| PKG="$ROOT/internal/sim/hostlife" |
| SCRATCH=${HOSTLIFE_SCRATCH:-${TMPDIR:?}/hostlife-sim} |
| BIN=${HOSTLIFE_BIN:-$SCRATCH/hostlife.test} |
| +SHAPE=${HOSTLIFE_BOXES:-1} |
| +RULES="$*" |
| +if [ -z "$RULES" ]; then |
| + RULES=$(sed -n '/^var allRules/,/^}/p' "$PKG/rules_test.go" | grep -o '^\s*"[a-z0-9-]*"' | tr -d ' "\t') |
| +elif [ "$RULES" = "@regionha" ]; then |
| + # every rule of the region HA block: one mutation check per guard |
| + RULES=$(sed -n '/^\t\/\/ region HA (two boxes per region, L18)/,/^}/p' "$PKG/rules_test.go" | grep -o '^\s*"[a-z0-9-]*"' | tr -d ' "\t') |
| +fi |
| +if [ -n "${HOSTLIFE_LIST:-}" ]; then |
| + printf '%s\n' $RULES |
| + exit 0 |
| +fi |
| mkdir -p "$SCRATCH/logs" "$SCRATCH/verdicts" || { echo "cannot create $SCRATCH" >&2; exit 2; } |
| if [ ! -x "$BIN" ]; then |
| echo "no test binary at $BIN; build it with: go test -c -o $BIN ./internal/sim/hostlife/" >&2 |
| @@ -59,10 +74,6 @@ if [ -n "$(find "$PKG" -name '*.go' -newer "$BIN")" ]; then |
| echo "the test binary $BIN is older than the source; rebuild it" >&2 |
| exit 2 |
| fi |
| -RULES="$*" |
| -if [ -z "$RULES" ]; then |
| - RULES=$(sed -n '/^var allRules/,/^}/p' "$PKG/rules_test.go" | grep -o '^\s*"[a-z0-9-]*"' | tr -d ' "\t') |
| -fi |
| # the rules that have witnesses (witness_test.go): a run of one of them |
| # with no witness output is an ERROR, never "none" (R3-6) |
| WRULES=$(grep -o '^\s*{"[a-z0-9-]*",' "$PKG/witness_test.go" | tr -d ' \t{",' | sort -u) |
| @@ -75,7 +86,7 @@ one() { |
| verdict="$SCRATCH/verdicts/$tag" |
| for x in $(echo "$r" | tr ',' ' '); do |
| if ! sed -n '/^var allRules/,/^}/p' "$PKG/rules_test.go" | grep -q "^\s*\"$x\","; then |
| - echo "ERROR $r: no rule named $x" | tee "$verdict" |
| + echo "ERROR $r [boxes=$SHAPE]: no rule named $x" | tee "$verdict" |
| return |
| fi |
| done |
| @@ -108,19 +119,19 @@ one() { |
| wit=held |
| fi |
| if [ $wrc -ne 0 ] || grep -q "^panic:\|test timed out" "$wlog"; then |
| - echo "ERROR $r: witness run rc=$wrc; see $wlog" | tee "$verdict" |
| + echo "ERROR $r [boxes=$SHAPE]: witness run rc=$wrc; see $wlog" | tee "$verdict" |
| return |
| fi |
| if [ "$wit" = none ]; then |
| for x in $(echo "$r" | tr ',' ' '); do |
| if echo "$WRULES" | grep -qx "$x"; then |
| - echo "ERROR $r: $x has witnesses but the run produced no witness output; see $wlog" | tee "$verdict" |
| + echo "ERROR $r [boxes=$SHAPE]: $x has witnesses but the run produced no witness output; see $wlog" | tee "$verdict" |
| return |
| fi |
| done |
| fi |
| if [ -z "$sweep" ]; then |
| - echo "ERROR $r: rc=$rc, no parsable sweep verdict; see $log" | tee "$verdict" |
| + echo "ERROR $r [boxes=$SHAPE]: rc=$rc, no parsable sweep verdict; see $log" | tee "$verdict" |
| return |
| fi |
| caught=0 |
| @@ -129,20 +140,20 @@ one() { |
| fi |
| if [ $caught -eq 1 ]; then |
| if [ "$expect" = "missed" ]; then |
| - echo "STALE $r: $sweep; witness $wit; but expected-outcomes.txt says missed" | tee "$verdict" |
| + echo "STALE $r [boxes=$SHAPE]: $sweep; witness $wit; but expected-outcomes.txt says missed" | tee "$verdict" |
| else |
| - echo "CAUGHT $r: $sweep; witness $wit" | tee "$verdict" |
| + echo "CAUGHT $r [boxes=$SHAPE]: $sweep; witness $wit" | tee "$verdict" |
| fi |
| elif [ "$expect" = "missed" ]; then |
| - echo "EXPECTED-MISS $r: $sweep; witness $wit" | tee "$verdict" |
| + echo "EXPECTED-MISS $r [boxes=$SHAPE]: $sweep; witness $wit" | tee "$verdict" |
| elif [ "$expect" = "rare" ] && [ -n "$depth" ] && [ "$SEEDS" -lt "$depth" ]; then |
| - echo "EXPECTED-MISS $r: $sweep; witness $wit (rare: caught at $depth seeds)" | tee "$verdict" |
| + echo "EXPECTED-MISS $r [boxes=$SHAPE]: $sweep; witness $wit (rare: caught at $depth seeds)" | tee "$verdict" |
| else |
| - echo "MISSED $r: $sweep; witness $wit" | tee "$verdict" |
| + echo "MISSED $r [boxes=$SHAPE]: $sweep; witness $wit" | tee "$verdict" |
| fi |
| } |
| export -f one |
| -export SEEDS PKG SCRATCH BIN WRULES |
| +export SEEDS PKG SCRATCH BIN WRULES SHAPE |
| printf '%s\n' $RULES | xargs -P "${HOSTLIFE_PAR:-8}" -I{} bash -c 'one "$@"' _ {} |
| xrc=$? |
| if [ $xrc -ne 0 ]; then |