amadan

carlos / platform Public

enginesim: classification, minted groups, the operator clear (#335 plan 1)

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
claude 34c24ae872ae28ff063ea1a0beb357977f1dff2e parent 797bda0
7 files changed, +1002 −51
  • internal/sim/engines/classify_test.go +491 −0
  • internal/sim/engines/edge_test.go +79 −17
  • internal/sim/engines/invariants_test.go +72 −0
  • internal/sim/engines/launch_test.go +49 −13
  • internal/sim/engines/rules_test.go +13 −0
  • internal/sim/engines/witness_test.go +260 −13
  • internal/sim/engines/world_test.go +38 −8
diff --git a/internal/sim/engines/classify_test.go b/internal/sim/engines/classify_test.go
new file mode 100644
index 000000000..7ba31d27a
--- /dev/null
+++ b/internal/sim/engines/classify_test.go
@@ -0,0 +1,491 @@
+package engines
+
+import (
+ "fmt"
+ "sort"
+ "strings"
+)
+
+// Classification, minted groups and the operator clear (spec §5.1 "The
+// column", "Platform-minted rows", "Becoming public is never automatic",
+// "Classification before serving"; §6.3).
+
+// ---------- minted groups ----------
+
+// followsOwner: the row is a platform-minted row that takes its execution
+// owner's mark and barrier. Only minted instance rows do: a minted static or
+// service row is 0 by construction (static-minted-public).
+func followsOwner(r *row) bool {
+ if !r.Platform || !on("minted-follow-owner") {
+ return false
+ }
+ return r.Kind == "instance" || (r.Kind == "static" && !on("static-minted-public"))
+}
+
+// resolveOwner is the edge's (and the agent's) owner for a minted row, under
+// the rules in force.
+func (b *box) resolveOwner(r *row) (string, bool) {
+ return b.resolveOwnerWith(r, on("owner-nonempty-unique"))
+}
+
+// resolveOwnerWith: the recorded owner, if its row exists; else the
+// non-platform instance row with the same account and app and the same
+// backend. strict is the spec's fallback: empty values never match, and a
+// match that is not unique counts as no match. Without it, empty values
+// match and the first match wins.
+func (b *box) resolveOwnerWith(r *row, strict bool) (string, bool) {
+ if r.Owner != "" {
+ if o := b.Rows[r.Owner]; o != nil && !o.Platform {
+ return r.Owner, true
+ }
+ return "", false
+ }
+ var found []string
+ for _, h := range hostsOf(b) {
+ c := b.Rows[h]
+ if c.Platform || c.Kind != "instance" || c.App != r.App {
+ continue
+ }
+ cs, ca, rs, ra := socketOf(c), addrOf(c), socketOf(r), addrOf(r)
+ if strict && ((cs != "" && cs == rs) || (ca != "" && ca == ra)) ||
+ !strict && (cs == rs || ca == ra) {
+ found = append(found, h)
+ }
+ }
+ if len(found) == 1 || (!strict && len(found) > 0) {
+ return found[0], true
+ }
+ return "", false
+}
+
+// socketOf and addrOf split a backend into the registry's Socket and Addr.
+func socketOf(r *row) string {
+ if strings.HasPrefix(r.Backend, "/") {
+ return r.Backend
+ }
+ return ""
+}
+
+func addrOf(r *row) string {
+ if r.Backend != "" && !strings.HasPrefix(r.Backend, "/") {
+ return r.Backend
+ }
+ return ""
+}
+
+func hostsOf(b *box) []string {
+ hosts := make([]string, 0, len(b.Rows))
+ for h := range b.Rows {
+ hosts = append(hosts, h)
+ }
+ sort.Strings(hosts)
+ return hosts
+}
+
+// truthGroup is the group a row really serves: a minted row's source, else
+// its own host. The oracle reads it; the protocol never does.
+func truthGroup(b *box, host string) string {
+ if r := b.Rows[host]; r != nil && r.Platform && r.Source != "" {
+ return r.Source
+ }
+ return host
+}
+
+// mint is the domains reconciler minting a platform row from src: it copies
+// the source's kind, backend and app (no version), and, being a row of the
+// same group, the group's mark. recordOwner is whether it writes
+// routes.owner (rows minted before the column was added have none until the
+// reconciler's next pass).
+func (w *world) mint(b *box, src, host string, recordOwner bool) {
+ s := b.Rows[src]
+ m := w.groupMark(b, w.group(b, src))
+ r := &row{Host: host, Kind: s.Kind, App: s.App, Backend: s.Backend, Platform: true, Source: src, PathTo: map[string]string{}}
+ if recordOwner {
+ r.Owner = src
+ }
+ b.Rows[host] = r
+ b.Mark[host] = m
+ b.Wrote++
+ w.logf("box%d: registry change %d: minted %s %s from %s (owner %q, mark %v)", b.ID, b.Wrote, r.Kind, host, src, r.Owner, m)
+}
+
+// reconcileOwners is the reconciler's backfill pass: it records the owner of
+// every minted instance row that has none. The row takes its owner group's
+// mark (one group, one mark).
+func (w *world) reconcileOwners(b *box) {
+ for _, h := range hostsOf(b) {
+ r := b.Rows[h]
+ if !r.Platform || r.Kind != "instance" || r.Owner != "" || b.Rows[r.Source] == nil {
+ continue
+ }
+ m := w.groupMark(b, w.group(b, r.Source))
+ r.Owner = r.Source
+ b.Mark[h] = m
+ b.Wrote++
+ w.logf("box%d: registry change %d: owner of %s recorded as %s (mark %v)", b.ID, b.Wrote, h, r.Owner, m)
+ }
+}
+
+// provision creates instance route host (a new route: NULL, unclassified),
+// then its first adoption classifies it before it is served: a declaring
+// build through the gate, a readable plain one as 0 (spec §5.1, "A route the
+// agent creates later ... is classified by its first adoption").
+func (w *world) provision(b *box, host, app, backend string, ver int) bool {
+ b.Rows[host] = &row{Host: host, Kind: "instance", App: app, Backend: backend, PathTo: map[string]string{}}
+ b.Wrote++
+ w.logf("box%d: registry change %d: provisioned %s (%s, %s), NULL until its first adoption", b.ID, b.Wrote, host, app, backend)
+ ok := w.adopt(b, host, ver, nil)
+ if w.groupMark(b, host) == markNull {
+ if m := w.classify(b, host); m != markNull {
+ w.writeMark(b, host, m)
+ }
+ }
+ return ok
+}
+
+// addStaticApp creates static app name with its minted platform row and a
+// static canary on its own channel (domains/reconcile.go:368).
+func (w *world) addStaticApp(b *box, name string) (minted, canary string) {
+ b.Rows[name] = &row{Host: name, Kind: "static", App: "acct/" + name, PathTo: map[string]string{}}
+ b.Mark[name] = markPublic // 0 by construction
+ b.Wrote++
+ w.logf("box%d: registry change %d: static app %s", b.ID, b.Wrote, name)
+ minted, canary = name+".acct.apps.example", "canary-"+name+".acct.apps.example"
+ w.mint(b, name, minted, true)
+ w.mint(b, name, canary, true)
+ return minted, canary
+}
+
+// ---------- grants ----------
+
+// groupHasGrant: a row of group g holds the doc-engine grant. With
+// grant-marks-group, any row of the group; without it, only the owner's own
+// row (a grant on a minted row is ignored, R6-1).
+func (w *world) groupHasGrant(b *box, g string) bool {
+ if !on("grant-marks-group") {
+ r := b.Rows[g]
+ return r != nil && r.Grant
+ }
+ for _, h := range w.groupHosts(b, g) {
+ if b.Rows[h].Grant {
+ return true
+ }
+ }
+ return false
+}
+
+// grantLoaded is the oracle's grant: a row whose true group is g holds the
+// grant and the edge has loaded the change that recorded it. It returns that
+// row, or "".
+func (w *world) grantLoaded(b *box, g string) string {
+ for _, h := range hostsOf(b) {
+ r := b.Rows[h]
+ if r.Grant && truthGroup(b, h) == g && b.Fenced >= r.GrantAt {
+ return h
+ }
+ }
+ return ""
+}
+
+// grant is `carlos route --host <host> --grant doc-engine`: it records the
+// grant, writes 1 on the group if the group now holds it, and returns once
+// the edge has loaded the change (or says it timed out).
+func (w *world) grant(b *box, host string) bool {
+ r := b.Rows[host]
+ if r == nil || r.Kind != "instance" || r.Grant {
+ return false
+ }
+ b.Wrote++
+ r.Grant, r.GrantAt = true, b.Wrote
+ g := w.group(b, host)
+ w.logf("box%d: registry change %d: --grant doc-engine on %s (group %s)", b.ID, b.Wrote, host, g)
+ if w.groupHasGrant(b, g) && w.groupMark(b, g) != markInternal {
+ w.writeMark(b, g, markInternal)
+ }
+ want := b.Wrote
+ for i := 0; i < fenceWaitTicks && b.Fenced < want; i++ {
+ w.reload(b)
+ }
+ if b.Fenced < want {
+ w.logf("box%d: --grant on %s: the edge has not loaded it; timed out", b.ID, host)
+ return false
+ }
+ return true
+}
+
+// revoke is --revoke doc-engine: the grant goes; the mark stays (becoming
+// public is never automatic).
+func (w *world) revoke(b *box, host string) {
+ r := b.Rows[host]
+ if r == nil || !r.Grant {
+ return
+ }
+ b.Wrote++
+ r.Grant = false
+ w.logf("box%d: registry change %d: --revoke doc-engine on %s; the mark stays", b.ID, b.Wrote, host)
+}
+
+// ---------- classification before serving ----------
+
+// classify is the upgrade's classification of group g: 1 if a row of the
+// group holds the grant, the live manifest declares, or the manifest of any
+// staged version declares (classify-staged); 0 if the live manifest is
+// readable and none of those holds; else NULL.
+func (w *world) classify(b *box, g string) mark {
+ if w.groupHasGrant(b, g) {
+ return markInternal
+ }
+ live, liveOK := w.builds[b.Live[g]]
+ liveOK = liveOK && b.Live[g] != 0 && live.ManifestOK
+ if liveOK && live.Declares {
+ return markInternal
+ }
+ if on("classify-staged") {
+ for _, v := range b.Staged[g] {
+ if bd := w.builds[v]; bd.ManifestOK && bd.Declares {
+ return markInternal
+ }
+ }
+ }
+ if liveOK {
+ return markPublic
+ }
+ return markNull
+}
+
+// classifiedGroups is every group with a row the classification covers: an
+// instance row, or a row that follows an owner.
+func (w *world) classifiedGroups(b *box) []string {
+ seen := map[string]bool{}
+ var out []string
+ for _, h := range hostsOf(b) {
+ r := b.Rows[h]
+ if r.Kind != "instance" && !followsOwner(r) {
+ continue
+ }
+ if g := w.group(b, h); !seen[g] {
+ seen[g] = true
+ out = append(out, g)
+ }
+ }
+ return out
+}
+
+// upgrade is the agent's first start on the build that adds routes.internal.
+// The column arrives NULL on every instance route; before any edge listener
+// opens, the agent classifies every NULL group. The edge then starts on the
+// classified map: in-flight requests did not survive the restart, and the
+// fence covers everything written. Running processes are untouched.
+func (w *world) upgrade(b *box) {
+ gs := w.classifiedGroups(b)
+ w.logf("box%d: upgrade: routes.internal arrives NULL on %v", b.ID, gs)
+ for _, g := range gs {
+ w.writeMark(b, g, markNull)
+ }
+ for _, g := range gs {
+ if m := w.classify(b, g); m != markNull {
+ w.writeMark(b, g, m)
+ } else {
+ w.logf("box%d: upgrade: %s stays NULL (live manifest unreadable): refused publicly, named every pass", b.ID, g)
+ }
+ }
+ b.loadEdge()
+ b.Epoch++
+ if len(b.Admitted) > 0 {
+ w.logf("box%d: upgrade: %d in-flight requests ended with the restart", b.ID, len(b.Admitted))
+ }
+ b.Admitted = nil
+ b.Fenced = b.Wrote
+ w.logf("box%d: upgrade: listeners open on the classified map, epoch %d, fenced %d", b.ID, b.Epoch, b.Fenced)
+}
+
+// residualAtUpgrade names the spec's stated residual if an upgrade of b now
+// would produce it: a running declaring build whose manifest cannot be read,
+// in a group the (correct) classification would mark 0 because the live
+// manifest reads and does not declare. The default world does not generate
+// it; Task 5's flag does.
+func (w *world) residualAtUpgrade(b *box) string {
+ for _, g := range w.groups(b) {
+ var unreadable *proc
+ for _, p := range b.Procs {
+ if bd := w.builds[p.Ver]; p.Group == g && bd.Declares && !bd.ManifestOK {
+ unreadable = p
+ }
+ }
+ if unreadable == nil {
+ continue
+ }
+ granted := false
+ for _, h := range hostsOf(b) {
+ granted = granted || (b.Rows[h].Grant && truthGroup(b, h) == g)
+ }
+ live, ok := w.builds[b.Live[g]]
+ if granted || b.Live[g] == 0 || !ok || !live.ManifestOK || live.Declares {
+ continue
+ }
+ staged := false
+ for _, v := range b.Staged[g] {
+ if bd := w.builds[v]; bd.ManifestOK && bd.Declares {
+ staged = true
+ }
+ }
+ if !staged {
+ return fmt.Sprintf("%s runs v%d (declares, manifest unreadable) while live v%d reads as plain", g, unreadable.Ver, b.Live[g])
+ }
+ }
+ return ""
+}
+
+// ---------- 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:
+// 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, and
+// 3. refuse unless every cgroup of the group is empty (public-stops-group);
+// 4. write 0 and release the lock.
+//
+// w.clearHook, if set, runs after step 1 ("locked") and after step 2
+// ("stopped").
+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 }()
+ }
+ if on("public-checks-live") {
+ live, ok := w.builds[b.Live[g]]
+ if b.Live[g] == 0 || !ok || !live.ManifestOK || live.Declares {
+ w.logf("box%d: --public %s: refused: the live release v%d is unreadable or declares doc_engine", b.ID, g, b.Live[g])
+ return false
+ }
+ }
+ if w.groupHasGrant(b, g) {
+ w.logf("box%d: --public %s: refused: a row of the group holds the doc-engine grant", b.ID, g)
+ return false
+ }
+ w.hook(b, g, "locked")
+ if on("public-stops-group") {
+ w.stopGroup(b, g)
+ w.logf("box%d: --public %s: the group is stopped", b.ID, g)
+ w.hook(b, g, "stopped")
+ if w.running(b, g) {
+ w.logf("box%d: --public %s: refused: a cgroup of the group is not empty", b.ID, g)
+ return false
+ }
+ } else {
+ w.hook(b, g, "stopped")
+ }
+ w.writeMark(b, g, markPublic)
+ w.logf("box%d: --public %s: 0 written; the lock is released", b.ID, g)
+ return true
+}
+
+func (w *world) hook(b *box, g, stage string) {
+ if w.clearHook != nil {
+ w.clearHook(b, g, stage)
+ }
+}
+
+// ---------- the random walk ----------
+
+// pickInstanceRow is any instance row of b, minted included, or "".
+func (w *world) pickInstanceRow(b *box) string {
+ var hs []string
+ for _, h := range hostsOf(b) {
+ if b.Rows[h].Kind == "instance" {
+ hs = append(hs, h)
+ }
+ }
+ if len(hs) == 0 {
+ return ""
+ }
+ return hs[w.rng.Intn(len(hs))]
+}
+
+// maxRows bounds a box's table in the walk.
+const maxRows = 24
+
+func init() {
+ actions = append(actions,
+ action{name: "upgrade", weight: 1, run: func(w *world) {
+ b := w.pickBox()
+ if why := w.residualAtUpgrade(b); why != "" {
+ w.logf("box%d: upgrade not generated: the stated residual (%s)", b.ID, why)
+ return
+ }
+ w.upgrade(b)
+ }},
+ action{name: "grant", weight: 1, run: func(w *world) {
+ b := w.pickBox()
+ if h := w.pickInstanceRow(b); h != "" {
+ w.grant(b, h)
+ }
+ }},
+ action{name: "revoke", weight: 1, run: func(w *world) {
+ b := w.pickBox()
+ if h := w.pickInstanceRow(b); h != "" {
+ w.revoke(b, h)
+ }
+ }},
+ action{name: "operator-public", weight: 2, run: func(w *world) {
+ b := w.pickBox()
+ g := w.pickGroup(b)
+ if g == "" {
+ return
+ }
+ switch w.rng.Intn(4) {
+ case 1: // an adoption tries to run during the clear
+ w.clearHook = func(hb *box, hg, stage string) {
+ if stage == "locked" {
+ w.adopt(hb, hg, w.pickVer(), nil)
+ }
+ }
+ case 2: // an awake repoint tries to run during the clear
+ w.clearHook = func(hb *box, hg, stage string) {
+ if stage == "locked" {
+ w.repointAwake(hb, hg, w.pickVer())
+ }
+ }
+ case 3: // a swap's incoming generation races the stop
+ w.clearHook = func(hb *box, hg, stage string) {
+ if stage == "stopped" {
+ w.launch(hb, hg, w.pickVer(), "swap")
+ }
+ }
+ }
+ w.operatorPublic(b, g)
+ w.clearHook = nil
+ }},
+ action{name: "adopt-awake", weight: 2, run: func(w *world) {
+ b := w.pickBox()
+ if g := w.pickGroup(b); g != "" {
+ w.repointAwake(b, g, w.pickVer())
+ }
+ }},
+ action{name: "add-tcp-instance", weight: 1, run: func(w *world) {
+ b := w.pickBox()
+ if len(b.Rows) >= maxRows {
+ return
+ }
+ w.nextID++
+ host := fmt.Sprintf("t%d", w.nextID)
+ app := []string{"acct/shop", "acct/tcp"}[w.rng.Intn(2)]
+ addr := fmt.Sprintf("10.0.%d.1:%d", b.ID, 9100+w.nextID) // unique: no ambiguous owner in the walk
+ w.provision(b, host, app, addr, w.pickVer())
+ w.mint(b, host, host+".acct.apps.example", w.rng.Intn(2) == 0)
+ }},
+ action{name: "add-static-app", weight: 1, run: func(w *world) {
+ b := w.pickBox()
+ if len(b.Rows) >= maxRows {
+ return
+ }
+ w.nextID++
+ w.addStaticApp(b, fmt.Sprintf("s%d", w.nextID))
+ }},
+ action{name: "reconcile-owners", weight: 1, run: func(w *world) {
+ w.reconcileOwners(w.pickBox())
+ }},
+ )
+}
diff --git a/internal/sim/engines/edge_test.go b/internal/sim/engines/edge_test.go
index b6404892d..0a79413a5 100644
--- a/internal/sim/engines/edge_test.go
+++ b/internal/sim/engines/edge_test.go
@@ -11,6 +11,12 @@ import "sort"
// 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.
+//
+// The edge resolves owners at load (spec §5.1, "Platform-minted rows"): a
+// row that follows an owner carries the resolved owner in its copy's Owner;
+// one whose owner cannot be found, or is found ambiguously, is served NULL
+// (refused) until the reconciler records its owner. Any other row's copy has
+// no Owner, so edgeGroup is its own host.
func (b *box) loadEdge() {
b.EdgeRows = make(map[string]row, len(b.Rows))
b.Serving = make(map[string]mark, len(b.Rows))
@@ -20,8 +26,16 @@ func (b *box) loadEdge() {
for p, to := range r.PathTo {
c.PathTo[p] = to
}
- b.EdgeRows[h] = c
b.Serving[h] = b.Mark[h]
+ c.Owner = ""
+ if followsOwner(r) {
+ if o, ok := b.resolveOwner(r); ok {
+ c.Owner = o
+ } else {
+ b.Serving[h] = markNull
+ }
+ }
+ b.EdgeRows[h] = c
}
}
@@ -57,15 +71,16 @@ 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 sets the group to 1 is the one a
-// fence must reach (SetAt).
+// 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.
func (w *world) writeMark(b *box, g string, m mark) {
- before := w.groupMark(b, g)
+ wasClosed := w.closed(b, g)
b.Wrote++
for _, h := range w.groupHosts(b, g) {
b.Mark[h] = m
}
- if m == markInternal && before != markInternal {
+ if !wasClosed && m != markPublic {
b.SetAt[g] = b.Wrote
}
w.logf("box%d: registry change %d: %s marked %v", b.ID, b.Wrote, g, m)
@@ -73,8 +88,28 @@ 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").
+//
+// 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.
func (w *world) fenced(b *box, g string) bool {
- return w.groupMark(b, g) == markInternal && b.Fenced >= b.SetAt[g]
+ return w.closed(b, g) && b.Fenced >= b.SetAt[g]
+}
+
+// closed: group g has a row and none of its registry rows is 0.
+func (w *world) closed(b *box, g string) bool {
+ hosts := w.groupHosts(b, g)
+ if len(hosts) == 0 {
+ return false
+ }
+ for _, h := range hosts {
+ if b.Mark[h] == markPublic {
+ return false
+ }
+ }
+ return true
}
// reload is the edge's registry poll. A failed reload swaps nothing and
@@ -96,7 +131,7 @@ func (w *world) reload(b *box) bool {
b.loadEdge()
changed := map[string]bool{}
for h, m := range b.Serving {
- if m == markInternal && old[h] != markInternal {
+ if (m == markInternal && old[h] != markInternal) || (m == markNull && old[h] == markPublic) {
changed[h] = true
}
}
@@ -129,45 +164,67 @@ func (w *world) reload(b *box) bool {
// 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 {
+ r, _ := w.admit(b, host, path)
+ return r
+}
+
+// The outcomes of admit.
+const (
+ admitted = "admitted" // proxied: the request holds a backend
+ answered = "answered" // a static row: the edge answers it itself
+ refused = "refused" // the internal refusal
+ unknown = "unknown" // no such host, alias target or path target
+)
+
+// admit is admitPublic with its outcome, for INV-AV. The edge treats NULL
+// like 1 (classify-null-refused).
+func (w *world) admit(b *box, host, path string) (*req, string) {
asked, ok := b.EdgeRows[host]
if !ok {
w.logf("box%d: public %s%s: unknown host", b.ID, host, path)
- return nil
+ return nil, unknown
}
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
+ return nil, unknown
}
}
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
+ return nil, unknown
}
}
checked := final
if !on("mark-on-final-upstream") {
checked = asked
}
- if m := b.Serving[checked.Host]; m != markPublic {
+ m := b.Serving[checked.Host]
+ if m == markNull && !on("classify-null-refused") {
+ w.logf("box%d: public %s%s: %s is NULL, served like 0", b.ID, host, path, checked.Host)
+ m = markPublic
+ }
+ if m != markPublic {
w.logf("box%d: public %s%s: internal refusal (%s is %v)", b.ID, host, path, checked.Host, m)
- return nil
+ return nil, refused
}
if final.Backend == "" {
w.logf("box%d: public %s%s: answered by the edge (%s)", b.ID, host, path, final.Host)
- return nil
+ return nil, answered
}
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
+ return r, admitted
}
// 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.
+// the instance row that carries it, whatever row the request came in by. A
+// minted row copies its source's backend; the process is the source's, so
+// the source's own row decides (the truth, whatever the edge resolved).
func (w *world) backendGroup(b *box, backend string) string {
hosts := make([]string, 0, len(b.Rows))
for h := range b.Rows {
@@ -175,7 +232,7 @@ func (w *world) backendGroup(b *box, backend string) string {
}
sort.Strings(hosts)
for _, h := range hosts {
- if r := b.Rows[h]; r.Kind == "instance" && r.Backend == backend {
+ if r := b.Rows[h]; r.Kind == "instance" && !r.Platform && r.Backend == backend {
return w.group(b, h)
}
}
@@ -185,7 +242,10 @@ func (w *world) backendGroup(b *box, backend string) string {
// 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.
+// doc_engine, nor one of a group that holds the doc-engine grant once the
+// edge has loaded the grant (the grant sets 1 whatever the manifest says,
+// spec §5.1 "The column"; a grant whose barrier timed out protects nothing
+// until the edge loads it, and the load drains every request admitted before).
func (w *world) deliver(r *req) {
b := w.boxes[r.Box]
idx := -1
@@ -215,6 +275,8 @@ func (w *world) deliver(r *req) {
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)
+ } else if r.Public && w.grantLoaded(b, g) != "" {
+ w.fail("INV-P", "box%d: public request %d (row %s) delivered to process %d of %s running v%d, whose group holds the doc-engine grant (on %s)", b.ID, r.ID, r.Row, p.ID, p.Group, p.Ver, w.grantLoaded(b, g))
}
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 4be0034c0..40d2357d8 100644
--- a/internal/sim/engines/invariants_test.go
+++ b/internal/sim/engines/invariants_test.go
@@ -90,3 +90,75 @@ func edgeGroup(b *box, host string) string {
}
return host
}
+
+// INV-AV (liveness, Task 3): at the end of the calm phase, every row of a
+// group whose mark is 0 answers a public request. It is what catches the
+// rules that only protect availability (static-minted-public,
+// owner-nonempty-unique), which no safety invariant can see. Checked in
+// final() only, after every edge has polled with its faults cleared.
+//
+// The truth, not the model's resolution, decides which rows must answer:
+// - a static or service row is 0 by construction (spec §5.1, "The column"),
+// minted or not;
+// - an instance row answers when its group's mark is 0: the registry mark
+// of its own row, or for a minted row, of the row it was minted from
+// (Source);
+// - alias rows are skipped: they answer as their target does.
+//
+// Not counted, as the spec's fail-closed choices or another rule's stated
+// refusal: a minted row whose owner the correct fallback cannot find
+// uniquely (refused and logged until the reconciler records its owner), and
+// any row an avExemption names.
+func (w *world) checkAV() {
+ for _, b := range w.boxes {
+ hosts := make([]string, 0, len(b.Rows))
+ for h := range b.Rows {
+ hosts = append(hosts, h)
+ }
+ sort.Strings(hosts)
+ for _, h := range hosts {
+ r := b.Rows[h]
+ switch r.Kind {
+ case "alias":
+ continue
+ case "instance":
+ owner := h
+ if r.Platform {
+ if _, ok := b.resolveOwnerWith(r, true); !ok {
+ w.logf("box%d: final: minted row %s has no unique owner; refused by design, not counted", b.ID, h)
+ continue
+ }
+ owner = r.Source
+ }
+ if b.Mark[owner] != markPublic {
+ continue
+ }
+ }
+ if why := w.avExempt(b, h); why != "" {
+ w.logf("box%d: final: %s exempt from INV-AV: %s", b.ID, h, why)
+ continue
+ }
+ req, outcome := w.admit(b, h, "/")
+ switch outcome {
+ case admitted:
+ w.deliver(req)
+ case answered:
+ default:
+ w.fail("INV-AV", "box%d: row %s (%s) of a public group is %s a public request at the end of the calm phase (registry %v, edge %v)", b.ID, h, r.Kind, outcome, b.Mark[h], b.Serving[h])
+ }
+ }
+ }
+}
+
+// avExemptions are later tasks' stated refusals of a public row (each
+// returns why, or ""), which INV-AV must not count.
+var avExemptions []func(w *world, b *box, host string) string
+
+func (w *world) avExempt(b *box, host string) string {
+ for _, f := range avExemptions {
+ if why := f(w, b, host); why != "" {
+ return why
+ }
+ }
+ return ""
+}
diff --git a/internal/sim/engines/launch_test.go b/internal/sim/engines/launch_test.go
index b5bf36f27..02b2c2f8b 100644
--- a/internal/sim/engines/launch_test.go
+++ b/internal/sim/engines/launch_test.go
@@ -94,6 +94,7 @@ func (w *world) launch(b *box, g string, ver int, path string) bool {
}
}
}
+ w.stage(b, g, ver) // a build runs from /opt/carlos/versions: it is staged
w.nextID++
p := &proc{ID: w.nextID, Group: g, Ver: ver, Slice: "inst:" + g}
b.Procs = append(b.Procs, p)
@@ -128,27 +129,57 @@ func (w *world) running(b *box, g string) bool {
// 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 !w.repoint(b, g, ver) {
+ return false
+ }
+ if between != nil {
+ between()
+ }
+ w.stopGroup(b, g)
+ return w.launch(b, g, ver, "adopt")
+}
+
+// repointAwake is adoption that repoints the live link and does not restart:
+// an awake hibernating route (release/adopt.go:1174), or a generation
+// rollout that only schedules the swap. What ran keeps running.
+func (w *world) repointAwake(b *box, g string, ver int) bool {
+ w.logf("box%d: adopt %s v%d without a restart (live v%d)", b.ID, g, ver, b.Live[g])
+ if !w.repoint(b, g, ver) {
+ return false
+ }
+ w.logf("box%d: %s keeps its running processes until their next start", b.ID, g)
+ return true
+}
+
+// repoint is adoption up to the repoint: the adoption 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)
+ return false
+ }
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)
- }
+ w.stage(b, 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()
+ return true
+}
+
+// stage records that build ver of group g is staged on the box.
+func (w *world) stage(b *box, g string, ver int) {
+ for _, v := range b.Staged[g] {
+ if v == ver {
+ return
+ }
}
- w.stopGroup(b, g)
- return w.launch(b, g, ver, "adopt")
+ b.Staged[g] = append(b.Staged[g], ver)
}
// wake is the activator waking group g by its wake plan: "recovery" starts
@@ -206,12 +237,17 @@ func (w *world) socketActivate(b *box, g string) {
func (w *world) pickBox() *box { return w.boxes[w.rng.Intn(len(w.boxes))] }
-// groups is every instance group of b's registry, sorted.
+// groups is every instance group of b's registry, sorted: the groups of the
+// instance rows that are not platform-minted (adoption skips minted rows,
+// release/adopt.go:1210; their processes are their source's).
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] {
+ if r.Kind != "instance" || r.Platform {
+ continue
+ }
+ if g := w.group(b, h); !seen[g] {
seen[g] = true
out = append(out, g)
}
diff --git a/internal/sim/engines/rules_test.go b/internal/sim/engines/rules_test.go
index 295b927d9..a8a54911c 100644
--- a/internal/sim/engines/rules_test.go
+++ b/internal/sim/engines/rules_test.go
@@ -53,4 +53,17 @@ var allRules = []string{
"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)
+
+ // Task 3: classification, minted groups, the operator clear (spec §5.1
+ // "The column", "Platform-minted rows", "Becoming public is never
+ // automatic", "Classification before serving"; §6.3)
+ "classify-null-refused", // the edge refuses NULL like 1 (R2-2)
+ "classify-staged", // the upgrade classifies 1 if any staged version declares (R8-1)
+ "minted-follow-owner", // a minted instance row is in its owner's group: one mark, one barrier (R5-1)
+ "grant-marks-group", // a grant on any row of the group marks the group (R6-1)
+ "static-minted-public", // a minted static row is 0 by construction, never classified (R6-2)
+ "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 steps 2-3: stop the group, refuse unless its cgroups are empty (R7-1, R8-2)
+ "public-holds-lock", // --public holds the adoption lock: the live link cannot move under it
}
diff --git a/internal/sim/engines/witness_test.go b/internal/sim/engines/witness_test.go
index 31cae6dba..103b1e94d 100644
--- a/internal/sim/engines/witness_test.go
+++ b/internal/sim/engines/witness_test.go
@@ -61,6 +61,26 @@ var witnesses = []witness{
"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},
+
+ // Task 3: classification, minted groups, the operator clear
+ {"classify-null-refused", "classify-null-refused", "INV-P",
+ "R2-2: the engine runs a declaring build whose live manifest cannot be read; the upgrade leaves it NULL; an edge that serves NULL like 0 admits a public request into the engine", wClassifyNullRefused},
+ {"classify-staged", "classify-staged", "INV-I1+INV-P",
+ "R8-1: an awake engine is repointed to a plain build without a restart, so the declaring build still runs; an upgrade that reads only the live manifest classifies the group 0, under the running engine (INV-I1) and a public request reaches it (INV-P)", wClassifyStaged},
+ {"minted-follow-owner", "minted-follow-owner", "INV-P",
+ "R5-1: an app minted a platform row while public; adoption of a declaring build marks and fences the app; a minted row that is its own group stays 0 and a public request by the minted host reaches the engine", wMintedFollowOwner},
+ {"grant-marks-group", "grant-marks-group", "INV-P",
+ "R6-1: --grant doc-engine on the minted row of a plain release; a grant that marks only when it is on the owner's own row leaves the group 0, and a public request by the minted host reaches the granted app", wGrantMarksGroup},
+ {"static-minted-public", "static-minted-public", "INV-AV",
+ "R6-2: a static app with a minted row and a canary; an upgrade that classifies minted static rows like instance rows leaves them NULL, and they never answer (liveness)", wStaticMintedPublic},
+ {"owner-nonempty-unique", "owner-nonempty-unique", "INV-AV",
+ "R7-2: two TCP instances of one app, the plain one's minted row minted before owners were recorded; a fallback that matches empty sockets puts the row in the engine's group, which marks it 1, so a public row never answers; with the rule, a match that is not unique is refused and logged, and INV-AV does not count it", wOwnerNonEmptyUnique},
+ {"public-checks-live", "public-checks-live", "INV-I1+INV-P",
+ "--public on a group whose live release declares; without step 1 the clear writes 0, and systemd's socket activation starts the declaring live build ungated (INV-I1) for a public request (INV-P)", wPublicChecksLive},
+ {"public-stops-group", "public-stops-group", "INV-I1+INV-P",
+ "R7-1/R8-2: a generation rollout repointed the live link to a plain build and only scheduled the swap, so the declaring generation still serves; a clear that neither stops the group nor checks its cgroups writes 0 under it", wPublicStopsGroup},
+ {"public-holds-lock", "public-holds-lock", "INV-I1+INV-P",
+ "--public checks a plain live release; without the adoption lock, adoption repoints to a declaring build before the stop; the clear writes 0 over a declaring live link, and socket activation starts it ungated", wPublicHoldsLock},
}
// TestWitnesses is the deterministic half of the mutation evidence.
@@ -306,14 +326,13 @@ func newWitness() *world {
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)
+// clearPublic is the operator's --public on group g (operatorPublic), then
+// the edge's next poll, as one witness step. False when the clear refused.
+func (w *world) clearPublic(b *box, g string) bool {
+ ok := w.operatorPublic(b, g)
w.reload(b)
w.check()
+ return ok
}
// publicEngine sets the engine group on box 0 to a public route serving the
@@ -322,7 +341,9 @@ func (w *world) stubPublic(b *box, g string) {
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.clearPublic(b, eng) {
+ t.Fatalf("witness: --public refused on a plain live release: %s", w.boxesState())
+ }
if !w.launch(b, eng, vPlain, "seed") {
t.Fatalf("witness: the plain build did not start under 0: %s", w.boxesState())
}
@@ -447,6 +468,12 @@ 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) }
+// oraclePublic makes box 0's engine group public on a plain live release.
+func oraclePublic(w *world, b *box) {
+ b.Live[eng] = vPlain
+ w.clearPublic(b, eng)
+}
+
// 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
@@ -461,7 +488,9 @@ func wGateFallback(t *testing.T, w *world) {
w.adopt(b, eng, vPlain, nil)
w.check()
b.Good[eng] = vEngine // the plain build has not proved itself yet
- w.stubPublic(b, eng)
+ if !w.clearPublic(b, eng) {
+ t.Fatalf("witness: --public refused on a plain live release: %s", w.boxesState())
+ }
r := w.admitPublic(b, engHost, "/")
if r == nil {
t.Fatalf("witness: a public request after --public was refused: %s", w.boxesState())
@@ -509,10 +538,218 @@ func wMarkOnFinalUpstreamPath(t *testing.T, w *world) {
markOnFinalUpstream(t, w, engSite, engSitePath)
}
+// ---------- Task 3: classification, minted groups, the operator clear ----------
+
+// requestBy sends one public request by host and delivers it if admitted.
+func (w *world) requestBy(b *box, host string) {
+ if r := w.admitPublic(b, host, "/"); r != nil {
+ w.deliver(r)
+ }
+}
+
+// wClassifyNullRefused (R2-2): the engine's live release declares but its
+// manifest cannot be read; the upgrade can classify it neither way, so it
+// stays NULL; a public request arrives.
+func wClassifyNullRefused(t *testing.T, w *world) {
+ b := w.boxes[0]
+ if !w.adopt(b, eng, vUnreadable, nil) {
+ t.Fatalf("witness: adoption of the engine refused: %s", w.boxesState())
+ }
+ w.check()
+ w.upgrade(b)
+ w.check()
+ if m := w.groupMark(b, eng); m != markNull {
+ t.Fatalf("witness: the upgrade classified an unreadable live release %v, want NULL", m)
+ }
+ w.requestBy(b, engHost)
+ w.check()
+}
+
+// wClassifyStaged (R8-1): the engine runs a declaring build; adoption of a
+// plain build repoints the awake route without a restart, so the declaring
+// build keeps running; then the agent upgrades and a public request arrives.
+func wClassifyStaged(t *testing.T, w *world) {
+ b := w.boxes[0]
+ if !w.adopt(b, eng, vEngine, nil) {
+ t.Fatalf("witness: adoption of the engine refused: %s", w.boxesState())
+ }
+ w.check()
+ if !w.repointAwake(b, eng, vPlain) {
+ t.Fatalf("witness: the awake repoint was refused: %s", w.boxesState())
+ }
+ w.check()
+ w.upgrade(b)
+ w.check()
+ w.requestBy(b, engHost)
+ w.check()
+}
+
+const (
+ tcpApp = "acct/tcp"
+ tcpA = "tcp-a"
+ tcpB = "tcp-b"
+ tcpC = "tcp-c"
+ tcpD = "tcp-d"
+ mintedB = "tcp-b.acct.apps.example"
+ mintedC = "tcp-c.acct.apps.example"
+)
+
+// tcpPublic provisions a TCP-backed instance tcp-b of a plain build and mints
+// its platform row with the owner recorded; both answer publicly.
+func (w *world) tcpPublic(t *testing.T, b *box) {
+ if !w.provision(b, tcpB, tcpApp, "10.0.0.7:9102", vPlain) {
+ t.Fatalf("witness: provisioning %s refused: %s", tcpB, w.boxesState())
+ }
+ w.mint(b, tcpB, mintedB, true)
+ w.reload(b)
+ w.check()
+ if r := w.admitPublic(b, mintedB, "/"); r == nil {
+ t.Fatalf("witness: the minted row of a public app refused a public request: %s", w.boxesState())
+ } else {
+ w.deliver(r)
+ }
+ w.check()
+ if len(w.violations) > 0 {
+ t.Fatalf("witness: the fixture violates: %v", w.violations)
+ }
+}
+
+// wMintedFollowOwner (R5-1): a public app with a minted row adopts a
+// declaring build; a public request arrives by the minted host.
+func wMintedFollowOwner(t *testing.T, w *world) {
+ b := w.boxes[0]
+ w.tcpPublic(t, b)
+ if !w.adopt(b, tcpB, vEngine, nil) {
+ t.Fatalf("witness: adoption of the declaring build refused: %s", w.boxesState())
+ }
+ w.check()
+ w.requestBy(b, mintedB)
+ w.check()
+}
+
+// wGrantMarksGroup (R6-1): a public app of a plain build with a minted row;
+// the operator grants doc-engine on the minted row; a public request arrives
+// by the minted host.
+func wGrantMarksGroup(t *testing.T, w *world) {
+ b := w.boxes[0]
+ w.tcpPublic(t, b)
+ w.grant(b, mintedB)
+ w.check()
+ w.requestBy(b, mintedB)
+ w.check()
+}
+
+// wStaticMintedPublic (R6-2): a static app with its minted row and a canary
+// on its own channel; the agent upgrades; at the end every public row must
+// answer.
+func wStaticMintedPublic(t *testing.T, w *world) {
+ b := w.boxes[0]
+ w.addStaticApp(b, "site")
+ w.reload(b)
+ w.check()
+ w.upgrade(b)
+ w.check()
+ w.final()
+}
+
+// wOwnerNonEmptyUnique (R7-2): app acct/tcp has TCP instances tcp-b (plain)
+// and, provisioned later, tcp-a (declaring); tcp-b's platform row was minted
+// before owners were recorded, so the edge finds its owner by backend. tcp-c
+// and tcp-d share one address, so tcp-c's minted row has an ambiguous owner.
+// At the end every public row with a findable owner must answer.
+func wOwnerNonEmptyUnique(t *testing.T, w *world) {
+ b := w.boxes[0]
+ for _, x := range []struct {
+ host, addr string
+ }{{tcpB, "10.0.0.7:9102"}, {tcpC, "10.0.0.7:9103"}, {tcpD, "10.0.0.7:9103"}} {
+ if !w.provision(b, x.host, tcpApp, x.addr, vPlain) {
+ t.Fatalf("witness: provisioning %s refused: %s", x.host, w.boxesState())
+ }
+ }
+ w.mint(b, tcpB, mintedB, false)
+ w.mint(b, tcpC, mintedC, false)
+ w.check()
+ if !w.provision(b, tcpA, tcpApp, "10.0.0.7:9101", vEngine) {
+ t.Fatalf("witness: provisioning %s refused: %s", tcpA, w.boxesState())
+ }
+ w.reload(b)
+ w.check()
+ if on("owner-nonempty-unique") {
+ if r := w.admitPublic(b, mintedC, "/"); r != nil {
+ t.Fatalf("witness: a minted row with an ambiguous owner was admitted: %s", w.boxesState())
+ }
+ }
+ w.final()
+}
+
+// wPublicChecksLive: the engine's live release declares; the operator runs
+// --public; a public request arrives and socket activation starts the unit.
+func wPublicChecksLive(t *testing.T, w *world) {
+ b := w.boxes[0]
+ if !w.adopt(b, eng, vEngine, nil) {
+ t.Fatalf("witness: adoption of the engine refused: %s", w.boxesState())
+ }
+ w.check()
+ w.clearPublic(b, eng)
+ r := w.admitPublic(b, engHost, "/")
+ w.socketActivate(b, eng)
+ if r != nil {
+ w.deliver(r)
+ }
+ w.check()
+}
+
+// wPublicStopsGroup (R7-1, R8-2): the engine runs a declaring generation; a
+// generation rollout of a plain build repoints the live link and only
+// schedules the swap; the operator runs --public; a public request arrives.
+func wPublicStopsGroup(t *testing.T, w *world) {
+ b := w.boxes[0]
+ if !w.adopt(b, eng, vEngine, nil) {
+ t.Fatalf("witness: adoption of the engine refused: %s", w.boxesState())
+ }
+ w.check()
+ if !w.repointAwake(b, eng, vPlain) {
+ t.Fatalf("witness: the rollout's repoint was refused: %s", w.boxesState())
+ }
+ w.check()
+ w.clearPublic(b, eng)
+ w.requestBy(b, engHost)
+ w.check()
+}
+
+// wPublicHoldsLock: the engine was adopted to a plain build (the mark stays
+// 1); the operator runs --public; after its checks pass and before it stops
+// the group, adoption of a declaring build runs; then a public request
+// arrives and socket activation starts the unit.
+func wPublicHoldsLock(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 == "locked" {
+ w.adopt(hb, g, vEngine, nil)
+ }
+ }
+ w.clearPublic(b, eng)
+ w.clearHook = nil
+ r := w.admitPublic(b, engHost, "/")
+ w.socketActivate(b, eng)
+ if r != nil {
+ w.deliver(r)
+ }
+ w.check()
+}
+
// 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.
+// 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).
func TestI1Oracle(t *testing.T) {
cases := []struct {
name string
@@ -520,26 +757,36 @@ func TestI1Oracle(t *testing.T) {
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) {
+ {"NULL written over 0, not yet fenced", func(w *world, b *box) {
+ oraclePublic(w, b)
+ w.writeMark(b, eng, markNull)
+ }, "not fenced"},
+ {"NULL written over 0 and fenced (the edge treats NULL like 1)", func(w *world, b *box) {
+ oraclePublic(w, b)
+ w.writeMark(b, eng, markNull)
+ w.reload(b)
+ }, ""},
+ {"NULL on one row, 0 served on the other", func(w *world, b *box) {
+ oraclePublic(w, b)
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)
+ oraclePublic(w, b)
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)
+ oraclePublic(w, b)
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)
+ oraclePublic(w, b)
w.writeMark(b, eng, markInternal)
b.Fenced = b.Wrote
- }, "serves " + engHost + " public"},
+ }, "serves " + eng + " public"},
}
for _, c := range cases {
w := newWitness()
diff --git a/internal/sim/engines/world_test.go b/internal/sim/engines/world_test.go
index ee29dbd9f..91a423520 100644
--- a/internal/sim/engines/world_test.go
+++ b/internal/sim/engines/world_test.go
@@ -51,11 +51,20 @@ type proc struct {
// 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).
+//
+// A platform-minted row (Platform) names in Source the host it was minted
+// from: the truth the oracle reads. Owner is what the registry has recorded
+// (routes.owner), "" for a row minted before owners were recorded; the edge
+// then finds the owner by App and backend (spec §5.1, "Platform-minted
+// rows"). App is the row's account/app. GrantAt is the registry change that
+// recorded the doc-engine grant.
type row struct {
Host, Kind, Owner, Backend string
Platform, Grant bool
PathTo map[string]string
Alias string
+ App, Source string
+ GrantAt int
}
// mark is a row's exposure mark.
@@ -105,6 +114,7 @@ type box struct {
Mark map[string]mark
Wrote, Fenced, Epoch int
ReloadFails, Armed bool
+ Locked bool // the adoption lock, held by --public
Live, Good map[string]int
Staged map[string][]int
Procs []*proc
@@ -127,6 +137,11 @@ type world struct {
stats map[string]int
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.
+ clearHook func(b *box, g, stage string)
+
verbose bool
}
@@ -155,11 +170,12 @@ func newWorld(seed int64, verbose bool) *world {
home, calling := newBox(0), newBox(1)
w.boxes = []*box{home, calling}
- // one engine group, eng, with its minted platform row
- 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 engine group, eng: its own route and its minted platform row
+ 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
// 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.Rows["shop"] = &row{Host: "shop", Kind: "instance", App: "acct/shop", 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
@@ -203,11 +219,14 @@ func (w *world) logf(format string, args ...any) {
// it runs the action, so steps 1 to chaosSteps are chaos and the rest calm.
func (w *world) calm() bool { return w.step > chaosSteps }
-// group is a row's group key: its owner for a minted instance row, else its
-// own host.
+// group is a row's group key: its owner for a minted instance row whose
+// owner the registry can find, else its own host (spec §5.1,
+// "Platform-minted rows"; resolveOwner).
func (w *world) group(b *box, host string) string {
- if r := b.Rows[host]; r != nil && r.Kind == "instance" && r.Owner != "" {
- return r.Owner
+ if r := b.Rows[host]; r != nil && followsOwner(r) {
+ if o, ok := b.resolveOwner(r); ok {
+ return o
+ }
}
return host
}
@@ -256,7 +275,18 @@ func (w *world) doStep() {
// final is the end-of-run oracle: what must hold once the calm steps are
// over. Later tasks add their end-state checks here.
+//
+// The faults are over: every edge's reload works again, and each edge polls
+// once, so every row has had its chance to answer. Then INV-AV.
func (w *world) final() {
+ for _, b := range w.boxes {
+ if b.ReloadFails {
+ b.ReloadFails = false
+ w.logf("box%d: final: the reload fault has cleared", b.ID)
+ }
+ w.reload(b)
+ }
+ w.checkAV()
w.logf("final: %d steps, %d violations, %d residuals", w.step, len(w.violations), len(w.residuals))
}