carlos / platform Public

settings-4: simulation models the carry fence (Astra round 2)

A move may race a root pass on the source: early (its fence first) it
publishes and the cut carries the record; late (after the carry) it meets
the cut's hold through the production publishGate and publishes nothing.
Invariant 1's carried watermark is the source's file at the hand-over, after
the race. The seed-531 shape's racing pass now meets the hold; a new scripted
shape races a failed completion both ways (kills M12). The planner recovery
path is not modelled; its gate is the host integration tests.

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

claude 1 week ago a9d15b440612c0103a3b031d109712c17a1d7189 parent b56409e

1 file changed, +151 −34

internal/release/updatesim_test.go +151 −34

diff --git a/internal/release/updatesim_test.go b/internal/release/updatesim_test.go

index 8ff4ee8d3..5dddd3947 100644

--- a/internal/release/updatesim_test.go

+++ b/internal/release/updatesim_test.go

@@ -23,7 +23,9 @@ import (

// wake calls DecideHeldWake (the held wake check, ruling R-HELD-PURE) and

// enforces it as the activator's wakeCheck does (refuse, run the target, or

// wait for root), then HeldExecStale and NextBuildState (beforeExec, ruling

-// R-MERGE); a graceful move calls CarryRequest (ruling R-SPEC-43A-2). What

+// R-MERGE); a graceful move calls CarryRequest (ruling R-SPEC-43A-2), and

+// root's write of its record passes publishGate, the re-check root makes

+// under the carry fence (ruling R-CARRY-FENCE). What

// surrounds them is not pure (settingsTarget's file and registry reads,

// adoptHost's bake, evidence and repoint, beforeExec's bucket write, the

// wake's wait) and is mirrored here in the smallest form that keeps its

@@ -100,6 +102,7 @@ import (

// and a line "INVARIANT <n> ..." per invariant any seed violated.

func TestUpdateRequestLifecycleSimulation(t *testing.T) {

t.Run("seed 531 shape, unpinned", testUpdateSimSeed531Unpinned)

+ t.Run("carry fence, a failed completion racing a cut", testUpdateSimCarryFence)

seeds := updateSimEnv(t, "UPDATESIM_SEEDS", 200)

par := updateSimEnv(t, "UPDATESIM_PAR", 1)

first := 0

@@ -170,16 +173,15 @@ func TestUpdateRequestLifecycleSimulation(t *testing.T) {

// testUpdateSimSeed531Unpinned replays the shape seed 531 found, through

// the model's own actions (so every invariant is checked at every step) and

// so through the production Target, NextConsumed, DecideHeldWake,

-// CarryRequest and NextBuildState. Box 0 resolves R1 to b2 in a root pass

-// that was already running when the cut began, so its write lands after the

-// cut carried box 0's record (the in-flight window; the random schedule does

-// not model it, as root skips a route once the cut has marked it moving):

-// the resolution stays in box 0's file only. Box 1 resolves R1 again, to b3,

+// CarryRequest, publishGate and NextBuildState. Box 0 runs a root pass that

+// was already running when the cut began; before the carry fence its write

+// landed after the cut carried box 0's record and stayed in box 0's file

+// only. Under the fence (ruling R-CARRY-FENCE) it comes after the carry, so

+// it meets the cut's hold and writes nothing. Box 1 resolves R1, to b3,

// under a pin set after the request, and its wake (running the pin) carries

-// {R1, b3} into the build state; the instance returns to box 0, whose file

-// still says {R1, b2}, and the pin is cleared. Rule 2 must then install the

-// build state's b3 (R-RESOLUTION-STATE-WINS), and the wake that runs it must

-// complete R1. This guards resolvedFor's order by itself.

+// {R1, b3} into the build state; the instance returns to box 0, which holds

+// no record of R1, and the pin is cleared. Rule 2 must then install the

+// build state's b3, and the wake that runs it must complete R1.

func testUpdateSimSeed531Unpinned(t *testing.T) {

w := newUpdateSimWorld(0, false)

w.scripted = true

@@ -204,7 +206,7 @@ func testUpdateSimSeed531Unpinned(t *testing.T) {

steps := []func() string{

func() string { w.settings.Pin = "b1"; return "pin b1 (after the request)" },

func() string {

- return w.moveToRacing(1, true, func() string { return w.rootPass(w.boxes[0], true) })

+ return w.moveToRacing(1, true, func() string { return w.rootPass(w.boxes[0], true) }, true)

func() string { w.head = "b3"; w.boxes[1].eligible["b3"] = true; return "promote b3, baked on box1" },

func() string { return w.rootPass(w.boxes[1], true) },

@@ -214,24 +216,97 @@ func testUpdateSimSeed531Unpinned(t *testing.T) {

func() string { return w.rootPass(w.boxes[0], true) },

func() string { return w.wake(w.boxes[0]) },

}

+ if !runScriptedSim(t, "the scripted seed-531 shape", w, steps) {

+ return

+ }

+ if c := w.boxes[0].consumed; c != nil && c.Resolved != nil && c.Resolved.Target == "b2" {

+ t.Errorf("scripted seed-531 shape: box0's racing pass published {R1, b2} under the cut's hold\ntrace:\n%s", strings.Join(w.trace, "\n"))

+ }

+ if st := w.state; st == nil || st.Completed != 1 || st.CompletedFailed || w.boxes[0].live != "b3" {

+ t.Errorf("scripted seed-531 shape: after the unpinned pass and wake on box0, live %q, build state %+v; want b3 live and R1 completed by it\ntrace:\n%s",

+ w.boxes[0].live, w.state, strings.Join(w.trace, "\n"))

+ }

+ t.Logf("trace:\n%s", strings.Join(w.trace, "\n"))

+// runScriptedSim runs a scripted shape's steps, checking every invariant

+// after each; false when one failed (reported).

+func runScriptedSim(t *testing.T, name string, w *simWorld, steps []func() string) bool {

+ t.Helper()

for i, step := range steps {

w.viols = nil

action := step()

w.trace = append(w.trace, fmt.Sprintf("%3d %s %s", i+1, action, w.summary()))

w.check()

for _, v := range w.viols {

- t.Errorf("INVARIANT %d (%s) violated in the scripted seed-531 shape at step %d (%s): %s\ntrace:\n%s",

- v.inv, updateSimInvariants[v.inv], i+1, action, v.msg, strings.Join(w.trace, "\n"))

+ t.Errorf("INVARIANT %d (%s) violated in %s at step %d (%s): %s\ntrace:\n%s",

+ v.inv, updateSimInvariants[v.inv], name, i+1, action, v.msg, strings.Join(w.trace, "\n"))

}

if len(w.viols) > 0 {

- return

+ return false

}

- if st := w.state; st == nil || st.Completed != 1 || st.CompletedFailed || w.boxes[0].live != "b3" {

- t.Errorf("scripted seed-531 shape: after the unpinned pass and wake on box0, live %q, build state %+v; want b3 live and R1 completed by it\ntrace:\n%s",

- w.boxes[0].live, w.state, strings.Join(w.trace, "\n"))

+ return true

+// testUpdateSimCarryFence is Astra round 2 finding 2's shape (ruling

+// R-CARRY-FENCE), scripted both ways. Box 0 resolves R1 to b2 and installs

+// it; b2 then fails on box 0, so root's next pass there records R1

+// completed, failed. That pass races a graceful cut to box 1. Early (its

+// fence first) it publishes, and the cut carries the failed completion: box

+// 1 never selects R1. Late (the cut's fence first) it meets the cut's hold

+// and publishes nothing: R1 is still pending with T b2, which box 1 does not

+// hold as failed, so box 1 installs b2 and its wake completes R1. A late

+// record published past the hold (the fence's re-check removed) is left

+// behind on box 0, and box 1 selects R1 after it completed (invariant 1).

+func testUpdateSimCarryFence(t *testing.T) {

+ for _, late := range []bool{false, true} {

+ name := "the carry fence, root's pass before the hold"

+ if late {

+ name = "the carry fence, root's pass after the carry"

+ }

+ w := newUpdateSimWorld(0, false)

+ w.scripted = true

+ for i := range w.boxes {

+ w.boxes[i] = newSimBox(fmt.Sprintf("box%d", i))

+ }

+ w.builds = []string{"b1", "b2"}

+ for i, b := range w.builds {

+ w.tags[b], w.major[b], w.promoted[b] = fmt.Sprintf("1.%d.0", i+1), 1, true

+ }

+ w.head = "b2"

+ for _, b := range w.boxes {

+ b.eligible["b1"], b.eligible["b2"] = true, true

+ }

+ w.state = &BuildState{Schema: 1, Host: updateSimHost, LastExecuted: "b1"}

+ w.lastRan, w.replica = "b1", true

+ w.at = 0

+ w.boxes[0].live, w.boxes[0].staged["b1"] = "b1", true

+ w.boxes[0].copy = BuildStateCopy{Known: true, Replica: true, State: cloneSimState(w.state)}

+ w.settings = UpdateSettings{Updates: UpdatesManual, InstallRequest: 1}

+ steps := []func() string{

+ func() string { return w.rootPass(w.boxes[0], true) },

+ func() string { w.boxes[0].failed["b2"] = true; return "mark-failed b2 on box0" },

+ func() string {

+ return w.moveToRacing(1, true, func() string { return w.rootPass(w.boxes[0], true) }, late)

+ },

+ func() string { return w.rootPass(w.boxes[1], true) },

+ func() string { return w.wake(w.boxes[1]) },

+ }

+ if !runScriptedSim(t, name, w, steps) {

+ continue

+ }

+ st, c := w.state, w.boxes[0].consumed

+ switch {

+ case !late && (st == nil || st.Completed != 1 || !st.CompletedFailed || w.boxes[1].live == "b2"):

+ t.Errorf("%s: build state %+v, box1 live %q; want R1 carried completed, failed, and b2 never installed on box1\ntrace:\n%s",

+ name, st, w.boxes[1].live, strings.Join(w.trace, "\n"))

+ case late && (c == nil || c.Completed != 0 || st == nil || st.Completed != 1 || st.CompletedFailed || w.boxes[1].live != "b2"):

+ t.Errorf("%s: box0's file %+v, build state %+v, box1 live %q; want nothing published on box0, b2 installed on box1 and R1 completed by its run\ntrace:\n%s",

+ name, c, st, w.boxes[1].live, strings.Join(w.trace, "\n"))

+ }

+ t.Logf("%s, trace:\n%s", name, strings.Join(w.trace, "\n"))

}

- t.Logf("trace:\n%s", strings.Join(w.trace, "\n"))

}

const (

@@ -268,7 +343,10 @@ func updateSimEnv(t *testing.T, name string, def int) int {

// (versions whose window has run here) and the agent's registry copy of the

// build state, which is what root reads.

type simBox struct {

- name string

+ name string

+ // status is the row's status on this box: "" (ready), or "moving" from

+ // the moment a cut holds it until the hand-over.

+ status string

consumed *Consumed

live string

failed map[string]bool

@@ -357,6 +435,8 @@ type updateSimStats struct {

heldRuns int // wakes that ran a held target

retainedRuns int // ... from a retained copy

keptCopies int // returns onto a kept, possibly stale, copy

+ racingEarly int // root passes racing a cut that published before its carry

+ racingFenced int // ... that met the move hold under the fence: nothing published

}

func (s *updateSimStats) add(o updateSimStats) {

@@ -383,6 +463,8 @@ func (s *updateSimStats) add(o updateSimStats) {

s.heldRuns += o.heldRuns

s.retainedRuns += o.retainedRuns

s.keptCopies += o.keptCopies

+ s.racingEarly += o.racingEarly

+ s.racingFenced += o.racingFenced

}

func (s updateSimStats) String() string {

@@ -392,11 +474,12 @@ func (s updateSimStats) String() string {

"left-behind records acted past %d, moves %d (returns %d, onto a kept copy %d), "+

"cuts that carried a request record %d (a failed completion %d), wakes refused unread %d, "+

"wakes with no decision for the settings %d (ran the installed build %d), wakes that waited on root %d, "+

- "held runs %d (from a retained copy %d)",

+ "held runs %d (from a retained copy %d), root passes racing a cut %d (published before the carry %d, fenced %d)",

s.resolutions, s.failedHeadResolutions, s.pinnedEligible, s.runCompletions, s.failedCompletions,

s.heldBakingPasses, s.heldRecoveries, s.unknownWithCompleted, s.unknownReturning, s.lostResolutions,

s.pickedUp, s.leftBehind, s.moves, s.returns, s.keptCopies, s.carriedRequests, s.carriedFailed,

- s.unreadRefusals, s.askRoot, s.askRootRuns, s.rootWaits, s.heldRuns, s.retainedRuns)

+ s.unreadRefusals, s.askRoot, s.askRootRuns, s.rootWaits, s.heldRuns, s.retainedRuns,

+ s.racingEarly+s.racingFenced, s.racingEarly, s.racingFenced)

}

func newUpdateSimWorld(seed int64, strict bool) *simWorld {

@@ -576,45 +659,70 @@ func (w *simWorld) refreshCopy(b *simBox) bool {

// returns to may still hold its row from the earlier stay, old copy and all

// (a rolled-back move's source keeps its row). It still has its old consumed

// file and live link either way.

+//

+// A third of moves race a root pass on the source that was already running

+// when the cut began (Astra round 2 finding 2). Under the carry fence it

+// either published before the cut's carry, which takes its record, or meets

+// the cut's hold and publishes nothing (moveToRacing).

func (w *simWorld) move() string {

j := w.rng.Intn(len(w.boxes) - 1)

if j >= w.at {

j++

}

- return w.moveTo(j, w.rng.Intn(100) < 50)

+ carried := w.rng.Intn(100) < 50

+ if w.rng.Intn(100) < 33 {

+ src := w.cur()

+ return w.moveToRacing(j, carried, func() string { return w.rootPass(src, true) }, w.rng.Intn(100) < 50)

+ }

+ return w.moveTo(j, carried)

}

// moveTo moves the instance to box j; carried is whether the destination's

// registry row carries the source's build-state copy.

func (w *simWorld) moveTo(j int, carried bool) string {

- return w.moveToRacing(j, carried, nil)

+ return w.moveToRacing(j, carried, nil, false)

}

-// moveToRacing is moveTo with race, when set, run on the source after the

-// cut's carry and before the hand-over (a root pass already in flight when

-// the cut began). Before the hand-over the cut carries the source's request

-// record into the build state under the lease (release.CarryRequest; ruling

-// R-SPEC-43A-2), and the source's registry copy follows the write, as

-// buildStates.write sets it.

-func (w *simWorld) moveToRacing(j int, carried bool, race func() string) string {

+// moveToRacing is moveTo with race, when set, a root pass on the source that

+// was already running when the cut began, modelled through the carry fence

+// (ruling R-CARRY-FENCE). Root's publication and the cut's carry serialize

+// on one lock, the cut takes it only once its hold is effective, and root

+// re-checks the hold under it (publishGate, in rootPass). So the race runs

+// either before the hold (early: its fence came first; it publishes, and

+// the carry below takes the record) or after the carry (late: its fence

+// came second; it meets the hold and publishes nothing). The cut holds the

+// row ("moving"), then carries the source's request record into the build

+// state under the lease (release.CarryRequest; ruling R-SPEC-43A-2), and the

+// source's registry copy follows the write, as buildStates.write sets it.

+// Invariant 1's carried watermark is the source's file at the hand-over,

+// after both (Astra round 2's simulation note: never sampled before a

+// racing callback).

+func (w *simWorld) moveToRacing(j int, carried bool, race func() string, late bool) string {

src := w.cur()

dst := w.boxes[j]

note := ""

+ if race != nil && !late {

+ note += " | racing (before the hold) " + race()

+ w.stats.racingEarly++

+ }

+ src.status = "moving"

next := CarryRequest(cloneSimState(w.state), cloneSimConsumed(src.consumed))

if !SameRequestState(w.state, &next) {

next.Schema, next.Host = 1, updateSimHost

w.state = &next

src.copy = BuildStateCopy{Known: true, Replica: w.replica, State: cloneSimState(&next)}

w.stats.carriedRequests++

- note = " carried " + simRes(next.Resolved) + fmt.Sprintf(" done %d%s", next.Completed, simFailedMark(next.CompletedFailed))

+ note += " carried " + simRes(next.Resolved) + fmt.Sprintf(" done %d%s", next.Completed, simFailedMark(next.CompletedFailed))

+ }

+ if race != nil && late {

+ note += " | racing (after the carry) " + race()

+ w.stats.racingFenced++

}

if c := src.consumed; c != nil && c.CompletedFailed && c.Completed > w.carried {

w.carried = c.Completed

w.stats.carriedFailed++

}

- if race != nil {

- note += " | racing " + race()

- }

+ src.status = ""

kept := false

switch {

case carried:

@@ -880,6 +988,15 @@ func (w *simWorld) rootPass(b *simBox, resolve bool) string {

in.Failed = func(v string) bool { return failed[v] }

}

dec = Target(in)

+ if resolve {

+ // publishConsumed: root's record is written under the carry

+ // fence, and only for a row no move holds (ruling

+ // R-CARRY-FENCE). A refused pass publishes nothing and installs

+ // nothing for the route: the decision never happened.

+ if err := publishGate(&registry.Route{Host: updateSimHost, Kind: "instance", Status: b.status}); err != nil {

+ return fmt.Sprintf("%s@%s %s: fenced: nothing published or installed", who, b.name, simDec(dec))

+ }

w.checkEvidence(dec, head)

w.checkDecision(b, in, dec, resolve, wmBefore, held)

if resolve {