amadan

carlos / platform Public

enginesim: the fence and the launch gate, I1 (#335 plan 1)

The edge's serving map, fenced counter and box-wide admission epoch;
the launch gate on every activator path, adoption's set-before, wakes,
systemd's own starts; INV-P and INV-I1; the 14 Task 2 rules, each with a
witness (gate-adopt only with set-before-repoint, which reaches the same
gate earlier); TestWitnesses in hostlife's shape.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
claude 68b2b65c2fcfbbaaf51c65eb777bbab5aa694a49 parent a54c582
6 files changed, +1178 −7
  • internal/sim/engines/edge_test.go +222 −0
  • internal/sim/engines/invariants_test.go +42 −0
  • internal/sim/engines/launch_test.go +369 −0
  • internal/sim/engines/rules_test.go +19 −1
  • internal/sim/engines/witness_test.go +476 −0
  • internal/sim/engines/world_test.go +50 −6
diff --git a/internal/sim/engines/edge_test.go b/internal/sim/engines/edge_test.go
new file mode 100644
index 000000000..b6404892d
--- /dev/null
+++ b/internal/sim/engines/edge_test.go
@@ -0,0 +1,222 @@
+package engines
+
+import "sort"
+
+// The edge side of the internal mark (spec §5.1 "Setting the mark: the
+// serving barrier", "What the edge does with it"; §5.9 box-wide fence; §6.3).
+//
+// The registry holds the mark (the intent); the edge serves the map its last
+// successful reload swapped in, and publishes the registry change it has
+// fenced. A launch trusts only the fence.
+
+// loadEdge swaps the registry into the edge's map: rows by value (a later
+// registry edit does not leak into the served map) and their marks.
+func (b *box) loadEdge() {
+ b.EdgeRows = make(map[string]row, len(b.Rows))
+ b.Serving = make(map[string]mark, len(b.Rows))
+ for h, r := range b.Rows {
+ c := *r
+ c.PathTo = make(map[string]string, len(r.PathTo))
+ for p, to := range r.PathTo {
+ c.PathTo[p] = to
+ }
+ b.EdgeRows[h] = c
+ b.Serving[h] = b.Mark[h]
+ }
+}
+
+// groupHosts is every registry row of group g, sorted.
+func (w *world) groupHosts(b *box, g string) []string {
+ var out []string
+ for h := range b.Rows {
+ if w.group(b, h) == g {
+ out = append(out, h)
+ }
+ }
+ sort.Strings(out)
+ return out
+}
+
+// groupMark is the registry's mark of group g: internal only if every row of
+// the group is, NULL if any row is NULL or the group has no row, else public.
+func (w *world) groupMark(b *box, g string) mark {
+ hosts := w.groupHosts(b, g)
+ if len(hosts) == 0 {
+ return markNull
+ }
+ all := markInternal
+ for _, h := range hosts {
+ switch b.Mark[h] {
+ case markNull:
+ return markNull
+ case markPublic:
+ all = markPublic
+ }
+ }
+ return all
+}
+
+// writeMark writes mark m on every registry row of group g: one registry
+// change, so Wrote counts it. A change that sets the group to 1 is the one a
+// fence must reach (SetAt).
+func (w *world) writeMark(b *box, g string, m mark) {
+ before := w.groupMark(b, g)
+ b.Wrote++
+ for _, h := range w.groupHosts(b, g) {
+ b.Mark[h] = m
+ }
+ if m == markInternal && before != markInternal {
+ b.SetAt[g] = b.Wrote
+ }
+ w.logf("box%d: registry change %d: %s marked %v", b.ID, b.Wrote, g, m)
+}
+
+// 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").
+func (w *world) fenced(b *box, g string) bool {
+ return w.groupMark(b, g) == markInternal && b.Fenced >= b.SetAt[g]
+}
+
+// reload is the edge's registry poll. A failed reload swaps nothing and
+// advances nothing. A successful one swaps the map; if any row went from not
+// internal to internal it bumps the box's admission epoch and cancels every
+// public request admitted under an older one (including those waiting in the
+// activator's queue); then the fenced counter reaches the registry.
+func (w *world) reload(b *box) bool {
+ if b.ReloadFails {
+ if !on("fence-needs-reload") {
+ b.Fenced = b.Wrote
+ w.logf("box%d: reload failed; fenced %d anyway", b.ID, b.Fenced)
+ return false
+ }
+ w.logf("box%d: reload failed; nothing swapped, fenced stays %d", b.ID, b.Fenced)
+ return false
+ }
+ old := b.Serving
+ b.loadEdge()
+ changed := map[string]bool{}
+ for h, m := range b.Serving {
+ if m == markInternal && old[h] != markInternal {
+ changed[h] = true
+ }
+ }
+ if len(changed) > 0 {
+ b.Epoch++
+ if on("fence-drains-admitted") {
+ kept := b.Admitted[:0]
+ for _, r := range b.Admitted {
+ // box-wide: every older public request on any row, deleted
+ // rows included (spec §5.9); without it, only the rows the
+ // change marked
+ if r.Public && r.Epoch < b.Epoch && (on("fence-box-wide") || changed[r.Row]) {
+ w.logf("box%d: fence cancels request %d (row %s, epoch %d)", b.ID, r.ID, r.Row, r.Epoch)
+ continue
+ }
+ kept = append(kept, r)
+ }
+ b.Admitted = kept
+ }
+ }
+ b.Fenced = b.Wrote
+ w.logf("box%d: reload: map swapped, epoch %d, fenced %d", b.ID, b.Epoch, b.Fenced)
+ return true
+}
+
+// admitPublic is the edge's internal check for a request with no caller: it
+// resolves the alias, the path map and the minted row to the final row, and
+// refuses when that row is internal or NULL (spec §5.1: the check runs on the
+// final resolved upstream's route). A static row answers without a proxy, so
+// nothing is admitted. Otherwise the request is admitted under the box's
+// epoch, holding the final row's backend.
+func (w *world) admitPublic(b *box, host, path string) *req {
+ asked, ok := b.EdgeRows[host]
+ if !ok {
+ w.logf("box%d: public %s%s: unknown host", b.ID, host, path)
+ return nil
+ }
+ final := asked
+ if asked.Alias != "" {
+ if final, ok = b.EdgeRows[asked.Alias]; !ok {
+ w.logf("box%d: public %s%s: alias target %s unknown", b.ID, host, path, asked.Alias)
+ return nil
+ }
+ }
+ if to, ok := final.PathTo[path]; ok {
+ if final, ok = b.EdgeRows[to]; !ok {
+ w.logf("box%d: public %s%s: path target %s unknown", b.ID, host, path, to)
+ return nil
+ }
+ }
+ checked := final
+ if !on("mark-on-final-upstream") {
+ checked = asked
+ }
+ if m := b.Serving[checked.Host]; m != markPublic {
+ w.logf("box%d: public %s%s: internal refusal (%s is %v)", b.ID, host, path, checked.Host, m)
+ return nil
+ }
+ if final.Backend == "" {
+ w.logf("box%d: public %s%s: answered by the edge (%s)", b.ID, host, path, final.Host)
+ return nil
+ }
+ w.nextID++
+ r := &req{ID: w.nextID, Epoch: b.Epoch, Row: checked.Host, Backend: final.Backend, Public: true, Box: b.ID}
+ b.Admitted = append(b.Admitted, r)
+ w.logf("box%d: public %s%s admitted as request %d (row %s, backend %s, epoch %d)", b.ID, host, path, r.ID, r.Row, r.Backend, r.Epoch)
+ return r
+}
+
+// backendGroup is the group whose process listens on backend: the group of
+// the instance row that carries it, whatever row the request came in by.
+func (w *world) backendGroup(b *box, backend string) string {
+ hosts := make([]string, 0, len(b.Rows))
+ for h := range b.Rows {
+ hosts = append(hosts, h)
+ }
+ sort.Strings(hosts)
+ for _, h := range hosts {
+ if r := b.Rows[h]; r.Kind == "instance" && r.Backend == backend {
+ return w.group(b, h)
+ }
+ }
+ return ""
+}
+
+// deliver resumes an admitted request: unless the fence cancelled it, its
+// proxy reaches the newest process of the group listening on its backend.
+// INV-P: a public request never reaches a process whose build declares
+// doc_engine.
+func (w *world) deliver(r *req) {
+ b := w.boxes[r.Box]
+ idx := -1
+ for i, x := range b.Admitted {
+ if x == r {
+ idx = i
+ }
+ }
+ if idx < 0 {
+ w.logf("box%d: request %d was cancelled; nothing delivered", b.ID, r.ID)
+ return
+ }
+ b.Admitted = append(b.Admitted[:idx], b.Admitted[idx+1:]...)
+ r.Held = false
+ g := w.backendGroup(b, r.Backend)
+ var p *proc
+ for _, x := range b.Procs {
+ if x.Group == g && g != "" {
+ p = x
+ }
+ }
+ if p == nil {
+ w.logf("box%d: request %d: no process on %s; wake failure answer", b.ID, r.ID, r.Backend)
+ return
+ }
+ r.Reached = p.ID
+ w.logf("box%d: request %d delivered to process %d (%s v%d)", b.ID, r.ID, p.ID, p.Group, p.Ver)
+ if r.Public && w.builds[p.Ver].Declares {
+ w.fail("INV-P", "box%d: public request %d (row %s) delivered to process %d of %s running v%d, which declares doc_engine", b.ID, r.ID, r.Row, p.ID, p.Group, p.Ver)
+ }
+ if p.Ver == b.Live[g] {
+ b.Good[g] = p.Ver // the live build answered: it is the good version now
+ }
+}
diff --git a/internal/sim/engines/invariants_test.go b/internal/sim/engines/invariants_test.go
index a1e618777..0cc849ce2 100644
--- a/internal/sim/engines/invariants_test.go
+++ b/internal/sim/engines/invariants_test.go
@@ -2,6 +2,7 @@ package engines
import (
"fmt"
+ "sort"
"strings"
)
@@ -24,3 +25,44 @@ func invariantOf(violation string) string {
}
return violation
}
+
+// The invariants of Task 2 (spec §5.1, §6.3):
+//
+// - 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.
+
+// check runs the state invariants. 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)
+ }
+ }
+ }
+ }
+}
+
+// edgeGroup is group over the edge's loaded rows.
+func edgeGroup(b *box, host string) string {
+ if r, ok := b.EdgeRows[host]; ok && r.Kind == "instance" && r.Owner != "" {
+ return r.Owner
+ }
+ return host
+}
diff --git a/internal/sim/engines/launch_test.go b/internal/sim/engines/launch_test.go
new file mode 100644
index 000000000..7d781928e
--- /dev/null
+++ b/internal/sim/engines/launch_test.go
@@ -0,0 +1,369 @@
+package engines
+
+import (
+ "fmt"
+ "sort"
+)
+
+// The launch gate (spec §5.1 "The invariant", "Setting the mark", "Starts
+// systemd makes on its own").
+//
+// I1: a process of a build whose manifest declares doc_engine starts only
+// after the edge has fenced its group as internal. Every activator launch
+// path ends in the gate; systemd's own starts (Restart=always, socket
+// activation) execute the live link and pass no gate, so they are safe only
+// because adoption gates before it repoints and nothing else moves the link.
+
+// fenceWaitTicks is the gate's bound: 30 s of the edge's reloads, one per
+// tick.
+const fenceWaitTicks = 3
+
+// gateRule names the rule that gates a launch path; systemd and socket
+// starts are not activator launches and have none.
+var gateRule = map[string]string{
+ "adopt": "gate-adopt",
+ "swap": "gate-swap",
+ "fallback": "gate-fallback",
+ "recovery": "gate-recovery",
+ "seed": "gate-seed",
+ "cmd": "gate-cmd",
+ "systemd": "",
+ "socket": "",
+}
+
+// gateSeesDeclaring is what the gate reads from the build's manifest: its
+// declaration, or, when the manifest cannot be read, declaring.
+func (w *world) gateSeesDeclaring(ver int) bool {
+ bd := w.builds[ver]
+ if !bd.ManifestOK {
+ return on("unreadable-declares")
+ }
+ return bd.Declares
+}
+
+// gate is the launch gate for a build about to start in group g: a build it
+// sees as declaring writes 1 if 1 is not already written, then always waits
+// for the edge's fence to cover the group's mark, within the bound. False is
+// a refused launch (the wake fails).
+func (w *world) gate(b *box, g string, ver int, path string) bool {
+ if !w.gateSeesDeclaring(ver) {
+ return true
+ }
+ wrote := false
+ if w.groupMark(b, g) != markInternal {
+ w.writeMark(b, g, markInternal)
+ wrote = true
+ }
+ if !wrote && !on("gate-waits-when-written") {
+ w.logf("box%d: gate(%s) %s v%d: 1 already written; not waiting", b.ID, path, g, ver)
+ return true
+ }
+ for i := 0; i < fenceWaitTicks && !w.fenced(b, g); i++ {
+ w.reload(b)
+ }
+ if !w.fenced(b, g) {
+ w.logf("box%d: gate(%s) %s v%d: no fence within the bound; refused", b.ID, path, g, ver)
+ return false
+ }
+ return true
+}
+
+// launch starts build ver in group g by path, through the gate where the
+// path has one. It returns false when the gate refuses.
+func (w *world) launch(b *box, g string, ver int, path string) bool {
+ rule, known := gateRule[path]
+ if !known {
+ panic(fmt.Sprintf("launch: unknown path %q", path))
+ }
+ if rule != "" && on(rule) && !w.gate(b, g, ver, path) {
+ return false
+ }
+ // a group keeps at most three processes: the oldest has exited
+ n := 0
+ for _, p := range b.Procs {
+ if p.Group == g {
+ n++
+ }
+ }
+ if n >= 3 {
+ for i, p := range b.Procs {
+ if p.Group == g {
+ b.Procs = append(b.Procs[:i], b.Procs[i+1:]...)
+ w.logf("box%d: process %d of %s exited", b.ID, p.ID, g)
+ break
+ }
+ }
+ }
+ w.nextID++
+ 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)
+ return true
+}
+
+// stopGroup stops every process of group g.
+func (w *world) stopGroup(b *box, g string) {
+ kept := b.Procs[:0]
+ for _, p := range b.Procs {
+ if p.Group != g {
+ kept = append(kept, p)
+ }
+ }
+ b.Procs = kept
+}
+
+func (w *world) running(b *box, g string) bool {
+ for _, p := range b.Procs {
+ if p.Group == g {
+ return true
+ }
+ }
+ return false
+}
+
+// adopt makes ver the live release of group g: set-before (the gate, reached
+// before the repoint; on a timeout the link does not move and the mark stays
+// 1), then the repoint, then the restart, itself a gated launch. between runs
+// after the repoint and before the restart: whatever systemd does there.
+func (w *world) adopt(b *box, g string, ver int, between func()) bool {
+ w.logf("box%d: adopt %s v%d (live v%d)", b.ID, g, ver, b.Live[g])
+ if on("set-before-repoint") && !w.gate(b, g, ver, "adopt") {
+ w.logf("box%d: adopt %s v%d: not repointed this pass", b.ID, g, ver)
+ return false
+ }
+ b.Live[g] = ver
+ staged := false
+ for _, v := range b.Staged[g] {
+ staged = staged || v == ver
+ }
+ if !staged {
+ b.Staged[g] = append(b.Staged[g], ver)
+ }
+ if b.Good[g] == 0 {
+ b.Good[g] = ver
+ }
+ w.logf("box%d: live link of %s -> v%d", b.ID, g, ver)
+ if between != nil {
+ between()
+ }
+ w.stopGroup(b, g)
+ return w.launch(b, g, ver, "adopt")
+}
+
+// wake is the activator waking group g by its wake plan: "recovery" starts
+// the recovery build, "fallback" first fails to start the live build and
+// falls back; both choose GoodVersion. The triggering request, if any, is
+// delivered afterwards (or finds the fence cancelled it).
+func (w *world) wake(b *box, g string, mode string, trigger *req) {
+ ver := b.Good[g]
+ if mode == "fallback" {
+ w.logf("box%d: wake %s: live v%d fails to start; falling back to good v%d", b.ID, g, b.Live[g], ver)
+ } else {
+ w.logf("box%d: wake %s: recovery build good v%d", b.ID, g, ver)
+ }
+ if ver != 0 {
+ w.launch(b, g, ver, mode)
+ }
+ if trigger != nil {
+ w.deliver(trigger)
+ }
+}
+
+// moveLive is anything other than adoption moving group g's live link (a
+// rollout tool, a hand repair). Only adoption, through the gate, and
+// --public may move a live link.
+func (w *world) moveLive(b *box, g string, ver int, who string) bool {
+ if on("live-link-only-adoption") {
+ w.logf("box%d: %s may not move the live link of %s; refused", b.ID, who, g)
+ return false
+ }
+ b.Live[g] = ver
+ w.logf("box%d: %s moved the live link of %s -> v%d", b.ID, who, g, ver)
+ return true
+}
+
+// systemdRestart is Restart=always: the unit's main process exits and
+// systemd starts /opt/carlos/live/<host> again, with no activator.
+func (w *world) systemdRestart(b *box, g string) {
+ if b.Live[g] == 0 {
+ return
+ }
+ w.stopGroup(b, g)
+ w.launch(b, g, b.Live[g], "systemd")
+}
+
+// socketActivate is carlos-app@.socket starting a stopped unit from the live
+// link, with no activator.
+func (w *world) socketActivate(b *box, g string) {
+ if b.Live[g] == 0 || w.running(b, g) {
+ return
+ }
+ w.launch(b, g, b.Live[g], "socket")
+}
+
+// ---------- the random walk ----------
+
+func (w *world) pickBox() *box { return w.boxes[w.rng.Intn(len(w.boxes))] }
+
+// groups is every instance group of b's registry, sorted.
+func (w *world) groups(b *box) []string {
+ seen := map[string]bool{}
+ var out []string
+ for h, r := range b.Rows {
+ if g := w.group(b, h); r.Kind == "instance" && !seen[g] {
+ seen[g] = true
+ out = append(out, g)
+ }
+ }
+ sort.Strings(out)
+ return out
+}
+
+func (w *world) pickGroup(b *box) string {
+ gs := w.groups(b)
+ if len(gs) == 0 {
+ return ""
+ }
+ return gs[w.rng.Intn(len(gs))]
+}
+
+func (w *world) pickVer() int { return 1 + w.rng.Intn(nBuilds) }
+
+// randomPublic sends one public request to a host of b's edge map, by its
+// own name, an alias or a path map.
+func (w *world) randomPublic(b *box) *req {
+ hosts := make([]string, 0, len(b.EdgeRows))
+ for h := range b.EdgeRows {
+ hosts = append(hosts, h)
+ }
+ if len(hosts) == 0 {
+ return nil
+ }
+ sort.Strings(hosts)
+ h := hosts[w.rng.Intn(len(hosts))]
+ paths := []string{"/"}
+ for p := range b.EdgeRows[h].PathTo {
+ paths = append(paths, p)
+ }
+ sort.Strings(paths[1:])
+ return w.admitPublic(b, h, paths[w.rng.Intn(len(paths))])
+}
+
+// heldFor is the oldest held request on b whose proxy reaches group g.
+func (w *world) heldFor(b *box, g string) *req {
+ for _, r := range b.Admitted {
+ if r.Held && w.backendGroup(b, r.Backend) == g {
+ return r
+ }
+ }
+ return nil
+}
+
+func init() {
+ actions = append(actions,
+ action{name: "adopt", weight: 3, run: func(w *world) {
+ b := w.pickBox()
+ g := w.pickGroup(b)
+ ver := w.pickVer()
+ var between func()
+ switch w.rng.Intn(3) {
+ case 1:
+ between = func() { w.systemdRestart(b, g) }
+ case 2:
+ between = func() {
+ if r := w.randomPublic(b); r != nil {
+ w.socketActivate(b, w.backendGroup(b, r.Backend))
+ w.deliver(r)
+ }
+ }
+ }
+ w.adopt(b, g, ver, between)
+ }},
+ action{name: "reload", weight: 4, run: func(w *world) { w.reload(w.pickBox()) }},
+ action{name: "reload-fails", weight: 1, run: func(w *world) {
+ b := w.pickBox()
+ b.ReloadFails = !b.ReloadFails && !w.calm()
+ w.logf("box%d: reload fails = %v", b.ID, b.ReloadFails)
+ }},
+ action{name: "public-request", weight: 6, run: func(w *world) {
+ b := w.pickBox()
+ r := w.randomPublic(b)
+ if r == nil {
+ return
+ }
+ if len(b.Admitted) <= 8 && w.rng.Intn(2) == 0 {
+ r.Held = true
+ w.logf("box%d: request %d held in the activator's queue", b.ID, r.ID)
+ return
+ }
+ w.deliver(r)
+ }},
+ action{name: "resume", weight: 3, run: func(w *world) {
+ var held []*req
+ for _, b := range w.boxes {
+ for _, r := range b.Admitted {
+ if r.Held {
+ held = append(held, r)
+ }
+ }
+ }
+ if len(held) == 0 {
+ return
+ }
+ sort.Slice(held, func(i, j int) bool { return held[i].ID < held[j].ID })
+ w.deliver(held[w.rng.Intn(len(held))])
+ }},
+ action{name: "wake", weight: 3, run: func(w *world) {
+ b := w.pickBox()
+ g := w.pickGroup(b)
+ mode := "recovery"
+ if w.rng.Intn(2) == 0 {
+ mode = "fallback"
+ }
+ w.stopGroup(b, g) // the group had gone to sleep
+ w.wake(b, g, mode, w.heldFor(b, g))
+ }},
+ action{name: "swap", weight: 2, run: func(w *world) {
+ b := w.pickBox()
+ g := w.pickGroup(b)
+ if w.launch(b, g, w.pickVer(), "swap") {
+ // the incoming generation serves; the outgoing ones stop
+ newest := b.Procs[len(b.Procs)-1]
+ kept := b.Procs[:0]
+ for _, p := range b.Procs {
+ if p.Group != g || p == newest {
+ kept = append(kept, p)
+ }
+ }
+ b.Procs = kept
+ }
+ }},
+ action{name: "seed", weight: 1, run: func(w *world) {
+ b := w.pickBox()
+ g := w.pickGroup(b)
+ w.stopGroup(b, g)
+ w.launch(b, g, w.pickVer(), "seed")
+ }},
+ action{name: "cmd", weight: 1, run: func(w *world) {
+ b := w.pickBox()
+ w.launch(b, w.pickGroup(b), w.pickVer(), "cmd")
+ }},
+ action{name: "systemd-restart", weight: 2, run: func(w *world) {
+ b := w.pickBox()
+ w.systemdRestart(b, w.pickGroup(b))
+ }},
+ action{name: "socket-activation", weight: 2, run: func(w *world) {
+ b := w.pickBox()
+ g := w.pickGroup(b)
+ w.stopGroup(b, g) // the unit exited idle; a connection arrives
+ w.socketActivate(b, g)
+ if r := w.heldFor(b, g); r != nil {
+ w.deliver(r)
+ }
+ }},
+ action{name: "repoint-live", weight: 1, run: func(w *world) {
+ b := w.pickBox()
+ w.moveLive(b, w.pickGroup(b), w.pickVer(), "a rollout tool")
+ }},
+ )
+}
diff --git a/internal/sim/engines/rules_test.go b/internal/sim/engines/rules_test.go
index e7dcc6500..295b927d9 100644
--- a/internal/sim/engines/rules_test.go
+++ b/internal/sim/engines/rules_test.go
@@ -35,4 +35,22 @@ func on(rule string) bool {
// allRules is the mutation list. Each task appends its rules, in spec order,
// with a comment naming the spec section each answers.
-var allRules = []string{}
+var allRules = []string{
+ // Task 2: the fence and the launch gate, I1 (spec §5.1 "The invariant",
+ // "Setting the mark: the serving barrier", "What the edge does with it",
+ // "Starts systemd makes on its own"; §5.9 the box-wide fence; §6.3)
+ "set-before-repoint", // adoption gates before it repoints the live link (R2-1)
+ "fence-needs-reload", // a failed reload advances nothing (R10-1)
+ "fence-drains-admitted", // the fence cancels public requests admitted before the swap (R3-1)
+ "fence-box-wide", // ... on every row of the box, deleted rows included (§5.9, R13-2)
+ "gate-adopt", // the gate on adoption's restart
+ "gate-swap", // ... on a swap's incoming generation (R7-1)
+ "gate-fallback", // ... on a wake plan's fallback build (R9-1)
+ "gate-recovery", // ... on a wake plan's recovery build (R9-1)
+ "gate-seed", // ... on a seed
+ "gate-cmd", // ... on a carlos run command
+ "gate-waits-when-written", // the gate waits for the fence when 1 is already written (R10-1)
+ "unreadable-declares", // an unreadable manifest is treated as declaring
+ "live-link-only-adoption", // nothing but adoption (and --public) moves a live link (R11)
+ "mark-on-final-upstream", // the edge checks the final resolved upstream's row (R1-2)
+}
diff --git a/internal/sim/engines/witness_test.go b/internal/sim/engines/witness_test.go
new file mode 100644
index 000000000..c3091034e
--- /dev/null
+++ b/internal/sim/engines/witness_test.go
@@ -0,0 +1,476 @@
+package engines
+
+import (
+ "fmt"
+ "os"
+ "sort"
+ "strings"
+ "testing"
+)
+
+// Witness scenarios, in hostlife's shape (internal/sim/hostlife/witness_test.go).
+//
+// The random sweep reaches some interleavings rarely. A witness is one
+// fixed, hand-scheduled scenario for one rule: it forces exactly the
+// interleaving the rule exists for, as a sequence of protocol steps, and
+// draws nothing from the world's RNG. It must hold (no invariant violated)
+// with the rules in place, and violate its named invariant when the rule's
+// mutation is applied, alone or in the stated combination.
+//
+// A witness calls w.check() at each step boundary, as doStep does in the
+// sweep; event invariants (INV-P at delivery) are recorded inside the step.
+
+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
+ 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},
+ {"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",
+ "R3-1: a request admitted at 0 waits in the activator's queue across the adoption; a fence that does not drain it lets it resume into the declaring build", wFenceDrainsAdmitted},
+ {"fence-box-wide", "fence-box-wide", "INV-P",
+ "R13-2: a request admitted through a service row aimed at the engine's backend; the row is deleted, the request held across a declaring adoption; a fence scoped to the group's rows leaves it, and it resumes into the engine", wFenceBoxWide},
+ {"gate-adopt", "gate-adopt,set-before-repoint", "INV-I1",
+ "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-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",
+ "a seed of a declaring build; ungated, it starts under 0", wGateSeed},
+ {"gate-cmd", "gate-cmd", "INV-I1",
+ "a carlos run command of a declaring build; ungated, it starts under 0", wGateCmd},
+ {"gate-waits-when-written", "gate-waits-when-written", "INV-I1",
+ "R10-1: adoption times out with 1 written and the reload failing; a gate that waits only when it wrote the mark lets wake recovery start a declaring GoodVersion under the public map", wGateWaitsWhenWritten},
+ {"unreadable-declares", "unreadable-declares", "INV-I1",
+ "a declaring build whose manifest cannot be read, launched under 0; read as non-declaring, it starts under 0", wUnreadableDeclares},
+ {"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},
+}
+
+// TestWitnesses is the deterministic half of the mutation evidence.
+//
+// With no mutation (the gate) it proves every witness's claim in full: the
+// scenario holds with every rule in place, holds under every proper subset of
+// its stated mutation set (so a rule a combination names is shown necessary,
+// not assumed), and under the whole set violates the failure the scenario
+// names, not merely some invariant.
+//
+// Under ENGINESIM_MUTATE=m (the harness) it runs the witnesses of the rules
+// in m; a witness whose set is within m must violate with its named failure.
+// ENGINESIM_WITNESS=rule runs one rule's witnesses with their trace.
+func TestWitnesses(t *testing.T) {
+ only := os.Getenv("ENGINESIM_WITNESS")
+ if mutated == "" {
+ ran := 0
+ for _, x := range witnesses {
+ if only != "" && x.rule != only {
+ continue
+ }
+ ran++
+ check(t, x, "", false, only != "")
+ for _, s := range properSubsets(x.needs) {
+ check(t, x, s, false, only != "")
+ }
+ check(t, x, x.needs, true, only != "")
+ }
+ if only != "" && ran == 0 {
+ t.Fatalf("no witness for rule %q", only)
+ }
+ return
+ }
+ set := mutationSet(mutated)
+ for _, x := range witnesses {
+ if only != "" && x.rule != only {
+ continue
+ }
+ if !set[x.rule] {
+ continue
+ }
+ needs := true
+ for _, m := range strings.Split(x.needs, ",") {
+ if !set[m] {
+ needs = false
+ }
+ }
+ if needs {
+ check(t, x, mutated, true, only != "")
+ continue
+ }
+ // the mutation set is not the witness's: report, enforce nothing
+ report(t, x, mutated, only != "")
+ }
+}
+
+// TestWitnessRulesKnown: every witness names a rule in allRules, and so does
+// every member of its mutation set.
+func TestWitnessRulesKnown(t *testing.T) {
+ known := map[string]bool{}
+ for _, r := range allRules {
+ known[r] = true
+ }
+ for _, x := range witnesses {
+ if !known[x.rule] {
+ t.Errorf("witness for unknown rule %q", x.rule)
+ }
+ for _, m := range strings.Split(x.needs, ",") {
+ if !known[m] {
+ t.Errorf("witness %s needs unknown rule %q", x.rule, m)
+ }
+ }
+ }
+}
+
+func report(t *testing.T, x witness, m string, trace bool) {
+ saved := mutated
+ mutated = m
+ defer func() { mutated = saved }()
+ w := newWitness()
+ x.run(t, w)
+ tag := "held"
+ if len(w.violations) > 0 {
+ tag = "violated: " + w.violations[0]
+ }
+ t.Logf("witness %s under %q (needs %q): %s", x.rule, m, x.needs, tag)
+ if trace {
+ dump(t, w)
+ }
+}
+
+// check runs one witness under mutation m, reports it, and fails the test if
+// the outcome is not the stated one: held when no violation is expected, the
+// named failure when one is.
+func check(t *testing.T, x witness, m string, expectViolation bool, trace bool) {
+ saved := mutated
+ mutated = m
+ defer func() { mutated = saved }()
+ w := newWitness()
+ x.run(t, w)
+ violated := len(w.violations) > 0
+ tag := "held"
+ if violated {
+ tag = "violated: " + w.violations[0]
+ }
+ t.Logf("witness %s under %q (needs %q): %s", x.rule, m, x.needs, tag)
+ switch {
+ 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):
+ t.Errorf("witness %s under %q violated, but not its named failure %q", x.rule, m, x.want)
+ dump(t, w)
+ case !expectViolation && violated:
+ t.Errorf("witness %s violated under %q, where it must hold", x.rule, m)
+ dump(t, w)
+ }
+ if trace {
+ dump(t, w)
+ }
+}
+
+// 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).
+func namedFailure(v, want string) bool {
+ for _, f := range strings.Split(want, "|") {
+ for i := 0; ; {
+ j := strings.Index(v[i:], f)
+ if j < 0 {
+ break
+ }
+ end := i + j + len(f)
+ last := f[len(f)-1]
+ if !(last >= '0' && last <= '9') || end == len(v) || v[end] < '0' || v[end] > '9' {
+ return true
+ }
+ i = i + j + 1
+ }
+ }
+ return false
+}
+
+func mutationSet(m string) map[string]bool {
+ set := map[string]bool{}
+ for _, x := range strings.Split(m, ",") {
+ if x != "" {
+ set[x] = true
+ }
+ }
+ return set
+}
+
+// properSubsets: every non-empty proper subset of a comma-separated set.
+func properSubsets(needs string) []string {
+ xs := strings.Split(needs, ",")
+ var out []string
+ for mask := 1; mask < (1<<len(xs))-1; mask++ {
+ var sub []string
+ for i, x := range xs {
+ if mask&(1<<i) != 0 {
+ sub = append(sub, x)
+ }
+ }
+ out = append(out, strings.Join(sub, ","))
+ }
+ return out
+}
+
+func dump(t *testing.T, w *world) {
+ for _, line := range w.trace {
+ t.Log(line)
+ }
+ t.Logf("state: %s", w.boxesState())
+}
+
+// boxesState is a one-line summary of every box, for a failing witness.
+func (w *world) boxesState() string {
+ var out []string
+ for _, b := range w.boxes {
+ hosts := make([]string, 0, len(b.Rows))
+ for h := range b.Rows {
+ hosts = append(hosts, h)
+ }
+ sort.Strings(hosts)
+ var marks []string
+ for _, h := range hosts {
+ marks = append(marks, fmt.Sprintf("%s=%v/%v", h, b.Mark[h], b.Serving[h]))
+ }
+ var procs []string
+ for _, p := range b.Procs {
+ procs = append(procs, fmt.Sprintf("%d:%s@v%d", p.ID, p.Group, p.Ver))
+ }
+ var adm []string
+ for _, r := range b.Admitted {
+ adm = append(adm, fmt.Sprintf("%d:%s@e%d", r.ID, r.Row, r.Epoch))
+ }
+ out = append(out, fmt.Sprintf("box%d{marks(reg/edge) %v wrote=%d fenced=%d epoch=%d reloadFails=%v live=%v good=%v procs=%v admitted=%v}",
+ b.ID, marks, b.Wrote, b.Fenced, b.Epoch, b.ReloadFails, b.Live, b.Good, procs, adm))
+ }
+ return strings.Join(out, " ")
+}
+
+// ---------- the fixture ----------
+
+// The witness builds: one of each kind, fixed, so no scenario depends on a
+// seed's draw.
+const (
+ vPlain = 1 // reads, does not declare
+ vEngine = 2 // reads, declares doc_engine
+ vUnreadable = 3 // declares, but its manifest cannot be read
+ vBlind = 4 // does not declare, manifest unreadable
+)
+
+func newWitness() *world {
+ w := newWorld(0, true)
+ w.builds = map[int]build{
+ vPlain: {Ver: vPlain, Declares: false, ManifestOK: true},
+ vEngine: {Ver: vEngine, Declares: true, ManifestOK: true},
+ vUnreadable: {Ver: vUnreadable, Declares: true, ManifestOK: false},
+ vBlind: {Ver: vBlind, Declares: false, ManifestOK: false},
+ }
+ w.logf("witness world: builds %s", w.buildsString())
+ return w
+}
+
+// stubPublic stands in for the operator's --public until Task 3's
+// operatorPublic: stop every process of the group, write 0, reload.
+func (w *world) stubPublic(b *box, g string) {
+ w.logf("witness: --public %s (stub: stop, write 0, reload)", g)
+ w.stopGroup(b, g)
+ w.writeMark(b, g, markPublic)
+ w.reload(b)
+ w.check()
+}
+
+// publicEngine sets the engine group on box 0 to a public route serving the
+// plain build: live and good are vPlain, the mark is 0 and fenced, and one
+// process runs.
+func (w *world) publicEngine(t *testing.T) *box {
+ b := w.boxes[0]
+ b.Live[eng], b.Good[eng] = vPlain, vPlain
+ w.stubPublic(b, eng)
+ if !w.launch(b, eng, vPlain, "seed") {
+ t.Fatalf("witness: the plain build did not start under 0: %s", w.boxesState())
+ }
+ w.check()
+ if len(w.violations) > 0 {
+ t.Fatalf("witness: the fixture violates: %v", w.violations)
+ }
+ return b
+}
+
+// ---------- the witnesses ----------
+
+// wSetBeforeRepoint (R2-1): adoption repoints the live link to a declaring
+// build; before its restart a public request arrives, socket activation
+// starts the live unit (no activator, no gate) and serves it. With the mark
+// set and fenced before the repoint, the request is refused.
+func wSetBeforeRepoint(t *testing.T, w *world) {
+ b := w.publicEngine(t)
+ w.stopGroup(b, eng)
+ w.adopt(b, eng, vEngine, func() {
+ if r := w.admitPublic(b, engHost, "/"); r != nil {
+ w.socketActivate(b, eng)
+ w.deliver(r)
+ }
+ })
+ 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.
+func wFenceDrainsAdmitted(t *testing.T, w *world) {
+ b := w.publicEngine(t)
+ r := w.admitPublic(b, engHost, "/")
+ if r == nil {
+ t.Fatalf("witness: a public request to a public route was refused")
+ }
+ r.Held = true
+ w.adopt(b, eng, vEngine, nil)
+ w.check()
+ w.deliver(r)
+ w.check()
+}
+
+// r10Sequence (R10-1): the edge's reload fails; adoption of a declaring
+// build writes 1 and times out without repointing; then wake recovery picks
+// the declaring GoodVersion.
+func r10Sequence(t *testing.T, w *world) {
+ b := w.publicEngine(t)
+ b.Good[eng] = vEngine
+ b.ReloadFails = true
+ w.logf("witness: the edge's reload starts failing")
+ w.adopt(b, eng, vEngine, nil)
+ w.check()
+ w.stopGroup(b, eng)
+ w.wake(b, eng, "recovery", nil)
+ w.check()
+}
+
+func wFenceNeedsReload(t *testing.T, w *world) { r10Sequence(t, w) }
+func wGateWaitsWhenWritten(t *testing.T, w *world) { r10Sequence(t, w) }
+
+// wFenceBoxWide (R13-2): a service row aimed at the engine's backend admits a
+// public request; the row is deleted and the request held; adoption of a
+// declaring build fences the group; the request resumes on the proxy it
+// already holds.
+func wFenceBoxWide(t *testing.T, w *world) {
+ b := w.publicEngine(t)
+ const svc = "svc.example"
+ b.Rows[svc] = &row{Host: svc, Kind: "service", Backend: b.Rows[engHost].Backend, PathTo: map[string]string{}}
+ b.Mark[svc] = markPublic
+ w.reload(b)
+ w.check()
+ r := w.admitPublic(b, svc, "/")
+ if r == nil {
+ t.Fatalf("witness: the service row refused a public request: %s", w.boxesState())
+ }
+ r.Held = true
+ delete(b.Rows, svc)
+ delete(b.Mark, svc)
+ w.logf("witness: row %s deleted; request %d still holds its proxy", svc, r.ID)
+ w.adopt(b, eng, vEngine, nil)
+ w.check()
+ w.deliver(r)
+ w.check()
+}
+
+// wGateAdopt: adoption of a declaring build with no other start.
+func wGateAdopt(t *testing.T, w *world) {
+ b := w.publicEngine(t)
+ w.adopt(b, eng, vEngine, nil)
+ w.check()
+}
+
+// wGateSwap (R7-1), wGateSeed, wGateCmd, wGateRecovery: a declaring build
+// started by that path under 0.
+func gatePath(path string) func(*testing.T, *world) {
+ return func(t *testing.T, w *world) {
+ b := w.publicEngine(t)
+ if path == "recovery" {
+ b.Good[eng] = vEngine
+ w.stopGroup(b, eng)
+ w.wake(b, eng, "recovery", nil)
+ } else {
+ w.launch(b, eng, vEngine, path)
+ }
+ w.check()
+ }
+}
+
+func wGateSwap(t *testing.T, w *world) { gatePath("swap")(t, w) }
+func wGateSeed(t *testing.T, w *world) { gatePath("seed")(t, w) }
+func wGateCmd(t *testing.T, w *world) { gatePath("cmd")(t, w) }
+func wGateRecovery(t *testing.T, w *world) { gatePath("recovery")(t, w) }
+
+// wGateFallback (R9-1): the group ran a declaring build, was adopted to a
+// plain one (the mark stays 1) and cleared with --public; a public request
+// wakes it, the first wake fails and the plan falls back to the declaring
+// GoodVersion.
+func wGateFallback(t *testing.T, w *world) {
+ 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()
+ w.adopt(b, eng, vPlain, nil)
+ w.check()
+ b.Good[eng] = vEngine // the plain build has not proved itself yet
+ w.stubPublic(b, eng)
+ r := w.admitPublic(b, engHost, "/")
+ if r == nil {
+ t.Fatalf("witness: a public request after --public was refused: %s", w.boxesState())
+ }
+ r.Held = true
+ w.wake(b, eng, "fallback", r)
+ w.check()
+}
+
+// wUnreadableDeclares: a build that declares but whose manifest cannot be
+// read, seeded under 0.
+func wUnreadableDeclares(t *testing.T, w *world) {
+ b := w.publicEngine(t)
+ w.launch(b, eng, vUnreadable, "seed")
+ w.check()
+}
+
+// wLiveLinkOnly (R11): something other than adoption moves the live link to
+// a declaring build, then systemd restarts the unit from the live link.
+func wLiveLinkOnly(t *testing.T, w *world) {
+ b := w.publicEngine(t)
+ w.moveLive(b, eng, vEngine, "a rollout tool")
+ w.check()
+ w.systemdRestart(b, eng)
+ 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) {
+ 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)
+ }
+ w.check()
+ }
+}
diff --git a/internal/sim/engines/world_test.go b/internal/sim/engines/world_test.go
index 70b035ee3..ee29dbd9f 100644
--- a/internal/sim/engines/world_test.go
+++ b/internal/sim/engines/world_test.go
@@ -18,6 +18,18 @@ const (
nBuilds = 4
)
+// The starting world's names.
+const (
+ eng = "eng" // the engine group (its owner's host; engine names have no dot)
+ engHost = "eng.acct.apps.example"
+ engAlias = "docs.example" // alias row on box 0, to engHost
+ engSite = "www.example" // static row on box 0, path map to engHost
+ engSitePath = "/convert"
+ shopAlias = "shop-alias.example" // alias row on box 1, to shop
+ shopSite = "shop-www.example" // static row on box 1, path map to shop
+ shopSitePath = "/app"
+)
+
// build is a platform build: whether it declares the internal-engine
// protocol, and whether the manifest it writes is in place.
type build struct {
@@ -35,12 +47,15 @@ type proc struct {
Unisolated, OwnPort bool
}
-// row is a host row of a box's table. Kind is instance, service or static;
-// Backend is a socket path or an address, "" for static.
+// row is a host row of a box's table. Kind is instance, service, static or
+// alias; Backend is a socket path or an address, "" for static and alias.
+// An alias row names its target host in Alias and copies its upstream
+// (edge.go:929); PathTo maps a path to the host that serves it (edge.go:1364).
type row struct {
Host, Kind, Owner, Backend string
Platform, Grant bool
PathTo map[string]string
+ Alias string
}
// mark is a row's exposure mark.
@@ -65,17 +80,25 @@ func (m mark) String() string {
// caller names who a request is on behalf of.
type caller struct{ Account, App, Engine string }
-// req is a request the box admitted or refused.
+// req is a request the box admitted. Row is the row whose mark admitted it;
+// Backend the proxy it holds from then on; Reached the process it was
+// delivered to (0 for none).
type req struct {
ID, Epoch int
Row, Backend string
Public bool
Caller *caller
Held bool
+ Box, Reached int
}
// box is one host of the fleet: box 0 is the engine's home, box 1 a calling
// box.
+//
+// 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").
type box struct {
ID int
Rows map[string]*row
@@ -86,6 +109,10 @@ type box struct {
Staged map[string][]int
Procs []*proc
Admitted []*req
+
+ EdgeRows map[string]row
+ Serving map[string]mark
+ SetAt map[string]int
}
type world struct {
@@ -98,6 +125,7 @@ type world struct {
violations []string
residuals []string
stats map[string]int
+ nextID int // process and request ids
verbose bool
}
@@ -121,18 +149,33 @@ func newWorld(seed int64, verbose bool) *world {
verbose: verbose,
}
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{}}
+ 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{}}
}
home, calling := newBox(0), newBox(1)
w.boxes = []*box{home, calling}
// one engine group, eng, with its minted platform row
- const engHost = "eng.acct.apps.example"
- home.Rows[engHost] = &row{Host: engHost, Kind: "instance", Owner: "eng", Backend: "/run/carlos/eng.sock", Platform: true, PathTo: map[string]string{}}
+ home.Rows[engHost] = &row{Host: engHost, Kind: "instance", Owner: eng, Backend: "/run/carlos/eng.sock", Platform: true, PathTo: map[string]string{}}
home.Mark[engHost] = markInternal
// one public app group, shop, on the calling box
calling.Rows["shop"] = &row{Host: "shop", Kind: "instance", Backend: "127.0.0.1:9001", PathTo: map[string]string{}}
calling.Mark["shop"] = markPublic
+ // on each box an alias row and a static row with a path map, both
+ // resolving to the box's group: rows of kinds that serve no release, 0
+ // by construction (spec §5.1, "What the edge does with it")
+ for _, x := range []struct {
+ b *box
+ alias, site, path, to string
+ }{{home, engAlias, engSite, engSitePath, engHost}, {calling, shopAlias, shopSite, shopSitePath, "shop"}} {
+ x.b.Rows[x.alias] = &row{Host: x.alias, Kind: "alias", Alias: x.to, PathTo: map[string]string{}}
+ x.b.Rows[x.site] = &row{Host: x.site, Kind: "static", PathTo: map[string]string{x.path: x.to}}
+ x.b.Mark[x.alias], x.b.Mark[x.site] = markPublic, markPublic
+ }
+ // the edges start with the registry loaded
+ for _, b := range w.boxes {
+ b.loadEdge()
+ }
for v := 1; v <= nBuilds; v++ {
w.builds[v] = build{Ver: v, Declares: w.rng.Intn(2) == 0, ManifestOK: w.rng.Intn(2) == 0}
@@ -208,6 +251,7 @@ func (w *world) doStep() {
w.stats[a.name]++
w.logf("action %s", a.name) // always traced: the determinism test compares the action sequence
a.run(w)
+ w.check()
}
// final is the end-of-run oracle: what must hold once the calm steps are