carlos / platform Public

sim: hostlife signs staging at the check; C3a and admission-triple rules; expected outcomes

- sign-at-check (model 18): a staging request signed at its SafeUntil
  check, so S3's signature-age limit bounds any later pause, even a whole-VM
  freeze; SafeUntil leaves room for the signature's life. Without it seed
  77725 of 100,000 leaves staging residue
- location-per-incarnation (claim C3a) as a rule, and an oracle that no
  restored or started database holds another incarnation's writes
- a worst-moment stale open stays paused until its moment, so the
  admission triple (exec-admission, hold-op-open, start-check-claim-gen)
  is reachable: 4 of 30,000; every pair of it 0
- expected-outcomes.txt for mutate.sh

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

claude 3 weeks ago 47e65af80c5858ee873990c3640ea54af06174bd parent eade8ef

7 files changed, +76 −18

internal/sim/hostlife/background_test.go +1 −0
internal/sim/hostlife/expected-outcomes.txt +20 −1
internal/sim/hostlife/moves_test.go +34 −14
internal/sim/hostlife/protocol_test.go +1 −0
internal/sim/hostlife/rules_test.go +2 −0
internal/sim/hostlife/sim_test.go +14 −1
internal/sim/hostlife/world_test.go +4 −2

diff --git a/internal/sim/hostlife/background_test.go b/internal/sim/hostlife/background_test.go

index d8c7c0fe1..e3c28c213 100644

--- a/internal/sim/hostlife/background_test.go

+++ b/internal/sim/hostlife/background_test.go

