| 1 | package rollout |
| 2 | |
| 3 | import ( |
| 4 | "os" |
| 5 | "testing" |
| 6 | "time" |
| 7 | ) |
| 8 | |
| 9 | // I9's deterministic witnesses (fix wave 1, item 3; Astra final review 1, |
| 10 | // finding 3). Each scripts the model's events around a grant and then |
| 11 | // delivers the grant through the real Manager and book. The code is not |
| 12 | // told of the restriction the model adds after the grant's issue, which is |
| 13 | // exactly what a mutant that moves no generation does (M14's renewal): the |
| 14 | // grant's generation still matches, the code accepts it and clears the |
| 15 | // marker, and I9 must report it. The control shows that a restriction that |
| 16 | // landed before the issue, in the same step, is not inside the check. |
| 17 | |
| 18 | // newI9WitnessSim is a seed whose book is on disk (seed%4 == 3), with h's |
| 19 | // hold-ran marker naming x (h's installed build) in the model and, saved, |
| 20 | // in the book, so the box publishes a generation for it and a grant for |
| 21 | // (x, h) is accepted. |
| 22 | func newI9WitnessSim(t *testing.T) (*sim, *simHost, string) { |
| 23 | t.Helper() |
| 24 | if os.Geteuid() == 0 { |
| 25 | t.Skip("as root a seed keeps its book in memory, and I9 is not checked") |
| 26 | } |
| 27 | s := newSim(3, t.TempDir(), t.TempDir(), map[string]bool{}) |
| 28 | t.Cleanup(func() { |
| 29 | s.cancel() |
| 30 | close(s.dead) |
| 31 | os.RemoveAll(s.dir) |
| 32 | }) |
| 33 | h := s.hosts[0] |
| 34 | x := s.installed[h.ch] |
| 35 | s.holdRanOn(h, x, s.now) |
| 36 | if err := s.book.MarkHoldRan(h.name, HoldRan{Account: "bab", App: "blog", Build: x, Exec: "w-witness-0", At: s.now}); err != nil { |
| 37 | t.Fatalf("MarkHoldRan: %v", err) |
| 38 | } |
| 39 | if s.published(x, h.name) == 0 { |
| 40 | t.Fatal("no published generation for the marker") |
| 41 | } |
| 42 | witnessStep(s) |
| 43 | return s, h, x |
| 44 | } |
| 45 | |
| 46 | // witnessStep moves the model one step on. |
| 47 | func witnessStep(s *sim) { |
| 48 | s.step++ |
| 49 | s.now = s.now.Add(time.Second) |
| 50 | } |
| 51 | |
| 52 | // lastGrant is the grant issueGrant just queued. |
| 53 | func lastGrant(t *testing.T, s *sim) simGrant { |
| 54 | t.Helper() |
| 55 | if len(s.grants) == 0 { |
| 56 | t.Fatal("no grant was issued") |
| 57 | } |
| 58 | return s.grants[len(s.grants)-1] |
| 59 | } |
| 60 | |
| 61 | // wantI9 runs fn, a delivery of a grant for h, and requires it to report an |
| 62 | // I9 violation. Without one it says whether the code accepted the grant |
| 63 | // (h's marker cleared), which is what makes a missed violation a miss. |
| 64 | func wantI9(t *testing.T, s *sim, h *simHost, fn func()) { |
| 65 | t.Helper() |
| 66 | defer func() { |
| 67 | r := recover() |
| 68 | v, ok := r.(simViolation) |
| 69 | if !ok || v.inv != "I9" { |
| 70 | _, still := s.book.HoldRanOn(h.name) |
| 71 | t.Fatalf("got %v, want an I9 violation (the code accepted the grant: %v)", r, !still) |
| 72 | } |
| 73 | t.Logf("caught: %s", v.msg) |
| 74 | }() |
| 75 | fn() |
| 76 | } |
| 77 | |
| 78 | // Astra's counterexample: issue G0; another hold execution of x begins on |
| 79 | // h; issue G1; that execution's run renews the marker (with M14's missing |
| 80 | // generation move); deliver G0 first. G1's issue must not answer the |
| 81 | // renewal: only an applied clear discharges a fact. |
| 82 | func TestI9WitnessAGrantsIssueMasksNothing(t *testing.T) { |
| 83 | s, h, x := newI9WitnessSim(t) |
| 84 | s.issueGrant(h, x) |
| 85 | g0 := lastGrant(t, s) |
| 86 | witnessStep(s) |
| 87 | start := s.now // another hold execution of x begins on h |
| 88 | witnessStep(s) |
| 89 | s.issueGrant(h, x) // G1: nothing has moved yet, so the same generation |
| 90 | witnessStep(s) |
| 91 | s.holdRanOn(h, x, start) // its run renews the marker; the code moves nothing |
| 92 | witnessStep(s) |
| 93 | wantI9(t, s, h, func() { s.deliver(g0) }) |
| 94 | } |
| 95 | |
| 96 | // A late outcome: an execution of x on h begins before the grant is issued, |
| 97 | // and its failure lands after the issue, with the grant not yet applied (so |
| 98 | // not PreRetry). It is inside the check, though its execution began first. |
| 99 | func TestI9WitnessALateOutcomeIsInsideTheCheck(t *testing.T) { |
| 100 | s, h, x := newI9WitnessSim(t) |
| 101 | start := s.now // the execution begins |
| 102 | witnessStep(s) |
| 103 | s.issueGrant(h, x) |
| 104 | g := lastGrant(t, s) |
| 105 | witnessStep(s) |
| 106 | // The failure lands. The code is not told (its generation does not |
| 107 | // move), so I8, which reads the disk for it, is not this witness's. |
| 108 | dir := s.dir |
| 109 | s.dir = "" |
| 110 | s.failure(x, h.name, time.Time{}, false, start) |
| 111 | s.dir = dir |
| 112 | witnessStep(s) |
| 113 | wantI9(t, s, h, func() { s.deliver(g) }) |
| 114 | } |
| 115 | |
| 116 | // A change in the grant's own step, after its issue: the step's own action |
| 117 | // runs a hold execution of x on h that renews the marker. The model's times |
| 118 | // cannot order the two, its transition numbers can. |
| 119 | func TestI9WitnessASameStepChangeIsInsideTheCheck(t *testing.T) { |
| 120 | s, h, x := newI9WitnessSim(t) |
| 121 | s.issueGrant(h, x) |
| 122 | g := lastGrant(t, s) |
| 123 | s.holdRanOn(h, x, s.now) // same step, after the issue |
| 124 | witnessStep(s) |
| 125 | wantI9(t, s, h, func() { s.deliver(g) }) |
| 126 | } |
| 127 | |
| 128 | // The control: a renewal that landed before the issue, in the same step, |
| 129 | // and that the code saw (its generation moved, and the grant names the new |
| 130 | // one), is what the grant was issued for. The grant clears it, and I9 holds. |
| 131 | func TestI9WitnessASameStepChangeBeforeTheIssueIsNotInsideTheCheck(t *testing.T) { |
| 132 | s, h, x := newI9WitnessSim(t) |
| 133 | s.holdRanOn(h, x, s.now) |
| 134 | if err := s.book.MarkHoldRan(h.name, HoldRan{Account: "bab", App: "blog", Build: x, Exec: "w-witness-1", At: s.now}); err != nil { |
| 135 | t.Fatalf("MarkHoldRan: %v", err) |
| 136 | } |
| 137 | s.issueGrant(h, x) |
| 138 | g := lastGrant(t, s) |
| 139 | witnessStep(s) |
| 140 | s.deliver(g) |
| 141 | if _, still := s.book.HoldRanOn(h.name); still { |
| 142 | t.Fatal("the grant was not accepted: the control proves nothing") |
| 143 | } |
| 144 | } |
| 145 | |
amadan