amadan
enginesim: a new row's NULL is never fenced; launches honour --public's group lock (#335 plan 1, final review)
Finding 1: a group has a fence generation (SetAt) only once a change has closed it; a newly created or unseen NULL row has none, so a first declaring launch writes 1 and waits for a fence whose epoch bump drains the box. The upgrade's restart records a generation for every closed group. I1 reads fencedTruth, which no mutation weakens. New rule new-group-fenced and witness wNewGroupFenced (the reviewer's held-request counterexample). Finding 2: the lock --public holds is per group and covers its whole run; every launch through the gate honours it (clear-launch-lock), adoption's repoint still honours it (public-holds-lock). New clear hook stage "confirmed" after the empty check, in the walk and in witness wClearLaunchLock.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
7 files changed,
+151
−35
internal/sim/engines/classify_test.go+23 −9internal/sim/engines/edge_test.go+32 −12internal/sim/engines/invariants_test.go+8 −4internal/sim/engines/launch_test.go+10 −3internal/sim/engines/rules_test.go+6 −1internal/sim/engines/witness_test.go+64 −1internal/sim/engines/world_test.go+8 −5
diff --git a/internal/sim/engines/classify_test.go b/internal/sim/engines/classify_test.go| index 78d6d4454..5e20dbc3c 100644 |
| --- a/internal/sim/engines/classify_test.go |
| +++ b/internal/sim/engines/classify_test.go |
| @@ -332,6 +332,13 @@ func (w *world) upgrade(b *box) { |
| } |
| b.Admitted = nil |
| b.Fenced = b.Wrote |
| + // the restart loaded every group's mark and drained the whole box: a |
| + // fence for every closed group, NULL included |
| + for _, g := range gs { |
| + if w.closed(b, g) && !w.recorded(b, g) { |
| + b.SetAt[g] = b.Wrote |
| + } |
| + } |
| w.logf("box%d: upgrade: listeners open on the classified map, epoch %d, fenced %d", b.ID, b.Epoch, b.Fenced) |
| } |
| @@ -389,7 +396,9 @@ func (w *world) upgradeResidual(b *box) (string, []*proc) { |
| // ---------- the operator clear ---------- |
| // operatorPublic is `carlos route --host <host> --public` on group g (spec |
| -// §5.1, "Becoming public is never automatic"). Holding the adoption lock: |
| +// §5.1, "Becoming public is never automatic"). Holding the group's lock for |
| +// its whole run (adoption's repoint honours it, public-holds-lock; so does |
| +// every launch through the gate, clear-launch-lock): |
| // 1. refuse unless the live manifest is readable and does not declare |
| // (public-checks-live), and no row of the group holds the grant; |
| // 2. stop the whole group (public-stops-group); |
| @@ -398,14 +407,12 @@ func (w *world) upgradeResidual(b *box) (string, []*proc) { |
| // |
| // Step 3 is what catches a stop that did not complete (w.clearStopMisses). |
| // |
| -// w.clearHook, if set, runs after step 1 ("locked") and after step 2 |
| -// ("stopped"). |
| +// w.clearHook, if set, runs after step 1 ("locked"), after step 2 |
| +// ("stopped") and after step 3 ("confirmed"). |
| func (w *world) operatorPublic(b *box, g string) bool { |
| - w.logf("box%d: --public %s: taking the adoption lock", b.ID, g) |
| - if on("public-holds-lock") { |
| - b.Locked = true |
| - defer func() { b.Locked = false }() |
| - } |
| + w.logf("box%d: --public %s: taking the group's lock", b.ID, g) |
| + b.Locked[g] = true |
| + defer delete(b.Locked, g) |
| if on("public-checks-live") { |
| live, ok := w.builds[b.Live[g]] |
| if b.Live[g] == 0 || !ok || !live.ManifestOK || live.Declares { |
| @@ -426,6 +433,7 @@ func (w *world) operatorPublic(b *box, g string) bool { |
| w.logf("box%d: --public %s: refused: a cgroup of the group is not empty", b.ID, g) |
| return false |
| } |
| + w.hook(b, g, "confirmed") |
| w.writeMark(b, g, markPublic) |
| w.logf("box%d: --public %s: 0 written; the lock is released", b.ID, g) |
| return true |
| @@ -505,7 +513,7 @@ func init() { |
| if g == "" { |
| return |
| } |
| - switch w.rng.Intn(4) { |
| + switch w.rng.Intn(5) { |
| case 1: // an adoption tries to run during the clear |
| w.clearHook = func(hb *box, hg, stage string) { |
| if stage == "locked" { |
| @@ -524,6 +532,12 @@ func init() { |
| w.launch(hb, hg, w.pickVer(), "swap") |
| } |
| } |
| + case 4: // a launch races the write of 0, after the empty check |
| + w.clearHook = func(hb *box, hg, stage string) { |
| + if stage == "confirmed" { |
| + w.launch(hb, hg, w.pickVer(), []string{"cmd", "recovery", "seed"}[w.rng.Intn(3)]) |
| + } |
| + } |
| } |
| w.clearStopMisses = w.rng.Intn(4) == 0 |
| w.operatorPublic(b, g) |
diff --git a/internal/sim/engines/edge_test.go b/internal/sim/engines/edge_test.go| index e619f82d8..42d9b7e8a 100644 |
| --- a/internal/sim/engines/edge_test.go |
| +++ b/internal/sim/engines/edge_test.go |
| @@ -71,11 +71,13 @@ func (w *world) groupMark(b *box, g string) mark { |
| } |
| // writeMark writes mark m on every registry row of group g: one registry |
| -// change, so Wrote counts it. A change that closes an open group (to 1, or to |
| -// NULL, which the edge refuses alike) is the one a fence must reach (SetAt). |
| -// 1 written over a closed NULL moves nothing: the edge already refuses it. |
| +// change, so Wrote counts it. A change that closes a group the edge has not |
| +// fenced closed (an open group, or a new row's NULL the edge has never |
| +// loaded) is the one a fence must reach: it records the group's fence |
| +// generation (SetAt). 1 written over a NULL whose generation is recorded |
| +// moves nothing: the edge already refuses it. |
| func (w *world) writeMark(b *box, g string, m mark) { |
| - wasClosed := w.closed(b, g) |
| + wasClosed := w.closed(b, g) && (w.recorded(b, g) || !on("new-group-fenced")) |
| b.Wrote++ |
| for _, h := range w.groupHosts(b, g) { |
| b.Mark[h] = m |
| @@ -89,16 +91,34 @@ func (w *world) writeMark(b *box, g string, m mark) { |
| } |
| } |
| -// fenced: the edge's fenced counter has reached the registry change that set |
| -// group g's mark to 1, and no later change has cleared it (I1's "fenced"). |
| +// recorded: group g has a fence generation, the registry change at which it |
| +// last closed (SetAt has the key). A group whose rows are new, or were |
| +// created NULL and never written, has none. |
| +func (w *world) recorded(b *box, g string) bool { |
| + _, ok := b.SetAt[g] |
| + return ok |
| +} |
| + |
| +// fenced is the gate's reading of I1's "fenced": the group is closed, it has |
| +// a fence generation, and the edge's fenced counter has reached it (no later |
| +// change has cleared it). |
| // |
| -// NULL counts as closed here: the edge refuses NULL like 1 (spec §5.1, "The |
| -// column"), and the upgrade deliberately leaves NULL a group whose live |
| -// manifest it cannot read, whatever runs in it ("Classification before |
| -// serving"). A group closed only by NULL is fenced once the edge has loaded |
| -// the change that closed it. |
| +// NULL counts as closed here only once the edge has loaded that NULL: the |
| +// group has a recorded generation, set by the change that closed it, and the |
| +// reload that reached it bumped the epoch and drained every older public |
| +// request on the box (the upgrade's restart is such a fence). A newly created |
| +// or unseen row is NULL in the registry but has no generation, so a first |
| +// declaring launch writes 1 and waits for the fence like any other |
| +// (new-group-fenced; final review, finding 1). |
| func (w *world) fenced(b *box, g string) bool { |
| - return w.closed(b, g) && b.Fenced >= b.SetAt[g] |
| + return (w.recorded(b, g) || !on("new-group-fenced")) && w.closed(b, g) && b.Fenced >= b.SetAt[g] |
| +} |
| + |
| +// fencedTruth is the oracle's fenced: fenced with every rule in place. I1 |
| +// reads it, so a mutation that weakens the gate's reading cannot weaken the |
| +// invariant too. |
| +func (w *world) fencedTruth(b *box, g string) bool { |
| + return w.recorded(b, g) && w.closed(b, g) && b.Fenced >= b.SetAt[g] |
| } |
| // closed: group g has a row and none of its registry rows is 0. |
diff --git a/internal/sim/engines/invariants_test.go b/internal/sim/engines/invariants_test.go| index d3746b984..8e921eed8 100644 |
| --- a/internal/sim/engines/invariants_test.go |
| +++ b/internal/sim/engines/invariants_test.go |
| @@ -37,8 +37,8 @@ func invariantOf(violation string) string { |
| // under a process already running. It is two conditions: |
| // 1. the fence itself, as the spec states I1: the edge's fenced counter |
| // has reached the registry change that set the group's mark to 1, and |
| -// nothing later cleared it (fenced). A group NULL, unloaded or written |
| -// but not yet fenced fails here. |
| +// nothing later cleared it (fencedTruth). A group open, NULL but never |
| +// loaded (a new row), unloaded or written but not yet fenced fails here. |
| // 2. the fact the fence stands for: no row of the group is served 0 by |
| // the edge's map. This catches a counter advanced without a swap, which |
| // condition 1 cannot see because it reads that counter. |
| @@ -48,8 +48,12 @@ func (w *world) i1Broken(b *box, p *proc) string { |
| if !w.builds[p.Ver].Declares { |
| return "" |
| } |
| - if !w.fenced(b, p.Group) { |
| - return fmt.Sprintf("the group is not fenced (registry %v, fenced %d, set at %d)", w.groupMark(b, p.Group), b.Fenced, b.SetAt[p.Group]) |
| + if !w.fencedTruth(b, p.Group) { |
| + at := "never" |
| + if w.recorded(b, p.Group) { |
| + at = fmt.Sprint(b.SetAt[p.Group]) |
| + } |
| + return fmt.Sprintf("the group is not fenced (registry %v, fenced %d, set at %s)", w.groupMark(b, p.Group), b.Fenced, at) |
| } |
| hosts := make([]string, 0, len(b.EdgeRows)) |
| for h := range b.EdgeRows { |
diff --git a/internal/sim/engines/launch_test.go b/internal/sim/engines/launch_test.go| index b5335a95b..61ce48892 100644 |
| --- a/internal/sim/engines/launch_test.go |
| +++ b/internal/sim/engines/launch_test.go |
| @@ -78,6 +78,13 @@ func (w *world) launch(b *box, g string, ver int, path string) bool { |
| if !known { |
| panic(fmt.Sprintf("launch: unknown path %q", path)) |
| } |
| + // the gate holds the group's lock from its check through process |
| + // creation; --public holds the same lock for its whole run, so a launch |
| + // that finds it held waits (here: is refused this pass) |
| + if rule != "" && b.Locked[g] && on("clear-launch-lock") { |
| + w.logf("box%d: %s %s v%d: --public holds the group's lock; not this pass", b.ID, path, g, ver) |
| + return false |
| + } |
| if rule != "" && on(rule) && !w.gate(b, g, ver, path) { |
| return false |
| } |
| @@ -155,12 +162,12 @@ func (w *world) repointAwake(b *box, g string, ver int) bool { |
| return true |
| } |
| -// repoint is adoption up to the repoint: the adoption lock (public-holds-lock), |
| +// repoint is adoption up to the repoint: the group's lock (public-holds-lock), |
| // set-before (the gate, reached before the repoint; on a timeout the link |
| // does not move and the mark stays 1), then the repoint. |
| func (w *world) repoint(b *box, g string, ver int) bool { |
| - if b.Locked && on("public-holds-lock") { |
| - w.logf("box%d: adopt %s v%d: --public holds the adoption lock; not this pass", b.ID, g, ver) |
| + if b.Locked[g] && on("public-holds-lock") { |
| + w.logf("box%d: adopt %s v%d: --public holds the group's lock; not this pass", b.ID, g, ver) |
| return false |
| } |
| if on("set-before-repoint") && !w.gate(b, g, ver, "adopt") { |
diff --git a/internal/sim/engines/rules_test.go b/internal/sim/engines/rules_test.go| index b7a6fc16c..b4e8b8b22 100644 |
| --- a/internal/sim/engines/rules_test.go |
| +++ b/internal/sim/engines/rules_test.go |
| @@ -65,7 +65,7 @@ var allRules = []string{ |
| "owner-nonempty-unique", // the owner fallback matches only non-empty backends, and only uniquely (R7-2) |
| "public-checks-live", // --public step 1: the live manifest is readable and does not declare |
| "public-stops-group", // --public step 2: stop the whole group (R7-1, R8-2) |
| - "public-holds-lock", // --public holds the adoption lock: the live link cannot move under it |
| + "public-holds-lock", // --public holds the group's lock: adoption cannot move the live link under it |
| "public-confirms-empty", // --public step 3: refuse unless every cgroup of the group is empty |
| // Task 4: the dedicated engine box and ingress (spec §5.9; §5.1 "The |
| @@ -86,4 +86,9 @@ var allRules = []string{ |
| "stale-clears-grants", // a stale, expired or never-read table grants nothing (§5.3, §6.4) |
| "armed-refuses-unisolated", // an armed box refuses flat, foreign and worker launches before they start (R3-2, R4-1) |
| "arm-checks-box", // arming refuses a box with an unisolated route or a non-empty carlos-exec@ cgroup (R5-2) |
| + |
| + // Final review (spec §5.1 "The invariant", "Becoming public is never |
| + // automatic") |
| + "new-group-fenced", // a new or unseen row's NULL is never fenced: a first declaring launch writes 1 and waits for the fence |
| + "clear-launch-lock", // the launch gate takes the group's lock, which --public holds for its whole run |
| } |
diff --git a/internal/sim/engines/witness_test.go b/internal/sim/engines/witness_test.go| index e1de808bb..c463bc041 100644 |
| --- a/internal/sim/engines/witness_test.go |
| +++ b/internal/sim/engines/witness_test.go |
| @@ -123,6 +123,12 @@ var witnesses = []witness{ |
| "R3-2: on an armed box, a flat instance starts (flat alone)", wArmedRefusesFlat}, |
| {"arm-checks-box", "arm-checks-box", "INV-ARM", |
| "R5-2: an app's worker runs in carlos-exec@ on an unarmed box; arming that does not check the box opens engine sockets beside it", wArmChecksBox}, |
| + |
| + // Final review |
| + {"new-group-fenced", "new-group-fenced", "INV-I1+INV-P", |
| + "a public request is admitted through a service row aimed at address X and held; the row is deleted; a declaring instance is provisioned at X; a new row's NULL taken as fenced lets its first launch skip the reload, so the held request is never drained and reaches the engine", wNewGroupFenced}, |
| + {"clear-launch-lock", "clear-launch-lock", "INV-I1+INV-P", |
| + "--public on an internal group whose live release is plain; after its empty check and before its write of 0, a carlos run command of a declaring build passes the gate (the group is still fenced as internal); a launch that ignores the group's lock starts it, and --public writes 0 under it", wClearLaunchLock}, |
| } |
| // TestWitnesses is the deterministic half of the mutation evidence. |
| @@ -986,7 +992,8 @@ func wPublicHoldsLock(t *testing.T, w *world) { |
| // A NULL group counts as closed once the edge has fenced the change that made |
| // it NULL: the edge refuses NULL like 1 (spec §5.1 "The column"), and the |
| // upgrade leaves a group NULL under a running declaring build whose live |
| -// manifest cannot be read (Task 3). |
| +// manifest cannot be read (Task 3). A new row's NULL, which no change closed |
| +// and no reload has drained, never counts (final review, finding 1). |
| func TestI1Oracle(t *testing.T) { |
| cases := []struct { |
| name string |
| @@ -1003,6 +1010,16 @@ func TestI1Oracle(t *testing.T) { |
| w.writeMark(b, eng, markNull) |
| w.reload(b) |
| }, ""}, |
| + {"a new row, NULL, with no fence generation", func(w *world, b *box) { |
| + for _, h := range []string{eng, engHost} { |
| + delete(b.Rows, h) |
| + delete(b.Mark, h) |
| + } |
| + delete(b.SetAt, eng) |
| + b.Rows[eng] = &row{Host: eng, Kind: "instance", App: "acct/eng", Backend: "/run/carlos/eng.sock", PathTo: map[string]string{}} |
| + b.Wrote++ |
| + w.reload(b) |
| + }, "not fenced"}, |
| {"NULL on one row, 0 served on the other", func(w *world, b *box) { |
| oraclePublic(w, b) |
| b.Mark[engHost] = markNull |
| @@ -1067,6 +1084,7 @@ func (w *world) engineFreeBox(t *testing.T) *box { |
| delete(b.Rows, h) |
| delete(b.Mark, h) |
| } |
| + delete(b.SetAt, eng) |
| b.Wrote++ |
| w.logf("witness: box0's engine rows removed (registry change %d)", b.Wrote) |
| w.reload(b) |
| @@ -1263,6 +1281,51 @@ func TestEngineBoxKeepsStaticRows(t *testing.T) { |
| } |
| } |
| +// wNewGroupFenced (final review, finding 1): on a box that homes nothing, a |
| +// service row aimed at address X admits a public request, which is held; the |
| +// row is deleted; a declaring instance is provisioned at X. Its row is new |
| +// and NULL, but the edge has never loaded it: its first launch must write 1 |
| +// and wait for a fence, whose epoch bump drains the held request. |
| +func wNewGroupFenced(t *testing.T, w *world) { |
| + b := w.engineFreeBox(t) |
| + w.addServiceRow(b, svcHost, tcpEAddr) |
| + w.reload(b) |
| + w.check() |
| + r := w.admitPublic(b, svcHost, "/") |
| + if r == nil { |
| + t.Fatalf("witness: the service row refused a public request: %s", w.boxesState()) |
| + } |
| + r.Held = true |
| + w.deleteRow(b, svcHost) |
| + if !w.provision(b, tcpE, tcpApp, tcpEAddr, vEngine) { |
| + t.Fatalf("witness: provisioning the declaring instance refused: %s", w.boxesState()) |
| + } |
| + w.check() |
| + w.deliver(r) |
| + w.check() |
| +} |
| + |
| +// wClearLaunchLock (final review, finding 2): the engine was adopted to a |
| +// plain build (the mark stays 1); the operator runs --public; after its empty |
| +// check, a carlos run command of the declaring build tries to start; then a |
| +// public request arrives. |
| +func wClearLaunchLock(t *testing.T, w *world) { |
| + b := w.boxes[0] |
| + if !w.adopt(b, eng, vEngine, nil) || !w.adopt(b, eng, vPlain, nil) { |
| + t.Fatalf("witness: adoption refused: %s", w.boxesState()) |
| + } |
| + w.check() |
| + w.clearHook = func(hb *box, g, stage string) { |
| + if stage == "confirmed" { |
| + w.launch(hb, g, vEngine, "cmd") |
| + } |
| + } |
| + w.clearPublic(b, eng) |
| + w.clearHook = nil |
| + w.requestBy(b, engHost) |
| + w.check() |
| +} |
| + |
| // ---------- Task 5: calls, identity, grants and arming ---------- |
| // shopEng is the grant every Task 5 world starts with: shop may call eng. |
diff --git a/internal/sim/engines/world_test.go b/internal/sim/engines/world_test.go| index 67ee029e9..8955bec69 100644 |
| --- a/internal/sim/engines/world_test.go |
| +++ b/internal/sim/engines/world_test.go |
| @@ -113,14 +113,15 @@ type req struct { |
| // Rows and Mark are the registry (the intent). EdgeRows and Serving are the |
| // edge's in-memory map, swapped in only by a successful reload. Wrote counts |
| // registry mark changes, Fenced is the change the edge has fenced, SetAt the |
| -// change that set a group's mark to 1 (spec §5.1, "Setting the mark"). |
| +// change that last closed a group (its fence generation; a group with no key |
| +// has never been fenced closed, spec §5.1, "Setting the mark"). |
| type box struct { |
| ID int |
| Rows map[string]*row |
| Mark map[string]mark |
| Wrote, Fenced, Epoch int |
| ReloadFails, Armed bool |
| - Locked bool // the adoption lock, held by --public |
| + Locked map[string]bool // the group's lock, held by --public for its whole run |
| Live, Good map[string]int |
| Staged map[string][]int |
| Procs []*proc |
| @@ -165,8 +166,9 @@ type world struct { |
| nextID int // process and request ids |
| // clearHook, when set, runs inside operatorPublic at each stage |
| - // ("locked": step 1 passed; "stopped": step 2 done), so a scenario or the |
| - // walk can interleave there. |
| + // ("locked": step 1 passed; "stopped": step 2 done; "confirmed": step 3 |
| + // passed, before the write of 0), so a scenario or the walk can |
| + // interleave there. |
| clearHook func(b *box, g, stage string) |
| // clearStopMisses, when set, makes operatorPublic's stop leave one |
| // process of the group behind (a unit or generation whose stop the |
| @@ -213,7 +215,7 @@ func newWorld(seed int64, verbose bool) *world { |
| newBox := func(id int) *box { |
| return &box{ID: id, Rows: map[string]*row{}, Mark: map[string]mark{}, Live: map[string]int{}, Good: map[string]int{}, Staged: map[string][]int{}, |
| EdgeRows: map[string]row{}, Serving: map[string]mark{}, SetAt: map[string]int{}, |
| - PortGrant: map[string]string{}, Listen: map[string]string{}, |
| + PortGrant: map[string]string{}, Listen: map[string]string{}, Locked: map[string]bool{}, |
| Unisolated: map[string]bool{}, Tampered: map[string]string{}} |
| } |
| home, calling := newBox(0), newBox(1) |
| @@ -223,6 +225,7 @@ func newWorld(seed int64, verbose bool) *world { |
| home.Rows[eng] = &row{Host: eng, Kind: "instance", App: "acct/eng", Backend: "/run/carlos/eng.sock", PathTo: map[string]string{}} |
| home.Rows[engHost] = &row{Host: engHost, Kind: "instance", App: "acct/eng", Owner: eng, Source: eng, Backend: "/run/carlos/eng.sock", Platform: true, PathTo: map[string]string{}} |
| home.Mark[eng], home.Mark[engHost] = markInternal, markInternal |
| + home.SetAt[eng] = 0 // closed from the start, and loaded below |
| // one public app group, shop, on the calling box |
| calling.Rows["shop"] = &row{Host: "shop", Kind: "instance", App: "acct/shop", Backend: "127.0.0.1:9001", PathTo: map[string]string{}} |
| calling.Mark["shop"] = markPublic |