@@ -20,6 +20,7 @@ func (w *world) traffic(b *box) {

// acknowledged to the client or the outside world either way: a

// write into a purged or foreign database is a lost write

w.acks = append(w.acks, ack{W: wr, Inc: p.Inc, Box: b.ID, At: w.now, Kind: "write"})

+ w.writeInc[wr] = p.Inc

if p.Main && w.rng.Intn(4) == 0 && b.Row != nil && b.Row.Inc == p.Inc {

w.nextW++

b.Timers = append(b.Timers, w.nextW)

diff --git a/internal/sim/hostlife/expected-outcomes.txt b/internal/sim/hostlife/expected-outcomes.txt

index 1cab9ebd4..0b01f17df 100644

--- a/internal/sim/hostlife/expected-outcomes.txt

+++ b/internal/sim/hostlife/expected-outcomes.txt

@@ -1 +1,20 @@

-# rule outcome reason (see mutate.sh)

+# rule outcome reason. Read by mutate.sh: a rule listed `missed` is not

+# expected to be caught alone, and is reported EXPECTED-MISS; the sweep

+# fails if it is caught (the expectation is stale). Spec §14.2.5 gives the

+# combination that catches each, or why none does.

+claim-cas-opid missed caught with revalidate-before-effect

+commit-before-open missed caught with dirty-return

+config-before-probe missed liveness only: a target that cannot render config fails its probe and rolls back

+readiness-key missed liveness only: T2 avoids a pointless cut

+readiness-quiet missed unreachable under claim rev 4: acknowledgements wait out their own horizon and CC11 holds

+declare-lost-compute missed caught with watchdog-independent (100000 seeds)

+watchdog-independent missed caught with declare-lost-compute (100000 seeds)

+exec-admission missed one of three admission fences; caught with hold-op-open and start-check-claim-gen

+hold-op-open missed one of three admission fences; caught with exec-admission and start-check-claim-gen

+start-check-claim-gen missed one of three admission fences; caught with exec-admission and hold-op-open

+start-check missed caught with exec-admission and hold-op-open

+strict-spawn missed caught with evidence-whole-tree

+touched-incomplete missed caught with legacy-discovery

+location-per-incarnation missed unexercised: guards completions later than the model's delete-to-recreate window

+door-by-version missed unexercised: subsumed by C3a, and not caught with it dropped either

+door-reread missed unexercised: subsumed by C3a, and not caught with it dropped either

diff --git a/internal/sim/hostlife/moves_test.go b/internal/sim/hostlife/moves_test.go

index e23df1460..48e305ea5 100644

--- a/internal/sim/hostlife/moves_test.go

+++ b/internal/sim/hostlife/moves_test.go

@@ -390,7 +390,13 @@ func (w *world) holdRow(b *box, status, holdOp string, c *claim) {

// openRow is the conditional open (moves §5.2).

func (w *world) openRow(b *box, holdOp string) bool {

if w.rng.Intn(6) == 0 {

- b.deferred = append(b.deferred, &localWrite{kind: "open", holdOp: holdOp, epoch: b.Epoch, at: w.now + 1 + w.pauseLen(), worst: w.rng.Intn(2) == 0})

+ d := &localWrite{kind: "open", holdOp: holdOp, epoch: b.Epoch, at: w.now + 1 + w.pauseLen()}

+ if w.rng.Intn(2) == 0 {

+ // the adversary keeps this one paused until its worst moment,

+ // or a long stall's end

+ d.worst, d.at = true, w.now+4000

+ }

+ b.deferred = append(b.deferred, d)

}

return w.openNow(b, holdOp)

}

@@ -449,12 +455,13 @@ func (w *world) maybeStallDuplicateFor(b *box, region int, r *request) {

}

type stalledSign struct {

- box int

- epoch int

- req *request

- signAt int

- until int

- checked bool // passed its SafeUntil check, not yet signed

+ box int

+ epoch int

+ req *request

+ signAt int

+ until int

+ checked bool // passed its SafeUntil check and signed, not yet sent

+ checkedAt int

}

// runStalled lets paused goroutines resume: deferred registry writes and

@@ -471,16 +478,28 @@ func (w *world) runStalled() {

continue

}

if s.checked {

- w.issue(b.ID, s.req) // signs, at most maxPause after the check

+ // the request is sent now, after a pause that a whole-VM

+ // freeze can stretch without bound. Signed at the check, its

+ // timestamp is the check's, and S3 refuses it once older than

+ // the signature-age limit (model 18); signed at send time, it

+ // is accepted however late

+ if on("sign-at-check") && w.now > s.checkedAt+sigAge {

+ w.stats["stale signature refused"]++

+ continue

+ }

+ w.issue(b.ID, s.req)

continue

}

- if on("sign-before-safeuntil") && w.localNow(b) > s.until-maxSkew-maxPause {

+ margin := maxSkew + maxPause

+ if on("sign-at-check") {

+ margin = maxSkew + sigAge // SafeUntil leaves room for the signature's whole valid life

+ }

+ if on("sign-before-safeuntil") && w.localNow(b) > s.until-margin {

continue // checked SafeUntil immediately before signing: too late

}

- // the check passed; the goroutine may still pause before the

- // signature, within the claim's §3.1 bound, which SafeUntil's

- // margin covers

- s.checked, s.signAt = true, w.now+w.rng.Intn(maxPause+1)

+ // the check passed and the request is signed; the goroutine may

+ // still pause before sending it

+ s.checked, s.checkedAt, s.signAt = true, w.now, w.now+w.rng.Intn(maxPause+1)

keep = append(keep, s)

}

w.stalled = keep

@@ -497,7 +516,7 @@ func (w *world) runStalled() {

// operation holds the row, at its worst moment: after that

// operation committed and stopped re-asserting the hold

worst := d.worst && d.kind == "open" && b.Row != nil && b.Row.HoldOp != "" && b.Row.HoldOp != d.holdOp &&

- w.claim != nil && w.claim.Op.Committed && w.rng.Intn(10) == 0

+ w.claim != nil && w.claim.Op.Committed && w.rng.Intn(3) == 0

if d.at > w.now && !worst {

rest = append(rest, d)

continue

@@ -1082,6 +1101,7 @@ func (w *world) pushStep(b *box, c *claim) {

w.nextW++

mark := w.nextW

w.acks = append(w.acks, ack{W: mark, Inc: c.Holder.Inc, Box: b.ID, At: w.now, Kind: "write"})

+ w.writeInc[mark] = c.Holder.Inc

writes = append(writes, mark)

w.cas(c, func(n *claim) bool {

if !sameOp(n.Op.ID, op.ID) || n.Op.Phase != "stopping" {

diff --git a/internal/sim/hostlife/protocol_test.go b/internal/sim/hostlife/protocol_test.go

index 675a9dc5e..620a24b5c 100644

--- a/internal/sim/hostlife/protocol_test.go

+++ b/internal/sim/hostlife/protocol_test.go

@@ -293,6 +293,7 @@ func (w *world) spawn(b *box, c *claim, want string, probe bool) bool {

}

// what the app sees

+ w.foreignWrites(b.DB, h.Inc, fmt.Sprintf("box %d start", b.ID))

if b.DB.Inc != 0 && b.DB.Inc != h.Inc {

w.violate("box %d started inc %d over a database of inc %d", b.ID, h.Inc, b.DB.Inc)

}

diff --git a/internal/sim/hostlife/rules_test.go b/internal/sim/hostlife/rules_test.go

index 58b8fd7c5..07baf07d6 100644

--- a/internal/sim/hostlife/rules_test.go

+++ b/internal/sim/hostlife/rules_test.go

@@ -28,6 +28,8 @@ var allRules = []string{

"claim-cas-opid", // C2: every CAS conditional on op.id

"revalidate-before-effect", // C3: a worker re-reads under its lease before acting

"sign-before-safeuntil", // C3/§3.1: a paused round signs only before its lease's SafeUntil

+ "sign-at-check", // model 18: signed at the check, so S3's age limit bounds any later pause

+ "location-per-incarnation", // claim rev 4 C3a (J2-R2-1): no location shared between incarnations

"fresh-admission", // C4: admission reads the claim fresh

"exec-admission", // C4/K1: op.exec names this box (and the role column, which is op.exec here)

"recovery-pass", // C2/§8: console claim-recovery pass

diff --git a/internal/sim/hostlife/sim_test.go b/internal/sim/hostlife/sim_test.go

index 406b0116a..0d46d5ef3 100644

--- a/internal/sim/hostlife/sim_test.go

+++ b/internal/sim/hostlife/sim_test.go

@@ -17,7 +17,7 @@ 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{}, 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{}, 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()

}

@@ -60,6 +60,7 @@ func (w *world) legacyStart() {

w.nextW++

writes = append(writes, w.nextW)

w.acks = append(w.acks, ack{W: w.nextW, Inc: inc, Box: b.ID, At: 0, Kind: "write"})

+ w.writeInc[w.nextW] = inc

}

b.Row = &row{Inc: inc, App: app0, Status: "ready"}

b.DB = &localDB{Inc: inc, Loc: locationFor(inc, true), Key: key, Writes: writes}

@@ -444,6 +445,7 @@ func (w *world) checkDurable(c *claim, when string) {

for _, x := range db.Writes {

have[x] = true

}

+ w.foreignWrites(db, c.Holder.Inc, "cold restore, "+when)

}

for _, a := range w.acks {

if a.Inc != c.Holder.Inc || a.Exempt || a.Kind != "write" || !need[a.W] {

@@ -456,6 +458,17 @@ func (w *world) checkDurable(c *claim, when string) {

}

+// foreignWrites: a database restored or started for incarnation inc holds

+// no write another incarnation acknowledged (C1, INV-4, claim C3a).

+func (w *world) foreignWrites(db *localDB, inc int, how string) {

+ for _, x := range db.Writes {

+ if i, ok := w.writeInc[x]; ok && i != inc {

+ w.violate("C3a (%s): incarnation %d's database holds write %d of incarnation %d", how, inc, x, i)

+ return

+ }

func (w *world) checkAcks(c *claim, e *box, writes []int, how string) {

have := map[int]bool{}

for _, x := range writes {

diff --git a/internal/sim/hostlife/world_test.go b/internal/sim/hostlife/world_test.go

index e61d079b8..082999935 100644

--- a/internal/sim/hostlife/world_test.go

+++ b/internal/sim/hostlife/world_test.go

@@ -50,7 +50,8 @@ const (

probeTries = 3

readyWait = 800 // abort a move whose readiness never comes

maxSkew = 1 // a box clock is within this of true time

- maxPause = 3 // the claim's §3.1 bound on a pause between a check and the act

+ maxPause = 3 // a typical pause between a check and the act (a VM freeze is longer)

+ sigAge = 30 // S3's signature-age limit; H covers it plus the longest request

beyondH = 20 // one long-tail request in this many completes after H (R2-1)

)

@@ -152,7 +153,7 @@ func (b *bucket) hasData(prefix string, skipLock bool) bool {

// locationFor is holder.location for an incarnation.

func locationFor(inc int, legacy bool) string {

- if legacy {

+ if legacy || !on("location-per-incarnation") {

return "instances/" + host + "/"

}

return fmt.Sprintf("instances/%s/%d/", host, inc)

@@ -509,6 +510,7 @@ type world struct {

boxes []*box

pending []*request

acks []ack

+ writeInc map[int]int // which incarnation acknowledged each write

durable map[string]map[int]bool // per generation prefix: writes a completed replica object holds

genParent map[string]string // generation prefix -> the one it superseded

nextW int