lib/machine/src/explore/distributed/driver.zig
daab053ee43316e1809a84551d573ddd1e5bf3d2
1 const canon = @import("canon.zig");
2 const explore = @import("../root.zig");
3 const profile = @import("../../profile/root.zig");
4 const property = @import("property.zig");
5 const state_owner = @import("state.zig");
6 const std = @import("std");
7 const types = @import("types.zig");
8 const workload = @import("workload.zig");
9 const world = @import("../../world/root.zig");
10
11 pub const Search = explore.Search(types.search_capacity);
12
13 pub const Input = explore.InputGenerator(.{
14 .steps = types.generator_steps,
15 .alternatives = 5,
16 });
17
18 pub const Schedule = explore.ScheduleGenerator(.{
19 .steps = types.generator_steps,
20 .nodes = types.node_count + 1,
21 .alternatives = types.node_count + 2,
22 });
23
24 pub const Fault = explore.FaultGenerator(.{
25 .steps = types.generator_steps,
26 .kinds = types.kinds.len,
27 .alternatives = types.kinds.len + 1,
28 });
29
30 pub const temporal: explore.TemporalPlan = .{
31 .steps = types.generator_steps,
32 .start_tick = types.start_tick,
33 .end_tick = types.end_tick,
34 };
35
36 /// The input, schedule, and fault sources that offer the alternatives for one
37 /// kind of choice, one step at a time (*generators*), each positioned where a
38 /// settled run the search keeps (*retained branch*) left it. The driver keeps
39 /// one set for every retained branch, so it can offer each child the choices
40 /// that follow its own parent's history. `init` builds the three over 8 steps
41 /// and virtual ticks 1 through 4096 from the selected machine configuration and
42 /// the 32-byte value the generators draw from (*seed*), and returns
43 /// `GeneratorUnavailable` when a generator cannot start. `advance` moves the
44 /// generator that matches the kind of one alternative taken at a step
45 /// (*decision*) past that decision. `advance` returns `StaleChoiceSite` when
46 /// the decision's step, alternative count, or chosen value differs from what
47 /// the generator offers, and `ChoiceOutOfRange` for an alternative past the
48 /// offered count. A topology decision returns `DecisionStreamMismatch`, because
49 /// the fixed six levels of choices every workload search walks have no topology
50 /// level, and a generator with no next step returns `GeneratorUnavailable`. A
51 /// child's set starts as a copy of its parent's.
52 pub const Cursors = struct {
53 input: Input,
54 schedule: Schedule,
55 faults: Fault,
56
57 pub fn init(selected: profile.Profile, seed: explore.Seed) types.Error!Cursors {
58 return .{
59 .input = try ready(Input, try Input.init(selected, seed, temporal)),
60 .schedule = try ready(Schedule, try Schedule.init(selected, seed, .{
61 .temporal = temporal,
62 .nodes = types.node_count,
63 })),
64 .faults = try ready(Fault, try Fault.init(selected, seed, .{
65 .temporal = temporal,
66 .kinds = &types.kinds,
67 })),
68 };
69 }
70
71 pub fn advance(
72 self: *Cursors,
73 decision: explore.SearchDecision,
74 ) types.Error!void {
75 switch (decision.site.stream) {
76 .input => {
77 const site = try requireSite(self.input.next());
78 try match(site, decision);
79 const chosen = try self.input.choose(site, decision.alternative);
80 if (!std.meta.eql(chosen, decision.choice.input)) {
81 return error.StaleChoiceSite;
82 }
83 },
84 .schedule => {
85 const site = try requireSite(self.schedule.next());
86 try match(site, decision);
87 const chosen = try self.schedule.choose(site, decision.alternative);
88 if (!std.meta.eql(chosen, decision.choice.schedule)) {
89 return error.StaleChoiceSite;
90 }
91 },
92 .fault => {
93 const site = try requireSite(self.faults.next());
94 try match(site, decision);
95 const chosen = try self.faults.choose(site, decision.alternative);
96 if (!std.meta.eql(chosen, decision.choice.fault)) {
97 return error.StaleChoiceSite;
98 }
99 },
100 .topology => return error.DecisionStreamMismatch,
101 }
102 }
103 };
104
105 /// One search of the three-node commit protocol under test (*workload*) that
106 /// covers every branch of the fixed six levels of choices every workload search
107 /// walks. The witness gate calls `start` and `run` once for each workload
108 /// variant and compares the summaries. The driver holds the search plus one
109 /// protocol state and one cursor set for each of 3584 settled runs the search
110 /// keeps (*retained branches*), all inside the value, so a caller allocates it
111 /// in memory it owns. `start` resets the driver for one variant, the selected
112 /// machine configuration, and the 32-byte value the generators draw from,
113 /// stores the initial protocol state as branch 0, and queues its first choices.
114 /// `run` steps the search until the queue of waiting choices empties or a
115 /// budget runs out, then returns a summary. A branch that violates a rule that
116 /// fails at the first event that breaks it (*safety rule*) is kept and counted,
117 /// and the driver grows no children from it. A step that prunes a choice or
118 /// ends incomplete returns `SearchPruned` or `SearchIncomplete`, so `run`
119 /// returns a summary only when no branch was skipped. The summary gives the
120 /// executions, the retained branches, the pruned count, the failures, the
121 /// reason the search stopped, and how many branches reached the long hang
122 /// alone, the late delivery alone, both together, or a queued acknowledgement.
123 /// `runner` gives the search a callback that restarts from a copy of the
124 /// parent's saved state and cursors, applies one alternative taken at a step,
125 /// and reports the position in a world's history (*moment*) reached, or a
126 /// failure when a safety rule is violated. `moment` computes the moment of one
127 /// retained branch from its saved state.
128 pub const Driver = struct {
129 config: types.Config,
130 origin: world.Root,
131 search: Search,
132 states: [types.search_capacity.retained]state_owner.State,
133 cursors: [types.search_capacity.retained]Cursors,
134 pending: state_owner.State,
135 pending_cursors: Cursors,
136 parent: explore.SearchBranchId,
137 leaf: bool,
138 failures: u32,
139
140 pub const capacity: explore.SearchCapacity = types.search_capacity;
141 pub const budget: explore.SearchBudget = types.budget;
142
143 pub fn start(
144 self: *Driver,
145 config: types.Config,
146 selected: profile.Profile,
147 seed: explore.Seed,
148 ) types.Error!void {
149 const contract = try profile.contractFingerprint(selected);
150 self.config = config;
151 self.origin = canon.origin(contract);
152 self.failures = 0;
153 self.parent = 0;
154 self.leaf = false;
155 self.states[0] = state_owner.State.init(canon.initialRoot(contract));
156 self.cursors[0] = try Cursors.init(selected, seed);
157 self.search = try Search.init(try self.moment(0), budget);
158 std.debug.assert(self.search.branches().len == 1);
159 try self.expand(0);
160 std.debug.assert(self.search.frontier().len > 0);
161 }
162
163 pub fn run(self: *Driver) types.Error!types.Exploration {
164 for (0..budget.executions + 1) |_| {
165 const frontier = self.search.frontier();
166 std.debug.assert(frontier.len <= capacity.frontier);
167 if (frontier.len == 0) return self.summary(.frontier_empty);
168 self.parent = frontier[0].parent;
169 std.debug.assert(self.parent < self.search.branches().len);
170 self.leaf = (try self.search.branch(self.parent)).depth + 1 == types.depth;
171 switch (self.search.step(self.runner())) {
172 .completed => |value| try self.settle(value.branch, true),
173 .failed => |value| try self.settle(value.branch, false),
174 .exhausted => |value| return self.summary(value.reason),
175 .pruned => return error.SearchPruned,
176 .incomplete => return error.SearchIncomplete,
177 }
178 }
179 return error.SearchIncomplete;
180 }
181
182 pub fn runner(self: *Driver) explore.SearchRunner {
183 return .{ .context = self, .execute = execute };
184 }
185
186 pub fn moment(self: *const Driver, id: explore.SearchBranchId) types.Error!world.Moment {
187 std.debug.assert(id < self.states.len);
188 return world.prepareMoment(self.origin, self.states[id].fabric);
189 }
190
191 fn settle(self: *Driver, id: explore.SearchBranchId, expand_next: bool) types.Error!void {
192 std.debug.assert(id > 0);
193 std.debug.assert(id < self.states.len);
194 std.debug.assert(id < capacity.retained);
195 self.states[id] = self.pending;
196 self.cursors[id] = self.pending_cursors;
197 if (!expand_next) {
198 self.failures += 1;
199 return;
200 }
201 try self.expand(id);
202 }
203
204 fn expand(self: *Driver, id: explore.SearchBranchId) types.Error!void {
205 const branch = try self.search.branch(id);
206 if (branch.depth >= types.depth) return;
207 std.debug.assert(branch.depth < types.tree.len);
208 const cursors = &self.cursors[id];
209 const expansion = switch (types.tree[branch.depth]) {
210 .input => try self.search.expandInput(
211 id,
212 try requireSite(cursors.input.next()),
213 ),
214 .schedule => try self.search.expandSchedule(
215 id,
216 try requireSite(cursors.schedule.next()),
217 ),
218 .fault => try self.search.expandFault(
219 id,
220 try requireSite(cursors.faults.next()),
221 ),
222 .topology => return error.DecisionStreamMismatch,
223 };
224 switch (expansion) {
225 .expanded => {},
226 .exhausted => return error.SearchIncomplete,
227 .pruned => return error.SearchPruned,
228 }
229 }
230
231 fn summary(
232 self: *const Driver,
233 reason: explore.SearchExhaustedReason,
234 ) types.Exploration {
235 const progress = self.search.progress();
236 std.debug.assert(progress.retained == self.search.branches().len);
237 std.debug.assert(progress.executions <= budget.executions);
238 var result: types.Exploration = .{
239 .config = self.config,
240 .executions = progress.executions,
241 .retained = progress.retained,
242 .pruned = progress.pruned,
243 .settled_failures = 0,
244 .reported_failures = self.failures,
245 .exhausted = reason,
246 .hang_only_branches = 0,
247 .delay_only_branches = 0,
248 .conjunction_branches = 0,
249 .queued_acknowledgement_branches = 0,
250 };
251 for (self.search.branches(), 0..) |branch, index| {
252 const conjunct = self.states[index].conjunct;
253 if (conjunct.queued_acknowledgement) {
254 result.queued_acknowledgement_branches += 1;
255 }
256 if (conjunct.both()) {
257 result.conjunction_branches += 1;
258 } else if (conjunct.persistent_hang) {
259 result.hang_only_branches += 1;
260 } else if (conjunct.delayed_delivery) {
261 result.delay_only_branches += 1;
262 }
263 switch (branch.settlement) {
264 .failed => {
265 result.settled_failures += 1;
266 std.debug.assert(conjunct.both());
267 },
268 .origin, .completed => {},
269 }
270 }
271 std.debug.assert(result.settled_failures == self.failures);
272 std.debug.assert(result.conjunction_branches >= result.settled_failures);
273 return result;
274 }
275 };
276
277 fn execute(
278 raw: *anyopaque,
279 parent: world.Moment,
280 decision: explore.SearchDecision,
281 ) explore.SearchExecution {
282 const self: *Driver = @ptrCast(@alignCast(raw));
283 std.debug.assert(self.parent < Driver.capacity.retained);
284 const expected = self.moment(self.parent) catch
285 return .{ .incomplete = .invalid_moment };
286 if (!std.meta.eql(expected, parent)) return .{ .incomplete = .invalid_moment };
287 self.pending = self.states[self.parent];
288 self.pending_cursors = self.cursors[self.parent];
289 self.pending_cursors.advance(decision) catch
290 return .{ .incomplete = .replay_rejected };
291 var events: types.Events = .{};
292 const verdicts = workload.evaluate(
293 self.config,
294 &self.pending,
295 decision,
296 &events,
297 self.leaf,
298 ) catch return .{ .incomplete = .trace_incomplete };
299 const reached = world.prepareMoment(self.origin, self.pending.fabric) catch
300 return .{ .incomplete = .invalid_moment };
301 if (property.violation(verdicts)) |failure| {
302 return .{ .failed = .{ .root = reached, .evaluation = failure } };
303 }
304 return .{ .completed = reached };
305 }
306
307 fn match(site: anytype, decision: explore.SearchDecision) types.Error!void {
308 if (!std.meta.eql(site.id, decision.site)) return error.StaleChoiceSite;
309 if (site.count != decision.alternative_count) return error.StaleChoiceSite;
310 if (decision.alternative >= site.count) return error.ChoiceOutOfRange;
311 }
312
313 fn requireSite(result: anytype) types.Error!@FieldType(@TypeOf(result), "item") {
314 return switch (result) {
315 .item => |value| value,
316 .exhausted, .incomplete => error.GeneratorUnavailable,
317 };
318 }
319
320 fn ready(comptime Generator: type, result: anytype) types.Error!Generator {
321 return switch (result) {
322 .item => |value| value,
323 .exhausted, .incomplete => error.GeneratorUnavailable,
324 };
325 }