carlos / platform Public

sim: hostlife on claim rev 5.1: the purge fence (CC21), and a harness without copies

- purge-claim-fence (claim rev 5.1 §5.3, CC21): before removing an expired
  registration whose host claim does not name the create, purge CASes a
  free or absent host claim to a purge fence; released at done. The purge
  id lives in the reservation, so a resumed purge releases its own fences
- fence-etag (CC22): the creator's claim CAS is conditional on the ETag it
  read when it registered. Without it, a fence placed and released while
  the creator was paused lets the CAS succeed after the purge
- the creator's re-read of its registration before the claim CAS is now
  its own step; it is subsumed by the fence and the ETag together
- a biased schedule pauses a creator between its re-read and its claim
  CAS, past the registration's expiry
- sweep-staging stays as CC20, now in claim rev 5.1
- mutate.sh runs one prebuilt test binary with HOSTLIFE_MUTATE, under
  $TMPDIR, with no per-rule copies of the source
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
claude agent, operated by paul@keymail.dev 93bf5edb020f0d6f523193a4aeccb525cc360489 parent 7e0c025
6 files changed, +170 −45
  • internal/sim/hostlife/console_test.go +113 −3
  • internal/sim/hostlife/expected-outcomes.txt +1 −0
  • internal/sim/hostlife/mutate.sh +30 −31
  • internal/sim/hostlife/rules_test.go +18 −5
  • internal/sim/hostlife/sim_test.go +3 −3
  • internal/sim/hostlife/world_test.go +5 −3
