amadan

carlos / platform Public

enginesim: I1 is the fence condition, checked at every start (#335 plan 1)

INV-I1 now requires the edge's fenced counter to cover the group's 1
(NULL, unloaded and written-but-unfenced groups fail), with the served-map
check kept for a counter advanced without a swap. It runs when each
process starts, on every path including systemd and socket starts, so an
unfenced start that adoption replaces within the step is still caught.
New witness: set-before-repoint with Restart=always between the repoint
and the restart. mark-on-final-upstream's alias and path-map scenarios
are separate witnesses. TestI1Oracle pins the unfenced states.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
claude 797bda096fbdbbe3a69519eb75eeada3a66ab035 parent 68b2b65
3 files changed, +150 −35
  • internal/sim/engines/invariants_test.go +44 −20
  • internal/sim/engines/launch_test.go +1 −0
  • internal/sim/engines/witness_test.go +105 −15
diff --git a/internal/sim/engines/invariants_test.go b/internal/sim/engines/invariants_test.go
index 0cc849ce2..4be0034c0 100644
--- a/internal/sim/engines/invariants_test.go
+++ b/internal/sim/engines/invariants_test.go
@@ -30,30 +30,54 @@ func invariantOf(violation string) string {
//
// - INV-P (event, recorded in deliver): a public request is never delivered
// to a process whose build declares doc_engine.
-// - INV-I1 (state, checked at every step boundary): no process of a
-// declaring build runs while its group is not fenced as internal. The
-// check reads the fact the fence stands for, the edge's served map (no
-// row of the group is served public), not the fenced counter a launch
-// reads: the counter is what a broken fence gets wrong. A row the edge
-// has not loaded, or serves NULL, is refused, so it does not count.
+// - INV-I1: no process of a declaring build runs unless its group is fenced
+// as internal. Checked when each process starts, on every launch path
+// (systemd and socket starts included), and again at every step boundary
+// for every running process, since a later change can unfence a group
+// 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.
+// 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.
-// check runs the state invariants. doStep calls it after every action; a
-// witness calls it at each of its step boundaries.
+// i1Broken reports why process p breaks I1, or "" when it does not.
+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])
+ }
+ hosts := make([]string, 0, len(b.EdgeRows))
+ for h := range b.EdgeRows {
+ hosts = append(hosts, h)
+ }
+ sort.Strings(hosts)
+ for _, h := range hosts {
+ if edgeGroup(b, h) == p.Group && b.Serving[h] == markPublic {
+ return fmt.Sprintf("the edge serves %s public", h)
+ }
+ }
+ return ""
+}
+
+// checkStart is I1 at the moment process p starts.
+func (w *world) checkStart(b *box, p *proc) {
+ if why := w.i1Broken(b, p); why != "" {
+ w.fail("INV-I1", "box%d: process %d of %s started v%d, which declares doc_engine: %s", b.ID, p.ID, p.Group, p.Ver, why)
+ }
+}
+
+// check runs the state invariants over every running process. doStep calls
+// it after every action; a witness calls it at each of its step boundaries.
func (w *world) check() {
for _, b := range w.boxes {
- hosts := make([]string, 0, len(b.EdgeRows))
- for h := range b.EdgeRows {
- hosts = append(hosts, h)
- }
- sort.Strings(hosts)
for _, p := range b.Procs {
- if !w.builds[p.Ver].Declares {
- continue
- }
- for _, h := range hosts {
- if edgeGroup(b, h) == p.Group && b.Serving[h] == markPublic {
- w.fail("INV-I1", "box%d: process %d of %s runs v%d, which declares doc_engine, while the edge serves %s public", b.ID, p.ID, p.Group, p.Ver, h)
- }
+ if why := w.i1Broken(b, p); why != "" {
+ w.fail("INV-I1", "box%d: process %d of %s runs v%d, which declares doc_engine: %s", b.ID, p.ID, p.Group, p.Ver, why)
}
}
}
diff --git a/internal/sim/engines/launch_test.go b/internal/sim/engines/launch_test.go
index 7d781928e..b5bf36f27 100644
--- a/internal/sim/engines/launch_test.go
+++ b/internal/sim/engines/launch_test.go
@@ -98,6 +98,7 @@ func (w *world) launch(b *box, g string, ver int, path string) bool {
p := &proc{ID: w.nextID, Group: g, Ver: ver, Slice: "inst:" + g}
b.Procs = append(b.Procs, p)
w.logf("box%d: %s started %s v%d as process %d", b.ID, path, g, ver, p.ID)
+ w.checkStart(b, p)
return true
}
diff --git a/internal/sim/engines/witness_test.go b/internal/sim/engines/witness_test.go
index c3091034e..31cae6dba 100644
--- a/internal/sim/engines/witness_test.go
+++ b/internal/sim/engines/witness_test.go
@@ -23,14 +23,16 @@ import (
type witness struct {
rule string // the rule it is for
needs string // the mutation set under which it must violate: the rule alone, or a combination the rule belongs to
- want string // the failure the scenario names: a substring of the first violation
+ want string // the failure the scenario names: a substring of the first violation; "+X" parts must also be recorded
note string // what it shows
run func(t *testing.T, w *world)
}
var witnesses = []witness{
- {"set-before-repoint", "set-before-repoint", "INV-P",
- "R2-1: adoption of a declaring build over a public route; between the repoint and the restart's gate a public request socket-activates the live unit and is served by the declaring build", wSetBeforeRepoint},
+ {"set-before-repoint", "set-before-repoint", "INV-I1+INV-P",
+ "R2-1: adoption of a declaring build over a public route; between the repoint and the restart's gate a public request socket-activates the live unit under 0 (INV-I1 at the start) and is served by the declaring build (INV-P)", wSetBeforeRepoint},
+ {"set-before-repoint", "set-before-repoint", "INV-I1",
+ "R2-1: between the repoint and the restart's gate, Restart=always starts the live unit, a declaring build, under 0; the restart then fences and replaces it, so only the check at the start sees it", wSetBeforeRepointSystemd},
{"fence-needs-reload", "fence-needs-reload", "INV-I1",
"R10-1: the edge's reload keeps failing; a failed reload that advances the fenced counter lets adoption repoint and start the declaring build under the public map", wFenceNeedsReload},
{"fence-drains-admitted", "fence-drains-admitted", "INV-P",
@@ -41,8 +43,8 @@ var witnesses = []witness{
"redundant alone: adoption's set-before is the same gate reached earlier, so with it in place the restart's gate finds the group fenced; with both gone adoption starts the declaring build under 0", wGateAdopt},
{"gate-swap", "gate-swap", "INV-I1",
"R7-1: a generation swap's incoming generation is a declaring build; ungated, it starts under 0", wGateSwap},
- {"gate-fallback", "gate-fallback", "INV-P",
- "R9-1: after --public the first wake fails and the wake plan falls back to a declaring GoodVersion; ungated, the triggering public request is served by it", wGateFallback},
+ {"gate-fallback", "gate-fallback", "INV-I1+INV-P",
+ "R9-1: after --public the first wake fails and the wake plan falls back to a declaring GoodVersion; ungated, it starts under 0 (INV-I1) and the triggering public request is served by it (INV-P)", wGateFallback},
{"gate-recovery", "gate-recovery", "INV-I1",
"R9-1: wake recovery picks a declaring GoodVersion; ungated, it starts under 0", wGateRecovery},
{"gate-seed", "gate-seed", "INV-I1",
@@ -56,7 +58,9 @@ var witnesses = []witness{
{"live-link-only-adoption", "live-link-only-adoption", "INV-I1",
"R11: something other than adoption moves the live link to a declaring build; systemd's Restart=always starts it, ungated, under 0", wLiveLinkOnly},
{"mark-on-final-upstream", "mark-on-final-upstream", "INV-P",
- "R1-2: public requests through an alias and through a path map whose final upstream is the engine; checked on the requested row, they reach the engine", wMarkOnFinalUpstream},
+ "R1-2: a public request through an alias whose final upstream is the engine; checked on the alias row, it reaches the engine", wMarkOnFinalUpstreamAlias},
+ {"mark-on-final-upstream", "mark-on-final-upstream", "INV-P",
+ "R1-2: a public request through a static row's path map whose final upstream is the engine; checked on the static row, it reaches the engine", wMarkOnFinalUpstreamPath},
}
// TestWitnesses is the deterministic half of the mutation evidence.
@@ -167,7 +171,7 @@ func check(t *testing.T, x witness, m string, expectViolation bool, trace bool)
case expectViolation && !violated:
t.Errorf("witness %s held under %q, which it must violate", x.rule, m)
dump(t, w)
- case expectViolation && !namedFailure(w.violations[0], x.want):
+ case expectViolation && !wantMet(w.violations, x.want):
t.Errorf("witness %s under %q violated, but not its named failure %q", x.rule, m, x.want)
dump(t, w)
case !expectViolation && violated:
@@ -179,6 +183,25 @@ func check(t *testing.T, x witness, m string, expectViolation bool, trace bool)
}
}
+// wantMet: the first violation names want's first part, and every further
+// "+" part is named by some recorded violation.
+func wantMet(vs []string, want string) bool {
+ parts := strings.Split(want, "+")
+ if len(vs) == 0 || !namedFailure(vs[0], parts[0]) {
+ return false
+ }
+ for _, f := range parts[1:] {
+ found := false
+ for _, v := range vs {
+ found = found || namedFailure(v, f)
+ }
+ if !found {
+ return false
+ }
+ }
+ return true
+}
+
// namedFailure: the violation names the witness's failure. want is one
// failure or several separated by "|"; a failure that ends in a digit must not
// run on into another (INV-I1 is not INV-I10).
@@ -328,6 +351,15 @@ func wSetBeforeRepoint(t *testing.T, w *world) {
w.check()
}
+// wSetBeforeRepointSystemd (R2-1): adoption repoints the live link to a
+// declaring build; before its restart, Restart=always starts the live unit
+// (no activator, no gate). No request is involved.
+func wSetBeforeRepointSystemd(t *testing.T, w *world) {
+ b := w.publicEngine(t)
+ w.adopt(b, eng, vEngine, func() { w.systemdRestart(b, eng) })
+ w.check()
+}
+
// wFenceDrainsAdmitted (R3-1): a request admitted at 0 waits in the
// activator's queue while adoption marks, fences, repoints and restarts; it
// then resumes.
@@ -457,20 +489,78 @@ func wLiveLinkOnly(t *testing.T, w *world) {
w.check()
}
-// wMarkOnFinalUpstream (R1-2): the engine runs fenced as internal; public
-// requests arrive through the alias row and through the path map of a static
-// row, both of which resolve to the engine's row.
-func wMarkOnFinalUpstream(t *testing.T, w *world) {
+// markOnFinalUpstream (R1-2): the engine runs fenced as internal; one public
+// request arrives by host and path, a row that resolves to the engine's row.
+func markOnFinalUpstream(t *testing.T, w *world, host, path string) {
b := w.boxes[0]
b.Live[eng], b.Good[eng] = vEngine, vEngine
if !w.launch(b, eng, vEngine, "seed") {
t.Fatalf("witness: the engine did not start under its fenced mark: %s", w.boxesState())
}
w.check()
- for _, try := range []struct{ host, path string }{{engAlias, "/"}, {engSite, engSitePath}} {
- if r := w.admitPublic(b, try.host, try.path); r != nil {
- w.deliver(r)
- }
+ if r := w.admitPublic(b, host, path); r != nil {
+ w.deliver(r)
+ }
+ w.check()
+}
+
+func wMarkOnFinalUpstreamAlias(t *testing.T, w *world) { markOnFinalUpstream(t, w, engAlias, "/") }
+func wMarkOnFinalUpstreamPath(t *testing.T, w *world) {
+ markOnFinalUpstream(t, w, engSite, engSitePath)
+}
+
+// TestI1Oracle pins INV-I1 on hand-built states of box 0's engine group with
+// a declaring process running: the fence condition alone catches a group that
+// is NULL, unloaded by the edge, or written and swapped but unacknowledged;
+// the served-map condition alone catches a counter advanced without a swap.
+func TestI1Oracle(t *testing.T) {
+ cases := []struct {
+ name string
+ setup func(w *world, b *box)
+ want string // "" holds; else a substring of the reason
+ }{
+ {"fenced as internal", func(w *world, b *box) {}, ""},
+ {"NULL in the registry and the map", func(w *world, b *box) {
+ b.Mark[engHost] = markNull
+ b.Serving[engHost] = markNull
+ }, "not fenced"},
+ {"written 1, absent from the edge's map", func(w *world, b *box) {
+ w.stubPublic(b, eng)
+ w.writeMark(b, eng, markInternal)
+ delete(b.EdgeRows, engHost)
+ delete(b.Serving, engHost)
+ }, "not fenced"},
+ {"written 1 and swapped in, fence not acknowledged", func(w *world, b *box) {
+ w.stubPublic(b, eng)
+ w.writeMark(b, eng, markInternal)
+ b.Serving[engHost] = markInternal
+ }, "not fenced"},
+ {"counter advanced without a swap", func(w *world, b *box) {
+ w.stubPublic(b, eng)
+ w.writeMark(b, eng, markInternal)
+ b.Fenced = b.Wrote
+ }, "serves " + engHost + " public"},
+ }
+ for _, c := range cases {
+ w := newWitness()
+ b := w.boxes[0]
+ c.setup(w, b)
+ p := &proc{ID: 99, Group: eng, Ver: vEngine, Slice: "inst:" + eng}
+ b.Procs = append(b.Procs, p)
+ why := w.i1Broken(b, p)
w.check()
+ switch {
+ case c.want == "" && (why != "" || len(w.violations) > 0):
+ t.Errorf("%s: want held, got %q %v", c.name, why, w.violations)
+ case c.want != "" && !strings.Contains(why, c.want):
+ t.Errorf("%s: reason %q, want it to name %q", c.name, why, c.want)
+ case c.want != "" && (len(w.violations) != 1 || invariantOf(w.violations[0]) != "INV-I1"):
+ t.Errorf("%s: check recorded %v, want one INV-I1", c.name, w.violations)
+ }
+ // a plain build in the same state breaks nothing
+ p.Ver = vPlain
+ if why := w.i1Broken(b, p); why != "" {
+ t.Errorf("%s: a non-declaring process breaks I1: %q", c.name, why)
+ }
}
}