carlos / platform Public

sim: the two-box baseline's three causes: INV-10 exempts files keys a park kept live (the at-rest sweep owns them once obsolete), a region's park-replica waits for every box's stop evidence, and an operator-named source that is also the target is replaced when it is fenced

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

Paul Campbell pushed by claude 2 weeks ago cf566b41ea115a0d37ae8b8d8d7b8709261a86ea parent cf1a2bd

5 files changed, +60 −10

internal/sim/hostlife/moves_test.go +3 −3
internal/sim/hostlife/protocol_test.go +25 −4
internal/sim/hostlife/regionha_test.go +29 −2
internal/sim/hostlife/sim_test.go +1 −1
internal/sim/hostlife/world_test.go +2 −0

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

index fd657a53a..5c25972ad 100644

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

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

@@ -1051,7 +1051,7 @@ func (w *world) landTarget(b *box, c *claim) {

w.violate("INV-9: the cut of %s waits on quiet_after[%d] until %d", op.ID, b.Region, c.Quiet[b.Region])

}

// an earlier stay of this incarnation, in its location here

- if w.parkStep(b, loc, fmt.Sprintf("superseded/%s/%s/install/", op.ID, host), c.Quiet[b.Region], w.opScope(c, loc), w.keepFilesLive(confine(loc))) {

+ if w.parkStep(b, loc, fmt.Sprintf("superseded/%s/%s/install/", op.ID, host), c.Quiet[b.Region], w.opScope(c, loc), w.keepFilesLive(b.Region, confine(loc))) {

w.cas(c, func(n *claim) bool { n.Op.LandPhase = "install-copy"; return sameOp(n.Op.ID, op.ID) })

}

case "install-copy":

@@ -1538,7 +1538,7 @@ func (w *world) recoverSource(b *box, c *claim) {

if !w.evidence(b, op.RollbackID) {

return

}

- if w.parkStep(b, c.Holder.Location, fmt.Sprintf("superseded/%s/%s/return/", op.ID, host), op.StopAt+horizonH, w.opScope(c, c.Holder.Location), w.keepFilesLive(confine(c.Holder.Location))) {

+ if w.parkStep(b, c.Holder.Location, fmt.Sprintf("superseded/%s/%s/return/", op.ID, host), op.StopAt+horizonH, w.opScope(c, c.Holder.Location), w.keepFilesLive(b.Region, confine(c.Holder.Location))) {

w.cas(c, func(n *claim) bool { n.Op.SrcPhase = "install-copy"; return sameOp(n.Op.ID, op.ID) })

}

case "install-copy":

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

return true

})

case "park":

- if w.parkStep(b, loc, fmt.Sprintf("superseded/%s/%s/push/", op.ID, host), op.StopAt+horizonH, w.opScope(c, loc), w.keepFilesLive(confine(loc))) {

+ if w.parkStep(b, loc, fmt.Sprintf("superseded/%s/%s/push/", op.ID, host), op.StopAt+horizonH, w.opScope(c, loc), w.keepFilesLive(b.Region, confine(loc))) {

w.cas(c, func(n *claim) bool { n.Op.Phase = "install"; return sameOp(n.Op.ID, op.ID) })

}

case "install":

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

index 3f442bcdb..3efe4951e 100644

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

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

@@ -157,10 +157,14 @@ func (w *world) evidence(b *box, opID string) bool {

return false

}

- if on("evidence-whole-tree") {

- return len(b.Procs) == 0

+ ok := !on("evidence-whole-tree") || len(b.Procs) == 0

+ if ok {

+ if b.StopEvidence == nil {

+ b.StopEvidence = map[string]bool{}

+ }

+ b.StopEvidence[opID] = true

}

- return true // the mutation certifies an empty cgroup, blind to escapees

+ return ok // the mutation certifies an empty cgroup, blind to escapees

}

// ---------- restore and spawn ----------

@@ -2281,6 +2285,16 @@ func (w *world) doObligation(b *box, c *claim, o obligation) {

if !w.evidence(b, o.Op) {

return

}

+ if w.perRegion > 1 {

+ // every box of the region publishes its own stop evidence

+ // (hostops collectEvidence over the inventory); the owner's

+ // alone proves nothing about its sibling

+ for _, x := range w.regionBoxes(b.Region) {

+ if x != b && !contains(c.Lost, x.ID) && !x.StopEvidence[o.Op] {

+ return

+ }

}

// a replicator's PUT signed before that evidence can land up to

// the horizon later: verify only after it (this model's finding).

@@ -2371,7 +2385,14 @@ func (w *world) doObligation(b *box, c *claim, o obligation) {

}

inner := keep

keep = func(k string) bool {

- return genOf(o.Prefix, k) != retire || w.filesLive(w.claim, k) || inner != nil && inner(k)

+ if genOf(o.Prefix, k) != retire || inner != nil && inner(k) {

+ return true

+ }

+ if w.filesLive(w.claim, k) {

+ w.markSweepOwed(b.Region, k)

+ return true

+ }

+ return false

}

if !w.parkStep(b, o.Prefix, o.Dest(), quiet, o.Scope, keep) {

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

index 1d4677fea..a32a4705f 100644

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

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

@@ -1640,6 +1640,12 @@ func (w *world) fence(b *box, c *claim, x *box) {

return false

case n.Op.Kind == "relocating" && n.Op.Src == x.ID:

w.fenceSource(n, x)

+ if n.Op.Tgt == x.ID && !w.replaceTarget(n, x) {

+ // an operator's replay made the source eligible and named it

+ // the target (model ruling 13): its fence is a target loss

+ // too, or pinning waits on a lost target for ever

+ return false // no spare yet

+ }

case n.Op.Kind == "relocating" && n.Op.Tgt == x.ID:

if !w.replaceTarget(n, x) {

return false // no spare yet

@@ -2297,9 +2303,30 @@ func (w *world) objectReferenced(c *claim, k string) bool {

// binds every park; moves' parks predate region HA's files tree). Only

// the two-box shape has files keys, so the one-box shape is unchanged.

// The mutation of files-live-set-moves-parks archives them with the rest.

-func (w *world) keepFilesLive(keep func(string) bool) func(string) bool {

+func (w *world) keepFilesLive(r int, keep func(string) bool) func(string) bool {

return func(k string) bool {

- return keep(k) || on("files-live-set-moves-parks") && w.filesLive(w.claim, k)

+ if keep(k) {

+ return true

+ }

+ if on("files-live-set-moves-parks") && w.filesLive(w.claim, k) {

+ w.markSweepOwed(r, k)

+ return true

+ }

+ return false

+ }

+// markSweepOwed: a park kept k only because the files live set named it;

+// once obsolete it is the at-rest sweep's (claim §6.2a, 1b-next ruling 21),

+// so INV-10 at an operation's end exempts it as it exempts a straggler.

+func (w *world) markSweepOwed(r int, k string) {

+ for i := range w.buckets {

+ if r >= 0 && i != r {

+ continue

+ }

+ for _, v := range w.buckets[i].objs[k] {

+ v.SweepOwed = true

+ }

}

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

index acce63db3..f99260ce4 100644

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

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

@@ -462,7 +462,7 @@ func (w *world) residueOf(exceptStragglers bool) []string {

continue // a pending chore of another operation covers it

}

for _, v := range bk.objs[k] {

- if !v.Marker && !(exceptStragglers && v.Straggler) {

+ if !v.Marker && !(exceptStragglers && (v.Straggler || v.SweepOwed)) {

out = append(out, fmt.Sprintf("r%d:%s", r, k))

break

}

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

index 7d5827e72..0049356e7 100644

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

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

@@ -124,6 +124,7 @@ type version struct {

B *blob

Marker bool

Straggler bool // created by a request that completed after H

+ SweepOwed bool // a dead generation's files key its park kept while live: the at-rest sweep's once obsolete (claim §6.2a)

}

type bucket struct {

@@ -450,6 +451,7 @@ type box struct {

Epoch int

plans []*plan

stopped map[string]bool

+ StopEvidence map[string]bool // published stop evidence, by operation (survives a restart)

mem map[string]bool

evidAt map[string]int

pendingTimers []int