amadan

carlos / platform Public

fix wave 1: I9 orders restriction transitions as they land and lets only an applied clear discharge a fact

A grant captures the model's transition number at issue; late outcomes and same-step changes are inside the check; issuance answers nothing. Deterministic witnesses for masking, a late outcome and a same-step change.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
claude 929dfc397300ac7f3ccadfc8277d131dfb4d5031 parent e22f840
2 files changed, +259 −74
  • internal/rollout/sim_i9_witness_test.go +144 −0
  • internal/rollout/sim_test.go +115 −74
diff --git a/internal/rollout/sim_i9_witness_test.go b/internal/rollout/sim_i9_witness_test.go
new file mode 100644
index 000000000..601a78a04
--- /dev/null
+++ b/internal/rollout/sim_i9_witness_test.go
@@ -0,0 +1,144 @@
+package rollout
+
+import (
+ "os"
+ "testing"
+ "time"
+)
+
+// I9's deterministic witnesses (fix wave 1, item 3; Astra final review 1,
+// finding 3). Each scripts the model's events around a grant and then
+// delivers the grant through the real Manager and book. The code is not
+// told of the restriction the model adds after the grant's issue, which is
+// exactly what a mutant that moves no generation does (M14's renewal): the
+// grant's generation still matches, the code accepts it and clears the
+// marker, and I9 must report it. The control shows that a restriction that
+// landed before the issue, in the same step, is not inside the check.
+
+// newI9WitnessSim is a seed whose book is on disk (seed%4 == 3), with h's
+// hold-ran marker naming x (h's installed build) in the model and, saved,
+// in the book, so the box publishes a generation for it and a grant for
+// (x, h) is accepted.
+func newI9WitnessSim(t *testing.T) (*sim, *simHost, string) {
+ t.Helper()
+ if os.Geteuid() == 0 {
+ t.Skip("as root a seed keeps its book in memory, and I9 is not checked")
+ }
+ s := newSim(3, t.TempDir(), t.TempDir(), map[string]bool{})
+ t.Cleanup(func() {
+ s.cancel()
+ close(s.dead)
+ os.RemoveAll(s.dir)
+ })
+ h := s.hosts[0]
+ x := s.installed[h.ch]
+ s.holdRanOn(h, x, s.now)
+ if err := s.book.MarkHoldRan(h.name, HoldRan{Account: "bab", App: "blog", Build: x, Exec: "w-witness-0", At: s.now}); err != nil {
+ t.Fatalf("MarkHoldRan: %v", err)
+ }
+ if s.published(x, h.name) == 0 {
+ t.Fatal("no published generation for the marker")
+ }
+ witnessStep(s)
+ return s, h, x
+}
+
+// witnessStep moves the model one step on.
+func witnessStep(s *sim) {
+ s.step++
+ s.now = s.now.Add(time.Second)
+}
+
+// lastGrant is the grant issueGrant just queued.
+func lastGrant(t *testing.T, s *sim) simGrant {
+ t.Helper()
+ if len(s.grants) == 0 {
+ t.Fatal("no grant was issued")
+ }
+ return s.grants[len(s.grants)-1]
+}
+
+// wantI9 runs fn, a delivery of a grant for h, and requires it to report an
+// I9 violation. Without one it says whether the code accepted the grant
+// (h's marker cleared), which is what makes a missed violation a miss.
+func wantI9(t *testing.T, s *sim, h *simHost, fn func()) {
+ t.Helper()
+ defer func() {
+ r := recover()
+ v, ok := r.(simViolation)
+ if !ok || v.inv != "I9" {
+ _, still := s.book.HoldRanOn(h.name)
+ t.Fatalf("got %v, want an I9 violation (the code accepted the grant: %v)", r, !still)
+ }
+ t.Logf("caught: %s", v.msg)
+ }()
+ fn()
+}
+
+// Astra's counterexample: issue G0; another hold execution of x begins on
+// h; issue G1; that execution's run renews the marker (with M14's missing
+// generation move); deliver G0 first. G1's issue must not answer the
+// renewal: only an applied clear discharges a fact.
+func TestI9WitnessAGrantsIssueMasksNothing(t *testing.T) {
+ s, h, x := newI9WitnessSim(t)
+ s.issueGrant(h, x)
+ g0 := lastGrant(t, s)
+ witnessStep(s)
+ start := s.now // another hold execution of x begins on h
+ witnessStep(s)
+ s.issueGrant(h, x) // G1: nothing has moved yet, so the same generation
+ witnessStep(s)
+ s.holdRanOn(h, x, start) // its run renews the marker; the code moves nothing
+ witnessStep(s)
+ wantI9(t, s, h, func() { s.deliver(g0) })
+}
+
+// A late outcome: an execution of x on h begins before the grant is issued,
+// and its failure lands after the issue, with the grant not yet applied (so
+// not PreRetry). It is inside the check, though its execution began first.
+func TestI9WitnessALateOutcomeIsInsideTheCheck(t *testing.T) {
+ s, h, x := newI9WitnessSim(t)
+ start := s.now // the execution begins
+ witnessStep(s)
+ s.issueGrant(h, x)
+ g := lastGrant(t, s)
+ witnessStep(s)
+ // The failure lands. The code is not told (its generation does not
+ // move), so I8, which reads the disk for it, is not this witness's.
+ dir := s.dir
+ s.dir = ""
+ s.failure(x, h.name, time.Time{}, false, start)
+ s.dir = dir
+ witnessStep(s)
+ wantI9(t, s, h, func() { s.deliver(g) })
+}
+
+// A change in the grant's own step, after its issue: the step's own action
+// runs a hold execution of x on h that renews the marker. The model's times
+// cannot order the two, its transition numbers can.
+func TestI9WitnessASameStepChangeIsInsideTheCheck(t *testing.T) {
+ s, h, x := newI9WitnessSim(t)
+ s.issueGrant(h, x)
+ g := lastGrant(t, s)
+ s.holdRanOn(h, x, s.now) // same step, after the issue
+ witnessStep(s)
+ wantI9(t, s, h, func() { s.deliver(g) })
+}
+
+// The control: a renewal that landed before the issue, in the same step,
+// and that the code saw (its generation moved, and the grant names the new
+// one), is what the grant was issued for. The grant clears it, and I9 holds.
+func TestI9WitnessASameStepChangeBeforeTheIssueIsNotInsideTheCheck(t *testing.T) {
+ s, h, x := newI9WitnessSim(t)
+ s.holdRanOn(h, x, s.now)
+ if err := s.book.MarkHoldRan(h.name, HoldRan{Account: "bab", App: "blog", Build: x, Exec: "w-witness-1", At: s.now}); err != nil {
+ t.Fatalf("MarkHoldRan: %v", err)
+ }
+ s.issueGrant(h, x)
+ g := lastGrant(t, s)
+ witnessStep(s)
+ s.deliver(g)
+ if _, still := s.book.HoldRanOn(h.name); still {
+ t.Fatal("the grant was not accepted: the control proves nothing")
+ }
+}
diff --git a/internal/rollout/sim_test.go b/internal/rollout/sim_test.go
index 79b18957e..6ed82ed45 100644
--- a/internal/rollout/sim_test.go
+++ b/internal/rollout/sim_test.go
@@ -99,19 +99,24 @@ import (
// agent opening the book from disk holds the build for the instance,
// and holds it down when the failure does.
// - I9: a stale grant never clears a later failure (the crash-epoch hard
-// limit, readiness round 2): when a signed `carlos instances retry`
-// grant issued at step t clears anything (RetryHostAt), no unanswered
-// failure fact of the grant's (build, host) has a start after t (a fact
-// that began in t's own step is skipped). The facts are the model's
-// (sim.facts), never the book's verdicts: every failure, hold-down and
-// hold run the model delivers that changes the model's own restriction
-// state (sim.grec, the hold-ran restriction), and every intent a
-// restart reconciles. A failure that makes a new record is a fact of
-// every host of the app, wherever it ran, since a new record holds
-// every host (spec §8.4). A fact is answered by a clear the spec allows
-// to lift it, issued after its start: a grant for its build on the
-// grant's host, a pointer naming its build (a record), or a lift of its
-// host's hold-ran restriction (a hold run).
+// limit, readiness round 2; fix wave 1, item 3). The model numbers every
+// restriction transition it causes or observes, in the order they land,
+// apart from the book (sim.tseq): each one that adds a restriction is a
+// fact (sim.facts: a record created, or merged with a change; a
+// hold-down; a hold-ran marker set, renewed or replacing another; an
+// intent a restart reconciles), and each one that removes one is a
+// clear (sim.clears: a grant's applied retry or marker clear, a record
+// a pointer clears or a prune drops, a marker lifted or replaced). A
+// grant captures the number when it is issued from published status.
+// When a grant is accepted (RetryHostAt clears anything), no fact of its
+// (build, host), nor a new record of its build (which holds every host,
+// spec §8.4), may have landed after that capture, unless a clear of that
+// restriction was applied after the fact. Facts are ordered by when they
+// land, not by when their execution began: a late outcome (an execution
+// begun before the grant whose failure lands after it, not PreRetry) and
+// a change in the grant's own step are inside the check. Issuing a grant
+// answers nothing; only an applied clear does. The facts are the
+// model's, never the book's verdicts.
// - I10: durable before use: every non-zero generation PublishedEpoch
// returns is the app's generation in the book's last landed file,
// re-read from disk at that moment, under the identity the file holds.
@@ -334,28 +339,43 @@ type simLate struct {
}
// simGrant is a signed `carlos instances retry` grant (I9): the build and
-// host it names, the book and generation status published for them, and
-// when it was issued (the step, and its time, which a fact's start is
-// compared with).
+// host it names, the book and generation status published for them, when
+// it was issued (the step, and its time, for messages), and the model's
+// transition number at that moment (cap, sim.tseq), which every fact is
+// ordered against.
type simGrant struct {
build, host, book string
epoch uint64
step int
at time.Time
+ cap uint64
}
-// simFact is one of I9's failure facts: something the model delivered that
-// restricts build on host (kind says what), by an execution that began at
-// start. app is a new record, made by a failure on host: it holds every host
-// of the app (spec §8.4: "the build's next failure writes a new record,
+// simFact is one of I9's facts: a transition (seq, sim.tseq) that added a
+// restriction of build on host (kind says what), from an execution that
+// began at start (for messages only: facts are ordered by seq, when they
+// landed). app is a new record, made by a failure on host: it holds every
+// host of the app (spec §8.4: "the build's next failure writes a new record,
// which holds every host"), so the fact is every host's, not host's alone.
type simFact struct {
build, host, kind string
start time.Time
+ seq uint64
marker bool // a hold run: its host's hold-ran restriction
app bool // a new record: every host of the app
}
+// simClear is a transition (seq) that removed a restriction, as applied:
+// never a grant's issue, only its clear. marker is the hold-ran
+// restriction of host (build "" is whichever build it named: a lift);
+// otherwise build's record restriction of host, or of every host when host
+// is "" (the record left the book: a pointer's clear or a prune).
+type simClear struct {
+ build, host, kind string
+ seq uint64
+ marker bool
+}
+
// simRec is the model's own failure record of a build (sim.grec): the hosts
// a host retry cleared, and those held down.
type simRec struct {
@@ -450,14 +470,16 @@ type sim struct {
// pending grants), as the agent does until a grant expires. They
// survive restarts and rebuilds.
grants []simGrant
- // facts are I9's failure facts, and issued, signed and lifted the clears
- // that answer them: when each (build, host) grant was issued, each
- // build's pointer signed, each host's hold-ran restriction lifted.
- // They survive restarts and rebuilds.
+ // tseq numbers every restriction transition the model causes or
+ // observes, in the order they land (I9), kept apart from the book: facts
+ // are the ones that added a restriction, clears the applied ones that
+ // removed one. Facts survive restarts and rebuilds. Clears do not: a
+ // crash rolls back whatever clear the book had not saved, and the model
+ // cannot tell which had landed, so after a restart no earlier clear
+ // discharges anything (the strict direction).
+ tseq uint64
facts []simFact
- issued map[[2]string][]time.Time
- signed map[string][]time.Time
- lifted map[string][]time.Time
+ clears []simClear
// grec is the model's own failure record per build (I9): which hosts a
// retry clears and which are held down, so a failure is a fact only when
// it changes what the spec says restricts its host (plan finding 7: an
@@ -499,7 +521,7 @@ func newSim(seed int64, opt, books string, staged map[string]bool) *sim {
exempt: map[string]map[string]bool{}, heldDown: map[string]map[string]bool{}, holdRan: map[string]string{},
holdRanAt: map[string]time.Time{}, holdRanSet: map[string]time.Time{}, retryAt: map[string]map[string]time.Time{},
clearedAt: map[string]time.Time{}, failedAt: map[string]time.Time{}, late: map[string]simLate{}, swaps: map[string]*simSwap{},
- issued: map[[2]string][]time.Time{}, signed: map[string][]time.Time{}, lifted: map[string][]time.Time{}, grec: map[string]*simRec{},
+ grec: map[string]*simRec{},
events: make(chan simEvent), dead: make(chan struct{})}
if seed%4 == 3 && os.Geteuid() != 0 {
// Root writes into a read-only directory, so it gets no faults, and
@@ -608,7 +630,6 @@ func (s *sim) newGen(id release.StagedIdentity) activator.Gen {
func (s *sim) sign(channel, b string) {
s.pointers[channel] = release.ChannelPointer{Schema: 1, Account: "bab", App: "blog", Channel: channel, Version: b, PromotedAt: s.now}
s.lastSigned[b] = s.now
- s.signed[b] = append(s.signed[b], s.now)
}
// demand is release.CanonicalDemand's contract, as the harness has it.
@@ -685,9 +706,9 @@ func (s *sim) failureOf(build, host string, stamp time.Time, heldDown bool, star
}
switch changed, created := s.recFailed(build, host, heldDown); {
case created:
- s.facts = append(s.facts, simFact{build: build, host: host, kind: kind, start: start, app: true})
+ s.addFact(simFact{build: build, host: host, kind: kind, start: start, app: true})
case changed || reconciled:
- s.facts = append(s.facts, simFact{build: build, host: host, kind: kind, start: start})
+ s.addFact(simFact{build: build, host: host, kind: kind, start: start})
}
s.checkI8(build, host, heldDown)
if stamp.IsZero() {
@@ -738,23 +759,33 @@ func (s *sim) recFailed(build, host string, heldDown bool) (changed, created boo
return changed, created
}
-// answered reports whether a clear the spec allows to lift f, for host, was
-// issued after f's execution began (I9): a grant for its build on host, a
-// pointer naming its build for a record, a lift of its host's hold-ran
-// restriction (a good write, a signed rollback) for a hold run. host is f's
-// own host but for a new record (f.app), which holds every host: there it
-// is the host of the grant I9 checks, and only that host's grant answers it.
-func (s *sim) answered(f simFact, host string) bool {
- after := func(ts []time.Time) bool {
- return slices.ContainsFunc(ts, func(t time.Time) bool { return t.After(f.start) })
- }
- if after(s.issued[[2]string{f.build, host}]) {
- return true
- }
- if f.marker {
- return after(s.lifted[f.host])
- }
- return after(s.signed[f.build])
+// addFact files f, a transition that added a restriction (I9), at the
+// model's next transition number.
+func (s *sim) addFact(f simFact) {
+ s.tseq++
+ f.seq = s.tseq
+ s.facts = append(s.facts, f)
+}
+
+// addClear files c, an applied transition that removed a restriction (I9),
+// at the model's next transition number.
+func (s *sim) addClear(c simClear) {
+ s.tseq++
+ c.seq = s.tseq
+ s.clears = append(s.clears, c)
+ s.logf("transition %d: %s cleared (build %q, host %q, marker %v)", c.seq, c.kind, c.build, c.host, c.marker)
+}
+
+// discharged reports whether a clear applied after f landed removed f's
+// restriction of host (I9): for a hold run, a lift or replacement of its
+// host's hold-ran marker; for a record fact, a grant's retry of its build
+// on host, or its build's record leaving the book. host is f's own host
+// but for a new record (f.app), which holds every host: there it is the
+// host of the grant I9 checks. A grant's issue never discharges anything.
+func (s *sim) discharged(f simFact, host string) bool {
+ return slices.ContainsFunc(s.clears, func(c simClear) bool {
+ return c.seq > f.seq && c.marker == f.marker && (c.build == "" || c.build == f.build) && (c.host == "" || c.host == host)
+ })
}
// diskFault opens or closes a window in which every save of the book fails
@@ -954,7 +985,7 @@ func (s *sim) finishSwap(sw *simSwap) activator.SwapResult {
// record: that holds every host of the app, so it is the app's
// fact (simFact.app).
if _, created := s.recFailed(a.Build, a.Host, res.Outcome == activator.SwapDown); created {
- s.facts = append(s.facts, simFact{build: a.Build, host: a.Host, kind: "an adoption failure", start: sw.started, app: true})
+ s.addFact(simFact{build: a.Build, host: a.Host, kind: "an adoption failure", start: sw.started, app: true})
}
}
if res.Outcome == activator.SwapFailed && a.Mode == activator.ModeHold && !sw.serves {
@@ -1160,10 +1191,11 @@ func (s *sim) pass() {
still[r.Build] = true
}
// The model's own records (I9) leave with the book's: a pointer's clear
- // or a prune.
+ // or a prune, a clear of the record for every host.
for _, b := range sortedKeys(s.grec) {
if !still[b] {
delete(s.grec, b)
+ s.addClear(simClear{build: b, kind: "the record (a pointer's clear or a prune)"})
}
}
for _, b := range sortedKeys(recorded) {
@@ -1213,7 +1245,7 @@ func (s *sim) pass() {
h.name, mark, s.holdRanAt[h.name].Sub(t0), h.good, s.installed[h.ch], p)
}
delete(s.holdRan, h.name)
- s.lifted[h.name] = append(s.lifted[h.name], s.now)
+ s.addClear(simClear{host: h.name, marker: true, kind: "a signed rollback's lift"})
s.logf("ground truth: a signed rollback onto %s lifted %s's hold-ran restriction (%s)", h.good, h.name, mark)
}
}
@@ -1347,10 +1379,14 @@ func (s *sim) holdRanOn(h *simHost, build string, start time.Time) {
if s.holdRan[h.name] == "" || start.After(s.holdRanAt[h.name]) {
s.holdRanAt[h.name] = start
}
+ if old := s.holdRan[h.name]; old != "" && old != build {
+ // The marker now names build: old's restriction of h is gone (I9).
+ s.addClear(simClear{build: old, host: h.name, marker: true, kind: "a marker replaced"})
+ }
s.holdRan[h.name] = build
s.holdRanSet[h.name] = s.now
// Every run is a new execution, which sets or renews the marker (I9).
- s.facts = append(s.facts, simFact{build: build, host: h.name, kind: "a hold run", start: start, marker: true})
+ s.addFact(simFact{build: build, host: h.name, kind: "a hold run", start: start, marker: true})
s.logf("ground truth: hold build %s ran on %s without a verdict", build, h.name)
}
@@ -1363,7 +1399,7 @@ func (s *sim) goodAt(h *simHost, build string, start time.Time) {
h.good = build
if s.holdRanSet[h.name].Before(start) {
if s.holdRan[h.name] != "" {
- s.lifted[h.name] = append(s.lifted[h.name], s.now)
+ s.addClear(simClear{host: h.name, marker: true, kind: "a good write's lift"})
}
delete(s.holdRan, h.name)
}
@@ -1958,13 +1994,11 @@ func (s *sim) issueGrant(h *simHost, b string) {
if epoch == 0 {
return
}
- g := simGrant{build: b, host: h.name, book: s.book.ID(), epoch: epoch, step: s.step, at: s.now}
+ g := simGrant{build: b, host: h.name, book: s.book.ID(), epoch: epoch, step: s.step, at: s.now, cap: s.tseq}
// Pending for the rest of the run: a grant expires after 24 h, and a
// run is minutes long.
s.grants = append(s.grants, g)
- k := [2]string{b, h.name}
- s.issued[k] = append(s.issued[k], s.now)
- s.logf("grant: instances retry %s onto %s issued (book %.8s, generation %d)", h.name, b, g.book, epoch)
+ s.logf("grant: instances retry %s onto %s issued (book %.8s, generation %d, transition %d)", h.name, b, g.book, epoch, g.cap)
}
// deliverGrants is the agent reading its pending grants (internal/host,
@@ -1981,7 +2015,8 @@ func (s *sim) deliverGrants() {
// deliver applies g. When it clears anything, I9 is checked first, then the
// model follows what it cleared: a record that now lists the host as
// retried (exempt, and the retry's place in the ordering), a marker of g's
-// build gone (the hold-ran restriction lifted).
+// build gone (the hold-ran restriction lifted), each an applied clear
+// (sim.clears).
func (s *sim) deliver(g simGrant) {
h := s.byName[g.host]
rec, recorded := s.book.Lookup("bab", "blog", g.build)
@@ -2009,36 +2044,39 @@ func (s *sim) deliver(g simGrant) {
r.retried[g.host] = true
delete(r.down, g.host)
}
+ s.addClear(simClear{build: g.build, host: g.host, kind: "a grant's retry"})
}
- if marked && !markStill && s.holdRan[h.name] == g.build {
- delete(s.holdRan, h.name)
+ if marked && !markStill {
+ s.addClear(simClear{build: g.build, host: g.host, marker: true, kind: "a grant's marker clear"})
+ if s.holdRan[h.name] == g.build {
+ delete(s.holdRan, h.name)
+ }
}
s.logf("grant: instances retry %s onto %s from step %d (generation %d) cleared it (record %v, marker %v)",
g.host, g.build, g.step, g.epoch, recCleared, marked && !markStill)
}
-// checkI9 is I9 at a grant that has just cleared something: no failure fact
-// of its (build, host) began after the grant was issued, unless a clear the
-// spec allows has answered it since. A new record is a fact of every host of
-// the app (simFact.app), so one made by a failure on another host counts
-// too, answered only by a grant for g's build on g's host or a pointer for
-// the build. A fact that began in the grant's own step (a start not after
-// g.at) is skipped: the model's times are per step, so it cannot order the
-// two by time. A rewake's execution in that step began before the grant
-// (rewakeRun runs before retryHeld), and is rightly skipped; one the step's
-// own action started began after it, and skipping it is the permissive
-// direction.
+// checkI9 is I9 at a grant the code has just accepted (it cleared
+// something): no fact of its (build, host) landed after the grant's capture
+// (a seq above g.cap), unless a clear of that restriction was applied after
+// the fact (discharged). A new record is a fact of every host of the app
+// (simFact.app), so one made by a failure on another host counts too,
+// discharged only by a retry of g's build on g's host or the record leaving
+// the book. Facts are ordered by when they landed, so a late outcome and a
+// change in the grant's own step after its issue are inside the check, and
+// one that landed before the issue, in the same step or earlier, is not:
+// the published generation the grant names already held it.
func (s *sim) checkI9(g simGrant) {
for _, f := range s.facts {
- if f.build != g.build || (!f.app && f.host != g.host) || !f.start.After(g.at) || s.answered(f, g.host) {
+ if f.build != g.build || (!f.app && f.host != g.host) || f.seq <= g.cap || s.discharged(f, g.host) {
continue
}
what := ""
if f.app {
what = " (a new record, which holds every host)"
}
- violate("I9", "a grant for %s on %s issued at step %d (%s, book %.8s, generation %d) cleared it after %s of %s on %s%s in an execution begun at %s, which nothing has answered",
- g.build, g.host, g.step, g.at.Sub(t0), g.book, g.epoch, f.kind, f.build, f.host, what, f.start.Sub(t0))
+ violate("I9", "a grant for %s on %s issued at step %d (%s, book %.8s, generation %d, transition %d) cleared it after %s of %s on %s%s (transition %d, an execution begun at %s), which no applied clear has discharged",
+ g.build, g.host, g.step, g.at.Sub(t0), g.book, g.epoch, g.cap, f.kind, f.build, f.host, what, f.seq, f.start.Sub(t0))
}
}
@@ -2137,6 +2175,9 @@ func (s *sim) agentRestart(rebuild bool) {
// The retry ordering is in memory only (FailureBook.cleared): no
// execution from before the restart is left for it to order.
s.retryAt, s.clearedAt = map[string]map[string]time.Time{}, map[string]time.Time{}
+ // A clear the book had not saved is rolled back, and the model keeps
+ // none across a restart (sim.tseq): no earlier clear discharges a fact.
+ s.clears = nil
b, err := OpenFailureBook(s.dir)
if err != nil {
panic(simCrash{msg: "reopen the book: " + err.Error()})