diff --git a/internal/sim/hostlife/console_test.go b/internal/sim/hostlife/console_test.go
index 766382ad9..0da67ff97 100644
--- a/internal/sim/hostlife/console_test.go
+++ b/internal/sim/hostlife/console_test.go
@@ -13,6 +13,12 @@ type consolePlan struct {
Host string // "h" or "h2" for a create
Inc int
Region int
+ Read bool // a create's registration re-read has passed
+ Stall int // the console is paused on this plan until then
+ // the claim's ETag as the create read it when it registered: its
+ // claim CAS is conditional on it (CC22)
+ SeenVer int
+ SeenAbsent bool
}
// doorPlan is one pull-door listing (claim rev 4 §6.5): O1 is the claim
@@ -135,17 +141,42 @@ func (w *world) createSteps(p *consolePlan) bool {
return true
}
w.stores[p.App] = true // the app exists, or exists again after a purge
+ // the host claim's ETag, read with the registration: the claim CAS
+ // is conditional on it (CC22), so any purge fence placed after
+ // this, even one since released, refuses the create
+ if p.Host == "h2" {
+ p.SeenVer = w.h2Epoch
+ } else if w.claim == nil {
+ p.SeenAbsent = true
+ } else {
+ p.SeenVer = w.claim.Ver
+ }
p.Step = 1
return false
case 1:
- if _, ok := ad.Reg[p.OpID]; on("admission-registration") && on("registration-check") && !ok {
- return abandon() // CC21: the registration is gone; the claim CAS must not follow
+ if !p.Read {
+ // the re-read, the last step before the claim CAS (claim rev
+ // 5.1 §5.3): stop if the registration is gone or admission is
+ // closed. Cheap, and not sufficient: the console can pause
+ // between this read and the CAS
+ if _, ok := ad.Reg[p.OpID]; on("admission-registration") && on("registration-check") && (!ok || ad.Closed) {
+ return abandon()
+ }
+ p.Read = true
+ if w.fail["pausecreate"] && w.rng.Intn(2) == 0 {
+ // the biased schedule: the console pauses here, past the
+ // registration's expiry, while a purge may run
+ p.Stall = w.now + 100 + w.rng.Intn(200)
+ w.logf("create %s: console paused before its claim CAS", p.OpID)
+ }
+ return false
}
if p.Host == "h2" {
- if w.h2.Kind != "" {
+ if w.h2.Kind != "" || on("fence-etag") && w.h2Epoch != p.SeenVer {
return abandon()
}
w.h2 = liteHost{Inc: p.Inc, App: p.App, Kind: "creating", OpID: p.OpID, At: w.now}
+ w.h2Epoch++ // every write changes the claim's ETag
w.logf("create %s: second host claimed for app %s", p.OpID, p.App)
p.Step = 2
return false
@@ -154,6 +185,11 @@ func (w *world) createSteps(p *consolePlan) bool {
if c != nil && (c.Holder != nil || (c.Op.Kind != "" && c.Op.Kind != "serving")) || w.recPend != nil {
return abandon()
}
+ if on("fence-etag") && (p.SeenAbsent != (c == nil) || c != nil && c.Ver != p.SeenVer) {
+ // If-Match the ETag read before the re-read (If-None-Match if
+ // absent): a fence placed and released meanwhile changed it
+ return abandon()
+ }
if c != nil && len(c.Obl) > 0 {
return false // a pending chore, such as a sweep, finishes first (CC11)
}
@@ -193,6 +229,7 @@ func (w *world) createSteps(p *consolePlan) bool {
return abandon()
}
w.h2.Rec = true
+ w.h2Epoch++ // every write changes the claim's ETag
p.Step = 3
return false
}
@@ -224,6 +261,7 @@ func (w *world) createSteps(p *consolePlan) bool {
return abandon()
}
w.h2.Kind = "serving" // a CAS from creating, like the main host's
+ w.h2Epoch++ // every write changes the claim's ETag
w.logf("create %s: second host serving", p.OpID)
delete(ad.Reg, p.OpID)
return true
@@ -400,6 +438,9 @@ func (w *world) consoleStep() {
return
}
i := w.rng.Intn(len(w.console))
+ if w.console[i].Stall > w.now {
+ return // this request's console goroutine is paused
+ }
if w.runPlan(w.console[i]) {
w.console = append(w.console[:i:i], w.console[i+1:]...)
}
@@ -524,6 +565,16 @@ func (w *world) purgeSteps(p *consolePlan) bool {
}()
}
ad := w.admit[p.App]
+ if p.OpID == "" {
+ // the purge id lives in the reservation, so a resumed purge
+ // releases its own fences
+ if id, ok := w.purgeOp[p.App]; ok {
+ p.OpID = id
+ } else {
+ p.OpID = w.newID("pg")
+ w.purgeOp[p.App] = p.OpID
+ }
+ }
switch p.Step {
case 0:
if on("purge-reserve-first") {
@@ -553,6 +604,11 @@ func (w *world) purgeSteps(p *consolePlan) bool {
claimed := e.Host == "h2" && w.h2.OpID == id && w.h2.Kind == "creating" ||
e.Host == "h" && w.claim != nil && w.claim.Op.ID == id && w.claim.Op.Kind == "creating"
if on("registration-recovery") && w.now > e.Until && !claimed {
+ // fence the host's claim first, so a paused creator's
+ // CAS from free or absent fails (CC21); then remove
+ if on("purge-claim-fence") && !w.fenceHost(e.Host, p) {
+ return false
+ }
delete(ad.Reg, id)
continue
}
@@ -571,6 +627,7 @@ func (w *world) purgeSteps(p *consolePlan) bool {
switch w.h2.Kind {
case "serving":
w.h2.Kind = "purging"
+ w.h2Epoch++ // every write changes the claim's ETag
case "purging":
default:
return false
@@ -590,8 +647,24 @@ func (w *world) purgeSteps(p *consolePlan) bool {
default:
if w.h2.App == p.App && w.h2.Kind == "purging" {
w.h2 = liteHost{} // record deleted, claim freed
+ w.h2Epoch++ // every write changes the claim's ETag
}
if c == nil || c.Holder == nil || c.Holder.App != p.App {
+ // done: release this purge's fences to free (CC21)
+ if c != nil && c.Holder == nil && c.Op.Kind == "purging" && c.Op.ID == p.OpID {
+ w.cas(c, func(n *claim) bool {
+ if n.Holder != nil || n.Op.ID != p.OpID {
+ return false
+ }
+ n.Op = opState{}
+ return true
+ })
+ }
+ if w.h2.Kind == "fenced" && w.h2.OpID == p.OpID {
+ w.h2 = liteHost{}
+ w.h2Epoch++ // every write changes the claim's ETag
+ }
+ delete(w.purgeOp, p.App)
w.purgeRes[p.App] = false
delete(w.purgeStep, p.App)
ad.Closed = false // the purge's completion reopens admission
@@ -602,6 +675,38 @@ func (w *world) purgeSteps(p *consolePlan) bool {
}
}
+// fenceHost CASes a host's claim from free or absent to a purge fence with
+// no holder (claim rev 5.1 §5.3, CC21). A claim held by anyone already
+// refuses a creator's CAS from free, so it needs no fence.
+func (w *world) fenceHost(h string, p *consolePlan) bool {
+ if h == "h2" {
+ switch {
+ case w.h2.Kind == "":
+ w.h2 = liteHost{Kind: "fenced", OpID: p.OpID, App: p.App}
+ w.h2Epoch++ // every write changes the claim's ETag
+ w.logf("purge %s: fenced the second host", p.App)
+ case w.h2.Kind == "fenced" && w.h2.OpID != p.OpID:
+ return false // another purge's fence: wait for it
+ }
+ return true
+ }
+ c := w.claim
+ if c != nil && (c.Holder != nil || c.Op.Kind != "") {
+ return !(c.Holder == nil && c.Op.Kind == "purging" && c.Op.ID != p.OpID)
+ }
+ ok := w.cas(c, func(n *claim) bool {
+ if n.Holder != nil || n.Op.Kind != "" {
+ return false
+ }
+ n.Op = opState{Kind: "purging", ID: p.OpID, App: p.App, Exec: -1}
+ return true
+ })
+ if ok {
+ w.logf("purge %s: fenced host %s", p.App, host)
+ }
+ return ok
+}
+
// resumePurges: the recovery pass restarts a purge whose plan was lost,
// from its reservation's journal.
func (w *world) resumePurges() {
@@ -715,8 +820,10 @@ func (w *world) recoveryPass() {
if h := w.h2; h.Kind == "creating" && w.now-h.At >= 15 {
if h.Rec {
w.h2.Kind = "serving"
+ w.h2Epoch++ // every write changes the claim's ETag
} else {
w.h2 = liteHost{}
+ w.h2Epoch++ // every write changes the claim's ETag
}
w.logf("recovery: second host's create %s -> %q", h.OpID, w.h2.Kind)
delete(w.admit[h.App].Reg, h.OpID)
@@ -776,6 +883,9 @@ func (w *world) recoveryPass() {
}
w.deleteSteps(c)
case "purging":
+ if c.Holder == nil {
+ return // a purge fence: its purge releases it (CC21)
+ }
if w.now-c.Op.ReqAt < 15 {
return
}
diff --git a/internal/sim/hostlife/expected-outcomes.txt b/internal/sim/hostlife/expected-outcomes.txt
index cfed5cf08..8b4d68582 100644
--- a/internal/sim/hostlife/expected-outcomes.txt
+++ b/internal/sim/hostlife/expected-outcomes.txt
@@ -17,3 +17,4 @@ strict-spawn missed caught with evidence-whole-tree
touched-incomplete missed caught with legacy-discovery
door-reread missed subsumed by C3a: caught with location-per-incarnation
door-by-version missed subsumed by C3a: caught with door-reread and location-per-incarnation
+registration-check missed a cheap extra: subsumed by purge-claim-fence and fence-etag together
diff --git a/internal/sim/hostlife/mutate.sh b/internal/sim/hostlife/mutate.sh
index 51c731272..a15c58db0 100755
--- a/internal/sim/hostlife/mutate.sh
+++ b/internal/sim/hostlife/mutate.sh
@@ -1,38 +1,50 @@
#!/bin/bash
# Mutation checks for the hostlife model (move-any-app spec §14.2).
#
-# Each rule is dropped in its own scratch copy of the module, never in
-# place: an interrupted in-place mutation once left a disabled guard in a
-# source file. Rules run in parallel.
+# Build the test binary once (this is the only step that writes the Go
+# build cache), then run the sweep. The sweep never copies or edits the
+# source: each rule runs the same binary with HOSTLIFE_MUTATE set.
#
+# go test -c -o "$TMPDIR/hostlife-sim/hostlife.test" ./internal/sim/hostlife/
# 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
#
# Classification (joint round 2, R2-10):
#
-# CAUGHT the test ran to completion and reported at least one seed
-# that violated an invariant, with the seed number parsed from
-# its output (so it can be replayed with HOSTLIFE_SEED);
-# MISSED the test ran to completion and every seed passed;
-# ERROR anything else: a build failure, a timeout, a panic, a
-# read-only cache, or output the harness cannot parse. An
-# error is never a detection.
+# CAUGHT the run completed and reported at least one seed that
+# violated an invariant, with the seed number parsed from its
+# output (so it can be replayed with HOSTLIFE_SEED);
+# MISSED the run completed and every seed passed;
+# ERROR anything else: an unknown rule, a stale binary, a panic, a
+# timeout, or output the harness cannot parse. An error is
+# never a detection.
#
# Expected outcomes live in expected-outcomes.txt beside this script: a
# rule listed there as `missed` (liveness-only, unreachable, or caught
# only in a stated combination) is reported as EXPECTED-MISS. The sweep
# exits nonzero on any ERROR, on any unexpected MISSED, and on any rule
-# listed as `missed` that is CAUGHT (the expectation is stale).
+# listed as `missed` that is CAUGHT (STALE).
#
-# Every run's full output is kept in $SCRATCH/logs/<rule>.log.
+# Scratch (the binary, every run's log, the verdicts) lives under
+# ${HOSTLIFE_SCRATCH:-$TMPDIR/hostlife-sim}; remove it once, after the
+# whole sweep.
set -u
SEEDS=${1:?seeds}
shift
ROOT=$(git -C "$(dirname "$0")" rev-parse --show-toplevel)
PKG="$ROOT/internal/sim/hostlife"
-SCRATCH=${HOSTLIFE_SCRATCH:-$HOME/.cache/hostlife-sim}
-mkdir -p "$SCRATCH/gotmp" "$SCRATCH/logs" "$SCRATCH/verdicts"
+SCRATCH=${HOSTLIFE_SCRATCH:-${TMPDIR:?}/hostlife-sim}
+BIN=${HOSTLIFE_BIN:-$SCRATCH/hostlife.test}
+mkdir -p "$SCRATCH/logs" "$SCRATCH/verdicts"
+if [ ! -x "$BIN" ]; then
+ echo "no test binary at $BIN; build it with: go test -c -o $BIN ./internal/sim/hostlife/" >&2
+ exit 2
+fi
+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')
@@ -42,7 +54,6 @@ rm -f "$SCRATCH"/verdicts/*
one() {
r=$1
tag=$(echo "$r" | tr ',' '+')
- d="$SCRATCH/mut-$tag"
log="$SCRATCH/logs/$tag.log"
verdict="$SCRATCH/verdicts/$tag"
for x in $(echo "$r" | tr ',' ' '); do
@@ -51,24 +62,13 @@ one() {
return
fi
done
- rm -rf "$d"
- mkdir -p "$d/internal/sim"
- cp "$ROOT/go.mod" "$ROOT/go.sum" "$d/"
- cp -a "$PKG" "$d/internal/sim/"
- sed -i "s/^var mutated = \"\"/var mutated = \"$r\"/" "$d/internal/sim/hostlife/rules_test.go"
- if ! grep -q "^var mutated = \"$r\"" "$d/internal/sim/hostlife/rules_test.go"; then
- echo "ERROR $r: could not set the mutation" | tee "$verdict"
- rm -rf "$d"
- return
- fi
- (cd "$d" && GOTMPDIR="$SCRATCH/gotmp" TMPDIR="$SCRATCH/gotmp" HOSTLIFE_SEEDS=$SEEDS \
- go test ./internal/sim/hostlife/ -run TestHostLifecycle -count=1 -timeout 180m -v) >"$log" 2>&1
+ HOSTLIFE_MUTATE=$r HOSTLIFE_SEEDS=$SEEDS "$BIN" -test.run TestHostLifecycle -test.count=1 -test.v -test.timeout 180m >"$log" 2>&1
rc=$?
expect=$(awk -v r="$r" '$1==r {print $2}' "$PKG/expected-outcomes.txt" 2>/dev/null)
nviol=$(grep -o "[0-9]* of $SEEDS seeds violated an invariant" "$log" | head -1 | awk '{print $1}')
seed=$(grep -o "first seed [0-9]*" "$log" | head -1 | awk '{print $3}')
- clean=$(grep -c "^ sim_test.go:[0-9]*: $SEEDS seeds, 0 failed" "$log")
- if [ $rc -ne 0 ] && [ -n "$nviol" ] && [ -n "$seed" ] && ! grep -q "^panic:\|build failed\|test timed out" "$log"; then
+ clean=$(grep -c "^ sim_test.go:[0-9]*: $SEEDS seeds, 0 failed.*mutated=\"$r\"" "$log")
+ if [ $rc -ne 0 ] && [ -n "$nviol" ] && [ -n "$seed" ] && ! grep -q "^panic:\|test timed out" "$log"; then
if [ "$expect" = "missed" ]; then
echo "STALE $r: $nviol of $SEEDS seeds violated (first seed $seed), but expected-outcomes.txt says missed" | tee "$verdict"
else
@@ -83,10 +83,9 @@ one() {
else
echo "ERROR $r: rc=$rc, no parsable verdict; see $log" | tee "$verdict"
fi
- rm -rf "$d"
}
export -f one
-export SEEDS ROOT PKG SCRATCH
+export SEEDS PKG SCRATCH BIN
printf '%s\n' $RULES | xargs -P "${HOSTLIFE_PAR:-8}" -I{} bash -c 'one "$@"' _ {}
bad=$(cat "$SCRATCH"/verdicts/* 2>/dev/null | grep -c "^ERROR\|^MISSED\|^STALE")
if [ "$bad" -gt 0 ]; then
diff --git a/internal/sim/hostlife/rules_test.go b/internal/sim/hostlife/rules_test.go
index f081a1b70..f1ebb2637 100644
--- a/internal/sim/hostlife/rules_test.go
+++ b/internal/sim/hostlife/rules_test.go
@@ -1,16 +1,27 @@
package hostlife
-import "strings"
+import (
+ "os"
+ "strings"
+)
// Every protocol rule the model enforces has a name here. The mutation
-// harness (spec §14.2) copies the tree to a scratch directory, sets
-// `mutated` below to one rule name, runs the simulation, and requires at
+// harness (spec §14.2) runs one prebuilt test binary with HOSTLIFE_MUTATE
+// set to one rule name (or a comma-separated combination), and requires at
// least one seed to fail. A rule whose mutation no seed catches is either
// redundant or untested, and the run says which.
//
-// Never edit `mutated` in place; the harness does it in a copy.
+// Never edit `mutated` in place; the harness sets HOSTLIFE_MUTATE.
var mutated = ""
+// HOSTLIFE_MUTATE sets `mutated` for one run of a prebuilt test binary, so
+// the mutation harness never edits or copies the source (mutate.sh).
+func init() {
+ if v := os.Getenv("HOSTLIFE_MUTATE"); v != "" {
+ mutated = v
+ }
+}
+
func on(rule string) bool {
for _, m := range strings.Split(mutated, ",") {
if m == rule {
@@ -48,7 +59,9 @@ var allRules = []string{
"purge-journal", // this model's finding: the reservation is the purge's journal
"admission-registration", // claim rev 4 §5.1 step 0, §5.3 step 1b (J2-R2-2)
"registration-recovery", // CC16: a registration is a lease, so a dead create cannot block purge
- "registration-check", // CC21: a create checks its registration immediately before its claim CAS
+ "registration-check", // claim rev 5.1 §5.3: the creator re-reads its registration before its claim CAS (cheap, not sufficient)
+ "purge-claim-fence", // claim rev 5.1 §5.3 (CC21): purge fences a free host claim before removing a registration
+ "fence-etag", // CC22: the claim CAS is If-Match the ETag read before the re-read, so a released fence still refuses it
"cancelled-creates", // claim rev 4 §5.1 (J2-R2-7): a late record PUT is removed
"orphan-no-deadline", // CC17: ... whenever it lands, not only before `until`
"door-by-version", // §6.5/J-N10
diff --git a/internal/sim/hostlife/sim_test.go b/internal/sim/hostlife/sim_test.go
index 2df214dd8..6fdf41281 100644
--- a/internal/sim/hostlife/sim_test.go
+++ b/internal/sim/hostlife/sim_test.go
@@ -17,12 +17,12 @@ const (
func newWorld(seed int64, verbose bool) *world {
w := &world{seed: seed, rng: rand.New(rand.NewSource(seed)), verbose: verbose,
stores: map[string]bool{app0: true, app1: true}, cfgVer: map[string]int{app0: 1, app1: 1}, purgeRes: map[string]bool{}, purgeStep: map[string]int{},
- control: newBucket(), delivered: map[int]bool{}, durable: map[string]map[int]bool{}, writeInc: map[int]int{}, legacyIncs: map[int]bool{}, genParent: map[string]string{}, execLease: map[int]execLease{}, fail: map[string]bool{}, stats: map[string]int{}}
+ control: newBucket(), delivered: map[int]bool{}, durable: map[string]map[int]bool{}, writeInc: map[int]int{}, legacyIncs: map[int]bool{}, purgeOp: map[string]string{}, genParent: map[string]string{}, execLease: map[int]execLease{}, fail: map[string]bool{}, stats: map[string]int{}}
for r := 0; r < nRegions; r++ {
w.buckets[r] = newBucket()
}
w.admit = map[string]*admission{app0: {Reg: map[string]regEntry{}}, app1: {Reg: map[string]regEntry{}}}
- for _, f := range []string{"partition", "freeze", "pause", "destroy", "disk", "recreate"} {
+ for _, f := range []string{"partition", "freeze", "pause", "destroy", "disk", "recreate", "pausecreate"} {
w.fail[f] = w.rng.Intn(2) == 0
}
for r := 0; r < nRegions; r++ {
@@ -205,7 +205,7 @@ func (w *world) quiescent() bool {
// atRest: the claim, record and boxes have converged.
func (w *world) atRest() bool {
- if w.h2.Kind == "creating" || w.h2.Kind == "purging" {
+ if w.h2.Kind == "creating" || w.h2.Kind == "purging" || w.h2.Kind == "fenced" {
return false
}
for _, ad := range w.admit {
diff --git a/internal/sim/hostlife/world_test.go b/internal/sim/hostlife/world_test.go
index ff8db6b52..20db542ad 100644
--- a/internal/sim/hostlife/world_test.go
+++ b/internal/sim/hostlife/world_test.go
@@ -501,9 +501,11 @@ type world struct {
purgeStep map[string]int // the reservation's durable phase (purge journal)
admit map[string]*admission
h2 liteHost
- recPend *pendingRec // a record PUT whose response was lost
- lastRegion int // where the host served when it was last deleted
- legacyIncs map[int]bool // incarnations that were adopted legacy hosts
+ recPend *pendingRec // a record PUT whose response was lost
+ lastRegion int // where the host served when it was last deleted
+ legacyIncs map[int]bool // incarnations that were adopted legacy hosts
+ purgeOp map[string]string // the purge id, kept in the reservation (the purge journal)
+ h2Epoch int // the second host claim\'s ETag, for its fence and release
floor bool
buckets [nRegions]*bucket
control *bucket